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	73, 4	⊢
	:
3	instantiation	5, 6, 7	⊢
	: , : , :
4	instantiation	8, 112, 114	⊢
	: , :
5	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
6	instantiation	46, 9, 27	⊢
	: , : , :
7	instantiation	57, 55, 10, 11, 12*, 13*	⊢
	: , : , :
8	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
9	instantiation	14, 15, 16	⊢
	: , : , :
10	instantiation	74, 75, 18	⊢
	: , :
11	instantiation	17, 75, 18, 86, 49, 19	⊢
	: , : , :
12	instantiation	147, 20, 21	⊢
	: , : , :
13	instantiation	22, 23, 24*	⊢
	: , :
14	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
15	instantiation	25, 26, 27	⊢
	: , : , :
16	instantiation	28, 86, 29, 142, 30, 31, 32*, 33*	⊢
	: , : , :
17	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
18	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
19	instantiation	34, 124	⊢
	:
20	instantiation	88, 35	⊢
	: , : , :
21	instantiation	36, 37	⊢
	:
22	theorem		⊢
	proveit.logic.equality.equals_reversal
23	instantiation	38, 105, 199, 192, 106, 39, 54, 63	⊢
	: , : , : , : , : , :
24	instantiation	147, 40, 41	⊢
	: , : , :
25	theorem		⊢
	proveit.logic.equality.sub_left_side_into
26	instantiation	42, 192, 112, 114, 43, 44*	⊢
	: , : , : , : , : , :
27	instantiation	88, 45	⊢
	: , : , :
28	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
29	instantiation	74, 137, 87	⊢
	: , :
30	instantiation	46, 47, 48	⊢
	: , : , :
31	instantiation	121, 49	⊢
	: , :
32	instantiation	50, 192, 199, 105, 51, 106, 63, 110, 64	⊢
	: , : , : , : , : , :
33	instantiation	52, 63, 54	⊢
	: , :
34	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
35	instantiation	53, 54	⊢
	:
36	theorem		⊢
	proveit.numbers.addition.elim_zero_left
37	instantiation	197, 189, 55	⊢
	: , : , :
38	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
39	instantiation	180	⊢
	: , :
40	instantiation	88, 56	⊢
	: , : , :
41	instantiation	181, 63	⊢
	:
42	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_factor_bound
43	instantiation	57, 136, 190, 58, 59, 60*, 61*	⊢
	: , : , :
44	instantiation	62, 192, 63, 64	⊢
	: , : , : , :
45	instantiation	147, 65, 66	⊢
	: , : , :
46	theorem		⊢
	proveit.logic.equality.sub_right_side_into
47	instantiation	67, 68, 69	⊢
	: , :
48	instantiation	70, 179, 71, 110, 158, 72*	⊢
	: , :
49	instantiation	73, 112	⊢
	:
50	theorem		⊢
	proveit.numbers.multiplication.disassociation
51	instantiation	180	⊢
	: , :
52	theorem		⊢
	proveit.numbers.multiplication.commutation
53	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
54	instantiation	197, 189, 142	⊢
	: , : , :
55	instantiation	74, 75, 86	⊢
	: , :
56	instantiation	76, 188, 196, 77*	⊢
	: , : , : , :
57	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
58	instantiation	197, 193, 78	⊢
	: , : , :
59	instantiation	79, 190, 137, 161, 80, 81	⊢
	: , : , :
60	instantiation	82, 116, 183, 83	⊢
	: , : , :
61	instantiation	147, 84, 85	⊢
	: , : , :
62	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
63	instantiation	197, 189, 86	⊢
	: , : , :
64	instantiation	197, 189, 87	⊢
	: , : , :
65	instantiation	88, 89	⊢
	: , : , :
66	instantiation	90, 158	⊢
	:
67	theorem		⊢
	proveit.numbers.absolute_value.weak_upper_bound
68	instantiation	91, 119, 142, 120	⊢
	: , : , :
69	instantiation	121, 92	⊢
	: , :
70	theorem		⊢
	proveit.numbers.absolute_value.abs_prod
71	instantiation	180	⊢
	: , :
72	instantiation	93, 94	⊢
	:
73	theorem		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
74	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
75	instantiation	197, 193, 95	⊢
	: , : , :
76	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
77	instantiation	147, 96, 97	⊢
	: , : , :
78	instantiation	197, 195, 98	⊢
	: , : , :
79	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
80	instantiation	99, 190, 161, 100, 101, 102, 103*	⊢
	: , : , :
81	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
82	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
83	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
84	instantiation	104, 105, 199, 192, 106, 107, 110, 116, 108	⊢
	: , : , : , : , : , :
85	instantiation	109, 116, 110, 111	⊢
	: , : , :
86	instantiation	197, 113, 112	⊢
	: , : , :
87	instantiation	197, 113, 114	⊢
	: , : , :
88	axiom		⊢
	proveit.logic.equality.substitution
89	instantiation	115, 116, 158, 117*	⊢
	: , :
90	theorem		⊢
	proveit.numbers.absolute_value.abs_even
91	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
92	instantiation	118, 119, 142, 120	⊢
	: , : , :
93	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
94	instantiation	121, 122	⊢
	: , :
95	instantiation	197, 123, 124	⊢
	: , : , :
96	instantiation	165, 199, 125, 126, 127, 128	⊢
	: , : , : , :
97	instantiation	129, 130, 131	⊢
	:
98	instantiation	197, 198, 132	⊢
	: , : , :
99	theorem		⊢
	proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
100	instantiation	155, 156, 134	⊢
	: , : , :
101	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
102	instantiation	133, 134	⊢
	:
103	instantiation	135, 183	⊢
	:
104	theorem		⊢
	proveit.numbers.addition.disassociation
105	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
106	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
107	instantiation	180	⊢
	: , :
108	instantiation	197, 189, 136	⊢
	: , : , :
109	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
110	instantiation	197, 189, 137	⊢
	: , : , :
111	instantiation	138	⊢
	:
112	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
113	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
114	instantiation	139, 140	⊢
	:
115	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
116	instantiation	197, 189, 161	⊢
	: , : , :
117	instantiation	181, 158	⊢
	:
118	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
119	instantiation	141, 142	⊢
	:
120	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_round_in_interval
121	theorem		⊢
	proveit.numbers.ordering.relax_less
122	instantiation	143, 172	⊢
	:
123	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
124	instantiation	144, 145, 146	⊢
	: , :
125	instantiation	180	⊢
	: , :
126	instantiation	180	⊢
	: , :
127	instantiation	147, 148, 149	⊢
	: , : , :
128	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
129	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
130	instantiation	197, 189, 150	⊢
	: , : , :
131	instantiation	178, 151	⊢
	:
132	instantiation	152, 153, 192	⊢
	: , :
133	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
134	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
135	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
136	instantiation	197, 193, 154	⊢
	: , : , :
137	instantiation	155, 156, 172	⊢
	: , : , :
138	axiom		⊢
	proveit.logic.equality.equals_reflexivity
139	theorem		⊢
	proveit.numbers.absolute_value.abs_nonzero_closure
140	instantiation	157, 158, 159	⊢
	:
141	theorem		⊢
	proveit.numbers.negation.real_closure
142	instantiation	160, 161, 190, 162	⊢
	: , :
143	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
144	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
145	instantiation	197, 164, 163	⊢
	: , : , :
146	instantiation	197, 164, 179	⊢
	: , : , :
147	axiom		⊢
	proveit.logic.equality.equals_transitivity
148	instantiation	165, 199, 166, 167, 168, 169	⊢
	: , : , : , :
149	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
150	instantiation	197, 193, 170	⊢
	: , : , :
151	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
152	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
153	instantiation	197, 171, 172	⊢
	: , : , :
154	instantiation	197, 195, 173	⊢
	: , : , :
155	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
156	instantiation	174, 175	⊢
	: , :
157	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
158	instantiation	197, 189, 176	⊢
	: , : , :
159	assumption		⊢
160	theorem		⊢
	proveit.numbers.division.div_real_closure
161	instantiation	197, 193, 177	⊢
	: , : , :
162	instantiation	178, 179	⊢
	:
163	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
164	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
165	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
166	instantiation	180	⊢
	: , :
167	instantiation	180	⊢
	: , :
168	instantiation	181, 183	⊢
	:
169	instantiation	182, 183	⊢
	:
170	instantiation	197, 195, 184	⊢
	: , : , :
171	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
172	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
173	instantiation	185, 188	⊢
	:
174	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
175	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
176	instantiation	186, 187	⊢
	:
177	instantiation	197, 195, 188	⊢
	: , : , :
178	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
179	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
180	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
181	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
182	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
183	instantiation	197, 189, 190	⊢
	: , : , :
184	instantiation	197, 198, 191	⊢
	: , : , :
185	theorem		⊢
	proveit.numbers.negation.int_closure
186	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
187	theorem		⊢
	proveit.physics.quantum.QPE._best_round_is_int
188	instantiation	197, 198, 192	⊢
	: , : , :
189	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
190	instantiation	197, 193, 194	⊢
	: , : , :
191	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
192	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
193	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
194	instantiation	197, 195, 196	⊢
	: , : , :
195	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
196	instantiation	197, 198, 199	⊢
	: , : , :
197	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
198	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
199	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements