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.number_sets.real_numbers.in_IntervalCO
2	reference	20	⊢
3	reference	121	⊢
4	instantiation	12, 6, 42	⊢
	: , : , :
5	instantiation	7, 8, 9	⊢
	: , :
6	instantiation	130, 158, 10	⊢
	: , :
7	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
8	instantiation	12, 11, 14	⊢
	: , : , :
9	instantiation	12, 13, 14	⊢
	: , : , :
10	instantiation	119, 131, 15	⊢
	: , :
11	instantiation	16, 20, 34, 21, 17, 18*, 23*	⊢
	: , : , :
12	theorem		⊢
	proveit.logic.equality.sub_left_side_into
13	instantiation	19, 20, 21, 133, 22, 23*, 24*	⊢
	: , : , :
14	instantiation	93, 25, 26	⊢
	: , : , :
15	instantiation	31, 27	⊢
	:
16	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
17	instantiation	28, 34, 133, 35	⊢
	: , : , :
18	instantiation	93, 29, 30	⊢
	: , : , :
19	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
20	instantiation	31, 121	⊢
	:
21	instantiation	32, 34, 133, 35	⊢
	: , : , :
22	instantiation	33, 34, 133, 35	⊢
	: , : , :
23	instantiation	125, 36, 37	⊢
	: , : , :
24	instantiation	38, 154, 39, 156, 107*, 40*, 41*	⊢
	: , : , : , :
25	instantiation	93, 42, 43	⊢
	: , : , :
26	instantiation	93, 44, 45	⊢
	: , : , :
27	instantiation	132, 129, 158, 84	⊢
	: , :
28	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
29	instantiation	46, 53	⊢
	:
30	instantiation	47, 53, 48	⊢
	: , :
31	theorem		⊢
	proveit.numbers.negation.real_closure
32	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
33	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
34	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
35	instantiation	49, 111, 50*	⊢
	:
36	instantiation	66, 67, 51, 159, 68, 52, 70, 73, 71, 53	⊢
	: , : , : , : , : , :
37	instantiation	54, 159, 67, 68, 70, 73, 71, 55	⊢
	: , : , : , : , : , : , : , :
38	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
39	instantiation	56, 154	⊢
	:
40	instantiation	57, 117, 90, 135	⊢
	: , :
41	instantiation	125, 58, 59	⊢
	: , : , :
42	instantiation	139, 60	⊢
	: , : , :
43	instantiation	61, 159, 67, 68, 152, 62, 63, 64*	⊢
	: , : , : , : , : , :
44	axiom		⊢
	proveit.physics.quantum.QPE._best_round_def
45	instantiation	65, 120	⊢
	:
46	theorem		⊢
	proveit.numbers.addition.elim_zero_right
47	theorem		⊢
	proveit.numbers.addition.commutation
48	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
49	theorem		⊢
	proveit.numbers.rounding.real_minus_floor_interval
50	instantiation	66, 67, 162, 159, 68, 69, 70, 73, 71	⊢
	: , : , : , : , : , :
51	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
52	instantiation	72	⊢
	: , : , :
53	instantiation	87, 73	⊢
	:
54	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
55	instantiation	74	⊢
	:
56	theorem		⊢
	proveit.numbers.negation.int_closure
57	theorem		⊢
	proveit.numbers.division.neg_frac_neg_numerator
58	instantiation	75, 162, 76, 77, 78, 79	⊢
	: , : , : , :
59	instantiation	80, 117, 90, 81	⊢
	: , : , :
60	instantiation	82, 153	⊢
	:
61	theorem		⊢
	proveit.numbers.multiplication.distribute_through_subtract
62	instantiation	160, 157, 131	⊢
	: , : , :
63	instantiation	83, 118, 152, 84	⊢
	: , :
64	instantiation	93, 85, 86	⊢
	: , : , :
65	theorem		⊢
	proveit.numbers.rounding.round_in_terms_of_floor
66	theorem		⊢
	proveit.numbers.addition.disassociation
67	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
68	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
69	instantiation	89	⊢
	: , :
70	instantiation	160, 157, 120	⊢
	: , : , :
71	instantiation	87, 88	⊢
	:
72	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
73	instantiation	160, 157, 121	⊢
	: , : , :
74	axiom		⊢
	proveit.logic.equality.equals_reflexivity
75	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
76	instantiation	89	⊢
	: , :
77	instantiation	89	⊢
	: , :
78	instantiation	151, 90	⊢
	:
79	instantiation	91, 117, 92*	⊢
	: , :
80	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
81	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
82	axiom		⊢
	proveit.physics.quantum.QPE._delta_b_def
83	theorem		⊢
	proveit.numbers.division.div_complex_closure
84	instantiation	147, 165	⊢
	:
85	instantiation	93, 94, 95	⊢
	: , : , :
86	instantiation	96, 97, 98, 99	⊢
	: , : , : , :
87	theorem		⊢
	proveit.numbers.negation.complex_closure
88	instantiation	163, 100, 101	⊢
	: , : , :
89	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
90	instantiation	160, 157, 134	⊢
	: , : , :
91	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
92	instantiation	142, 117	⊢
	:
93	theorem		⊢
	proveit.logic.equality.sub_right_side_into
94	instantiation	102, 117, 118, 103, 104	⊢
	: , : , : , : , :
95	instantiation	125, 105, 106	⊢
	: , : , :
96	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
97	instantiation	139, 107	⊢
	: , : , :
98	instantiation	139, 108	⊢
	: , : , :
99	instantiation	151, 118	⊢
	:
100	instantiation	166, 109	⊢
	: , :
101	instantiation	110, 111	⊢
	:
102	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
103	instantiation	160, 113, 112	⊢
	: , : , :
104	instantiation	160, 113, 114	⊢
	: , : , :
105	instantiation	139, 115	⊢
	: , : , :
106	instantiation	139, 116	⊢
	: , : , :
107	instantiation	141, 117	⊢
	:
108	instantiation	141, 118	⊢
	:
109	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.int_within_complex
110	axiom		⊢
	proveit.numbers.rounding.floor_is_an_int
111	instantiation	119, 120, 121	⊢
	: , :
112	instantiation	160, 123, 122	⊢
	: , : , :
113	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
114	instantiation	160, 123, 124	⊢
	: , : , :
115	instantiation	125, 126, 127	⊢
	: , : , :
116	instantiation	139, 128	⊢
	: , : , :
117	instantiation	160, 157, 133	⊢
	: , : , :
118	instantiation	160, 157, 129	⊢
	: , : , :
119	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
120	instantiation	130, 158, 131	⊢
	: , :
121	instantiation	132, 133, 134, 135	⊢
	: , :
122	instantiation	160, 137, 136	⊢
	: , : , :
123	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
124	instantiation	160, 137, 138	⊢
	: , : , :
125	axiom		⊢
	proveit.logic.equality.equals_transitivity
126	instantiation	139, 140	⊢
	: , : , :
127	instantiation	141, 152	⊢
	:
128	instantiation	142, 152	⊢
	:
129	instantiation	160, 145, 143	⊢
	: , : , :
130	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
131	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
132	theorem		⊢
	proveit.numbers.division.div_real_closure
133	instantiation	160, 145, 144	⊢
	: , : , :
134	instantiation	160, 145, 146	⊢
	: , : , :
135	instantiation	147, 148	⊢
	:
136	instantiation	160, 149, 165	⊢
	: , : , :
137	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
138	instantiation	160, 149, 150	⊢
	: , : , :
139	axiom		⊢
	proveit.logic.equality.substitution
140	instantiation	151, 152	⊢
	:
141	theorem		⊢
	proveit.numbers.division.frac_one_denom
142	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
143	instantiation	160, 155, 153	⊢
	: , : , :
144	instantiation	160, 155, 154	⊢
	: , : , :
145	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
146	instantiation	160, 155, 156	⊢
	: , : , :
147	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
148	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
149	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
150	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
151	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
152	instantiation	160, 157, 158	⊢
	: , : , :
153	theorem		⊢
	proveit.physics.quantum.QPE._best_round_is_int
154	instantiation	160, 161, 159	⊢
	: , : , :
155	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
156	instantiation	160, 161, 162	⊢
	: , : , :
157	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
158	instantiation	163, 164, 165	⊢
	: , : , :
159	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
160	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
161	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
162	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
163	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
164	instantiation	166, 167	⊢
	: , :
165	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
166	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
167	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements