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