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	reference	4	⊢
2	instantiation	4, 5, 6	,  ⊢
	: , : , :
3	instantiation	70, 7, 8	,  ⊢
	: , : , :
4	theorem		⊢
	proveit.logic.equality.sub_left_side_into
5	instantiation	9, 77, 10, 11, 12, 13*, 14*	,  ⊢
	: , : , :
6	instantiation	70, 15, 16	,  ⊢
	: , : , :
7	instantiation	45, 17	,  ⊢
	: , : , :
8	instantiation	29, 77, 37	,  ⊢
	: , :
9	theorem		⊢
	proveit.numbers.exponentiation.exp_eq
10	instantiation	18, 19, 23	⊢
	: , :
11	instantiation	18, 19, 26	⊢
	: , :
12	instantiation	20, 109, 93, 21*, 22*	⊢
	: , :
13	instantiation	25, 42, 23, 77, 24*	,  ⊢
	: , : , :
14	instantiation	25, 42, 26, 77, 27*	,  ⊢
	: , : , :
15	instantiation	45, 28	,  ⊢
	: , : , :
16	instantiation	29, 77, 34	,  ⊢
	: , :
17	instantiation	86, 30, 31	,  ⊢
	: , : , :
18	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
19	instantiation	146, 120, 32	⊢
	: , : , :
20	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.exp_neg2pi_i_x
21	instantiation	33, 56, 79, 44	⊢
	: , :
22	instantiation	33, 51, 79, 44	⊢
	: , :
23	instantiation	35, 34	⊢
	:
24	instantiation	36, 34, 77	,  ⊢
	: , :
25	theorem		⊢
	proveit.numbers.exponentiation.complex_power_of_complex_power
26	instantiation	35, 37	⊢
	:
27	instantiation	36, 37, 77	,  ⊢
	: , :
28	instantiation	86, 38, 39	,  ⊢
	: , : , :
29	theorem		⊢
	proveit.numbers.multiplication.commutation
30	instantiation	45, 40	,  ⊢
	: , : , :
31	instantiation	47, 41	,  ⊢
	: , :
32	instantiation	146, 126, 42	⊢
	: , : , :
33	theorem		⊢
	proveit.numbers.division.neg_frac_neg_numerator
34	instantiation	43, 56, 79, 44	⊢
	: , :
35	theorem		⊢
	proveit.numbers.negation.complex_closure
36	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
37	instantiation	43, 51, 79, 44	⊢
	: , :
38	instantiation	45, 46	,  ⊢
	: , : , :
39	instantiation	47, 48	,  ⊢
	: , :
40	instantiation	86, 49, 50	,  ⊢
	: , : , :
41	instantiation	55, 77, 51, 57, 58, 59*, 60*	,  ⊢
	: , : , : , :
42	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
43	theorem		⊢
	proveit.numbers.division.div_complex_closure
44	instantiation	52, 143	⊢
	:
45	axiom		⊢
	proveit.logic.equality.substitution
46	instantiation	86, 53, 54	,  ⊢
	: , : , :
47	theorem		⊢
	proveit.logic.equality.equals_reversal
48	instantiation	55, 77, 56, 57, 58, 59*, 60*	,  ⊢
	: , : , : , :
49	instantiation	64, 98, 65, 148, 99, 66, 111, 112, 102, 77, 95	,  ⊢
	: , : , : , : , : , : , :
50	instantiation	67, 148, 68, 98, 61, 99, 77, 111, 112, 102, 95	,  ⊢
	: , : , : , : , : , :
51	instantiation	70, 62, 63	⊢
	: , : , :
52	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
53	instantiation	64, 98, 65, 148, 99, 66, 111, 112, 102, 77, 103	,  ⊢
	: , : , : , : , : , : , :
54	instantiation	67, 148, 68, 98, 69, 99, 77, 111, 112, 102, 103	,  ⊢
	: , : , : , : , : , :
55	theorem		⊢
	proveit.numbers.division.prod_of_fracs
56	instantiation	70, 71, 72	⊢
	: , : , :
57	instantiation	146, 74, 73	⊢
	: , : , :
58	instantiation	146, 74, 75	⊢
	: , : , :
59	instantiation	76, 77	⊢
	:
60	instantiation	78, 79	⊢
	:
61	instantiation	84	⊢
	: , : , : , :
62	instantiation	110, 96, 80	⊢
	: , :
63	instantiation	86, 81, 82	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
65	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
66	instantiation	83	⊢
	: , : , :
67	theorem		⊢
	proveit.numbers.multiplication.association
68	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
69	instantiation	84	⊢
	: , : , : , :
70	theorem		⊢
	proveit.logic.equality.sub_right_side_into
71	instantiation	110, 96, 85	⊢
	: , :
72	instantiation	86, 87, 88	⊢
	: , : , :
73	instantiation	146, 90, 89	⊢
	: , : , :
74	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
75	instantiation	146, 90, 91	⊢
	: , : , :
76	theorem		⊢
	proveit.numbers.division.frac_one_denom
77	instantiation	146, 120, 92	⊢
	: , : , :
78	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
79	instantiation	146, 120, 93	⊢
	: , : , :
80	instantiation	110, 102, 95	⊢
	: , :
81	instantiation	97, 148, 133, 98, 94, 99, 96, 102, 95	⊢
	: , : , : , : , : , :
82	instantiation	97, 98, 133, 99, 100, 94, 111, 112, 102, 95	⊢
	: , : , : , : , : , :
83	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
84	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
85	instantiation	110, 102, 103	⊢
	: , :
86	axiom		⊢
	proveit.logic.equality.equals_transitivity
87	instantiation	97, 148, 133, 98, 101, 99, 96, 102, 103	⊢
	: , : , : , : , : , :
88	instantiation	97, 98, 133, 99, 100, 101, 111, 112, 102, 103	⊢
	: , : , : , : , : , :
89	instantiation	146, 105, 104	⊢
	: , : , :
90	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
91	instantiation	146, 105, 106	⊢
	: , : , :
92	instantiation	146, 124, 107	⊢
	: , : , :
93	instantiation	146, 124, 108	⊢
	: , : , :
94	instantiation	113	⊢
	: , :
95	instantiation	146, 120, 109	⊢
	: , : , :
96	instantiation	110, 111, 112	⊢
	: , :
97	theorem		⊢
	proveit.numbers.multiplication.disassociation
98	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
99	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
100	instantiation	113	⊢
	: , :
101	instantiation	113	⊢
	: , :
102	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
103	instantiation	146, 120, 114	⊢
	: , : , :
104	instantiation	146, 116, 115	⊢
	: , : , :
105	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
106	instantiation	146, 116, 143	⊢
	: , : , :
107	instantiation	146, 129, 117	⊢
	: , : , :
108	instantiation	146, 129, 140	⊢
	: , : , :
109	instantiation	146, 124, 118	⊢
	: , : , :
110	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
111	instantiation	146, 120, 119	⊢
	: , : , :
112	instantiation	146, 120, 121	⊢
	: , : , :
113	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
114	instantiation	146, 124, 122	⊢
	: , : , :
115	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
116	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
117	instantiation	146, 131, 123	⊢
	: , : , :
118	instantiation	146, 129, 138	⊢
	: , : , :
119	instantiation	146, 124, 125	⊢
	: , : , :
120	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
121	instantiation	146, 126, 127	⊢
	: , : , :
122	instantiation	146, 129, 128	⊢
	: , : , :
123	assumption		⊢
124	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
125	instantiation	146, 129, 130	⊢
	: , : , :
126	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
127	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
128	instantiation	146, 131, 132	⊢
	: , : , :
129	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
130	instantiation	146, 147, 133	⊢
	: , : , :
131	instantiation	134, 135, 136	⊢
	: , :
132	instantiation	137, 138, 143	⊢
	: , :
133	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
134	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
135	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
136	instantiation	139, 140, 141	⊢
	: , :
137	theorem		⊢
	proveit.numbers.modular.mod_natpos_in_interval
138	assumption		⊢
139	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
140	instantiation	146, 142, 143	⊢
	: , : , :
141	instantiation	144, 145	⊢
	:
142	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
143	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
144	theorem		⊢
	proveit.numbers.negation.int_closure
145	instantiation	146, 147, 148	⊢
	: , : , :
146	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
147	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
148	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements