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