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.strong_bound_via_right_term_bound
2	reference	189	⊢
3	instantiation	6, 182	⊢
	:
4	instantiation	6, 8	⊢
	:
5	instantiation	7, 8, 182, 9	⊢
	: , :
6	theorem		⊢
	proveit.numbers.negation.real_closure
7	theorem		⊢
	proveit.numbers.negation.negated_strong_bound
8	instantiation	121, 182, 11	⊢
	: , :
9	instantiation	10, 182, 11, 189, 12, 183, 54*	⊢
	: , : , :
10	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
11	instantiation	13, 79, 32, 23	⊢
	: , :
12	instantiation	14, 32, 79, 15, 16, 17*	⊢
	: , : , :
13	theorem		⊢
	proveit.numbers.division.div_real_closure
14	theorem		⊢
	proveit.numbers.division.strong_div_from_numer_bound__pos_denom
15	instantiation	18, 19, 20	⊢
	: , : , :
16	instantiation	49, 48	⊢
	:
17	instantiation	21, 22, 23	⊢
	:
18	theorem		⊢
	proveit.logic.equality.sub_left_side_into
19	instantiation	24, 79, 188, 25, 26, 27*, 28*	⊢
	: , : , :
20	instantiation	128, 29, 30, 31*	⊢
	: , : , :
21	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
22	instantiation	195, 167, 32	⊢
	: , : , :
23	instantiation	91, 33	⊢
	:
24	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
25	instantiation	169, 87, 182	⊢
	: , :
26	instantiation	128, 34, 35	⊢
	: , : , :
27	instantiation	124, 36, 37	⊢
	: , : , :
28	instantiation	38, 39, 40, 41	⊢
	: , : , : , :
29	instantiation	128, 42, 43	⊢
	: , : , :
30	instantiation	112, 197, 175, 107, 156, 109, 110, 162, 44*, 45*	⊢
	: , : , : , : , : , :
31	instantiation	124, 46, 47	⊢
	: , : , :
32	instantiation	153, 165, 175	⊢
	: , :
33	instantiation	195, 114, 48	⊢
	: , : , :
34	instantiation	49, 50	⊢
	:
35	instantiation	112, 197, 175, 144, 51, 145, 162, 52, 110, 53*, 54*	⊢
	: , : , : , : , : , :
36	instantiation	106, 197, 175, 144, 59, 145, 55, 61, 110	⊢
	: , : , : , : , : , :
37	instantiation	56, 144, 175, 145, 59, 61, 110	⊢
	: , : , : , :
38	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
39	instantiation	106, 144, 175, 197, 145, 58, 71, 162, 57	⊢
	: , : , : , : , : , :
40	instantiation	106, 175, 144, 58, 59, 145, 71, 162, 61, 110	⊢
	: , : , : , : , : , :
41	instantiation	69, 197, 175, 60, 71, 162, 61, 110, 62*	⊢
	: , : , : , : , : , :
42	instantiation	88, 63	⊢
	: , :
43	instantiation	112, 197, 175, 144, 107, 145, 157, 109, 110, 64*	⊢
	: , : , : , : , : , :
44	instantiation	124, 65, 66	⊢
	: , : , :
45	instantiation	67, 197, 156, 162	⊢
	: , : , : , :
46	instantiation	106, 144, 175, 145, 68, 107, 71, 109, 110	⊢
	: , : , : , : , : , :
47	instantiation	69, 197, 175, 70, 71, 109, 110, 72*	⊢
	: , : , : , : , : , :
48	instantiation	73, 165, 74	⊢
	:
49	theorem		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
50	instantiation	176, 178, 75	⊢
	: , :
51	instantiation	158	⊢
	: , :
52	instantiation	195, 167, 76	⊢
	: , : , :
53	instantiation	124, 77, 78	⊢
	: , : , :
54	instantiation	127, 162	⊢
	:
55	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
56	theorem		⊢
	proveit.numbers.addition.elim_zero_any
57	instantiation	195, 167, 79	⊢
	: , : , :
58	instantiation	158	⊢
	: , :
59	instantiation	158	⊢
	: , :
60	instantiation	158	⊢
	: , :
61	instantiation	195, 167, 97	⊢
	: , : , :
62	instantiation	88, 80, 81*	⊢
	: , :
63	instantiation	150, 157, 159, 82*, 152*	⊢
	: , : , :
64	instantiation	124, 83, 84	⊢
	: , : , :
65	instantiation	143, 197, 175, 140, 156, 162	⊢
	: , : , : , : , : , :
66	instantiation	124, 85, 86	⊢
	: , : , :
67	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
68	instantiation	158	⊢
	: , :
69	theorem		⊢
	proveit.numbers.addition.association
70	instantiation	158	⊢
	: , :
71	instantiation	195, 167, 87	⊢
	: , : , :
72	instantiation	88, 89, 90*	⊢
	: , :
73	theorem		⊢
	proveit.numbers.exponentiation.sqrd_pos_closure
74	instantiation	91, 92	⊢
	:
75	instantiation	131, 93, 132	⊢
	: , :
76	instantiation	195, 173, 93	⊢
	: , : , :
77	instantiation	143, 197, 175, 144, 94, 145, 162, 136	⊢
	: , : , : , : , : , :
78	instantiation	124, 95, 96	⊢
	: , : , :
79	instantiation	169, 97, 189	⊢
	: , :
80	instantiation	112, 144, 175, 197, 145, 98, 110, 99, 162, 100*	⊢
	: , : , : , : , : , :
81	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_3
82	instantiation	161, 157	⊢
	:
83	instantiation	101, 175, 102, 103, 104, 105	⊢
	: , : , : , :
84	instantiation	106, 197, 175, 144, 107, 145, 108, 109, 110	⊢
	: , : , : , : , : , :
85	instantiation	134, 144, 175, 145, 113, 135, 156, 162, 111*	⊢
	: , : , : , : , : , :
86	instantiation	134, 197, 175, 144, 135, 145, 136, 162, 137*	⊢
	: , : , : , : , : , :
87	instantiation	121, 149, 138	⊢
	: , :
88	theorem		⊢
	proveit.logic.equality.equals_reversal
89	instantiation	112, 144, 175, 197, 145, 113, 156, 162	⊢
	: , : , : , : , : , :
90	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
91	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
92	instantiation	195, 114, 115	⊢
	: , : , :
93	instantiation	176, 116, 178	⊢
	: , :
94	instantiation	158	⊢
	: , :
95	instantiation	124, 117, 118	⊢
	: , : , :
96	instantiation	119, 120, 136	⊢
	: , :
97	instantiation	121, 122, 182	⊢
	: , :
98	instantiation	158	⊢
	: , :
99	instantiation	195, 167, 122	⊢
	: , : , :
100	instantiation	123, 162	⊢
	:
101	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
102	instantiation	158	⊢
	: , :
103	instantiation	158	⊢
	: , :
104	instantiation	124, 125, 126	⊢
	: , : , :
105	instantiation	127, 157	⊢
	:
106	theorem		⊢
	proveit.numbers.addition.disassociation
107	instantiation	158	⊢
	: , :
108	instantiation	128, 129, 130	⊢
	: , : , :
109	instantiation	195, 167, 170	⊢
	: , : , :
110	instantiation	195, 167, 189	⊢
	: , : , :
111	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
112	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
113	instantiation	158	⊢
	: , :
114	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
115	instantiation	131, 174, 132	⊢
	: , :
116	instantiation	195, 179, 133	⊢
	: , : , :
117	instantiation	141, 197, 144, 145, 162, 136	⊢
	: , : , : , : , : , : , :
118	instantiation	134, 144, 175, 197, 145, 135, 162, 136, 137*	⊢
	: , : , : , : , : , :
119	theorem		⊢
	proveit.numbers.multiplication.commutation
120	instantiation	195, 167, 138	⊢
	: , : , :
121	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
122	instantiation	195, 191, 139	⊢
	: , : , :
123	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
124	axiom		⊢
	proveit.logic.equality.equals_transitivity
125	instantiation	143, 197, 175, 144, 140, 145, 157, 156, 162	⊢
	: , : , : , : , : , :
126	instantiation	141, 144, 197, 145, 157, 156, 162	⊢
	: , : , : , : , : , : , :
127	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
128	theorem		⊢
	proveit.logic.equality.sub_right_side_into
129	instantiation	155, 142, 162	⊢
	: , :
130	instantiation	143, 144, 175, 197, 145, 146, 156, 157, 162	⊢
	: , : , : , : , : , :
131	theorem		⊢
	proveit.numbers.addition.add_real_pos_closure_bin
132	instantiation	195, 179, 147	⊢
	: , : , :
133	instantiation	195, 184, 148	⊢
	: , : , :
134	theorem		⊢
	proveit.numbers.multiplication.association
135	instantiation	158	⊢
	: , :
136	instantiation	195, 167, 149	⊢
	: , : , :
137	instantiation	150, 162, 159, 151*, 152*	⊢
	: , : , :
138	instantiation	153, 182, 175	⊢
	: , :
139	instantiation	195, 193, 154	⊢
	: , : , :
140	instantiation	158	⊢
	: , :
141	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
142	instantiation	155, 156, 157	⊢
	: , :
143	theorem		⊢
	proveit.numbers.multiplication.disassociation
144	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
145	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
146	instantiation	158	⊢
	: , :
147	instantiation	195, 184, 159	⊢
	: , : , :
148	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
149	instantiation	195, 191, 160	⊢
	: , : , :
150	theorem		⊢
	proveit.numbers.exponentiation.product_of_posnat_powers
151	instantiation	161, 162	⊢
	:
152	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
153	theorem		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
154	instantiation	195, 196, 163	⊢
	: , : , :
155	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
156	instantiation	195, 167, 164	⊢
	: , : , :
157	instantiation	195, 167, 165	⊢
	: , : , :
158	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
159	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
160	instantiation	195, 193, 166	⊢
	: , : , :
161	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
162	instantiation	195, 167, 182	⊢
	: , : , :
163	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
164	instantiation	195, 191, 168	⊢
	: , : , :
165	instantiation	169, 170, 189	⊢
	: , :
166	instantiation	195, 196, 171	⊢
	: , : , :
167	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
168	instantiation	195, 193, 172	⊢
	: , : , :
169	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
170	instantiation	195, 173, 174	⊢
	: , : , :
171	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
172	instantiation	195, 196, 175	⊢
	: , : , :
173	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
174	instantiation	176, 177, 178	⊢
	: , :
175	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
176	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
177	instantiation	195, 179, 180	⊢
	: , : , :
178	instantiation	181, 182, 183	⊢
	:
179	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
180	instantiation	195, 184, 185	⊢
	: , : , :
181	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
182	instantiation	186, 188, 189, 190	⊢
	: , : , :
183	instantiation	187, 188, 189, 190	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
185	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
186	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
187	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
188	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
189	instantiation	195, 191, 192	⊢
	: , : , :
190	axiom		⊢
	proveit.physics.quantum.QPE._eps_in_interval
191	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
192	instantiation	195, 193, 194	⊢
	: , : , :
193	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
194	instantiation	195, 196, 197	⊢
	: , : , :
195	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
196	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
197	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements