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