Proof of proveit.physics.quantum.QPE._alpha_m_evaluation theorem

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import k, l, m, n, t, defaults
from proveit.logic import InSet
from proveit.numbers import Mult
from proveit.physics.quantum.QPE import ( _m_domain, _t ) # QPE Common Expressions
from proveit.physics.quantum.QPE import (                 # QPE Axioms
    _alpha_m_def, _Psi_def )
from proveit.physics.quantum.QPE import (                 # QPE Theorems
    _phase_is_real, _psi_t_formula, _t_in_natural_pos )
from proveit.physics.quantum.QFT import invFT_on_matrix_elem

%proving _alpha_m_evaluation

Under these presumptions, we begin our proof of
_alpha_m_evaluation:
(see dependencies)

defaults.assumptions = _alpha_m_evaluation.conditions

defaults.assumptions:

_alpha_m_def

 ⊢  

alpha_m_eq_01 = _alpha_m_def.instantiate()

alpha_m_eq_01:  ⊢  

_Psi_def

 ⊢  

alpha_m_eq_02 = _Psi_def.sub_right_side_into(alpha_m_eq_01)

alpha_m_eq_02:  ⊢  

_psi_t_formula

 ⊢  

# This instantiation requires we know that _t is in NaturalPos
psi_formula = _psi_t_formula.instantiate({t:_t})

psi_formula:  ⊢  

# Auto_simplification here pulls the constant coefficient
# out to the front of the bra-ket; for that auto-simplification
# factoring to work, however, we need the _phase_is_real theorem
# and the correct domain assumption for m.
alpha_m_eq_03 = psi_formula.sub_right_side_into(alpha_m_eq_02)

alpha_m_eq_03:  ⊢  

alpha_m_eq_04 = alpha_m_eq_03.inner_expr().rhs.operands[1].distribute(2)

alpha_m_eq_04:  ⊢  

# for convenience and clarity we name the summation domain
k_domain = psi_formula.rhs.operands[1].domain

k_domain:

invFT_on_matrix_elem

 ⊢  

matrix_elem = invFT_on_matrix_elem.instantiate(
    {n:_t, l:m}, assumptions=[InSet(k, k_domain), InSet(m, _m_domain)])

matrix_elem: ,  ⊢  

# We don't want to combine the two different exponentials through auto-simplification.
Mult.change_simplification_directives(combine_all_exponents=False)
alpha_m_eq_05 = (alpha_m_eq_04.inner_expr().rhs.operands[1]
               .summand.operands[1].substitute(matrix_elem))

alpha_m_eq_05:  ⊢  

_alpha_m_evaluation may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

proveit.physics.quantum.QPE._alpha_m_evaluation has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	331, 2, 3	⊢
	: , : , :
2	instantiation	4, 5, 6	⊢
	: , :
3	instantiation	7, 398, 8, 9, 10, 11	⊢
	: , : , : , :
4	theorem		⊢
	proveit.logic.equality.rhs_via_equality
5	instantiation	306, 12, 13	⊢
	: , : , :
6	instantiation	341, 14, 15*, 16*, 17*	⊢
	: , : , :
7	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
8	instantiation	338	⊢
	: , :
9	instantiation	338	⊢
	: , :
10	instantiation	107, 18	⊢
	: , :
11	instantiation	341, 19	⊢
	: , : , :
12	instantiation	306, 20, 21, 22*	⊢
	: , : , :
13	modus ponens	23, 152	⊢
14	modus ponens	24, 25	⊢
15	instantiation	101, 366	⊢
	: , :
16	instantiation	101, 366	⊢
	: , :
17	instantiation	331, 26, 27	⊢
	: , : , :
18	instantiation	196, 28, 29, 30	⊢
	: , : , : , :
19	modus ponens	31, 32	⊢
20	instantiation	306, 33, 34	⊢
	: , : , :
21	instantiation	35, 400	⊢
	:
22	instantiation	331, 36, 37	⊢
	: , : , :
23	instantiation	38, 390, 398, 322, 210, 323, 39*	⊢
	: , : , : , : , : , : , : , :
