Show the Proof

import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof

	step type	requirements	statement
0	instantiation	1, 2, 3	⊢
	: , : , :
1	reference	294	⊢
2	instantiation	294, 4, 5	⊢
	: , : , :
3	modus ponens	6, 7	⊢
4	instantiation	294, 8, 9	⊢
	: , : , :
5	instantiation	21, 22, 10, 11*, 20*, 12*	⊢
	: , : , : , : , :
6	instantiation	13, 347	⊢
	: , : , : , : , : , :
7	generalization	14	⊢
8	instantiation	15, 22, 16, 17, 18, 39, 19*, 25*, 20*	⊢
	: , : , : , : , : , : , : , :
9	instantiation	21, 22, 23, 24*, 25*, 26*	⊢
	: , : , : , : , :
10	instantiation	37, 32, 39	⊢
	: , : , : , :
11	instantiation	40, 27	,  ⊢
	:
12	instantiation	42, 402, 306, 308	⊢
	: , : , : , : , :
13	axiom		⊢
	proveit.core_expr_types.lambda_maps.lambda_substitution
14	instantiation	28, 29	⊢
	: , : , :
15	theorem		⊢
	proveit.statistics.prob_of_disjoint_events_is_prob_sum
16	instantiation	30, 386, 31, 38, 32	⊢
	: , : , :
17	instantiation	309	⊢
	:
18	instantiation	33, 297, 298, 314, 400, 34	⊢
	: , : , : , :
19	instantiation	35, 36	,  ⊢
	:
20	instantiation	42, 402, 306, 308	⊢
	: , : , : , : , :
21	theorem		⊢
	proveit.statistics.prob_of_all_as_sum
22	theorem		⊢
	proveit.physics.quantum.QPE._Omega_is_sample_space
23	instantiation	37, 38, 39	⊢
	: , : , : , :
24	instantiation	40, 41	,  ⊢
	:
25	instantiation	42, 402, 306, 308	⊢
	: , : , : , : , :
26	instantiation	42, 402, 306, 308	⊢
	: , : , : , : , :
27	instantiation	54, 260, 43	,  ⊢
	: , :
28	axiom		⊢
	proveit.core_expr_types.conditionals.condition_replacement
29	instantiation	44, 384	⊢
	:
30	theorem		⊢
	proveit.logic.sets.unification.union_inclusion
31	instantiation	328	⊢
	: , :
32	instantiation	50, 297, 314, 400, 45	⊢
	: , : , : , :
33	theorem		⊢
	proveit.numbers.number_sets.integers.disjoint_intervals
34	instantiation	74, 324, 46, 77, 47, 59	⊢
	: , :
35	axiom		⊢
	proveit.logic.booleans.eq_true_intro
36	instantiation	368, 48, 49	,  ⊢
	: , : , :
37	theorem		⊢
	proveit.logic.sets.functions.injections.subset_injection
38	instantiation	50, 297, 298, 400, 51	⊢
	: , : , : , :
39	instantiation	52, 53	⊢
	: , :
40	theorem		⊢
	proveit.physics.quantum.QPE._outcome_prob
41	instantiation	54, 260, 264	,  ⊢
	: , :
42	theorem		⊢
	proveit.core_expr_types.conditionals.true_condition_elimination
43	instantiation	408, 55, 56	,  ⊢
	: , : , :
44	theorem		⊢
	proveit.physics.quantum.QPE._fail_sum_prob_conds_equiv_lemma
45	instantiation	74, 324, 57, 58, 59, 60	⊢
	: , :
46	instantiation	336	⊢
	: , : , :
47	instantiation	65, 286, 89, 61, 62, 63*, 64*	⊢
	: , : , :
48	instantiation	65, 66, 228, 67, 68, 69*, 70*	,  ⊢
	: , : , :
49	instantiation	71, 72, 73*	,  ⊢
	:
50	theorem		⊢
	proveit.numbers.number_sets.integers.interval_subset_eq
51	instantiation	74, 324, 75, 76, 77, 78	⊢
	: , :
52	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
53	instantiation	79, 80	⊢
	: , : , :
54	theorem		⊢
	proveit.physics.quantum.QPE._mod_add_closure
55	instantiation	392, 314, 400	⊢
	: , :
56	assumption		⊢
57	instantiation	336	⊢
	: , : , :
58	instantiation	81, 82, 83	⊢
	: , : , :
59	instantiation	117, 378, 351, 84, 85, 86*	⊢
	: , : , :
60	instantiation	108, 118, 87	⊢
	: , :
61	instantiation	301, 195, 389	⊢
	: , :
62	instantiation	88, 89, 195, 389, 90, 91	⊢
	: , : , :
63	instantiation	332, 92	⊢
	: , :
64	instantiation	319, 93, 94, 95	⊢
	: , : , : , :
65	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
66	instantiation	301, 351, 96	,  ⊢
	: , :
67	instantiation	408, 395, 97	⊢
	: , : , :
68	instantiation	98, 228, 99, 378, 230, 316	,  ⊢
	: , : , :
69	instantiation	288, 100, 101	,  ⊢
	: , : , :
70	instantiation	288, 102, 103	,  ⊢
	: , : , :
71	theorem		⊢
	proveit.physics.quantum.QPE._modabs_in_full_domain_simp
72	instantiation	104, 297, 400, 264, 105	,  ⊢
	: , : , :
73	instantiation	106, 107	,  ⊢
	:
74	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_all
75	instantiation	336	⊢
	: , : , :
76	instantiation	108, 109, 110	⊢
	: , :
77	instantiation	117, 111, 351, 124, 125, 112*, 113*	⊢
	: , : , :
78	instantiation	174, 114	⊢
	: , :
79	theorem		⊢
	proveit.logic.sets.functions.bijections.membership_unfolding
80	instantiation	115, 116	⊢
	: , : , :
81	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
82	instantiation	117, 186, 378, 118, 119, 120*, 121*	⊢
	: , : , :
83	instantiation	174, 122	⊢
	: , :
84	instantiation	301, 124, 378	⊢
	: , :
85	instantiation	123, 351, 124, 378, 125, 126	⊢
	: , : , :
86	instantiation	319, 127, 293, 128	⊢
	: , : , : , :
87	instantiation	309	⊢
	:
88	theorem		⊢
	proveit.numbers.ordering.less_add_right
89	instantiation	220, 389, 130	⊢
	: , :
90	instantiation	129, 389, 130, 351, 300, 131	⊢
	: , : , :
91	instantiation	161, 410	⊢
	:
92	instantiation	319, 199, 132, 133	⊢
	: , : , : , :
93	instantiation	305, 306, 410, 402, 308, 134, 167, 381, 269	⊢
	: , : , : , : , : , :
94	instantiation	305, 410, 306, 134, 283, 308, 167, 381, 327, 343	⊢
	: , : , : , : , : , :
95	instantiation	319, 135, 136, 137	⊢
	: , : , : , :
96	instantiation	318, 228	,  ⊢
	:
97	instantiation	408, 403, 138	⊢
	: , : , :
98	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
99	instantiation	408, 395, 139	⊢
	: , : , :
100	instantiation	305, 402, 410, 306, 171, 308, 202, 339, 173	,  ⊢
	: , : , : , : , : , :
101	instantiation	140, 202, 339, 141	,  ⊢
	: , : , :
102	instantiation	334, 142	⊢
	: , : , :
103	instantiation	288, 143, 144	,  ⊢
	: , : , :
104	theorem		⊢
	proveit.numbers.number_sets.integers.in_interval
105	instantiation	183, 145, 146	,  ⊢
	: , :
106	theorem		⊢
	proveit.numbers.absolute_value.abs_neg_elim
107	instantiation	174, 204	,  ⊢
	: , :
108	theorem		⊢
	proveit.numbers.ordering.relax_equal_to_less_eq
109	instantiation	408, 395, 147	⊢
	: , : , :
110	instantiation	309	⊢
	:
111	instantiation	148, 324, 149, 186, 378, 302	⊢
	: , :
112	instantiation	319, 150, 151, 152	⊢
	: , : , : , :
113	instantiation	332, 153	⊢
	: , :
114	instantiation	203, 231, 205	⊢
	: , : , :
115	theorem		⊢
	proveit.logic.sets.functions.bijections.elim_domain_condition
116	modus ponens	154, 155	⊢
117	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
118	instantiation	361, 362, 405	⊢
	: , : , :
119	instantiation	156, 405	⊢
	:
120	instantiation	341, 367, 157	⊢
	: , :
121	instantiation	288, 158, 159	⊢
	: , : , :
122	instantiation	232, 266	⊢
	:
123	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right
124	instantiation	408, 395, 160	⊢
	: , : , :
125	instantiation	250, 394, 393, 384	⊢
	: , : , :
126	instantiation	161, 402	⊢
	:
127	instantiation	288, 162, 163	⊢
	: , : , :
128	instantiation	332, 303	⊢
	: , :
129	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
130	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
131	instantiation	232, 386	⊢
	:
132	instantiation	309	⊢
	:
133	instantiation	332, 164	⊢
	: , :
134	instantiation	328	⊢
	: , :
135	instantiation	165, 402, 167, 381, 327, 343	⊢
	: , : , : , : , : , : , :
136	instantiation	274, 306, 410, 308, 166, 246, 167, 327, 381, 343, 168*	⊢
	: , : , : , : , : , :
137	instantiation	274, 402, 410, 306, 246, 308, 339, 381, 343, 247*	⊢
	: , : , : , : , : , :
138	instantiation	399, 298, 394	⊢
	: , :
139	instantiation	408, 403, 298	⊢
	: , : , :
140	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
141	instantiation	309	⊢
	:
142	instantiation	288, 169, 170	⊢
	: , : , :
143	instantiation	305, 402, 410, 306, 171, 308, 327, 339, 173	,  ⊢
	: , : , : , : , : , :
144	instantiation	172, 339, 173, 285	,  ⊢
	: , : , :
145	instantiation	330, 297, 298, 280	,  ⊢
	: , : , :
146	instantiation	174, 175	,  ⊢
	: , :
147	instantiation	408, 403, 297	⊢
	: , : , :
148	theorem		⊢
	proveit.numbers.addition.add_real_closure
149	instantiation	336	⊢
	: , : , :
150	instantiation	288, 176, 177	⊢
	: , : , :
151	instantiation	309	⊢
	:
152	instantiation	332, 178	⊢
	: , :
153	instantiation	319, 199, 179, 180	⊢
	: , : , : , :
154	instantiation	181, 182*	⊢
	: , : , : , : , : , :
155	instantiation	183, 184, 185	⊢
	: , :
156	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
157	instantiation	408, 388, 186	⊢
	: , : , :
158	instantiation	288, 187, 188	⊢
	: , : , :
159	instantiation	189, 337, 293	⊢
	: , :
160	instantiation	408, 403, 393	⊢
	: , : , :
161	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
162	instantiation	334, 190	⊢
	: , : , :
163	instantiation	288, 191, 192	⊢
	: , : , :
164	instantiation	288, 193, 194	⊢
	: , : , :
165	theorem		⊢
	proveit.numbers.addition.leftward_commutation
166	instantiation	328	⊢
	: , :
167	instantiation	408, 388, 195	⊢
	: , : , :
168	instantiation	288, 196, 197, 198*	⊢
	: , : , :
169	instantiation	334, 199	⊢
	: , : , :
170	instantiation	288, 200, 201	⊢
	: , : , :
171	instantiation	328	⊢
	: , :
172	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_21
173	instantiation	338, 202	,  ⊢
	:
174	theorem		⊢
	proveit.numbers.ordering.relax_less
175	instantiation	203, 204, 205	,  ⊢
	: , : , :
176	instantiation	334, 271	⊢
	: , : , :
177	instantiation	288, 206, 207	⊢
	: , : , :
178	instantiation	334, 287	⊢
	: , : , :
179	instantiation	332, 208	⊢
	: , :
180	instantiation	332, 209	⊢
	: , :
181	theorem		⊢
	proveit.logic.sets.functions.bijections.bijection_transitivity
182	instantiation	334, 210	⊢
	: , : , :
183	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
184	instantiation	211, 212, 297, 400, 260	⊢
	: , : , : , : , :
185	theorem		⊢
	proveit.physics.quantum.QPE._sample_space_bijection
186	instantiation	408, 395, 213	⊢
	: , : , :
187	instantiation	334, 303	⊢
	: , : , :
188	instantiation	334, 287	⊢
	: , : , :
189	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
190	instantiation	288, 214, 215	⊢
	: , : , :
191	instantiation	305, 306, 410, 402, 308, 216, 337, 343, 367	⊢
	: , : , : , : , : , :
192	instantiation	226, 367, 337, 227	⊢
	: , : , :
193	instantiation	334, 217	⊢
	: , : , :
194	instantiation	288, 218, 219	⊢
	: , : , :
195	instantiation	220, 389, 351	⊢
	: , :
196	instantiation	334, 221	⊢
	: , : , :
197	instantiation	332, 222	⊢
	: , :
198	instantiation	288, 223, 224	⊢
	: , : , :
199	instantiation	225, 339, 367	⊢
	: , :
200	instantiation	305, 306, 410, 402, 308, 283, 327, 343, 367	⊢
	: , : , : , : , : , :
201	instantiation	226, 367, 327, 227	⊢
	: , : , :
202	instantiation	408, 388, 228	,  ⊢
	: , : , :
203	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
204	instantiation	229, 230, 231	,  ⊢
	: , : , :
205	instantiation	232, 405	⊢
	:
206	instantiation	305, 402, 324, 306, 325, 308, 339, 326, 367, 327	⊢
	: , : , : , : , : , :
207	instantiation	291, 306, 410, 308, 233, 339, 326, 367, 285	⊢
	: , : , : , : , : , : , : , :
208	instantiation	263, 269, 339, 343, 234	⊢
	: , : , :
209	instantiation	288, 235, 236	⊢
	: , : , :
210	instantiation	332, 237	⊢
	: , :
211	theorem		⊢
	proveit.numbers.modular.interval_left_shift_bijection
212	instantiation	238, 410, 391	⊢
	: , :
213	instantiation	408, 403, 313	⊢
	: , : , :
214	instantiation	334, 270	⊢
	: , : , :
215	instantiation	288, 239, 240	⊢
	: , : , :
216	instantiation	328	⊢
	: , :
217	instantiation	241, 381	⊢
	:
218	instantiation	305, 402, 410, 306, 283, 308, 242, 327, 343	⊢
	: , : , : , : , : , :
219	instantiation	243, 306, 410, 308, 283, 327, 343	⊢
	: , : , : , :
220	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
221	instantiation	332, 244	⊢
	: , :
222	instantiation	245, 306, 410, 402, 308, 246, 381, 343, 339	⊢
	: , : , : , : , : , :
223	instantiation	334, 247	⊢
	: , : , :
224	instantiation	248, 339	⊢
	:
225	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
226	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
227	instantiation	309	⊢
	:
228	instantiation	408, 395, 249	,  ⊢
	: , : , :
229	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less
230	instantiation	250, 297, 298, 280	,  ⊢
	: , : , :
231	instantiation	251, 252	⊢
	:
232	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
233	instantiation	328	⊢
	: , :
234	instantiation	294, 253, 254	⊢
	: , : , :
235	instantiation	288, 255, 256	⊢
	: , : , :
236	instantiation	288, 257, 258	⊢
	: , : , :
237	instantiation	259, 260, 261	⊢
	: , :
238	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
239	instantiation	305, 306, 410, 402, 308, 307, 337, 312, 367	⊢
	: , : , : , : , : , :
240	instantiation	274, 402, 410, 306, 275, 308, 337, 312, 367, 276*	⊢
	: , : , : , : , : , :
241	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
242	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
243	theorem		⊢
	proveit.numbers.addition.elim_zero_any
244	instantiation	262, 339	⊢
	:
245	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
246	instantiation	328	⊢
	: , :
247	instantiation	263, 367, 381, 311	⊢
	: , : , :
248	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
249	instantiation	408, 403, 264	,  ⊢
	: , : , :
250	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
251	theorem		⊢
	proveit.numbers.number_sets.integers.negative_if_in_neg_int
252	instantiation	265, 266	⊢
	:
253	instantiation	288, 267, 268	⊢
	: , : , :
254	instantiation	341, 339, 269	⊢
	: , :
255	instantiation	334, 270	⊢
	: , : , :
256	instantiation	334, 271	⊢
	: , : , :
257	instantiation	288, 272, 273	⊢
	: , : , :
258	instantiation	274, 306, 410, 402, 308, 275, 312, 367, 327, 276*	⊢
	: , : , : , : , : , :
259	axiom		⊢
	proveit.physics.quantum.QPE._mod_add_def
260	theorem		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
261	instantiation	408, 277, 278	⊢
	: , : , :
262	theorem		⊢
	proveit.numbers.negation.mult_neg_one_left
263	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
264	instantiation	408, 279, 280	,  ⊢
	: , : , :
265	theorem		⊢
	proveit.numbers.negation.int_neg_closure
266	instantiation	281, 282, 347	⊢
	: , :
267	instantiation	305, 402, 410, 306, 283, 308, 339, 327, 343	⊢
	: , : , : , : , : , :
268	instantiation	284, 339, 343, 285	⊢
	: , : , :
269	instantiation	408, 388, 286	⊢
	: , : , :
270	instantiation	334, 303	⊢
	: , : , :
271	instantiation	334, 287	⊢
	: , : , :
272	instantiation	288, 289, 290	⊢
	: , : , :
273	instantiation	291, 306, 402, 410, 308, 292, 337, 312, 367, 327, 293	⊢
	: , : , : , : , : , : , : , :
274	theorem		⊢
	proveit.numbers.addition.association
275	instantiation	328	⊢
	: , :
276	instantiation	294, 295, 296	⊢
	: , : , :
277	instantiation	392, 297, 400	⊢
	: , :
278	assumption		⊢
279	instantiation	392, 297, 298	⊢
	: , :
280	assumption		⊢
281	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
282	instantiation	299, 372, 300	⊢
	:
283	instantiation	328	⊢
	: , :
284	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_12
285	instantiation	309	⊢
	:
286	instantiation	301, 302, 353	⊢
	: , :
287	instantiation	334, 303	⊢
	: , : , :
288	axiom		⊢
	proveit.logic.equality.equals_transitivity
289	instantiation	305, 306, 410, 402, 308, 307, 337, 312, 304	⊢
	: , : , : , : , : , :
290	instantiation	305, 410, 324, 306, 307, 325, 308, 337, 312, 326, 367, 327	⊢
	: , : , : , : , : , :
291	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
292	instantiation	328	⊢
	: , :
293	instantiation	309	⊢
	:
294	theorem		⊢
	proveit.logic.equality.sub_right_side_into
295	instantiation	310, 367, 381, 311	⊢
	: , : , :
296	instantiation	341, 367, 312	⊢
	: , :
297	instantiation	399, 313, 394	⊢
	: , :
298	instantiation	406, 314	⊢
	:
299	theorem		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
300	instantiation	315, 316, 317	⊢
	: , : , :
301	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
302	instantiation	318, 351	⊢
	:
303	instantiation	319, 320, 321, 322	⊢
	: , : , : , :
304	instantiation	323, 324, 325, 326, 367, 327	⊢
	: , :
305	theorem		⊢
	proveit.numbers.addition.disassociation
306	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
307	instantiation	328	⊢
	: , :
308	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
309	axiom		⊢
	proveit.logic.equality.equals_reflexivity
310	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add_reversed
311	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
312	instantiation	408, 388, 329	⊢
	: , : , :
313	instantiation	406, 400	⊢
	:
314	instantiation	399, 372, 394	⊢
	: , :
315	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
316	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
317	instantiation	330, 394, 393, 384	⊢
	: , : , :
318	theorem		⊢
	proveit.numbers.negation.real_closure
319	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
320	instantiation	334, 331	⊢
	: , : , :
321	instantiation	332, 333	⊢
	: , :
322	instantiation	334, 335	⊢
	: , : , :
323	theorem		⊢
	proveit.numbers.addition.add_complex_closure
324	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
325	instantiation	336	⊢
	: , : , :
326	instantiation	338, 337	⊢
	:
327	instantiation	338, 339	⊢
	:
328	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
329	instantiation	408, 395, 340	⊢
	: , : , :
330	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
331	instantiation	341, 342, 343	⊢
	: , :
332	theorem		⊢
	proveit.logic.equality.equals_reversal
333	instantiation	344, 381, 353, 352, 369	⊢
	: , : , :
334	axiom		⊢
	proveit.logic.equality.substitution
335	instantiation	345, 346, 347	⊢
	: , :
336	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
337	instantiation	348, 349, 350	⊢
	: , :
338	theorem		⊢
	proveit.numbers.negation.complex_closure
339	instantiation	408, 388, 351	⊢
	: , : , :
340	instantiation	408, 403, 401	⊢
	: , : , :
341	theorem		⊢
	proveit.numbers.addition.commutation
342	instantiation	408, 388, 352	⊢
	: , : , :
343	instantiation	408, 388, 353	⊢
	: , : , :
344	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
345	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
346	instantiation	408, 354, 355	⊢
	: , : , :
347	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
348	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
349	instantiation	356, 367, 357, 358	⊢
	: , :
350	instantiation	408, 388, 359	⊢
	: , : , :
351	instantiation	408, 395, 360	⊢
	: , : , :
352	instantiation	361, 362, 398	⊢
	: , : , :
353	instantiation	408, 395, 363	⊢
	: , : , :
354	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
355	instantiation	408, 364, 365	⊢
	: , : , :
356	theorem		⊢
	proveit.numbers.division.div_complex_closure
357	instantiation	366, 381, 367	⊢
	: , :
358	instantiation	368, 369, 370	⊢
	: , : , :
359	instantiation	408, 395, 371	⊢
	: , : , :
360	instantiation	408, 403, 372	⊢
	: , : , :
361	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
362	instantiation	373, 374	⊢
	: , :
363	instantiation	408, 403, 375	⊢
	: , : , :
364	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
365	instantiation	408, 376, 377	⊢
	: , : , :
366	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
367	instantiation	408, 388, 378	⊢
	: , : , :
368	theorem		⊢
	proveit.logic.equality.sub_left_side_into
369	instantiation	379, 386	⊢
	:
370	instantiation	380, 381	⊢
	:
371	instantiation	408, 403, 382	⊢
	: , : , :
372	instantiation	408, 383, 384	⊢
	: , : , :
373	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
374	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
375	instantiation	406, 394	⊢
	:
376	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
377	instantiation	408, 385, 386	⊢
	: , : , :
378	instantiation	408, 395, 387	⊢
	: , : , :
379	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
380	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
381	instantiation	408, 388, 389	⊢
	: , : , :
382	instantiation	390, 407, 391	⊢
	: , :
383	instantiation	392, 394, 393	⊢
	: , :
384	assumption		⊢
385	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
386	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
387	instantiation	408, 403, 394	⊢
	: , : , :
388	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
389	instantiation	408, 395, 396	⊢
	: , : , :
390	theorem		⊢
	proveit.numbers.exponentiation.exp_int_closure
391	instantiation	408, 397, 398	⊢
	: , : , :
392	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
393	instantiation	399, 400, 401	⊢
	: , :
394	instantiation	408, 409, 402	⊢
	: , : , :
395	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
396	instantiation	408, 403, 407	⊢
	: , : , :
397	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
398	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
399	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
400	instantiation	408, 404, 405	⊢
	: , : , :
401	instantiation	406, 407	⊢
	:
402	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
403	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
404	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
405	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
406	theorem		⊢
	proveit.numbers.negation.int_closure
407	instantiation	408, 409, 410	⊢
	: , : , :
408	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
409	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
410	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements