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	163	⊢
2	instantiation	4, 255, 5, 99, 6, 7, 8*	,  ⊢
	: , : , :
3	instantiation	9, 77, 173, 133, 10*	⊢
	: , :
4	theorem		⊢
	proveit.numbers.division.weak_div_from_numer_bound__pos_denom
5	instantiation	254, 255, 40	⊢
	: , :
6	instantiation	177, 11, 12	,  ⊢
	: , : , :
7	instantiation	13, 137	⊢
	:
8	instantiation	226, 14, 15	⊢
	: , : , :
9	theorem		⊢
	proveit.numbers.division.div_as_mult
10	instantiation	226, 16, 17	⊢
	: , : , :
11	instantiation	46, 18, 19	,  ⊢
	: , : , :
12	instantiation	163, 20, 21	⊢
	: , : , :
13	theorem		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
14	instantiation	184, 101, 186, 22, 140*	⊢
	: , : , :
15	instantiation	203, 22	⊢
	:
16	instantiation	182, 23	⊢
	: , : , :
17	instantiation	24, 217, 25, 86, 42, 26*	⊢
	: , : , :
18	instantiation	27, 115, 28, 266, 29, 30*	⊢
	: , : , :
19	instantiation	31, 266, 115, 32, 33, 34*	,  ⊢
	: , : , :
20	instantiation	35, 255, 57, 266, 140*	⊢
	: , : , :
21	instantiation	36, 288, 239, 241, 173, 37, 38, 39*	⊢
	: , : , : , : , : , :
22	instantiation	286, 259, 40	⊢
	: , : , :
23	instantiation	41, 217, 260, 258, 42, 43*	⊢
	: , : , :
24	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
25	instantiation	213, 260, 87	⊢
	: , :
26	instantiation	226, 44, 45	⊢
	: , : , :
27	theorem		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
28	instantiation	213, 98, 97	⊢
	: , :
29	instantiation	46, 47, 48	⊢
	: , : , :
30	instantiation	226, 49, 50	⊢
	: , : , :
31	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
32	instantiation	213, 99, 258	⊢
	: , :
33	instantiation	163, 51, 52	⊢
	: , : , :
34	instantiation	226, 53, 54	⊢
	: , : , :
35	theorem		⊢
	proveit.numbers.modular.mod_abs_scaled
36	theorem		⊢
	proveit.numbers.multiplication.distribute_through_subtract
37	instantiation	286, 259, 83	⊢
	: , : , :
38	instantiation	286, 259, 256	⊢
	: , : , :
39	instantiation	163, 55, 56	⊢
	: , : , :
40	instantiation	131, 57, 266, 58	⊢
	: , :
41	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
42	instantiation	85, 248	⊢
	:
43	instantiation	59, 245, 244, 60*	⊢
	: , :
44	instantiation	238, 239, 283, 288, 241, 61, 245, 63, 62	⊢
	: , : , : , : , : , :
45	instantiation	243, 245, 63, 64	⊢
	: , : , :
46	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
47	instantiation	163, 65, 66, 67*	⊢
	: , : , :
48	instantiation	177, 68, 69	⊢
	: , : , :
49	instantiation	238, 288, 283, 239, 70, 241, 72, 73, 71	⊢
	: , : , : , : , : , :
50	instantiation	243, 72, 73, 74	⊢
	: , : , :
51	assumption		⊢
52	axiom		⊢
	proveit.physics.quantum.QPE._best_floor_def
53	instantiation	238, 239, 283, 288, 241, 75, 77, 242, 244	⊢
	: , : , : , : , : , :
54	instantiation	76, 244, 77, 246	⊢
	: , : , :
55	instantiation	163, 78, 79	⊢
	: , : , :
56	instantiation	122, 80, 81, 82	⊢
	: , : , : , :
57	instantiation	213, 83, 84	⊢
	: , :
58	instantiation	85, 250	⊢
	:
59	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
60	instantiation	202, 245	⊢
	:
61	instantiation	257	⊢
	: , :
62	instantiation	286, 259, 86	⊢
	: , : , :
63	instantiation	286, 259, 87	⊢
	: , : , :
64	instantiation	261	⊢
	:
65	instantiation	88, 116, 132, 137, 89*	⊢
	: , : , :
66	instantiation	95, 146, 181	⊢
	: , :
67	instantiation	90, 91, 137, 92, 93*	⊢
	: , :
68	instantiation	110, 94	⊢
	: , :
69	instantiation	95, 96, 180	⊢
	: , :
70	instantiation	257	⊢
	: , :
71	instantiation	286, 259, 97	⊢
	: , : , :
72	instantiation	286, 259, 115	⊢
	: , : , :
73	instantiation	286, 259, 98	⊢
	: , : , :
74	instantiation	261	⊢
	:
75	instantiation	257	⊢
	: , :
76	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
77	instantiation	286, 259, 99	⊢
	: , : , :
78	instantiation	100, 244, 175, 101, 186	⊢
	: , : , : , : , :
79	instantiation	226, 102, 103	⊢
	: , : , :
80	instantiation	182, 104	⊢
	: , : , :
81	instantiation	182, 105	⊢
	: , : , :
82	instantiation	172, 175	⊢
	:
83	instantiation	106, 190, 255, 133	⊢
	: , :
84	instantiation	176, 256	⊢
	:
85	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
86	instantiation	176, 260	⊢
	:
87	instantiation	176, 107	⊢
	:
88	theorem		⊢
	proveit.numbers.modular.mod_abs_of_difference_bound
89	instantiation	226, 108, 109	⊢
	: , : , :
90	theorem		⊢
	proveit.numbers.modular.mod_abs_x_reduce_to_abs_x
91	instantiation	213, 193, 162	⊢
	: , :
92	instantiation	110, 111	⊢
	: , :
93	instantiation	112, 113, 114*	⊢
	:
94	instantiation	148, 265, 266, 209	⊢
	: , : , :
95	theorem		⊢
	proveit.numbers.addition.commutation
96	instantiation	286, 259, 153	⊢
	: , : , :
97	instantiation	176, 115	⊢
	:
98	instantiation	131, 116, 255, 133	⊢
	: , :
99	instantiation	286, 272, 117	⊢
	: , : , :
100	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
101	instantiation	286, 200, 118	⊢
	: , : , :
102	instantiation	182, 119	⊢
	: , : , :
103	instantiation	182, 120	⊢
	: , : , :
104	instantiation	203, 244	⊢
	:
105	instantiation	203, 175	⊢
	:
106	theorem		⊢
	proveit.numbers.division.div_real_closure
107	instantiation	269, 270, 206	⊢
	: , : , :
108	instantiation	182, 121	⊢
	: , : , :
109	instantiation	122, 123, 124, 125	⊢
	: , : , : , :
110	theorem		⊢
	proveit.numbers.ordering.relax_less
111	instantiation	126, 127, 128	⊢
	: , : , :
112	theorem		⊢
	proveit.numbers.absolute_value.abs_neg_elim
113	instantiation	129, 130	⊢
	: , :
114	instantiation	141, 181, 180	⊢
	: , :
115	instantiation	131, 132, 255, 133	⊢
	: , :
116	instantiation	213, 190, 162	⊢
	: , :
117	instantiation	286, 134, 135	⊢
	: , : , :
118	instantiation	286, 136, 137	⊢
	: , : , :
119	instantiation	226, 138, 139	⊢
	: , : , :
120	instantiation	182, 140	⊢
	: , : , :
121	instantiation	141, 175, 181	⊢
	: , :
122	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
123	instantiation	238, 239, 283, 288, 241, 143, 175, 146, 142	⊢
	: , : , : , : , : , :
124	instantiation	238, 283, 239, 143, 144, 241, 175, 146, 161, 181	⊢
	: , : , : , : , : , :
125	instantiation	145, 239, 288, 241, 175, 146, 181, 147	⊢
	: , : , : , : , : , : , : , :
126	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
127	instantiation	148, 265, 266, 149	⊢
	: , : , :
128	instantiation	177, 150, 151	⊢
	: , : , :
129	theorem		⊢
	proveit.numbers.addition.subtraction.nonpos_difference
130	instantiation	152, 237	⊢
	:
131	theorem		⊢
	proveit.numbers.modular.mod_abs_real_closure
132	instantiation	213, 190, 153	⊢
	: , :
133	instantiation	154, 218, 155	⊢
	: , :
134	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_nonzero_within_rational
135	instantiation	156, 218, 157	⊢
	: , :
136	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
137	instantiation	158, 195, 260	⊢
	: , :
138	instantiation	182, 159	⊢
	: , : , :
139	instantiation	203, 173	⊢
	:
140	instantiation	202, 173	⊢
	:
141	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_subtract
142	instantiation	160, 161, 181	⊢
	: , :
143	instantiation	257	⊢
	: , :
144	instantiation	257	⊢
	: , :
145	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
146	instantiation	286, 259, 162	⊢
	: , : , :
147	instantiation	261	⊢
	:
148	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
149	instantiation	163, 164, 165	⊢
	: , : , :
150	instantiation	166, 233	⊢
	:
151	instantiation	226, 167, 168	⊢
	: , : , :
152	theorem		⊢
	proveit.numbers.rounding.floor_x_le_x
153	instantiation	176, 193	⊢
	:
154	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
155	instantiation	286, 231, 169	⊢
	: , : , :
156	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_nonzero_closure
157	instantiation	262, 170, 171	⊢
	: , :
158	theorem		⊢
	proveit.numbers.exponentiation.exp_real_pos_closure
159	instantiation	172, 173	⊢
	:
160	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
161	instantiation	174, 175	⊢
	:
162	instantiation	176, 237	⊢
	:
163	theorem		⊢
	proveit.logic.equality.sub_right_side_into
164	instantiation	177, 209, 178	⊢
	: , : , :
165	instantiation	179, 180, 181	⊢
	: , :
166	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
167	instantiation	182, 183	⊢
	: , : , :
168	instantiation	184, 185, 186, 204, 187*, 188*	⊢
	: , : , :
169	instantiation	286, 249, 285	⊢
	: , : , :
170	instantiation	286, 205, 285	⊢
	: , : , :
171	instantiation	281, 189	⊢
	:
172	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
173	instantiation	286, 259, 255	⊢
	: , : , :
174	theorem		⊢
	proveit.numbers.negation.complex_closure
175	instantiation	286, 259, 190	⊢
	: , : , :
176	theorem		⊢
	proveit.numbers.negation.real_closure
177	theorem		⊢
	proveit.logic.equality.sub_left_side_into
178	instantiation	191, 192	⊢
	:
179	theorem		⊢
	proveit.numbers.absolute_value.abs_diff_reversal
180	instantiation	286, 259, 237	⊢
	: , : , :
181	instantiation	286, 259, 193	⊢
	: , : , :
182	axiom		⊢
	proveit.logic.equality.substitution
183	instantiation	194, 195, 260, 266, 196, 197, 198*	⊢
	: , : , : , :
184	theorem		⊢
	proveit.numbers.division.frac_cancel_left
185	instantiation	286, 200, 199	⊢
	: , : , :
186	instantiation	286, 200, 201	⊢
	: , : , :
187	instantiation	202, 217	⊢
	:
188	instantiation	203, 204	⊢
	:
189	instantiation	286, 205, 206	⊢
	: , : , :
190	instantiation	286, 272, 207	⊢
	: , : , :
191	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
192	instantiation	208, 265, 266, 209	⊢
	: , : , :
193	instantiation	286, 272, 210	⊢
	: , : , :
194	theorem		⊢
	proveit.numbers.exponentiation.exp_factored_real
195	instantiation	286, 211, 212	⊢
	: , : , :
196	instantiation	213, 260, 258	⊢
	: , :
197	instantiation	214, 215	⊢
	: , :
198	instantiation	216, 217	⊢
	:
199	instantiation	286, 219, 218	⊢
	: , : , :
200	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
201	instantiation	286, 219, 220	⊢
	: , : , :
202	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
203	theorem		⊢
	proveit.numbers.division.frac_one_denom
204	instantiation	286, 259, 221	⊢
	: , : , :
205	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
206	axiom		⊢
	proveit.physics.quantum.QPE._n_in_natural_pos
207	instantiation	286, 280, 222	⊢
	: , : , :
208	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
209	instantiation	223, 237	⊢
	:
210	instantiation	286, 280, 224	⊢
	: , : , :
211	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
212	instantiation	286, 225, 248	⊢
	: , : , :
213	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
214	theorem		⊢
	proveit.logic.equality.equals_reversal
215	instantiation	226, 227, 228	⊢
	: , : , :
216	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
217	instantiation	286, 259, 229	⊢
	: , : , :
218	instantiation	286, 231, 230	⊢
	: , : , :
219	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
220	instantiation	286, 231, 232	⊢
	: , : , :
221	instantiation	269, 270, 233	⊢
	: , : , :
222	instantiation	286, 234, 235	⊢
	: , : , :
223	theorem		⊢
	proveit.numbers.rounding.real_minus_floor_interval
224	instantiation	236, 237	⊢
	:
225	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
226	axiom		⊢
	proveit.logic.equality.equals_transitivity
227	instantiation	238, 288, 283, 239, 240, 241, 244, 245, 242	⊢
	: , : , : , : , : , :
228	instantiation	243, 244, 245, 246	⊢
	: , : , :
229	instantiation	286, 272, 247	⊢
	: , : , :
230	instantiation	286, 249, 248	⊢
	: , : , :
231	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
232	instantiation	286, 249, 250	⊢
	: , : , :
233	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
234	instantiation	251, 252, 253	⊢
	: , :
235	assumption		⊢
236	axiom		⊢
	proveit.numbers.rounding.floor_is_an_int
237	instantiation	254, 255, 256	⊢
	: , :
238	theorem		⊢
	proveit.numbers.addition.disassociation
239	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
240	instantiation	257	⊢
	: , :
241	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
242	instantiation	286, 259, 258	⊢
	: , : , :
243	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
244	instantiation	286, 259, 266	⊢
	: , : , :
245	instantiation	286, 259, 260	⊢
	: , : , :
246	instantiation	261	⊢
	:
247	instantiation	286, 280, 278	⊢
	: , : , :
248	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
249	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
250	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
251	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
252	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
253	instantiation	262, 271, 274	⊢
	: , :
254	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
255	instantiation	286, 272, 263	⊢
	: , : , :
256	instantiation	264, 265, 266, 267	⊢
	: , : , :
257	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
258	instantiation	286, 272, 268	⊢
	: , : , :
259	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
260	instantiation	269, 270, 285	⊢
	: , : , :
261	axiom		⊢
	proveit.logic.equality.equals_reflexivity
262	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
263	instantiation	286, 280, 271	⊢
	: , : , :
264	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
265	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
266	instantiation	286, 272, 273	⊢
	: , : , :
267	axiom		⊢
	proveit.physics.quantum.QPE._phase_in_interval
268	instantiation	286, 280, 274	⊢
	: , : , :
269	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
270	instantiation	275, 276	⊢
	: , :
271	instantiation	277, 278, 279	⊢
	: , :
272	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
273	instantiation	286, 280, 282	⊢
	: , : , :
274	instantiation	281, 282	⊢
	:
275	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
276	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
277	theorem		⊢
	proveit.numbers.exponentiation.exp_int_closure
278	instantiation	286, 287, 283	⊢
	: , : , :
279	instantiation	286, 284, 285	⊢
	: , : , :
280	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
281	theorem		⊢
	proveit.numbers.negation.int_closure
282	instantiation	286, 287, 288	⊢
	: , : , :
283	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
284	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
285	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
286	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
287	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
288	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements