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	11	⊢
2	instantiation	26, 4, 13	⊢
	: , : , :
3	instantiation	5, 43, 107, 130, 6*	⊢
	: , :
4	instantiation	7, 8, 9	⊢
	: , : , :
5	theorem		⊢
	proveit.numbers.division.div_as_mult
6	instantiation	62, 10, 19	⊢
	: , : , :
7	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
8	instantiation	11, 12, 13	⊢
	: , : , :
9	instantiation	14, 65, 15, 116, 16, 17, 18*, 19*	⊢
	: , : , :
10	instantiation	67, 20	⊢
	: , : , :
11	theorem		⊢
	proveit.logic.equality.sub_left_side_into
12	instantiation	21, 149, 90, 92, 22, 23*	⊢
	: , : , : , : , : , :
13	instantiation	67, 24	⊢
	: , : , :
14	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
15	instantiation	25, 110, 66	⊢
	: , :
16	instantiation	26, 27, 28	⊢
	: , : , :
17	instantiation	99, 29	⊢
	: , :
18	instantiation	30, 149, 152, 83, 31, 84, 43, 88, 44	⊢
	: , : , : , : , : , :
19	instantiation	32, 43, 33	⊢
	: , :
20	instantiation	34, 35, 36, 81*	⊢
	: , :
21	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_factor_bound
22	instantiation	37, 109, 129, 38, 39, 40*, 41*	⊢
	: , : , :
23	instantiation	42, 149, 43, 44	⊢
	: , : , : , :
24	instantiation	62, 45, 46	⊢
	: , : , :
25	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
26	theorem		⊢
	proveit.logic.equality.sub_right_side_into
27	instantiation	47, 48, 49	⊢
	: , :
28	instantiation	50, 142, 51, 88, 125, 52*	⊢
	: , :
29	instantiation	53, 90	⊢
	:
30	theorem		⊢
	proveit.numbers.multiplication.disassociation
31	instantiation	108	⊢
	: , :
32	theorem		⊢
	proveit.numbers.multiplication.commutation
33	instantiation	150, 136, 116	⊢
	: , : , :
34	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
35	instantiation	150, 54, 55	⊢
	: , : , :
36	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
37	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
38	instantiation	150, 139, 56	⊢
	: , : , :
39	instantiation	57, 129, 110, 128, 58, 59	⊢
	: , : , :
40	instantiation	60, 94, 107, 61	⊢
	: , : , :
41	instantiation	62, 63, 64	⊢
	: , : , :
42	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
43	instantiation	150, 136, 65	⊢
	: , : , :
44	instantiation	150, 136, 66	⊢
	: , : , :
45	instantiation	67, 68	⊢
	: , : , :
46	instantiation	69, 125	⊢
	:
47	theorem		⊢
	proveit.numbers.absolute_value.weak_upper_bound
48	instantiation	70, 97, 116, 98	⊢
	: , : , :
49	instantiation	99, 71	⊢
	: , :
50	theorem		⊢
	proveit.numbers.absolute_value.abs_prod
51	instantiation	108	⊢
	: , :
52	instantiation	72, 73	⊢
	:
53	theorem		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
54	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
55	instantiation	150, 74, 75	⊢
	: , : , :
56	instantiation	150, 147, 76	⊢
	: , : , :
57	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
58	instantiation	77, 129, 128, 78, 79, 80, 81*	⊢
	: , : , :
59	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
60	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
61	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
62	axiom		⊢
	proveit.logic.equality.equals_transitivity
63	instantiation	82, 83, 152, 149, 84, 85, 88, 94, 86	⊢
	: , : , : , : , : , :
64	instantiation	87, 94, 88, 89	⊢
	: , : , :
65	instantiation	150, 91, 90	⊢
	: , : , :
66	instantiation	150, 91, 92	⊢
	: , : , :
67	axiom		⊢
	proveit.logic.equality.substitution
68	instantiation	93, 94, 125, 95*	⊢
	: , :
69	theorem		⊢
	proveit.numbers.absolute_value.abs_even
70	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
71	instantiation	96, 97, 116, 98	⊢
	: , : , :
72	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
73	instantiation	99, 100	⊢
	: , :
74	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
75	instantiation	150, 101, 102	⊢
	: , : , :
76	instantiation	150, 151, 103	⊢
	: , : , :
77	theorem		⊢
	proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
78	instantiation	122, 123, 105	⊢
	: , : , :
79	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
80	instantiation	104, 105	⊢
	:
81	instantiation	106, 107	⊢
	:
82	theorem		⊢
	proveit.numbers.addition.disassociation
83	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
84	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
85	instantiation	108	⊢
	: , :
86	instantiation	150, 136, 109	⊢
	: , : , :
87	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
88	instantiation	150, 136, 110	⊢
	: , : , :
89	instantiation	111	⊢
	:
90	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
91	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
92	instantiation	112, 113	⊢
	:
93	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
94	instantiation	150, 136, 128	⊢
	: , : , :
95	instantiation	114, 125	⊢
	:
96	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
97	instantiation	115, 116	⊢
	:
98	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_round_in_interval
99	theorem		⊢
	proveit.numbers.ordering.relax_less
100	instantiation	117, 132	⊢
	:
101	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
102	instantiation	150, 118, 142	⊢
	: , : , :
103	instantiation	119, 120, 149	⊢
	: , :
104	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
105	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
106	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
107	instantiation	150, 136, 129	⊢
	: , : , :
108	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
109	instantiation	150, 139, 121	⊢
	: , : , :
110	instantiation	122, 123, 132	⊢
	: , : , :
111	axiom		⊢
	proveit.logic.equality.equals_reflexivity
112	theorem		⊢
	proveit.numbers.absolute_value.abs_nonzero_closure
113	instantiation	124, 125, 126	⊢
	:
114	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
115	theorem		⊢
	proveit.numbers.negation.real_closure
116	instantiation	127, 128, 129, 130	⊢
	: , :
117	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
118	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
119	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
120	instantiation	150, 131, 132	⊢
	: , : , :
121	instantiation	150, 147, 133	⊢
	: , : , :
122	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
123	instantiation	134, 135	⊢
	: , :
124	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
125	instantiation	150, 136, 137	⊢
	: , : , :
126	assumption		⊢
127	theorem		⊢
	proveit.numbers.division.div_real_closure
128	instantiation	150, 139, 138	⊢
	: , : , :
129	instantiation	150, 139, 140	⊢
	: , : , :
130	instantiation	141, 142	⊢
	:
131	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
132	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
133	instantiation	143, 146	⊢
	:
134	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
135	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
136	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
137	instantiation	144, 145	⊢
	:
138	instantiation	150, 147, 146	⊢
	: , : , :
139	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
140	instantiation	150, 147, 148	⊢
	: , : , :
141	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
142	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
143	theorem		⊢
	proveit.numbers.negation.int_closure
144	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
145	theorem		⊢
	proveit.physics.quantum.QPE._best_round_is_int
146	instantiation	150, 151, 149	⊢
	: , : , :
147	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
148	instantiation	150, 151, 152	⊢
	: , : , :
149	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
150	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
151	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
152	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements