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, 6, 7	,  ⊢
	: , : , : , : , : , : , :
1	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
2	reference	63	⊢
3	reference	144	⊢
4	reference	64	⊢
5	instantiation	149, 139, 8	⊢
	: , : , :
6	reference	134	⊢
7	instantiation	149, 139, 9	,  ⊢
	: , : , :
8	instantiation	10, 11, 12	⊢
	: , : , :
9	instantiation	21, 41, 117, 13	,  ⊢
	: , : , :
10	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
11	instantiation	14, 15	⊢
	: , :
12	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
13	instantiation	16, 17	,  ⊢
	:
14	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
15	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
16	theorem		⊢
	proveit.trigonometry.sine_pos_interval
17	instantiation	18, 41, 101, 19, 20	,  ⊢
	: , : , :
18	theorem		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalOO
19	instantiation	21, 41, 32, 30	,  ⊢
	: , : , :
20	instantiation	22, 23, 24	,  ⊢
	: , :
21	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
22	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
23	instantiation	25, 41, 32, 30	,  ⊢
	: , : , :
24	instantiation	26, 27, 28	,  ⊢
	: , : , :
25	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
26	theorem		⊢
	proveit.numbers.ordering.transitivity_less_eq_less
27	instantiation	29, 41, 32, 30	,  ⊢
	: , : , :
28	instantiation	31, 32, 33, 70, 34, 35*, 36*	⊢
	: , : , :
29	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_upper_bound
30	instantiation	37, 38, 39	,  ⊢
	:
31	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
32	instantiation	116, 101, 140, 118	⊢
	: , :
33	instantiation	75, 76, 41	⊢
	: , :
34	instantiation	40, 76, 41, 101, 42, 43	⊢
	: , : , :
35	instantiation	44, 45, 46, 47	⊢
	: , : , : , :
36	instantiation	106, 48, 49	⊢
	: , : , :
37	theorem		⊢
	proveit.physics.quantum.QPE._scaled_abs_delta_b_floor_diff_interval
38	assumption		⊢
39	assumption		⊢
40	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
41	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
42	instantiation	50, 115	⊢
	:
43	instantiation	51, 90	⊢
	:
44	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
45	instantiation	106, 52, 53	⊢
	: , : , :
46	instantiation	54	⊢
	:
47	instantiation	55, 69	⊢
	: , :
48	instantiation	84, 69	⊢
	: , : , :
49	instantiation	55, 56, 57*	⊢
	: , :
50	theorem		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
51	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
52	instantiation	106, 58, 59	⊢
	: , : , :
53	instantiation	60, 61	⊢
	:
54	axiom		⊢
	proveit.logic.equality.equals_reflexivity
55	theorem		⊢
	proveit.logic.equality.equals_reversal
56	instantiation	62, 63, 151, 144, 64, 65, 88, 87	⊢
	: , : , : , : , : , :
57	instantiation	106, 66, 67	⊢
	: , : , :
58	instantiation	84, 68	⊢
	: , : , :
59	instantiation	84, 69	⊢
	: , : , :
60	theorem		⊢
	proveit.numbers.addition.elim_zero_left
61	instantiation	149, 139, 70	⊢
	: , : , :
62	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
63	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
64	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
65	instantiation	131	⊢
	: , :
66	instantiation	84, 71	⊢
	: , : , :
67	instantiation	132, 87	⊢
	:
68	instantiation	72, 88	⊢
	:
69	instantiation	73, 87, 134, 118, 74*	⊢
	: , :
70	instantiation	75, 76, 101	⊢
	: , :
71	instantiation	77, 138, 148, 78*	⊢
	: , : , : , :
72	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
73	theorem		⊢
	proveit.numbers.division.div_as_mult
74	instantiation	106, 79, 80	⊢
	: , : , :
75	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
76	instantiation	149, 145, 81	⊢
	: , : , :
77	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
78	instantiation	106, 82, 83	⊢
	: , : , :
79	instantiation	84, 85	⊢
	: , : , :
80	instantiation	86, 87, 88	⊢
	: , :
81	instantiation	149, 89, 90	⊢
	: , : , :
82	instantiation	121, 151, 91, 92, 93, 94	⊢
	: , : , : , :
83	instantiation	95, 96, 97	⊢
	:
84	axiom		⊢
	proveit.logic.equality.substitution
85	instantiation	98, 99, 119, 100*	⊢
	: , :
86	theorem		⊢
	proveit.numbers.multiplication.commutation
87	instantiation	149, 139, 101	⊢
	: , : , :
88	instantiation	149, 139, 102	⊢
	: , : , :
89	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
90	instantiation	103, 104, 105	⊢
	: , :
91	instantiation	131	⊢
	: , :
92	instantiation	131	⊢
	: , :
93	instantiation	106, 107, 108	⊢
	: , : , :
94	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
95	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
96	instantiation	149, 139, 109	⊢
	: , : , :
97	instantiation	130, 110	⊢
	:
98	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
99	instantiation	149, 111, 112	⊢
	: , : , :
100	instantiation	113, 134	⊢
	:
101	instantiation	149, 114, 115	⊢
	: , : , :
102	instantiation	116, 117, 140, 118	⊢
	: , :
103	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
104	instantiation	149, 120, 119	⊢
	: , : , :
105	instantiation	149, 120, 143	⊢
	: , : , :
106	axiom		⊢
	proveit.logic.equality.equals_transitivity
107	instantiation	121, 151, 122, 123, 124, 125	⊢
	: , : , : , :
108	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
109	instantiation	149, 145, 126	⊢
	: , : , :
110	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
111	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
112	instantiation	149, 127, 128	⊢
	: , : , :
113	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
114	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
115	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
116	theorem		⊢
	proveit.numbers.division.div_real_closure
117	instantiation	149, 145, 129	⊢
	: , : , :
118	instantiation	130, 143	⊢
	:
119	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
120	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
121	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
122	instantiation	131	⊢
	: , :
123	instantiation	131	⊢
	: , :
124	instantiation	132, 134	⊢
	:
125	instantiation	133, 134	⊢
	:
126	instantiation	149, 147, 135	⊢
	: , : , :
127	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
128	instantiation	149, 136, 137	⊢
	: , : , :
129	instantiation	149, 147, 138	⊢
	: , : , :
130	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
131	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
132	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
133	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
134	instantiation	149, 139, 140	⊢
	: , : , :
135	instantiation	149, 150, 141	⊢
	: , : , :
136	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
137	instantiation	149, 142, 143	⊢
	: , : , :
138	instantiation	149, 150, 144	⊢
	: , : , :
139	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
140	instantiation	149, 145, 146	⊢
	: , : , :
141	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
142	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
143	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
144	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
145	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
146	instantiation	149, 147, 148	⊢
	: , : , :
147	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
148	instantiation	149, 150, 151	⊢
	: , : , :
149	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
150	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
151	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements