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	,  ⊢
	: , : , :
1	theorem		⊢
	proveit.logic.booleans.disjunction.singular_constructive_dilemma
2	instantiation	7, 9	⊢
	: , :
3	instantiation	8, 9	⊢
	: , :
4	reference	13	⊢
5	deduction	10	,  ⊢
6	deduction	11	,  ⊢
7	axiom		⊢
	proveit.logic.booleans.disjunction.left_in_bool
8	axiom		⊢
	proveit.logic.booleans.disjunction.right_in_bool
9	instantiation	12, 13	⊢
	:
10	instantiation	38, 14, 116	, ,  ⊢
	: , :
11	instantiation	38, 15, 116	, ,  ⊢
	: , :
12	theorem		⊢
	proveit.logic.booleans.in_bool_if_true
13	instantiation	16, 164, 17	⊢
	: , :
14	instantiation	19, 20, 21, 18	, ,  ⊢
	: , : , :
15	instantiation	19, 20, 21, 22	, ,  ⊢
	: , : , :
16	theorem		⊢
	proveit.numbers.ordering.less_or_greater_eq
17	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
18	instantiation	44, 23, 24	, ,  ⊢
	: , :
19	theorem		⊢
	proveit.logic.sets.unification.membership_folding
20	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
21	instantiation	152	⊢
	: , :
22	instantiation	48, 25, 26	, ,  ⊢
	: , :
23	instantiation	31, 181, 36, 174, 27	, ,  ⊢
	: , : , :
24	instantiation	29, 28	, ,  ⊢
	: , :
25	instantiation	29, 30	, ,  ⊢
	: , :
26	instantiation	31, 47, 190, 174, 32	, ,  ⊢
	: , : , :
27	instantiation	38, 66, 33	, ,  ⊢
	: , :
28	instantiation	35, 47, 190, 174, 34	, ,  ⊢
	: , : , :
29	theorem		⊢
	proveit.logic.sets.membership.unfold_not_in_set
30	instantiation	35, 181, 36, 174, 37	, ,  ⊢
	: , : , :
31	theorem		⊢
	proveit.numbers.number_sets.integers.in_interval
32	instantiation	38, 39, 63	, ,  ⊢
	: , :
33	instantiation	51, 151, 169, 40, 41, 42*, 43*	, ,  ⊢
	: , : , :
34	instantiation	44, 45, 46	, ,  ⊢
	: , :
35	theorem		⊢
	proveit.numbers.number_sets.integers.int_not_in_interval
36	instantiation	192, 47	⊢
	:
37	instantiation	48, 49, 50	, ,  ⊢
	: , :
38	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
39	instantiation	51, 165, 169, 52, 53, 54*, 55*	, ,  ⊢
	: , : , :
40	instantiation	82, 83, 56	, ,  ⊢
	: , : , :
41	instantiation	69, 56	, ,  ⊢
	:
42	instantiation	107, 57, 58	⊢
	: , : , :
43	instantiation	96, 59	,  ⊢
	: , :
44	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_only_left
45	instantiation	60, 161, 61	,  ⊢
	: , : , :
46	instantiation	64, 164, 62, 63	⊢
	: , :
47	instantiation	188, 175, 187	⊢
	: , :
48	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_only_right
49	instantiation	64, 65, 164, 66	⊢
	: , :
50	instantiation	157, 67, 148	,  ⊢
	: , : , :
51	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
52	instantiation	162, 164, 68	,  ⊢
	: , :
53	instantiation	69, 70	, ,  ⊢
	:
54	instantiation	71, 156, 154	⊢
	: , :
55	instantiation	107, 72, 73	,  ⊢
	: , : , :
56	instantiation	74, 75	, ,  ⊢
	:
57	instantiation	135, 191, 198, 140, 137, 141, 156, 143, 144	⊢
	: , : , : , : , : , :
58	instantiation	76, 156, 143, 77	⊢
	: , : , :
59	instantiation	122, 78, 79, 80	,  ⊢
	: , : , : , :
60	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
61	instantiation	81, 100	⊢
	:
62	instantiation	82, 83, 195	⊢
	: , : , :
63	instantiation	84, 181, 190, 178	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.ordering.not_less_from_less_eq
65	instantiation	196, 172, 85	⊢
	: , : , :
66	instantiation	167, 181, 190, 178	⊢
	: , : , :
67	instantiation	86, 87	⊢
	:
68	instantiation	168, 165	⊢
	:
69	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
70	instantiation	145, 88, 89	, ,  ⊢
	:
71	theorem		⊢
	proveit.numbers.addition.commutation
72	instantiation	135, 140, 198, 191, 141, 90, 143, 142, 154	,  ⊢
	: , : , : , : , : , :
73	instantiation	91, 154, 143, 92	,  ⊢
	: , : , :
74	theorem		⊢
	proveit.numbers.negation.nat_pos_closure
75	instantiation	93, 94, 95	, ,  ⊢
	:
76	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
77	instantiation	132	⊢
	:
78	instantiation	133, 154, 156	⊢
	: , :
79	instantiation	132	⊢
	:
80	instantiation	96, 97	,  ⊢
	: , :
81	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
82	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
83	instantiation	98, 99	⊢
	: , :
84	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
85	instantiation	196, 176, 181	⊢
	: , : , :
86	theorem		⊢
	proveit.numbers.number_sets.integers.negative_if_in_neg_int
87	instantiation	126, 100	⊢
	:
88	instantiation	188, 174, 101	,  ⊢
	: , :
89	instantiation	102, 103	,  ⊢
	: , :
90	instantiation	152	⊢
	: , :
91	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
92	instantiation	132	⊢
	:
93	theorem		⊢
	proveit.numbers.number_sets.integers.neg_int_is_int_neg
94	instantiation	188, 175, 174	,  ⊢
	: , :
95	instantiation	104, 164, 165, 153, 105, 106*	, ,  ⊢
	: , : , :
96	theorem		⊢
	proveit.logic.equality.equals_reversal
97	instantiation	107, 108, 109	,  ⊢
	: , : , :
98	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
99	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
100	instantiation	110, 127, 111	⊢
	: , :
101	instantiation	196, 112, 113	⊢
	: , : , :
102	theorem		⊢
	proveit.numbers.addition.subtraction.pos_difference
103	instantiation	115, 116, 114	,  ⊢
	: , : , :
104	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
105	instantiation	115, 116, 117	,  ⊢
	: , : , :
106	instantiation	118, 143, 119	⊢
	: , :
107	axiom		⊢
	proveit.logic.equality.equals_transitivity
108	instantiation	120, 121	,  ⊢
	: , : , :
109	instantiation	122, 123, 124, 125	,  ⊢
	: , : , : , :
110	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
111	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
112	theorem		⊢
	proveit.numbers.number_sets.integers.neg_int_within_int
113	instantiation	126, 127	⊢
	:
114	instantiation	130, 178, 128*	,  ⊢
	:
115	theorem		⊢
	proveit.logic.equality.sub_right_side_into
116	instantiation	129, 183	⊢
	: , :
117	instantiation	130, 178, 131*	,  ⊢
	:
118	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_reverse
119	instantiation	132	⊢
	:
120	axiom		⊢
	proveit.logic.equality.substitution
121	instantiation	133, 154, 143	,  ⊢
	: , :
122	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
123	instantiation	135, 140, 198, 191, 141, 136, 142, 138, 134	,  ⊢
	: , : , : , : , : , :
124	instantiation	135, 198, 140, 136, 137, 141, 142, 138, 143, 144	,  ⊢
	: , : , : , : , : , :
125	instantiation	139, 191, 140, 141, 142, 143, 144	,  ⊢
	: , : , : , : , : , : , : , :
126	theorem		⊢
	proveit.numbers.negation.int_neg_closure
127	instantiation	145, 175, 146	⊢
	:
128	instantiation	147, 148	⊢
	:
129	theorem		⊢
	proveit.logic.booleans.conjunction.right_from_and
130	theorem		⊢
	proveit.physics.quantum.QPE._modabs_in_full_domain_simp
131	instantiation	149, 150	⊢
	:
132	axiom		⊢
	proveit.logic.equality.equals_reflexivity
133	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
134	instantiation	196, 166, 151	⊢
	: , : , :
135	theorem		⊢
	proveit.numbers.addition.disassociation
136	instantiation	152	⊢
	: , :
137	instantiation	152	⊢
	: , :
138	instantiation	196, 166, 153	⊢
	: , : , :
139	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general_rev
140	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
141	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
142	instantiation	155, 154	⊢
	:
143	instantiation	196, 166, 164	⊢
	: , : , :
144	instantiation	155, 156	⊢
	:
145	theorem		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
146	instantiation	157, 158, 159	⊢
	: , : , :
147	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
148	assumption		⊢
149	theorem		⊢
	proveit.numbers.absolute_value.abs_neg_elim
150	instantiation	160, 161	⊢
	: , :
151	instantiation	162, 164, 163	⊢
	: , :
152	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
153	instantiation	168, 164	⊢
	:
154	instantiation	196, 166, 165	⊢
	: , : , :
155	theorem		⊢
	proveit.numbers.negation.complex_closure
156	instantiation	196, 166, 169	⊢
	: , : , :
157	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
158	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
159	instantiation	167, 187, 185, 180	⊢
	: , : , :
160	theorem		⊢
	proveit.numbers.ordering.relax_less
161	assumption		⊢
162	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
163	instantiation	168, 169	⊢
	:
164	instantiation	196, 172, 170	⊢
	: , : , :
165	instantiation	196, 172, 171	⊢
	: , : , :
166	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
167	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
168	theorem		⊢
	proveit.numbers.negation.real_closure
169	instantiation	196, 172, 173	⊢
	: , : , :
170	instantiation	196, 176, 174	⊢
	: , : , :
171	instantiation	196, 176, 175	⊢
	: , : , :
172	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
173	instantiation	196, 176, 187	⊢
	: , : , :
174	instantiation	196, 177, 178	⊢
	: , : , :
175	instantiation	196, 179, 180	⊢
	: , : , :
176	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
177	instantiation	184, 181, 190	⊢
	: , :
178	instantiation	182, 183	⊢
	: , :
179	instantiation	184, 187, 185	⊢
	: , :
180	assumption		⊢
181	instantiation	188, 186, 187	⊢
	: , :
182	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
183	assumption		⊢
184	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
185	instantiation	188, 190, 189	⊢
	: , :
186	instantiation	192, 190	⊢
	:
187	instantiation	196, 197, 191	⊢
	: , : , :
188	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
189	instantiation	192, 193	⊢
	:
190	instantiation	196, 194, 195	⊢
	: , : , :
191	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
192	theorem		⊢
	proveit.numbers.negation.int_closure
193	instantiation	196, 197, 198	⊢
	: , : , :
194	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
195	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
196	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
197	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
198	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements