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