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