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