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