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