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