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.numbers.division.div_complex_closure
2	instantiation	6, 178, 5	⊢
	: , :
3	instantiation	6, 178, 7	⊢
	: , :
4	instantiation	8, 9	⊢
	: , :
5	instantiation	11, 10	⊢
	:
6	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
7	instantiation	11, 12	⊢
	:
8	theorem		⊢
	proveit.numbers.addition.subtraction.nonzero_difference_if_different
9	instantiation	13, 14	⊢
	: , :
10	instantiation	136, 16, 15	⊢
	: , :
11	theorem		⊢
	proveit.numbers.negation.complex_closure
12	instantiation	136, 16, 17	⊢
	: , :
13	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
14	instantiation	36, 18, 19	⊢
	: , : , :
15	instantiation	150, 20, 21	⊢
	: , : , :
16	instantiation	212, 205, 22	⊢
	: , : , :
17	instantiation	150, 23, 24	⊢
	: , : , :
18	instantiation	25, 26, 27, 28*	⊢
	:
19	instantiation	195, 29	⊢
	: , : , :
20	instantiation	117, 60, 30	⊢
	: , :
21	instantiation	187, 31, 32	⊢
	: , : , :
22	instantiation	212, 180, 33	⊢
	: , : , :
23	instantiation	117, 60, 51	⊢
	: , :
24	instantiation	187, 34, 35	⊢
	: , : , :
25	theorem		⊢
	proveit.numbers.exponentiation.unit_complex_polar_num_neq_one
26	instantiation	150, 83, 70	⊢
	: , : , :
27	instantiation	36, 37, 38	⊢
	: , : , :
28	instantiation	39, 40	⊢
	: , :
29	instantiation	114, 214, 207, 119, 84, 121, 203, 160, 75, 125	⊢
	: , : , : , : , : , : , :
30	instantiation	150, 41, 42	⊢
	: , : , :
31	instantiation	109, 207, 120, 119, 43, 121, 60, 75, 125, 53	⊢
	: , : , : , : , : , :
32	instantiation	109, 119, 214, 120, 121, 84, 43, 203, 160, 75, 125, 53	⊢
	: , : , : , : , : , :
33	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
34	instantiation	109, 207, 214, 119, 52, 121, 60, 75, 125	⊢
	: , : , : , : , : , :
35	instantiation	109, 119, 214, 121, 84, 52, 203, 160, 75, 125	⊢
	: , : , : , : , : , :
36	theorem		⊢
	proveit.logic.equality.sub_left_side_into
37	instantiation	44, 45, 46, 68, 66	⊢
	: , :
38	instantiation	153, 47, 48, 49	⊢
	: , : , : , :
39	theorem		⊢
	proveit.logic.equality.equals_reversal
40	instantiation	195, 50	⊢
	: , : , :
41	instantiation	117, 51, 53	⊢
	: , :
42	instantiation	109, 119, 214, 207, 121, 52, 75, 125, 53	⊢
	: , : , : , : , : , :
43	instantiation	133	⊢
	: , : , :
44	theorem		⊢
	proveit.logic.booleans.disjunction.right_if_not_left
45	instantiation	54, 55	⊢
	:
46	instantiation	56, 57	⊢
	: , :
47	instantiation	58, 59, 60, 61, 62*	⊢
	: , :
48	instantiation	194, 125	⊢
	:
49	instantiation	179	⊢
	:
50	instantiation	187, 63, 64	⊢
	: , : , :
51	instantiation	117, 75, 125	⊢
	: , :
52	instantiation	132	⊢
	: , :
53	instantiation	212, 205, 65	⊢
	: , : , :
54	axiom		⊢
	proveit.logic.booleans.negation.operand_is_bool
55	instantiation	67, 66	⊢
	:
56	axiom		⊢
	proveit.logic.booleans.disjunction.right_in_bool
57	instantiation	67, 68	⊢
	:
58	theorem		⊢
	proveit.numbers.division.div_as_mult
59	instantiation	150, 69, 70	⊢
	: , : , :
60	instantiation	212, 205, 91	⊢
	: , : , :
61	instantiation	71, 214, 84, 165, 72	⊢
	: , :
62	instantiation	187, 73, 74	⊢
	: , : , :
63	instantiation	114, 119, 120, 121, 111, 203, 160, 125, 75	⊢
	: , : , : , : , : , : , :
64	instantiation	118, 207, 120, 119, 111, 121, 75, 203, 160, 125	⊢
	: , : , : , : , : , :
65	instantiation	76, 77, 78	⊢
	: , : , :
66	instantiation	79, 80	⊢
	: , :
67	theorem		⊢
	proveit.logic.booleans.in_bool_if_true
68	instantiation	81, 82	⊢
	:
69	instantiation	212, 205, 83	⊢
	: , : , :
70	instantiation	109, 119, 214, 207, 121, 84, 203, 160, 125	⊢
	: , : , : , : , : , :
71	theorem		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
72	instantiation	212, 174, 141	⊢
	: , : , :
73	instantiation	195, 85	⊢
	: , : , :
74	instantiation	187, 86, 87	⊢
	: , : , :
75	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
76	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
77	instantiation	88, 89	⊢
	: , :
78	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
79	theorem		⊢
	proveit.logic.equality.unfold_not_equals
80	assumption		⊢
81	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_zero_or_non_int
82	instantiation	90, 207, 119, 121	⊢
	: , : , : , : , :
83	instantiation	98, 91, 135	⊢
	: , :
84	instantiation	132	⊢
	: , :
85	instantiation	92, 203, 160, 149, 146, 129, 93*	⊢
	: , : , :
86	instantiation	187, 94, 95	⊢
	: , : , :
87	instantiation	187, 96, 97	⊢
	: , : , :
88	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
89	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
90	theorem		⊢
	proveit.logic.sets.enumeration.in_enumerated_set
91	instantiation	98, 206, 171	⊢
	: , :
92	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_product
93	instantiation	99, 165, 199, 100*	⊢
	: , :
94	instantiation	187, 101, 102	⊢
	: , : , :
95	instantiation	187, 103, 104	⊢
	: , : , :
96	instantiation	105, 119, 120, 121, 123, 160, 125, 126	⊢
	: , : , : , :
97	instantiation	187, 106, 107	⊢
	: , : , :
98	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
99	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
100	instantiation	142, 203	⊢
	:
101	instantiation	109, 119, 120, 207, 121, 111, 203, 160, 125, 108	⊢
	: , : , : , : , : , :
102	instantiation	109, 120, 214, 119, 111, 110, 121, 203, 160, 125, 124, 126	⊢
	: , : , : , : , : , :
103	instantiation	114, 119, 120, 207, 121, 111, 203, 160, 125, 124, 126	⊢
	: , : , : , : , : , : , :
104	instantiation	187, 112, 113	⊢
	: , : , :
105	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
106	instantiation	114, 207, 119, 121, 160, 125, 126	⊢
	: , : , : , : , : , : , :
107	instantiation	118, 119, 214, 207, 121, 115, 160, 126, 125, 116*	⊢
	: , : , : , : , : , :
108	instantiation	117, 124, 126	⊢
	: , :
109	theorem		⊢
	proveit.numbers.multiplication.disassociation
110	instantiation	132	⊢
	: , :
111	instantiation	133	⊢
	: , : , :
112	instantiation	118, 119, 214, 120, 121, 122, 123, 124, 203, 160, 125, 126	⊢
	: , : , : , : , : , :
113	instantiation	195, 127	⊢
	: , : , :
114	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
115	instantiation	132	⊢
	: , :
116	instantiation	128, 160, 190, 149, 129, 130*, 131*	⊢
	: , : , :
117	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
118	theorem		⊢
	proveit.numbers.multiplication.association
119	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
120	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
121	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
122	instantiation	132	⊢
	: , :
123	instantiation	133	⊢
	: , : , :
124	instantiation	212, 205, 134	⊢
	: , : , :
125	instantiation	212, 205, 135	⊢
	: , : , :
126	instantiation	136, 160, 137	⊢
	: , :
127	instantiation	150, 138, 139	⊢
	: , : , :
128	theorem		⊢
	proveit.numbers.exponentiation.product_of_real_powers
129	instantiation	140, 141	⊢
	:
130	instantiation	142, 160	⊢
	:
131	instantiation	187, 143, 144	⊢
	: , : , :
132	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
133	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
134	instantiation	145, 190, 206, 146	⊢
	: , :
135	instantiation	147, 148	⊢
	:
136	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
137	instantiation	212, 205, 149	⊢
	: , : , :
138	instantiation	150, 151, 152	⊢
	: , : , :
139	instantiation	153, 154, 155, 156	⊢
	: , : , : , :
140	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
141	instantiation	212, 157, 181	⊢
	: , : , :
142	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
143	instantiation	195, 158	⊢
	: , : , :
144	instantiation	159, 160	⊢
	:
145	theorem		⊢
	proveit.numbers.division.div_real_closure
146	instantiation	161, 201	⊢
	:
147	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
148	theorem		⊢
	proveit.physics.quantum.QPE._best_round_is_int
149	instantiation	212, 208, 162	⊢
	: , : , :
150	theorem		⊢
	proveit.logic.equality.sub_right_side_into
151	instantiation	163, 178, 164, 165	⊢
	: , : , : , : , :
152	instantiation	187, 166, 167	⊢
	: , : , :
153	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
154	instantiation	195, 168	⊢
	: , : , :
155	instantiation	195, 168	⊢
	: , : , :
156	instantiation	202, 178	⊢
	:
157	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
158	instantiation	169, 178, 170	⊢
	: , :
159	theorem		⊢
	proveit.numbers.exponentiation.exp_zero_eq_one
160	instantiation	212, 205, 171	⊢
	: , : , :
161	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
162	instantiation	212, 210, 172	⊢
	: , : , :
163	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_denom_left
164	instantiation	212, 174, 173	⊢
	: , : , :
165	instantiation	212, 174, 175	⊢
	: , : , :
166	instantiation	195, 176	⊢
	: , : , :
167	instantiation	195, 177	⊢
	: , : , :
168	instantiation	197, 178	⊢
	:
169	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
170	instantiation	179	⊢
	:
171	instantiation	212, 180, 181	⊢
	: , : , :
172	instantiation	182, 204	⊢
	:
173	instantiation	212, 184, 183	⊢
	: , : , :
174	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
175	instantiation	212, 184, 185	⊢
	: , : , :
176	instantiation	195, 186	⊢
	: , : , :
177	instantiation	187, 188, 189	⊢
	: , : , :
178	instantiation	212, 205, 190	⊢
	: , : , :
179	axiom		⊢
	proveit.logic.equality.equals_reflexivity
180	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
181	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
182	theorem		⊢
	proveit.numbers.negation.int_closure
183	instantiation	212, 192, 191	⊢
	: , : , :
184	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
185	instantiation	212, 192, 193	⊢
	: , : , :
186	instantiation	194, 203	⊢
	:
187	axiom		⊢
	proveit.logic.equality.equals_transitivity
188	instantiation	195, 196	⊢
	: , : , :
189	instantiation	197, 203	⊢
	:
190	instantiation	212, 208, 198	⊢
	: , : , :
191	instantiation	212, 200, 199	⊢
	: , : , :
192	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
193	instantiation	212, 200, 201	⊢
	: , : , :
194	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
195	axiom		⊢
	proveit.logic.equality.substitution
196	instantiation	202, 203	⊢
	:
197	theorem		⊢
	proveit.numbers.division.frac_one_denom
198	instantiation	212, 210, 204	⊢
	: , : , :
199	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
200	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
201	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
202	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
203	instantiation	212, 205, 206	⊢
	: , : , :
204	instantiation	212, 213, 207	⊢
	: , : , :
205	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
206	instantiation	212, 208, 209	⊢
	: , : , :
207	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
208	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
209	instantiation	212, 210, 211	⊢
	: , : , :
210	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
211	instantiation	212, 213, 214	⊢
	: , : , :
212	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
213	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
214	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements