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