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