24	instantiation	140, 390	⊢
	: , : , : , : , : , : , :
25	generalization	40	⊢
26	instantiation	341, 41	⊢
	: , : , :
27	instantiation	331, 42, 43	⊢
	: , : , :
28	instantiation	315, 257, 227, 228, 44*	⊢
	: , :
29	instantiation	341, 45	⊢
	: , : , :
30	instantiation	107, 46	⊢
	: , :
31	instantiation	121, 390	⊢
	: , : , : , : , : , :
32	generalization	47	⊢
33	instantiation	48, 356	⊢
	:
34	axiom		⊢
	proveit.physics.quantum.QPE._Psi_def
35	conjecture		⊢
	proveit.physics.quantum.QPE._psi_t_formula
36	instantiation	341, 49	⊢
	: , : , :
37	instantiation	331, 50, 51	⊢
	: , : , :
38	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_distribution_over_summation
39	instantiation	331, 52, 53	⊢
	: , : , :
40	instantiation	54, 400, 366, 356, 55*	,  ⊢
	: , : , :
41	instantiation	331, 56, 57	⊢
	: , : , :
42	instantiation	321, 403, 398, 322, 58, 323, 241, 60	⊢
	: , : , : , : , : , :
43	instantiation	179, 322, 398, 403, 323, 59, 241, 60, 61*	⊢
	: , : , : , : , : , :
44	instantiation	331, 62, 63	⊢
	: , : , :
45	instantiation	107, 64	⊢
	: , :
46	instantiation	331, 65, 66	⊢
	: , : , :
47	instantiation	138, 67	⊢
	: , : , :
48	axiom		⊢
	proveit.physics.quantum.QPE._alpha_m_def
49	instantiation	196, 68, 69, 70	⊢
	: , : , : , :
50	instantiation	331, 71, 72	⊢
	: , : , :
51	instantiation	157, 158, 241, 73, 152, 74*	⊢
	: , : , :
52	instantiation	341, 75, 76*, 77*	⊢
	: , : , :
53	modus ponens	78, 79	⊢
54	conjecture		⊢
	proveit.physics.quantum.QFT.invFT_on_matrix_elem
55	instantiation	80, 226, 227, 228	,  ⊢
	: , :
56	instantiation	341, 81	⊢
	: , : , :
57	instantiation	331, 82, 83	⊢
	: , : , :
58	instantiation	338	⊢
	: , :
59	instantiation	338	⊢
	: , :
60	modus ponens	84, 143	⊢
61	instantiation	85, 241, 390, 86*, 87*	⊢
	: , : , :
62	instantiation	341, 88	⊢
	: , : , :
63	instantiation	290, 89	⊢
	:
64	instantiation	90, 202, 361, 91*	⊢
	: , :
65	instantiation	341, 92	⊢
	: , : , :
66	instantiation	184, 361, 93, 370, 316	⊢
	: , : , :
67	deduction	94	⊢
68	instantiation	155, 241, 403, 322, 323, 95	⊢
	: , : , : , : , : , :
69	instantiation	156, 403, 241, 95	⊢
	: , : , : , : , :
70	instantiation	157, 392, 241, 151, 95	⊢
	: , : , :
71	instantiation	331, 96, 97	⊢
	: , : , :
72	instantiation	156, 403, 398, 241, 151, 152	⊢
	: , : , : , : , :
73	instantiation	327	⊢
	: , : , :
74	instantiation	175, 241, 98	⊢
	: , :
75	modus ponens	99, 100	⊢
76	instantiation	101, 366	⊢
	: , :
77	instantiation	101, 366	⊢
	: , :
78	instantiation	102, 390	⊢
	: , : , : , :
79	generalization	103	⊢
80	conjecture		⊢
	proveit.numbers.division.neg_frac_neg_numerator
81	modus ponens	104, 105	⊢
82	instantiation	341, 106	⊢
	: , : , :
83	instantiation	107, 108	⊢
	: , :
84	instantiation	109	⊢
	: , : , :
85	conjecture		⊢
	proveit.numbers.exponentiation.product_of_posnat_powers
86	instantiation	360, 241	⊢
	:
87	conjecture		⊢
	proveit.numbers.numerals.decimals.add_1_1
88	instantiation	184, 361, 354, 232, 316, 110*	⊢
	: , : , :
89	instantiation	278, 361, 111	⊢
	: , :
90	conjecture		⊢
	proveit.numbers.multiplication.mult_neg_left
91	instantiation	196, 112, 113, 127	⊢
	: , : , : , :
92	instantiation	331, 114, 115	⊢
	: , : , :
93	instantiation	116, 221	⊢
	:
94	instantiation	343, 238, 181	,  ⊢
	: , :
95	instantiation	190, 261, 244, 187	⊢
	: , : , : , :
96	instantiation	155, 241, 403, 322, 323, 117	⊢
	: , : , : , : , : , :
97	instantiation	150, 398, 392, 322, 206, 151, 323, 118	⊢
	: , : , : , : , : , :
98	instantiation	280, 119, 172	⊢
	: , : , :
99	instantiation	140, 390	⊢
	: , : , : , : , : , : , :
100	generalization	120	⊢
101	conjecture		⊢
	proveit.core_expr_types.conditionals.satisfied_condition_reduction
102	axiom		⊢
	proveit.linear_algebra.addition.scalar_sum_extends_number_sum
103	instantiation	335, 238, 176	,  ⊢
	: , :
104	instantiation	121, 390	⊢
	: , : , : , : , : , :
105	generalization	122	⊢
106	modus ponens	123, 124	⊢
107	theorem		⊢
	proveit.logic.equality.equals_reversal
108	instantiation	125, 323, 241	⊢
	: , :
109	conjecture		⊢
	proveit.numbers.summation.summation_complex_closure
110	instantiation	126, 344, 257, 127*	⊢
	: , :
111	instantiation	211, 344	⊢
	:
112	instantiation	321, 322, 398, 403, 323, 234, 345, 344, 361	⊢
	: , : , : , : , : , :
113	instantiation	331, 128, 129	⊢
	: , : , :
114	instantiation	341, 282	⊢
	: , : , :
115	instantiation	315, 257, 130, 281, 131*	⊢
	: , :
116	conjecture		⊢
	proveit.numbers.negation.real_closure
117	instantiation	280, 152, 132	⊢
	: , : , :
118	instantiation	280, 133, 134	⊢
	: , : , :
119	instantiation	207, 261, 262, 208, 187	⊢
	: , : , : , :
120	instantiation	196, 135, 136, 137	,  ⊢
	: , : , : , :
121	axiom		⊢
	proveit.core_expr_types.lambda_maps.lambda_substitution
122	instantiation	138, 139	⊢
	: , : , :
123	instantiation	140, 390	⊢
	: , : , : , : , : , : , :
124	generalization	141	⊢
125	modus ponens	142, 143	⊢
126	conjecture		⊢
	proveit.numbers.multiplication.mult_neg_right
127	instantiation	273, 344	⊢
	:
128	instantiation	144, 322, 398, 323, 145, 345, 344, 361	⊢
	: , : , : , : , : , : , :
129	instantiation	331, 146, 147	⊢
	: , : , :
130	instantiation	278, 361, 202	⊢
	: , :
131	instantiation	331, 148, 149	⊢
	: , : , :
132	instantiation	150, 403, 392, 322, 151, 323, 152	⊢
	: , : , : , : , : , :
133	instantiation	190, 261, 262, 153, 187	⊢
	: , : , : , :
134	instantiation	209, 158, 154	⊢
	: , : , :
135	instantiation	155, 238, 398, 322, 210, 323, 160	,  ⊢
	: , : , : , : , : , :
136	instantiation	156, 398, 403, 238, 210, 160	,  ⊢
	: , : , : , : , :
137	instantiation	157, 158, 238, 159, 160, 161*	,  ⊢
	: , : , :
138	axiom		⊢
	proveit.core_expr_types.conditionals.conditional_substitution
139	deduction	162	⊢
140	conjecture		⊢
	proveit.core_expr_types.lambda_maps.general_lambda_substitution
141	instantiation	331, 163, 164	,  ⊢
	: , : , :
142	instantiation	165, 403, 390, 322	⊢
	: , : , : , : , : , :
143	generalization	166	⊢
144	conjecture		⊢
	proveit.numbers.multiplication.rightward_commutation
145	instantiation	338	⊢
	: , :
146	instantiation	179, 403, 398, 322, 167, 323, 344, 361, 345	⊢
	: , : , : , : , : , :
147	instantiation	341, 168	⊢
	: , : , :
148	instantiation	341, 169	⊢
	: , : , :
149	instantiation	290, 170	⊢
	:
150	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_disassociation
151	instantiation	338	⊢
	: , :
152	instantiation	280, 171, 172	⊢
	: , : , :
153	instantiation	260, 261, 262, 173	⊢
	: , : , :
154	instantiation	327	⊢
	: , : , :
155	conjecture		⊢
	proveit.physics.quantum.algebra.scalar_mult_absorption
156	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_pulling_scalar_out_front
157	conjecture		⊢
	proveit.physics.quantum.algebra.scalar_mult_factorization
158	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat3
159	instantiation	327	⊢
	: , : , :
160	instantiation	280, 174, 192	,  ⊢
	: , : , :
161	instantiation	175, 238, 176	,  ⊢
	: , :
162	instantiation	321, 403, 398, 322, 177, 323, 238, 241, 181	,  ⊢
	: , : , : , : , : , :
163	instantiation	178, 322, 403, 323, 238, 241, 181	,  ⊢
	: , : , : , : , : , : , :
164	instantiation	179, 403, 398, 322, 180, 323, 241, 238, 181	,  ⊢
	: , : , : , : , : , :
165	conjecture		⊢
	proveit.numbers.multiplication.distribute_through_summation
166	instantiation	335, 238, 181	,  ⊢
	: , :
167	instantiation	338	⊢
	: , :
168	instantiation	306, 182, 183	⊢
	: , : , :
169	instantiation	184, 361, 221, 232, 316, 185*	⊢
	: , : , :
170	instantiation	278, 361, 186	⊢
	: , :
171	instantiation	190, 261, 262, 208, 187	⊢
	: , : , : , :
172	instantiation	209, 392, 210	⊢
	: , : , :
173	instantiation	280, 188, 189	⊢
	: , : , :
174	instantiation	190, 261, 262, 208, 239	,  ⊢
	: , : , : , :
175	axiom		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
176	instantiation	280, 191, 192	,  ⊢
	: , : , :
177	instantiation	338	⊢
	: , :
178	conjecture		⊢
	proveit.numbers.multiplication.leftward_commutation
179	conjecture		⊢
	proveit.numbers.multiplication.association
180	instantiation	338	⊢
	: , :
181	instantiation	278, 254, 193	,  ⊢
	: , :
182	instantiation	306, 194, 195	⊢
	: , : , :
183	instantiation	196, 197, 198, 199	⊢
	: , : , : , :
184	conjecture		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
185	instantiation	331, 200, 201	⊢
	: , : , :
186	instantiation	211, 202	⊢
	:
187	modus ponens	203, 204	⊢
188	instantiation	242, 261, 262, 205, 244	⊢
	: , : , : , : , :
189	instantiation	209, 392, 206	⊢
	: , : , :
190	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_op_ket_in_QmultCodomain
191	instantiation	207, 261, 262, 208, 239	,  ⊢
	: , : , : , :
192	instantiation	209, 392, 210	⊢
	: , : , :
193	instantiation	211, 212	,  ⊢
	:
194	instantiation	213, 257, 352, 214	⊢
	: , : , : , : , :
195	instantiation	331, 215, 216	⊢
	: , : , :
196	conjecture		⊢
	proveit.logic.equality.four_chain_transitivity
197	instantiation	341, 217	⊢
	: , : , :
198	instantiation	341, 217	⊢
	: , : , :
199	instantiation	273, 257	⊢
	:
200	instantiation	321, 322, 398, 403, 323, 234, 345, 344, 218	⊢
	: , : , : , : , : , :
201	instantiation	219, 398, 322, 234, 323, 345, 344, 257, 220*	⊢
	: , : , : , : , :
202	instantiation	401, 369, 221	⊢
	: , : , :
203	instantiation	222, 390, 237	⊢
	: , : , : , : , : , :
204	generalization	223	⊢
205	instantiation	260, 261, 262, 224	⊢
	: , : , :
206	instantiation	338	⊢
	: , :
207	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_op_ket_is_ket
208	instantiation	260, 261, 262, 225	⊢
	: , : , :
209	axiom		⊢
	proveit.physics.quantum.algebra.multi_qmult_def
210	instantiation	338	⊢
	: , :
211	conjecture		⊢
	proveit.numbers.negation.complex_closure
212	instantiation	296, 226, 227, 228	,  ⊢
	: , :
213	conjecture		⊢
	proveit.numbers.division.mult_frac_cancel_numer_left
214	instantiation	401, 358, 229	⊢
	: , : , :
215	instantiation	341, 230	⊢
	: , : , :
216	instantiation	341, 231	⊢
	: , : , :
217	instantiation	272, 257	⊢
	:
218	instantiation	401, 369, 232	⊢
	: , : , :
219	conjecture		⊢
	proveit.numbers.multiplication.mult_neg_any
220	instantiation	233, 398, 322, 234, 323, 345, 344	⊢
	: , : , : , :
221	instantiation	401, 380, 235	⊢
	: , : , :
222	conjecture		⊢
	proveit.linear_algebra.addition.summation_closure
223	instantiation	236, 237, 238, 239	⊢
	: , : , : , :
224	instantiation	240, 241, 261, 262, 243	⊢
	: , : , : , :
225	instantiation	242, 261, 262, 243, 244	⊢
	: , : , : , : , :
226	instantiation	306, 245, 246	,  ⊢
	: , : , :
227	instantiation	401, 369, 247	⊢
	: , : , :
228	instantiation	330, 301	⊢
	:
229	instantiation	401, 367, 248	⊢
	: , : , :
230	instantiation	331, 249, 250	⊢
	: , : , :
231	instantiation	341, 251	⊢
	: , : , :
232	instantiation	401, 380, 252	⊢
	: , : , :
233	conjecture		⊢
	proveit.numbers.multiplication.elim_one_any
234	instantiation	338	⊢
	: , :
235	instantiation	401, 373, 314	⊢
	: , : , :
236	conjecture		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
237	instantiation	253, 301	⊢
	:
238	instantiation	278, 254, 255	⊢
	: , :
239	instantiation	256, 400, 366	⊢
	: , :
240	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_op_complex_closure
241	instantiation	296, 257, 258, 259	⊢
	: , :
242	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_op_op_is_op
243	instantiation	260, 261, 262, 263	⊢
	: , : , :
244	instantiation	264, 301, 265	⊢
	: , : , :
245	instantiation	335, 309, 266	,  ⊢
	: , :
246	instantiation	331, 267, 268	,  ⊢
	: , : , :
247	instantiation	401, 380, 269	⊢
	: , : , :
248	instantiation	401, 378, 270	⊢
	: , : , :
249	instantiation	341, 271	⊢
	: , : , :
250	instantiation	272, 361	⊢
	:
251	instantiation	273, 361	⊢
	:
252	instantiation	401, 389, 387	⊢
	: , : , :
253	conjecture		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
254	instantiation	401, 369, 274	⊢
	: , : , :
255	instantiation	306, 275, 276	⊢
	: , : , :
256	conjecture		⊢
	proveit.physics.quantum.algebra.num_ket_in_register_space
257	instantiation	401, 369, 277	⊢
	: , : , :
258	instantiation	278, 361, 279	⊢
	: , :
259	instantiation	280, 281, 282	⊢
	: , : , :
260	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_op_is_linmap
261	instantiation	283, 301	⊢
	:
262	conjecture		⊢
	proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
263	instantiation	284, 400, 356	⊢
	: , :
264	conjecture		⊢
	proveit.physics.quantum.algebra.qmult_matrix_is_linmap
265	instantiation	362, 285, 286	⊢
	: , : , :
266	instantiation	306, 287, 288	,  ⊢
	: , : , :
267	instantiation	321, 403, 310, 322, 289, 323, 309, 336, 325, 305	,  ⊢
	: , : , : , : , : , :
268	instantiation	321, 322, 398, 310, 323, 311, 289, 361, 326, 336, 325, 305	,  ⊢
	: , : , : , : , : , :
269	instantiation	401, 389, 386	⊢
	: , : , :
270	instantiation	401, 388, 390	⊢
	: , : , :
271	instantiation	290, 361	⊢
	:
272	conjecture		⊢
	proveit.numbers.division.frac_one_denom
273	conjecture		⊢
	proveit.numbers.multiplication.elim_one_right
274	instantiation	401, 349, 291	⊢
	: , : , :
275	instantiation	335, 309, 292	⊢
	: , :
276	instantiation	331, 293, 294	⊢
	: , : , :
277	instantiation	401, 380, 295	⊢
	: , : , :
278	conjecture		⊢
	proveit.numbers.exponentiation.exp_complex_closure
279	instantiation	296, 344, 361, 316	⊢
	: , :
280	theorem		⊢
	proveit.logic.equality.sub_left_side_into
281	instantiation	297, 368, 298	⊢
	: , :
282	instantiation	341, 299	⊢
	: , : , :
283	conjecture		⊢
	proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
284	conjecture		⊢
	proveit.physics.quantum.algebra.num_bra_is_lin_map
285	instantiation	300, 301	⊢
	:
286	instantiation	302, 400	⊢
	:
287	instantiation	335, 303, 305	,  ⊢
	: , :
288	instantiation	321, 322, 398, 403, 323, 304, 336, 325, 305	,  ⊢
	: , : , : , : , : , :
289	instantiation	327	⊢
	: , : , :
290	conjecture		⊢
	proveit.numbers.multiplication.elim_one_left
291	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
292	instantiation	306, 307, 308	⊢
	: , : , :
293	instantiation	321, 403, 310, 322, 312, 323, 309, 336, 337, 325	⊢
	: , : , : , : , : , :
294	instantiation	321, 322, 398, 310, 323, 311, 312, 361, 326, 336, 337, 325	⊢
	: , : , : , : , : , :
295	instantiation	401, 389, 397	⊢
	: , : , :
296	conjecture		⊢
	proveit.numbers.division.div_complex_closure
297	conjecture		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
298	instantiation	401, 313, 314	⊢
	: , : , :
299	instantiation	315, 344, 361, 316, 317*	⊢
	: , :
300	conjecture		⊢
	proveit.linear_algebra.matrices.unitaries_are_matrices
301	instantiation	318, 398, 395	⊢
	: , :
302	conjecture		⊢
	proveit.physics.quantum.QFT.invFT_is_unitary
303	instantiation	335, 336, 325	⊢
	: , :
304	instantiation	338	⊢
	: , :
305	instantiation	401, 369, 319	⊢
	: , : , :
306	theorem		⊢
	proveit.logic.equality.sub_right_side_into
307	instantiation	335, 320, 325	⊢
	: , :
308	instantiation	321, 322, 398, 403, 323, 324, 336, 337, 325	⊢
	: , : , : , : , : , :
309	instantiation	335, 361, 326	⊢
	: , :
310	conjecture		⊢
	proveit.numbers.numerals.decimals.nat3
311	instantiation	338	⊢
	: , :
312	instantiation	327	⊢
	: , : , :
313	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
314	instantiation	328, 374, 329	⊢
	: , :
315	conjecture		⊢
	proveit.numbers.division.div_as_mult
316	instantiation	330, 392	⊢
	:
317	instantiation	331, 332, 333	⊢
	: , : , :
318	conjecture		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
319	instantiation	401, 380, 334	⊢
	: , : , :
320	instantiation	335, 336, 337	⊢
	: , :
321	conjecture		⊢
	proveit.numbers.multiplication.disassociation
322	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
323	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
324	instantiation	338	⊢
	: , :
325	instantiation	401, 369, 339	⊢
	: , : , :
326	instantiation	401, 369, 340	⊢
	: , : , :
327	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
328	conjecture		⊢
	proveit.numbers.multiplication.mult_rational_pos_closure_bin
329	instantiation	401, 391, 400	⊢
	: , : , :
330	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
331	axiom		⊢
	proveit.logic.equality.equals_transitivity
332	instantiation	341, 342	⊢
	: , : , :
333	instantiation	343, 344, 345	⊢
	: , :
334	instantiation	401, 389, 346	⊢
	: , : , :
335	conjecture		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
336	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
337	instantiation	401, 369, 347	⊢
	: , : , :
338	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
339	instantiation	401, 380, 348	⊢
	: , : , :
340	instantiation	401, 349, 350	⊢
	: , : , :
341	axiom		⊢
	proveit.logic.equality.substitution
342	instantiation	351, 352, 390, 353*	⊢
	: , :
343	conjecture		⊢
	proveit.numbers.multiplication.commutation
344	instantiation	401, 369, 354	⊢
	: , : , :
345	instantiation	401, 369, 355	⊢
	: , : , :
346	instantiation	401, 365, 356	⊢
	: , : , :
347	conjecture		⊢
	proveit.physics.quantum.QPE._phase_is_real
348	instantiation	401, 389, 357	⊢
	: , : , :
349	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
350	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
351	conjecture		⊢
	proveit.numbers.exponentiation.neg_power_as_div
352	instantiation	401, 358, 359	⊢
	: , : , :
353	instantiation	360, 361	⊢
	:
354	instantiation	362, 363, 400	⊢
	: , : , :
355	instantiation	401, 380, 364	⊢
	: , : , :
356	assumption		⊢
357	instantiation	401, 365, 366	⊢
	: , : , :
358	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
359	instantiation	401, 367, 368	⊢
	: , : , :
360	conjecture		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
361	instantiation	401, 369, 370	⊢
	: , : , :
362	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
363	instantiation	371, 372	⊢
	: , :
364	instantiation	401, 373, 374	⊢
	: , : , :
365	instantiation	375, 376, 377	⊢
	: , :
366	assumption		⊢
367	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
368	instantiation	401, 378, 379	⊢
	: , : , :
369	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
370	instantiation	401, 380, 381	⊢
	: , : , :
371	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
372	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
373	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
374	instantiation	382, 383, 384	⊢
	: , :
375	conjecture		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
376	conjecture		⊢
	proveit.numbers.number_sets.integers.zero_is_int
377	instantiation	385, 386, 387	⊢
	: , :
378	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
379	instantiation	401, 388, 392	⊢
	: , : , :
380	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
381	instantiation	401, 389, 394	⊢
	: , : , :
382	conjecture		⊢
	proveit.numbers.division.div_rational_pos_closure
383	instantiation	401, 391, 390	⊢
	: , : , :
384	instantiation	401, 391, 392	⊢
	: , : , :
385	conjecture		⊢
	proveit.numbers.addition.add_int_closure_bin
386	instantiation	393, 394, 395	⊢
	: , :
387	instantiation	396, 397	⊢
	:
388	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
389	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
390	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
391	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
392	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
393	conjecture		⊢
	proveit.numbers.exponentiation.exp_int_closure
394	instantiation	401, 402, 398	⊢
	: , : , :
395	instantiation	401, 399, 400	⊢
	: , : , :
396	conjecture		⊢
	proveit.numbers.negation.int_closure
397	instantiation	401, 402, 403	⊢
	: , : , :
398	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
399	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
400	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
401	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
402	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
403	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements