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	6, 4, 5	,  ⊢
	: , : , :
3	instantiation	6, 7, 8	,  ⊢
	: , : , :
4	instantiation	11, 9, 10	,  ⊢
	: , : , :
5	instantiation	14, 180	⊢
	:
6	theorem		⊢
	proveit.logic.equality.sub_left_side_into
7	instantiation	11, 12, 13	,  ⊢
	: , : , :
8	instantiation	14, 145	⊢
	:
9	instantiation	50, 96, 15, 51, 16, 17*	⊢
	: , : , :
10	instantiation	18, 51, 96, 48, 19	,  ⊢
	: , : , :
11	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less
12	instantiation	20, 21, 22, 23*	,  ⊢
	: , : , :
13	instantiation	24, 174, 216, 25, 175, 26, 200	⊢
	: , : , : , : , :
14	theorem		⊢
	proveit.numbers.addition.elim_zero_left
15	instantiation	199, 45	⊢
	:
16	instantiation	69, 71, 45, 27	⊢
	: , :
17	instantiation	28, 98, 29, 145, 30	⊢
	: , : , :
18	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
19	instantiation	31, 96, 111, 68	⊢
	: , : , :
20	theorem		⊢
	proveit.logic.equality.sub_right_side_into
21	instantiation	32, 33, 34	,  ⊢
	: , : , :
22	instantiation	35, 202, 36, 37, 145, 87, 122, 38*	⊢
	: , : , :
23	instantiation	161, 39, 40	⊢
	: , : , :
24	theorem		⊢
	proveit.numbers.addition.term_as_strong_upper_bound
25	instantiation	110, 41	⊢
	:
26	instantiation	42, 43	⊢
	:
27	instantiation	91, 121, 93, 104, 44, 95	⊢
	: , : , :
28	theorem		⊢
	proveit.numbers.addition.subtraction.negated_add
29	instantiation	214, 190, 45	⊢
	: , : , :
30	instantiation	161, 46, 81	⊢
	: , : , :
31	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
32	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
33	instantiation	47, 51, 48, 111, 49	,  ⊢
	: , : , :
34	instantiation	50, 111, 51, 52, 53	⊢
	: , : , :
35	theorem		⊢
	proveit.numbers.division.distribute_frac_through_sum
36	instantiation	188	⊢
	: , :
37	instantiation	214, 190, 54	⊢
	: , : , :
38	instantiation	55, 86, 87, 122, 65*	⊢
	: , :
39	instantiation	147, 56	⊢
	: , : , :
40	instantiation	161, 57, 58	⊢
	: , : , :
41	instantiation	59, 216, 174, 175, 60	⊢
	: , : , : , : , :
42	theorem		⊢
	proveit.numbers.negation.real_neg_closure
43	instantiation	61, 62, 63, 122	⊢
	: , :
44	instantiation	64, 154, 185, 137	⊢
	: , : , :
45	instantiation	120, 104, 121, 122	⊢
	: , :
46	instantiation	147, 65	⊢
	: , : , :
47	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
48	instantiation	66, 96, 111, 68	⊢
	: , : , :
49	instantiation	67, 96, 111, 68	⊢
	: , : , :
50	theorem		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
51	instantiation	199, 71	⊢
	:
52	instantiation	199, 70	⊢
	:
53	instantiation	69, 70, 71, 72	⊢
	: , :
54	instantiation	214, 207, 73	⊢
	: , : , :
55	theorem		⊢
	proveit.numbers.division.neg_frac_neg_numerator
56	instantiation	74, 75, 100, 76*	⊢
	: , :
57	instantiation	173, 216, 209, 174, 77, 175, 98, 80	⊢
	: , : , : , : , : , :
58	instantiation	78, 174, 209, 216, 175, 79, 98, 80, 81*	⊢
	: , : , : , : , : , :
59	theorem		⊢
	proveit.numbers.addition.add_nat_pos_from_nonneg
60	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
61	theorem		⊢
	proveit.numbers.division.div_real_pos_closure
62	instantiation	214, 83, 82	⊢
	: , : , :
63	instantiation	214, 83, 84	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
65	instantiation	85, 86, 87, 122, 88*	⊢
	: , :
66	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
67	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_upper_bound
68	instantiation	89, 90	⊢
	:
69	theorem		⊢
	proveit.numbers.negation.negated_weak_bound
70	instantiation	120, 92, 121, 122	⊢
	: , :
71	instantiation	120, 93, 121, 122	⊢
	: , :
72	instantiation	91, 121, 92, 93, 94, 95	⊢
	: , : , :
73	instantiation	214, 212, 168	⊢
	: , : , :
74	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
75	instantiation	214, 190, 96	⊢
	: , : , :
76	instantiation	97, 98	⊢
	:
77	instantiation	188	⊢
	: , :
78	theorem		⊢
	proveit.numbers.addition.association
79	instantiation	188	⊢
	: , :
80	instantiation	99, 100	⊢
	:
81	instantiation	101, 213, 203, 102*	⊢
	: , : , : , :
82	instantiation	214, 103, 151	⊢
	: , : , :
83	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
84	instantiation	214, 103, 138	⊢
	: , : , :
85	theorem		⊢
	proveit.numbers.division.div_as_mult
86	instantiation	214, 190, 104	⊢
	: , : , :
87	instantiation	214, 190, 121	⊢
	: , : , :
88	instantiation	161, 105, 106	⊢
	: , : , :
89	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_in_interval
90	assumption		⊢
91	theorem		⊢
	proveit.numbers.division.weak_div_from_numer_bound__pos_denom
92	instantiation	214, 207, 107	⊢
	: , : , :
93	instantiation	214, 207, 108	⊢
	: , : , :
94	instantiation	109, 154, 185, 137	⊢
	: , : , :
95	instantiation	110, 138	⊢
	:
96	instantiation	199, 111	⊢
	:
97	theorem		⊢
	proveit.numbers.negation.double_negation
98	instantiation	214, 190, 111	⊢
	: , : , :
99	theorem		⊢
	proveit.numbers.negation.complex_closure
100	instantiation	214, 190, 112	⊢
	: , : , :
101	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
102	instantiation	161, 113, 114	⊢
	: , : , :
103	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
104	instantiation	204, 205, 196	⊢
	: , : , :
105	instantiation	147, 115	⊢
	: , : , :
106	instantiation	116, 171, 117, 189, 131, 118*	⊢
	: , : , :
107	instantiation	214, 212, 154	⊢
	: , : , :
108	instantiation	214, 212, 119	⊢
	: , : , :
109	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
110	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
111	instantiation	120, 200, 186, 131	⊢
	: , :
112	instantiation	120, 200, 121, 122	⊢
	: , :
113	instantiation	155, 209, 123, 124, 125, 126	⊢
	: , : , : , :
114	instantiation	127, 128, 129	⊢
	:
115	instantiation	130, 171, 198, 191, 131, 132*	⊢
	: , : , :
116	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
117	instantiation	133, 198, 191	⊢
	: , :
118	instantiation	161, 134, 135	⊢
	: , : , :
119	instantiation	214, 136, 137	⊢
	: , : , :
120	theorem		⊢
	proveit.numbers.division.div_real_closure
121	instantiation	204, 205, 138	⊢
	: , : , :
122	instantiation	143, 138	⊢
	:
123	instantiation	188	⊢
	: , :
124	instantiation	188	⊢
	: , :
125	instantiation	161, 139, 140	⊢
	: , : , :
126	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
127	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
128	instantiation	214, 190, 141	⊢
	: , : , :
129	instantiation	143, 142	⊢
	:
130	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
131	instantiation	143, 202	⊢
	:
132	instantiation	144, 179, 145, 146*	⊢
	: , :
133	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
134	instantiation	147, 148	⊢
	: , : , :
135	instantiation	149, 150, 151, 152*	⊢
	: , :
136	instantiation	153, 154, 185	⊢
	: , :
137	assumption		⊢
138	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
139	instantiation	155, 209, 156, 157, 158, 159	⊢
	: , : , : , :
140	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
141	instantiation	214, 207, 160	⊢
	: , : , :
142	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
143	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
144	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
145	instantiation	214, 190, 200	⊢
	: , : , :
146	instantiation	170, 179	⊢
	:
147	axiom		⊢
	proveit.logic.equality.substitution
148	instantiation	161, 162, 163	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
150	instantiation	214, 164, 165	⊢
	: , : , :
151	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
152	instantiation	166, 171	⊢
	:
153	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
154	instantiation	167, 168, 213	⊢
	: , :
155	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
156	instantiation	188	⊢
	: , :
157	instantiation	188	⊢
	: , :
158	instantiation	169, 171	⊢
	:
159	instantiation	170, 171	⊢
	:
160	instantiation	214, 212, 172	⊢
	: , : , :
161	axiom		⊢
	proveit.logic.equality.equals_transitivity
162	instantiation	173, 174, 209, 216, 175, 176, 179, 180, 177	⊢
	: , : , : , : , : , :
163	instantiation	178, 179, 180, 181	⊢
	: , : , :
164	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
165	instantiation	214, 182, 183	⊢
	: , : , :
166	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
167	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
168	instantiation	184, 185	⊢
	:
169	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
170	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
171	instantiation	214, 190, 186	⊢
	: , : , :
172	instantiation	214, 215, 187	⊢
	: , : , :
173	theorem		⊢
	proveit.numbers.addition.disassociation
174	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
175	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
176	instantiation	188	⊢
	: , :
177	instantiation	214, 190, 189	⊢
	: , : , :
178	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
179	instantiation	214, 190, 198	⊢
	: , : , :
180	instantiation	214, 190, 191	⊢
	: , : , :
181	instantiation	192	⊢
	:
182	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
183	instantiation	214, 193, 194	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.negation.int_closure
185	instantiation	214, 195, 196	⊢
	: , : , :
186	instantiation	214, 207, 197	⊢
	: , : , :
187	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
188	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
189	instantiation	199, 198	⊢
	:
190	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
191	instantiation	199, 200	⊢
	:
192	axiom		⊢
	proveit.logic.equality.equals_reflexivity
193	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
194	instantiation	214, 201, 202	⊢
	: , : , :
195	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
196	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
197	instantiation	214, 212, 203	⊢
	: , : , :
198	instantiation	204, 205, 206	⊢
	: , : , :
199	theorem		⊢
	proveit.numbers.negation.real_closure
200	instantiation	214, 207, 208	⊢
	: , : , :
201	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
202	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
203	instantiation	214, 215, 209	⊢
	: , : , :
204	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
205	instantiation	210, 211	⊢
	: , :
206	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
207	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
208	instantiation	214, 212, 213	⊢
	: , : , :
209	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
210	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
211	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
212	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
213	instantiation	214, 215, 216	⊢
	: , : , :
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