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	reference	83	⊢
2	instantiation	4, 30, 47, 5, 6, 7*	⊢
	: , : , :
3	instantiation	8, 36, 9, 159, 10, 11*	⊢
	: , : , :
4	theorem		⊢
	proveit.numbers.division.strong_div_from_numer_bound__pos_denom
5	instantiation	12, 47, 95, 13, 14, 15*, 16*	⊢
	: , : , :
6	instantiation	97, 31	⊢
	:
7	instantiation	17, 18, 19	⊢
	:
8	theorem		⊢
	proveit.numbers.exponentiation.exp_eq_real
9	instantiation	191, 20, 21	⊢
	: , : , :
10	instantiation	22, 33, 144, 43, 23*	⊢
	: , :
11	instantiation	24, 25	⊢
	:
12	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
13	instantiation	191, 170, 26	⊢
	: , : , :
14	instantiation	97, 27	⊢
	:
15	instantiation	127, 28, 29	⊢
	: , : , :
16	theorem		⊢
	proveit.numbers.numerals.decimals.add_5_4
17	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
18	instantiation	191, 181, 30	⊢
	: , : , :
19	instantiation	188, 31	⊢
	:
20	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_nonneg_within_real
21	instantiation	32, 33	⊢
	:
22	theorem		⊢
	proveit.numbers.absolute_value.abs_eq
23	instantiation	34, 35	⊢
	:
24	theorem		⊢
	proveit.numbers.exponentiation.exponentiated_one
25	instantiation	191, 181, 36	⊢
	: , : , :
26	instantiation	191, 186, 37	⊢
	: , : , :
27	theorem		⊢
	proveit.numbers.numerals.decimals.posnat5
28	instantiation	38, 40	⊢
	:
29	instantiation	39, 40, 41	⊢
	: , :
30	instantiation	191, 170, 42	⊢
	: , : , :
31	theorem		⊢
	proveit.numbers.numerals.decimals.posnat9
32	theorem		⊢
	proveit.numbers.absolute_value.abs_complex_closure
33	instantiation	83, 144, 43	⊢
	: , : , :
34	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
35	instantiation	44, 184	⊢
	:
36	instantiation	191, 170, 45	⊢
	: , : , :
37	instantiation	191, 183, 46	⊢
	: , : , :
38	theorem		⊢
	proveit.numbers.addition.elim_zero_right
39	theorem		⊢
	proveit.numbers.addition.commutation
40	instantiation	191, 181, 47	⊢
	: , : , :
41	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
42	instantiation	191, 186, 48	⊢
	: , : , :
43	instantiation	83, 49, 50	⊢
	: , : , :
44	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
45	instantiation	191, 186, 51	⊢
	: , : , :
46	theorem		⊢
	proveit.numbers.numerals.decimals.nat5
47	instantiation	191, 170, 52	⊢
	: , : , :
48	instantiation	191, 183, 53	⊢
	: , : , :
49	instantiation	127, 54, 84	⊢
	: , : , :
50	instantiation	55, 193, 56	⊢
	: , :
51	instantiation	191, 183, 132	⊢
	: , : , :
52	instantiation	191, 186, 57	⊢
	: , : , :
53	theorem		⊢
	proveit.numbers.numerals.decimals.nat9
54	modus ponens	58, 59	⊢
55	theorem		⊢
	proveit.numbers.modular.int_mod_elimination
56	instantiation	62, 63, 64, 185, 60	⊢
	: , : , :
57	instantiation	191, 183, 61	⊢
	: , : , :
58	theorem		⊢
	proveit.physics.quantum.QPE._alpha_ideal_case
59	instantiation	62, 63, 64, 77, 65	⊢
	: , : , :
60	instantiation	69, 66, 67	⊢
	: , :
61	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
62	theorem		⊢
	proveit.numbers.number_sets.integers.in_interval
63	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
64	instantiation	68, 187, 103	⊢
	: , :
65	instantiation	69, 70, 71	⊢
	: , :
66	instantiation	127, 70, 84	⊢
	: , : , :
67	instantiation	127, 71, 84	⊢
	: , : , :
68	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
69	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
70	instantiation	72, 182, 95, 150, 73, 74, 75*	⊢
	: , : , :
71	instantiation	76, 77, 187, 103, 78, 79	⊢
	: , : , :
72	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
73	instantiation	80, 95, 159, 96	⊢
	: , : , :
74	instantiation	81, 87	⊢
	: , :
75	instantiation	82, 175	⊢
	:
76	theorem		⊢
	proveit.numbers.ordering.less_add_right_weak_int
77	instantiation	83, 185, 84	⊢
	: , : , :
78	instantiation	85, 182, 150, 159, 86, 87, 158*	⊢
	: , : , :
79	instantiation	88, 89, 90	⊢
	: , :
80	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
81	theorem		⊢
	proveit.numbers.ordering.relax_less
82	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
83	theorem		⊢
	proveit.logic.equality.sub_left_side_into
84	instantiation	91, 182, 150, 161, 92, 93*	⊢
	: , : , :
85	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
86	instantiation	94, 95, 159, 96	⊢
	: , : , :
87	instantiation	97, 193	⊢
	:
88	theorem		⊢
	proveit.numbers.ordering.relax_equal_to_less_eq
89	instantiation	191, 170, 98	⊢
	: , : , :
90	instantiation	151	⊢
	:
91	theorem		⊢
	proveit.numbers.multiplication.left_mult_eq_real
92	instantiation	99, 100	⊢
	: , :
93	instantiation	127, 101, 102	⊢
	: , : , :
94	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
95	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
96	axiom		⊢
	proveit.physics.quantum.QPE._phase_in_interval
97	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
98	instantiation	191, 186, 103	⊢
	: , : , :
99	theorem		⊢
	proveit.logic.equality.equals_reversal
100	instantiation	104, 171, 115, 105, 116, 106*, 107*	⊢
	: , : , :
101	instantiation	127, 108, 109	⊢
	: , : , :
102	instantiation	110, 111, 112, 113	⊢
	: , : , : , :
103	instantiation	114, 176	⊢
	:
104	theorem		⊢
	proveit.numbers.addition.right_add_eq_rational
105	instantiation	127, 115, 116	⊢
	: , : , :
106	instantiation	117, 149	⊢
	:
107	instantiation	155, 118, 119	⊢
	: , : , :
108	instantiation	120, 144, 145, 121, 122	⊢
	: , : , : , : , :
109	instantiation	155, 123, 124	⊢
	: , : , :
110	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
111	instantiation	165, 125	⊢
	: , : , :
112	instantiation	165, 126	⊢
	: , : , :
113	instantiation	174, 145	⊢
	:
114	theorem		⊢
	proveit.numbers.negation.int_closure
115	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.zero_is_rational
116	instantiation	127, 128, 129	⊢
	: , : , :
117	theorem		⊢
	proveit.numbers.addition.elim_zero_left
118	instantiation	130, 131, 132, 184, 133, 134, 137, 135, 149	⊢
	: , : , : , : , : , :
119	instantiation	136, 149, 137, 138	⊢
	: , : , :
120	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
121	instantiation	191, 140, 139	⊢
	: , : , :
122	instantiation	191, 140, 141	⊢
	: , : , :
123	instantiation	165, 142	⊢
	: , : , :
124	instantiation	165, 143	⊢
	: , : , :
125	instantiation	167, 144	⊢
	:
126	instantiation	167, 145	⊢
	:
127	theorem		⊢
	proveit.logic.equality.sub_right_side_into
128	instantiation	146, 185	⊢
	:
129	assumption		⊢
130	theorem		⊢
	proveit.numbers.addition.disassociation
131	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
132	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
133	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
134	instantiation	147	⊢
	: , :
135	instantiation	148, 149	⊢
	:
136	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
137	instantiation	191, 181, 150	⊢
	: , : , :
138	instantiation	151	⊢
	:
139	instantiation	191, 153, 152	⊢
	: , : , :
140	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
141	instantiation	191, 153, 154	⊢
	: , : , :
142	instantiation	155, 156, 157	⊢
	: , : , :
143	instantiation	165, 158	⊢
	: , : , :
144	instantiation	191, 181, 159	⊢
	: , : , :
145	instantiation	191, 181, 160	⊢
	: , : , :
146	axiom		⊢
	proveit.physics.quantum.QPE._delta_b_def
147	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
148	theorem		⊢
	proveit.numbers.negation.complex_closure
149	instantiation	191, 181, 161	⊢
	: , : , :
150	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
151	axiom		⊢
	proveit.logic.equality.equals_reflexivity
152	instantiation	191, 163, 162	⊢
	: , : , :
153	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
154	instantiation	191, 163, 164	⊢
	: , : , :
155	axiom		⊢
	proveit.logic.equality.equals_transitivity
156	instantiation	165, 166	⊢
	: , : , :
157	instantiation	167, 175	⊢
	:
158	instantiation	168, 175	⊢
	:
159	instantiation	191, 170, 169	⊢
	: , : , :
160	instantiation	191, 170, 178	⊢
	: , : , :
161	instantiation	191, 170, 171	⊢
	: , : , :
162	instantiation	191, 172, 193	⊢
	: , : , :
163	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
164	instantiation	191, 172, 173	⊢
	: , : , :
165	axiom		⊢
	proveit.logic.equality.substitution
166	instantiation	174, 175	⊢
	:
167	theorem		⊢
	proveit.numbers.division.frac_one_denom
168	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
169	instantiation	191, 186, 176	⊢
	: , : , :
170	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
171	instantiation	177, 178, 179, 180	⊢
	: , :
172	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
173	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
174	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
175	instantiation	191, 181, 182	⊢
	: , : , :
176	instantiation	191, 183, 184	⊢
	: , : , :
177	theorem		⊢
	proveit.numbers.division.div_rational_closure
178	instantiation	191, 186, 185	⊢
	: , : , :
179	instantiation	191, 186, 187	⊢
	: , : , :
180	instantiation	188, 193	⊢
	:
181	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
182	instantiation	189, 190, 193	⊢
	: , : , :
183	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
184	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
185	theorem		⊢
	proveit.physics.quantum.QPE._best_round_is_int
186	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
187	instantiation	191, 192, 193	⊢
	: , : , :
188	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
189	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
190	instantiation	194, 195	⊢
	: , :
191	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
192	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
193	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
194	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
195	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements