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	theorem		⊢
	proveit.logic.equality.sub_left_side_into
2	instantiation	4, 71, 79, 5	⊢
	: , : , :
3	instantiation	6, 52	⊢
	:
4	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oo_lower_bound
5	instantiation	7, 8	⊢
	:
6	theorem		⊢
	proveit.numbers.addition.elim_zero_left
7	instantiation	9, 131, 10, 11, 12	⊢
	: , : , : , :
8	assumption		⊢
9	theorem		⊢
	proveit.logic.sets.enumeration.true_for_each_then_true_for_all
10	instantiation	109	⊢
	: , :
11	instantiation	14, 71, 79, 72, 13	⊢
	: , : , :
12	instantiation	14, 71, 79, 75, 15	⊢
	: , : , :
13	instantiation	18, 16, 17	⊢
	: , :
14	theorem		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalOO
15	instantiation	18, 19, 20	⊢
	: , :
16	instantiation	25, 71, 78, 21, 22, 23*, 24*	⊢
	: , : , :
17	instantiation	68, 78, 79, 80	⊢
	: , : , :
18	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
19	instantiation	25, 89, 26, 27, 28*, 29*	⊢
	: , : , :
20	instantiation	33, 30, 42	⊢
	: , : , :
21	instantiation	38, 72, 79	⊢
	: , :
22	instantiation	39, 78, 72, 79, 31, 32	⊢
	: , : , :
23	instantiation	33, 34, 35	⊢
	: , : , :
24	instantiation	92, 36, 37	⊢
	: , : , :
25	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
26	instantiation	38, 75, 99	⊢
	: , :
27	instantiation	39, 89, 75, 99, 40, 70	⊢
	: , : , :
28	instantiation	41, 65, 53, 42	⊢
	: , : , :
29	instantiation	92, 43, 44	⊢
	: , : , :
30	instantiation	45, 75, 99, 46, 47	⊢
	: , : , :
31	instantiation	56, 78, 79, 80	⊢
	: , : , :
32	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
33	theorem		⊢
	proveit.logic.equality.sub_right_side_into
34	instantiation	48, 52	⊢
	:
35	instantiation	49, 52, 50	⊢
	: , :
36	instantiation	59, 60, 131, 108, 61, 51, 54, 53, 52	⊢
	: , : , : , : , : , :
37	instantiation	64, 53, 54, 55	⊢
	: , : , :
38	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
39	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
40	instantiation	56, 89, 99, 90	⊢
	: , : , :
41	theorem		⊢
	proveit.numbers.addition.subtraction.negated_add
42	instantiation	57, 100, 128, 58*	⊢
	: , : , : , :
43	instantiation	59, 60, 131, 108, 61, 62, 66, 65, 63	⊢
	: , : , : , : , : , :
44	instantiation	64, 65, 66, 67	⊢
	: , : , :
45	theorem		⊢
	proveit.numbers.ordering.less_add_right
46	instantiation	68, 89, 99, 90	⊢
	: , : , :
47	instantiation	69, 70	⊢
	: , :
48	theorem		⊢
	proveit.numbers.addition.elim_zero_right
49	theorem		⊢
	proveit.numbers.addition.commutation
50	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
51	instantiation	109	⊢
	: , :
52	instantiation	129, 116, 71	⊢
	: , : , :
53	instantiation	129, 116, 79	⊢
	: , : , :
54	instantiation	129, 116, 72	⊢
	: , : , :
55	instantiation	76	⊢
	:
56	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
57	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
58	instantiation	92, 73, 74	⊢
	: , : , :
59	theorem		⊢
	proveit.numbers.addition.disassociation
60	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
61	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
62	instantiation	109	⊢
	: , :
63	instantiation	129, 116, 89	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
65	instantiation	129, 116, 99	⊢
	: , : , :
66	instantiation	129, 116, 75	⊢
	: , : , :
67	instantiation	76	⊢
	:
68	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
69	theorem		⊢
	proveit.numbers.ordering.relax_less
70	instantiation	77, 115	⊢
	:
71	instantiation	98, 79	⊢
	:
72	instantiation	88, 78, 79, 80	⊢
	: , : , :
73	instantiation	101, 131, 81, 82, 83, 84	⊢
	: , : , : , :
74	instantiation	85, 86, 87	⊢
	:
75	instantiation	88, 89, 99, 90	⊢
	: , : , :
76	axiom		⊢
	proveit.logic.equality.equals_reflexivity
77	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
78	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
79	instantiation	129, 122, 91	⊢
	: , : , :
80	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
81	instantiation	109	⊢
	: , :
82	instantiation	109	⊢
	: , :
83	instantiation	92, 93, 94	⊢
	: , : , :
84	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
85	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
86	instantiation	129, 116, 95	⊢
	: , : , :
87	instantiation	96, 97	⊢
	:
88	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
89	instantiation	98, 99	⊢
	:
90	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_round_in_interval
91	instantiation	129, 127, 100	⊢
	: , : , :
92	axiom		⊢
	proveit.logic.equality.equals_transitivity
93	instantiation	101, 131, 102, 103, 104, 105	⊢
	: , : , : , :
94	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
95	instantiation	129, 122, 106	⊢
	: , : , :
96	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
97	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
98	theorem		⊢
	proveit.numbers.negation.real_closure
99	instantiation	129, 122, 107	⊢
	: , : , :
100	instantiation	129, 130, 108	⊢
	: , : , :
101	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
102	instantiation	109	⊢
	: , :
103	instantiation	109	⊢
	: , :
104	instantiation	110, 112	⊢
	:
105	instantiation	111, 112	⊢
	:
106	instantiation	129, 127, 113	⊢
	: , : , :
107	instantiation	129, 114, 115	⊢
	: , : , :
108	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
109	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
110	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
111	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
112	instantiation	129, 116, 117	⊢
	: , : , :
113	instantiation	129, 130, 118	⊢
	: , : , :
114	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
115	instantiation	119, 120, 121	⊢
	: , :
116	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
117	instantiation	129, 122, 123	⊢
	: , : , :
118	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
119	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
120	instantiation	129, 125, 124	⊢
	: , : , :
121	instantiation	129, 125, 126	⊢
	: , : , :
122	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
123	instantiation	129, 127, 128	⊢
	: , : , :
124	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
125	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
126	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
127	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
128	instantiation	129, 130, 131	⊢
	: , : , :
129	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
130	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
131	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements