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	generalization	1	⊢
1	instantiation	116, 2, 3	,  ⊢
	: , : , :
2	instantiation	116, 4, 5	,  ⊢
	: , : , :
3	instantiation	144, 145, 111, 190, 146, 112, 157, 158, 149, 6	⊢
	: , : , : , : , : , :
4	instantiation	116, 7, 8	,  ⊢
	: , : , :
5	instantiation	19, 9, 10, 11	⊢
	: , : , : , :
6	instantiation	12, 130, 28	⊢
	: , :
7	instantiation	116, 13, 14	,  ⊢
	: , : , :
8	instantiation	15, 52, 63	⊢
	: , :
9	instantiation	73, 16	⊢
	: , : , :
10	instantiation	73, 17	⊢
	: , : , :
11	instantiation	75, 18	⊢
	: , :
12	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
13	instantiation	19, 20, 21, 22	,  ⊢
	: , : , : , :
14	instantiation	23, 107, 52, 63	⊢
	: , : , :
15	theorem		⊢
	proveit.numbers.addition.commutation
16	instantiation	113, 145, 111, 190, 146, 112, 157, 158, 149, 130	⊢
	: , : , : , : , : , :
17	instantiation	134, 24, 25	⊢
	: , : , :
18	instantiation	26, 190, 183, 145, 27, 146, 89, 130, 28	⊢
	: , : , : , : , : , :
19	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
20	instantiation	73, 29	,  ⊢
	: , : , :
21	instantiation	73, 30	⊢
	: , : , :
22	instantiation	75, 31	,  ⊢
	: , :
23	theorem		⊢
	proveit.numbers.exponentiation.product_of_complex_powers
24	instantiation	73, 32	⊢
	: , : , :
25	instantiation	75, 33	⊢
	: , :
26	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
27	instantiation	159	⊢
	: , :
28	instantiation	64, 46	⊢
	:
29	instantiation	134, 34, 35	,  ⊢
	: , : , :
30	instantiation	134, 36, 37	⊢
	: , : , :
31	instantiation	38, 39, 40, 140, 41, 42	,  ⊢
	: , : , :
32	instantiation	134, 43, 44	⊢
	: , : , :
33	instantiation	45, 89, 46	⊢
	: , :
34	instantiation	73, 47	,  ⊢
	: , : , :
35	instantiation	75, 48	,  ⊢
	: , :
36	instantiation	73, 49	⊢
	: , : , :
37	instantiation	75, 50	⊢
	: , :
38	theorem		⊢
	proveit.numbers.exponentiation.real_power_of_product
39	instantiation	51, 67, 52	⊢
	: , :
40	instantiation	51, 67, 63	⊢
	: , :
41	instantiation	66, 67, 52, 69	⊢
	: , :
42	instantiation	53, 54, 55	⊢
	: , : , :
43	instantiation	73, 56	⊢
	: , : , :
44	instantiation	75, 57	⊢
	: , :
45	theorem		⊢
	proveit.numbers.multiplication.mult_neg_right
46	instantiation	81, 150, 125, 82	⊢
	: , :
47	instantiation	134, 58, 59	,  ⊢
	: , : , :
48	instantiation	60, 67, 65, 69	,  ⊢
	: , :
49	instantiation	113, 145, 114, 190, 146, 61, 157, 158, 149, 130, 123	⊢
	: , : , : , : , : , :
50	instantiation	62, 67, 63, 69	⊢
	: , :
51	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
52	instantiation	64, 65	⊢
	:
53	theorem		⊢
	proveit.logic.equality.sub_left_side_into
54	instantiation	66, 67, 68, 69	⊢
	: , :
55	instantiation	73, 70	⊢
	: , : , :
56	instantiation	113, 145, 111, 190, 146, 112, 157, 158, 149, 150	⊢
	: , : , : , : , : , :
57	instantiation	93, 89, 150, 96, 95, 71*, 72*	⊢
	: , : , : , :
58	instantiation	73, 74	,  ⊢
	: , : , :
59	instantiation	75, 76	,  ⊢
	: , :
60	instantiation	77, 163	⊢
	:
61	instantiation	132	⊢
	: , : , : , :
62	instantiation	78, 163	⊢
	:
63	instantiation	116, 79, 80	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.negation.complex_closure
65	instantiation	81, 94, 125, 82	⊢
	: , :
66	theorem		⊢
	proveit.numbers.exponentiation.exp_not_eq_zero
67	instantiation	188, 165, 83	⊢
	: , : , :
68	instantiation	116, 84, 85	⊢
	: , : , :
69	instantiation	86, 87	⊢
	:
70	instantiation	88, 190, 157, 158, 149, 130	⊢
	: , : , : , : , : , : , :
71	instantiation	122, 89	⊢
	:
72	instantiation	90, 125	⊢
	:
73	axiom		⊢
	proveit.logic.equality.substitution
74	instantiation	134, 91, 92	,  ⊢
	: , : , :
75	theorem		⊢
	proveit.logic.equality.equals_reversal
76	instantiation	93, 94, 123, 95, 96, 97*, 98*	,  ⊢
	: , : , : , :
77	theorem		⊢
	proveit.numbers.exponentiation.int_exp_of_neg_exp
78	theorem		⊢
	proveit.numbers.exponentiation.int_exp_of_exp
79	instantiation	156, 143, 99	⊢
	: , :
80	instantiation	134, 100, 101	⊢
	: , : , :
81	theorem		⊢
	proveit.numbers.division.div_complex_closure
82	instantiation	102, 185	⊢
	:
83	instantiation	188, 172, 107	⊢
	: , : , :
84	instantiation	156, 127, 103	⊢
	: , :
85	instantiation	134, 104, 105	⊢
	: , : , :
86	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
87	instantiation	188, 106, 107	⊢
	: , : , :
88	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
89	instantiation	116, 108, 109	⊢
	: , : , :
90	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
91	instantiation	110, 111, 190, 145, 112, 146, 157, 158, 149, 123, 150	,  ⊢
	: , : , : , : , : , : , :
92	instantiation	113, 145, 114, 190, 146, 115, 157, 158, 149, 150, 123	,  ⊢
	: , : , : , : , : , :
93	theorem		⊢
	proveit.numbers.division.prod_of_fracs
94	instantiation	116, 117, 118	⊢
	: , : , :
95	instantiation	188, 120, 119	⊢
	: , : , :
96	instantiation	188, 120, 121	⊢
	: , : , :
97	instantiation	122, 123	⊢
	:
98	instantiation	124, 125	⊢
	:
99	instantiation	156, 149, 130	⊢
	: , :
100	instantiation	144, 190, 183, 145, 126, 146, 143, 149, 130	⊢
	: , : , : , : , : , :
101	instantiation	144, 145, 183, 146, 147, 126, 157, 158, 149, 130	⊢
	: , : , : , : , : , :
102	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
103	instantiation	156, 158, 130	⊢
	: , :
104	instantiation	144, 190, 183, 145, 129, 146, 127, 158, 130	⊢
	: , : , : , : , : , :
105	instantiation	144, 145, 183, 146, 128, 129, 157, 149, 158, 130	⊢
	: , : , : , : , : , :
106	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
107	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
108	instantiation	156, 143, 149	⊢
	: , :
109	instantiation	144, 145, 183, 190, 146, 147, 157, 158, 149	⊢
	: , : , : , : , : , :
110	theorem		⊢
	proveit.numbers.multiplication.rightward_commutation
111	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
112	instantiation	131	⊢
	: , : , :
113	theorem		⊢
	proveit.numbers.multiplication.association
114	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
115	instantiation	132	⊢
	: , : , : , :
116	theorem		⊢
	proveit.logic.equality.sub_right_side_into
117	instantiation	156, 143, 133	⊢
	: , :
118	instantiation	134, 135, 136	⊢
	: , : , :
119	instantiation	188, 138, 137	⊢
	: , : , :
120	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
121	instantiation	188, 138, 139	⊢
	: , : , :
122	theorem		⊢
	proveit.numbers.division.frac_one_denom
123	instantiation	188, 165, 140	⊢
	: , : , :
124	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
125	instantiation	188, 165, 141	⊢
	: , : , :
126	instantiation	159	⊢
	: , :
127	instantiation	156, 157, 149	⊢
	: , :
128	instantiation	159	⊢
	: , :
129	instantiation	159	⊢
	: , :
130	instantiation	188, 165, 142	⊢
	: , : , :
131	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
132	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
133	instantiation	156, 149, 150	⊢
	: , :
134	axiom		⊢
	proveit.logic.equality.equals_transitivity
135	instantiation	144, 190, 183, 145, 148, 146, 143, 149, 150	⊢
	: , : , : , : , : , :
136	instantiation	144, 145, 183, 146, 147, 148, 157, 158, 149, 150	⊢
	: , : , : , : , : , :
137	instantiation	188, 152, 151	⊢
	: , : , :
138	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
139	instantiation	188, 152, 153	⊢
	: , : , :
140	instantiation	188, 170, 154	⊢
	: , : , :
141	instantiation	188, 170, 155	⊢
	: , : , :
142	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
143	instantiation	156, 157, 158	⊢
	: , :
144	theorem		⊢
	proveit.numbers.multiplication.disassociation
145	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
146	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
147	instantiation	159	⊢
	: , :
148	instantiation	159	⊢
	: , :
149	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
150	instantiation	188, 165, 160	⊢
	: , : , :
151	instantiation	188, 161, 185	⊢
	: , : , :
152	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
153	instantiation	188, 161, 162	⊢
	: , : , :
154	instantiation	188, 178, 163	⊢
	: , : , :
155	instantiation	188, 178, 181	⊢
	: , : , :
156	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
157	instantiation	188, 165, 164	⊢
	: , : , :
158	instantiation	188, 165, 166	⊢
	: , : , :
159	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
160	instantiation	188, 170, 167	⊢
	: , : , :
161	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
162	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
163	instantiation	188, 168, 169	⊢
	: , : , :
164	instantiation	188, 170, 171	⊢
	: , : , :
165	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
166	instantiation	188, 172, 173	⊢
	: , : , :
167	instantiation	188, 178, 174	⊢
	: , : , :
168	instantiation	175, 176, 177	⊢
	: , :
169	assumption		⊢
170	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
171	instantiation	188, 178, 179	⊢
	: , : , :
172	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
173	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
174	assumption		⊢
175	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
176	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
177	instantiation	180, 181, 182	⊢
	: , :
178	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
179	instantiation	188, 189, 183	⊢
	: , : , :
180	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
181	instantiation	188, 184, 185	⊢
	: , : , :
182	instantiation	186, 187	⊢
	:
183	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
184	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
185	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
186	theorem		⊢
	proveit.numbers.negation.int_closure
187	instantiation	188, 189, 190	⊢
	: , : , :
188	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
189	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
190	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements