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	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
2	instantiation	5, 4, 7	⊢
	: , : , :
3	instantiation	5, 6, 7	⊢
	: , : , :
4	instantiation	8, 87, 128, 12, 9, 14, 10*	⊢
	: , : , :
5	theorem		⊢
	proveit.logic.equality.sub_right_side_into
6	instantiation	11, 87, 12, 148, 13, 14, 22*	⊢
	: , : , :
7	instantiation	15, 16, 97, 69, 34, 17*	⊢
	: , : , :
8	theorem		⊢
	proveit.numbers.division.weak_div_from_numer_bound__pos_denom
9	instantiation	18, 19, 20	⊢
	: , : , :
10	instantiation	21, 131, 69, 34, 22*	⊢
	: , :
11	theorem		⊢
	proveit.numbers.division.strong_div_from_numer_bound__pos_denom
12	instantiation	93, 37, 40	⊢
	: , :
13	instantiation	23, 24, 25	⊢
	: , : , :
14	instantiation	26, 116	⊢
	:
15	theorem		⊢
	proveit.numbers.division.distribute_frac_through_subtract
16	instantiation	190, 151, 37	⊢
	: , : , :
17	instantiation	118, 27, 28	⊢
	: , : , :
18	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
19	instantiation	39, 58, 128, 40, 29, 30*	⊢
	: , : , :
20	instantiation	31, 40, 58, 37, 32	⊢
	: , : , :
21	theorem		⊢
	proveit.numbers.division.neg_frac_neg_numerator
22	instantiation	33, 131, 69, 34, 35*	⊢
	: , :
23	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
24	instantiation	36, 40, 37, 129, 38	⊢
	: , : , :
25	instantiation	39, 129, 40, 41, 42, 43*	⊢
	: , : , :
26	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
27	instantiation	44, 45, 46, 49, 47*	⊢
	: , : , :
28	instantiation	48, 49	⊢
	:
29	instantiation	60, 152, 109, 148, 50, 62, 51*, 63*	⊢
	: , : , :
30	instantiation	52, 113	⊢
	:
31	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
32	instantiation	53, 58, 129, 59	⊢
	: , : , :
33	theorem		⊢
	proveit.numbers.division.div_as_mult
34	instantiation	102, 116	⊢
	:
35	instantiation	118, 54, 55	⊢
	: , : , :
36	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
37	instantiation	56, 58, 129, 59	⊢
	: , : , :
38	instantiation	57, 58, 129, 59	⊢
	: , : , :
39	theorem		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
40	instantiation	161, 109	⊢
	:
41	instantiation	93, 148, 152	⊢
	: , :
42	instantiation	60, 152, 145, 109, 61, 62, 63*, 64*	⊢
	: , : , :
43	instantiation	118, 65, 66	⊢
	: , : , :
44	theorem		⊢
	proveit.numbers.division.frac_cancel_left
45	instantiation	190, 121, 67	⊢
	: , : , :
46	instantiation	190, 121, 68	⊢
	: , : , :
47	instantiation	117, 69	⊢
	:
48	theorem		⊢
	proveit.numbers.division.frac_one_denom
49	instantiation	190, 151, 70	⊢
	: , : , :
50	instantiation	71, 170, 185, 158	⊢
	: , : , :
51	instantiation	81, 114, 131, 72*	⊢
	: , :
52	theorem		⊢
	proveit.numbers.addition.elim_zero_left
53	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
54	instantiation	110, 73	⊢
	: , : , :
55	instantiation	74, 124, 75, 150, 91, 76*	⊢
	: , : , :
56	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
57	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
58	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
59	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
60	theorem		⊢
	proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound
61	instantiation	77, 170, 185, 158	⊢
	: , : , :
62	instantiation	78, 79	⊢
	: , :
63	instantiation	81, 114, 97, 80*	⊢
	: , :
64	instantiation	81, 114, 127, 82*	⊢
	: , :
65	instantiation	132, 187, 176, 133, 83, 134, 114, 131, 139	⊢
	: , : , : , : , : , :
66	instantiation	137, 114, 131, 84	⊢
	: , : , :
67	instantiation	190, 141, 85	⊢
	: , : , :
68	instantiation	190, 141, 86	⊢
	: , : , :
69	instantiation	190, 151, 87	⊢
	: , : , :
70	instantiation	88, 89	⊢
	:
71	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
72	instantiation	126, 131	⊢
	:
73	instantiation	90, 124, 162, 152, 91, 92*	⊢
	: , : , :
74	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
75	instantiation	93, 162, 152	⊢
	: , :
76	instantiation	118, 94, 95	⊢
	: , : , :
77	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
78	theorem		⊢
	proveit.numbers.ordering.relax_less
79	instantiation	96, 183	⊢
	:
80	instantiation	126, 97	⊢
	:
81	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
82	instantiation	118, 98, 99	⊢
	: , : , :
83	instantiation	149	⊢
	: , :
84	instantiation	153	⊢
	:
85	instantiation	190, 154, 100	⊢
	: , : , :
86	instantiation	190, 154, 101	⊢
	: , : , :
87	instantiation	171, 172, 116	⊢
	: , : , :
88	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
89	theorem		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
90	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
91	instantiation	102, 166	⊢
	:
92	instantiation	103, 138, 114, 104*	⊢
	: , :
93	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
94	instantiation	110, 105	⊢
	: , : , :
95	instantiation	106, 107, 189, 108*	⊢
	: , :
96	theorem		⊢
	proveit.numbers.number_sets.integers.negative_if_in_neg_int
97	instantiation	190, 151, 109	⊢
	: , : , :
98	instantiation	110, 111	⊢
	: , : , :
99	instantiation	112, 113, 114, 115*	⊢
	: , :
100	instantiation	190, 165, 116	⊢
	: , : , :
101	instantiation	190, 165, 189	⊢
	: , : , :
102	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
103	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
104	instantiation	117, 138	⊢
	:
105	instantiation	118, 119, 120	⊢
	: , : , :
106	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
107	instantiation	190, 121, 122	⊢
	: , : , :
108	instantiation	123, 124	⊢
	:
109	instantiation	190, 159, 125	⊢
	: , : , :
110	axiom		⊢
	proveit.logic.equality.substitution
111	instantiation	126, 127	⊢
	:
112	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
113	instantiation	190, 151, 128	⊢
	: , : , :
114	instantiation	190, 151, 129	⊢
	: , : , :
115	instantiation	130, 131	⊢
	:
116	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
117	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
118	axiom		⊢
	proveit.logic.equality.equals_transitivity
119	instantiation	132, 133, 176, 187, 134, 135, 138, 139, 136	⊢
	: , : , : , : , : , :
120	instantiation	137, 138, 139, 140	⊢
	: , : , :
121	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
122	instantiation	190, 141, 142	⊢
	: , : , :
123	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
124	instantiation	190, 151, 143	⊢
	: , : , :
125	instantiation	190, 169, 144	⊢
	: , : , :
126	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
127	instantiation	190, 151, 145	⊢
	: , : , :
128	instantiation	190, 159, 146	⊢
	: , : , :
129	instantiation	190, 159, 147	⊢
	: , : , :
130	theorem		⊢
	proveit.numbers.negation.double_negation
131	instantiation	190, 151, 148	⊢
	: , : , :
132	theorem		⊢
	proveit.numbers.addition.disassociation
133	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
134	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
135	instantiation	149	⊢
	: , :
136	instantiation	190, 151, 150	⊢
	: , : , :
137	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
138	instantiation	190, 151, 162	⊢
	: , : , :
139	instantiation	190, 151, 152	⊢
	: , : , :
140	instantiation	153	⊢
	:
141	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
142	instantiation	190, 154, 155	⊢
	: , : , :
143	instantiation	190, 159, 156	⊢
	: , : , :
144	instantiation	190, 157, 158	⊢
	: , : , :
145	instantiation	190, 159, 160	⊢
	: , : , :
146	instantiation	190, 169, 178	⊢
	: , : , :
147	instantiation	190, 169, 179	⊢
	: , : , :
148	instantiation	171, 172, 192	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
150	instantiation	161, 162	⊢
	:
151	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
152	instantiation	190, 163, 164	⊢
	: , : , :
153	axiom		⊢
	proveit.logic.equality.equals_reflexivity
154	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
155	instantiation	190, 165, 166	⊢
	: , : , :
156	instantiation	190, 169, 167	⊢
	: , : , :
157	instantiation	168, 170, 185	⊢
	: , :
158	assumption		⊢
159	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
160	instantiation	190, 169, 170	⊢
	: , : , :
161	theorem		⊢
	proveit.numbers.negation.real_closure
162	instantiation	171, 172, 173	⊢
	: , : , :
163	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_neg_within_real
164	instantiation	190, 174, 175	⊢
	: , : , :
165	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
166	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
167	instantiation	190, 186, 176	⊢
	: , : , :
168	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
169	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
170	instantiation	177, 178, 179	⊢
	: , :
171	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
172	instantiation	180, 181	⊢
	: , :
173	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
174	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_neg_within_real_neg
175	instantiation	190, 182, 183	⊢
	: , : , :
176	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
177	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
178	instantiation	184, 185	⊢
	:
179	instantiation	190, 186, 187	⊢
	: , : , :
180	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
181	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
182	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.neg_int_within_rational_neg
183	instantiation	188, 189	⊢
	:
184	theorem		⊢
	proveit.numbers.negation.int_closure
185	instantiation	190, 191, 192	⊢
	: , : , :
186	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
187	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
188	theorem		⊢
	proveit.numbers.negation.int_neg_closure
189	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
190	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
191	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
192	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
*equality replacement requirements