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	106	⊢
2	instantiation	4, 43, 175, 97, 98, 5	⊢
	: , : , : , : , : , :
3	instantiation	10, 170, 164, 97, 30, 11, 98, 6	⊢
	: , : , : , : , : , :
4	theorem		⊢
	proveit.physics.quantum.algebra.scalar_mult_absorption
5	instantiation	66, 12, 7	⊢
	: , : , :
6	instantiation	66, 8, 9	⊢
	: , : , :
7	instantiation	10, 175, 164, 97, 11, 98, 12	⊢
	: , : , : , : , : , :
8	instantiation	19, 55, 56, 13, 21	⊢
	: , : , : , :
9	instantiation	29, 14, 15	⊢
	: , : , :
10	theorem		⊢
	proveit.physics.quantum.algebra.qmult_disassociation
11	instantiation	112	⊢
	: , :
12	instantiation	66, 16, 17	⊢
	: , : , :
13	instantiation	54, 55, 56, 18	⊢
	: , : , :
14	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
15	instantiation	102	⊢
	: , : , :
16	instantiation	19, 55, 56, 20, 21	⊢
	: , : , : , :
17	instantiation	29, 164, 22	⊢
	: , : , :
18	instantiation	66, 23, 24	⊢
	: , : , :
19	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_ket_in_QmultCodomain
20	instantiation	54, 55, 56, 25	⊢
	: , : , :
21	modus ponens	26, 27	⊢
22	instantiation	112	⊢
	: , :
23	instantiation	31, 55, 56, 28, 32	⊢
	: , : , : , : , :
24	instantiation	29, 164, 30	⊢
	: , : , :
25	instantiation	31, 55, 56, 44, 32	⊢
	: , : , : , : , :
26	instantiation	33, 162, 39	⊢
	: , : , : , : , : , :
27	generalization	34	⊢
28	instantiation	54, 55, 56, 35	⊢
	: , : , :
29	axiom		⊢
	proveit.physics.quantum.algebra.multi_qmult_def
30	instantiation	112	⊢
	: , :
31	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_op_is_op
32	instantiation	36, 70, 37	⊢
	: , : , :
33	theorem		⊢
	proveit.linear_algebra.addition.summation_closure
34	instantiation	38, 39, 40, 41	⊢
	: , : , : , :
35	instantiation	42, 43, 55, 56, 44	⊢
	: , : , : , :
36	theorem		⊢
	proveit.physics.quantum.algebra.qmult_matrix_is_linmap
37	instantiation	134, 45, 46	⊢
	: , : , :
38	theorem		⊢
	proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
39	instantiation	47, 70	⊢
	:
40	instantiation	64, 48, 49	⊢
	: , :
41	instantiation	50, 172, 138	⊢
	: , :
42	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_complex_closure
43	instantiation	78, 51, 52, 53	⊢
	: , :
44	instantiation	54, 55, 56, 57	⊢
	: , : , :
45	instantiation	58, 70	⊢
	:
46	instantiation	59, 172	⊢
	:
47	theorem		⊢
	proveit.linear_algebra.complex_vec_set_is_vec_space
48	instantiation	173, 141, 60	⊢
	: , : , :
49	instantiation	83, 61, 62	⊢
	: , : , :
50	theorem		⊢
	proveit.physics.quantum.algebra.num_ket_in_register_space
51	instantiation	173, 141, 63	⊢
	: , : , :
52	instantiation	64, 133, 65	⊢
	: , :
53	instantiation	66, 67, 68	⊢
	: , : , :
54	theorem		⊢
	proveit.physics.quantum.algebra.qmult_op_is_linmap
55	instantiation	69, 70	⊢
	:
56	theorem		⊢
	proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
57	instantiation	71, 172, 72	⊢
	: , :
58	theorem		⊢
	proveit.linear_algebra.matrices.unitaries_are_matrices
59	theorem		⊢
	proveit.physics.quantum.QFT.invFT_is_unitary
60	instantiation	173, 122, 73	⊢
	: , : , :
61	instantiation	109, 86, 74	⊢
	: , :
62	instantiation	106, 75, 76	⊢
	: , : , :
63	instantiation	173, 152, 77	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.exponentiation.exp_complex_closure
65	instantiation	78, 118, 133, 93	⊢
	: , :
66	theorem		⊢
	proveit.logic.equality.sub_left_side_into
67	instantiation	79, 140, 80	⊢
	: , :
68	instantiation	115, 81	⊢
	: , : , :
69	theorem		⊢
	proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
70	instantiation	82, 170, 167	⊢
	: , :
71	theorem		⊢
	proveit.physics.quantum.algebra.num_bra_is_lin_map
72	assumption		⊢
73	theorem		⊢
	proveit.numbers.number_sets.real_numbers.e_is_real_pos
74	instantiation	83, 84, 85	⊢
	: , : , :
75	instantiation	96, 175, 87, 97, 89, 98, 86, 110, 111, 100	⊢
	: , : , : , : , : , :
76	instantiation	96, 97, 170, 87, 98, 88, 89, 133, 101, 110, 111, 100	⊢
	: , : , : , : , : , :
77	instantiation	173, 161, 169	⊢
	: , : , :
78	theorem		⊢
	proveit.numbers.division.div_complex_closure
79	theorem		⊢
	proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
80	instantiation	173, 90, 91	⊢
	: , : , :
81	instantiation	92, 118, 133, 93, 94*	⊢
	: , :
82	theorem		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
83	theorem		⊢
	proveit.logic.equality.sub_right_side_into
84	instantiation	109, 95, 100	⊢
	: , :
85	instantiation	96, 97, 170, 175, 98, 99, 110, 111, 100	⊢
	: , : , : , : , : , :
86	instantiation	109, 133, 101	⊢
	: , :
87	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
88	instantiation	112	⊢
	: , :
89	instantiation	102	⊢
	: , : , :
90	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
91	instantiation	103, 146, 104	⊢
	: , :
92	theorem		⊢
	proveit.numbers.division.div_as_mult
93	instantiation	105, 164	⊢
	:
94	instantiation	106, 107, 108	⊢
	: , : , :
95	instantiation	109, 110, 111	⊢
	: , :
96	theorem		⊢
	proveit.numbers.multiplication.disassociation
97	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
98	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
99	instantiation	112	⊢
	: , :
100	instantiation	173, 141, 113	⊢
	: , : , :
101	instantiation	173, 141, 114	⊢
	: , : , :
102	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
103	theorem		⊢
	proveit.numbers.multiplication.mult_rational_pos_closure_bin
104	instantiation	173, 163, 172	⊢
	: , : , :
105	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
106	axiom		⊢
	proveit.logic.equality.equals_transitivity
107	instantiation	115, 116	⊢
	: , : , :
108	instantiation	117, 118, 119	⊢
	: , :
109	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
110	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.i_is_complex
111	instantiation	173, 141, 120	⊢
	: , : , :
112	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
113	instantiation	173, 152, 121	⊢
	: , : , :
114	instantiation	173, 122, 123	⊢
	: , : , :
115	axiom		⊢
	proveit.logic.equality.substitution
116	instantiation	124, 125, 162, 126*	⊢
	: , :
117	theorem		⊢
	proveit.numbers.multiplication.commutation
118	instantiation	173, 141, 127	⊢
	: , : , :
119	instantiation	173, 141, 128	⊢
	: , : , :
120	theorem		⊢
	proveit.physics.quantum.QPE._phase_is_real
121	instantiation	173, 161, 129	⊢
	: , : , :
122	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
123	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
124	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
125	instantiation	173, 130, 131	⊢
	: , : , :
126	instantiation	132, 133	⊢
	:
127	instantiation	134, 135, 172	⊢
	: , : , :
128	instantiation	173, 152, 136	⊢
	: , : , :
129	instantiation	173, 137, 138	⊢
	: , : , :
130	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
131	instantiation	173, 139, 140	⊢
	: , : , :
132	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
133	instantiation	173, 141, 142	⊢
	: , : , :
134	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
135	instantiation	143, 144	⊢
	: , :
136	instantiation	173, 145, 146	⊢
	: , : , :
137	instantiation	147, 148, 149	⊢
	: , :
138	assumption		⊢
139	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
140	instantiation	173, 150, 151	⊢
	: , : , :
141	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
142	instantiation	173, 152, 153	⊢
	: , : , :
143	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
144	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
145	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
146	instantiation	154, 155, 156	⊢
	: , :
147	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
148	theorem		⊢
	proveit.numbers.number_sets.integers.zero_is_int
149	instantiation	157, 158, 159	⊢
	: , :
150	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
151	instantiation	173, 160, 164	⊢
	: , : , :
152	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
153	instantiation	173, 161, 166	⊢
	: , : , :
154	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
155	instantiation	173, 163, 162	⊢
	: , : , :
156	instantiation	173, 163, 164	⊢
	: , : , :
157	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
158	instantiation	165, 166, 167	⊢
	: , :
159	instantiation	168, 169	⊢
	:
160	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
161	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
162	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
163	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
164	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
165	theorem		⊢
	proveit.numbers.exponentiation.exp_int_closure
166	instantiation	173, 174, 170	⊢
	: , : , :
167	instantiation	173, 171, 172	⊢
	: , : , :
168	theorem		⊢
	proveit.numbers.negation.int_closure
169	instantiation	173, 174, 175	⊢
	: , : , :
170	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
171	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
172	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
173	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
174	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
175	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements