logo

Show the Proof

In [1]:
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
Out[1]:
 step typerequirementsstatement
0instantiation1, 2, 3  ⊢  
  : , : , :
1reference118  ⊢  
2instantiation118, 4, 5  ⊢  
  : , : , :
3instantiation6, 26, 55, 7, 24, 8*  ⊢  
  : , : , :
4instantiation118, 9, 10  ⊢  
  : , : , :
5instantiation11, 187, 182, 55, 23, 24  ⊢  
  : , : , : , : , :
6theorem  ⊢  
 proveit.physics.quantum.algebra.scalar_mult_factorization
7instantiation114  ⊢  
  : , : , :
8instantiation12, 55, 13  ⊢  
  : , :
9instantiation14, 55, 187, 109, 110, 15  ⊢  
  : , : , : , : , : , :
10instantiation22, 182, 176, 109, 42, 23, 110, 16  ⊢  
  : , : , : , : , : , :
11theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_pulling_scalar_out_front
12axiom  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult
13instantiation78, 17, 29  ⊢  
  : , : , :
14theorem  ⊢  
 proveit.physics.quantum.algebra.scalar_mult_absorption
15instantiation78, 24, 18  ⊢  
  : , : , :
16instantiation78, 19, 20  ⊢  
  : , : , :
17instantiation21, 67, 68, 32, 33  ⊢  
  : , : , : , :
18instantiation22, 187, 176, 109, 23, 110, 24  ⊢  
  : , : , : , : , : , :
19instantiation31, 67, 68, 25, 33  ⊢  
  : , : , : , :
20instantiation41, 26, 27  ⊢  
  : , : , :
21theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_ket_is_ket
22theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_disassociation
23instantiation124  ⊢  
  : , :
24instantiation78, 28, 29  ⊢  
  : , : , :
25instantiation66, 67, 68, 30  ⊢  
  : , : , :
26theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat3
27instantiation114  ⊢  
  : , : , :
28instantiation31, 67, 68, 32, 33  ⊢  
  : , : , : , :
29instantiation41, 176, 34  ⊢  
  : , : , :
30instantiation78, 35, 36  ⊢  
  : , : , :
31theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_ket_in_QmultCodomain
32instantiation66, 67, 68, 37  ⊢  
  : , : , :
33modus ponens38, 39  ⊢  
34instantiation124  ⊢  
  : , :
35instantiation43, 67, 68, 40, 44  ⊢  
  : , : , : , : , :
36instantiation41, 176, 42  ⊢  
  : , : , :
37instantiation43, 67, 68, 56, 44  ⊢  
  : , : , : , : , :
38instantiation45, 174, 51  ⊢  
  : , : , : , : , : , :
39generalization46  ⊢  
40instantiation66, 67, 68, 47  ⊢  
  : , : , :
41axiom  ⊢  
 proveit.physics.quantum.algebra.multi_qmult_def
42instantiation124  ⊢  
  : , :
43theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_op_is_op
44instantiation48, 82, 49  ⊢  
  : , : , :
45theorem  ⊢  
 proveit.linear_algebra.addition.summation_closure
46instantiation50, 51, 52, 53  ⊢  
  : , : , : , :
47instantiation54, 55, 67, 68, 56  ⊢  
  : , : , : , :
48theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_matrix_is_linmap
49instantiation146, 57, 58  ⊢  
  : , : , :
50theorem  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
51instantiation59, 82  ⊢  
  :
52instantiation76, 60, 61  ⊢  
  : , :
53instantiation62, 184, 150  ⊢  
  : , :
54theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_complex_closure
55instantiation90, 63, 64, 65  ⊢  
  : , :
56instantiation66, 67, 68, 69  ⊢  
  : , : , :
57instantiation70, 82  ⊢  
  :
58instantiation71, 184  ⊢  
  :
59theorem  ⊢  
 proveit.linear_algebra.complex_vec_set_is_vec_space
60instantiation185, 153, 72  ⊢  
  : , : , :
61instantiation95, 73, 74  ⊢  
  : , : , :
62theorem  ⊢  
 proveit.physics.quantum.algebra.num_ket_in_register_space
63instantiation185, 153, 75  ⊢  
  : , : , :
64instantiation76, 145, 77  ⊢  
  : , :
65instantiation78, 79, 80  ⊢  
  : , : , :
66theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_is_linmap
67instantiation81, 82  ⊢  
  :
68theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
69instantiation83, 184, 84  ⊢  
  : , :
70theorem  ⊢  
 proveit.linear_algebra.matrices.unitaries_are_matrices
71theorem  ⊢  
 proveit.physics.quantum.QFT.invFT_is_unitary
72instantiation185, 134, 85  ⊢  
  : , : , :
73instantiation121, 98, 86  ⊢  
  : , :
74instantiation118, 87, 88  ⊢  
  : , : , :
75instantiation185, 164, 89  ⊢  
  : , : , :
76theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
77instantiation90, 130, 145, 105  ⊢  
  : , :
78theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
79instantiation91, 152, 92  ⊢  
  : , :
80instantiation127, 93  ⊢  
  : , : , :
81theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
82instantiation94, 182, 179  ⊢  
  : , :
83theorem  ⊢  
 proveit.physics.quantum.algebra.num_bra_is_lin_map
84assumption  ⊢  
85theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
86instantiation95, 96, 97  ⊢  
  : , : , :
87instantiation108, 187, 99, 109, 101, 110, 98, 122, 123, 112  ⊢  
  : , : , : , : , : , :
88instantiation108, 109, 182, 99, 110, 100, 101, 145, 113, 122, 123, 112  ⊢  
  : , : , : , : , : , :
89instantiation185, 173, 181  ⊢  
  : , : , :
90theorem  ⊢  
 proveit.numbers.division.div_complex_closure
91theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
92instantiation185, 102, 103  ⊢  
  : , : , :
93instantiation104, 130, 145, 105, 106*  ⊢  
  : , :
94theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
95theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
96instantiation121, 107, 112  ⊢  
  : , :
97instantiation108, 109, 182, 187, 110, 111, 122, 123, 112  ⊢  
  : , : , : , : , : , :
98instantiation121, 145, 113  ⊢  
  : , :
99theorem  ⊢  
 proveit.numbers.numerals.decimals.nat3
100instantiation124  ⊢  
  : , :
101instantiation114  ⊢  
  : , : , :
102theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
103instantiation115, 158, 116  ⊢  
  : , :
104theorem  ⊢  
 proveit.numbers.division.div_as_mult
105instantiation117, 176  ⊢  
  :
106instantiation118, 119, 120  ⊢  
  : , : , :
107instantiation121, 122, 123  ⊢  
  : , :
108theorem  ⊢  
 proveit.numbers.multiplication.disassociation
109axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
110theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
111instantiation124  ⊢  
  : , :
112instantiation185, 153, 125  ⊢  
  : , : , :
113instantiation185, 153, 126  ⊢  
  : , : , :
114theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
115theorem  ⊢  
 proveit.numbers.multiplication.mult_rational_pos_closure_bin
116instantiation185, 175, 184  ⊢  
  : , : , :
117theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
118axiom  ⊢  
 proveit.logic.equality.equals_transitivity
119instantiation127, 128  ⊢  
  : , : , :
120instantiation129, 130, 131  ⊢  
  : , :
121theorem  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
122theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
123instantiation185, 153, 132  ⊢  
  : , : , :
124theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
125instantiation185, 164, 133  ⊢  
  : , : , :
126instantiation185, 134, 135  ⊢  
  : , : , :
127axiom  ⊢  
 proveit.logic.equality.substitution
128instantiation136, 137, 174, 138*  ⊢  
  : , :
129theorem  ⊢  
 proveit.numbers.multiplication.commutation
130instantiation185, 153, 139  ⊢  
  : , : , :
131instantiation185, 153, 140  ⊢  
  : , : , :
132theorem  ⊢  
 proveit.physics.quantum.QPE._phase_is_real
133instantiation185, 173, 141  ⊢  
  : , : , :
134theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
135theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
136theorem  ⊢  
 proveit.numbers.exponentiation.neg_power_as_div
137instantiation185, 142, 143  ⊢  
  : , : , :
138instantiation144, 145  ⊢  
  :
139instantiation146, 147, 184  ⊢  
  : , : , :
140instantiation185, 164, 148  ⊢  
  : , : , :
141instantiation185, 149, 150  ⊢  
  : , : , :
142theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
143instantiation185, 151, 152  ⊢  
  : , : , :
144theorem  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
145instantiation185, 153, 154  ⊢  
  : , : , :
146theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
147instantiation155, 156  ⊢  
  : , :
148instantiation185, 157, 158  ⊢  
  : , : , :
149instantiation159, 160, 161  ⊢  
  : , :
150assumption  ⊢  
151theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
152instantiation185, 162, 163  ⊢  
  : , : , :
153theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
154instantiation185, 164, 165  ⊢  
  : , : , :
155theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
156theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
157theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
158instantiation166, 167, 168  ⊢  
  : , :
159theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
160theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
161instantiation169, 170, 171  ⊢  
  : , :
162theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
163instantiation185, 172, 176  ⊢  
  : , : , :
164theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
165instantiation185, 173, 178  ⊢  
  : , : , :
166theorem  ⊢  
 proveit.numbers.division.div_rational_pos_closure
167instantiation185, 175, 174  ⊢  
  : , : , :
168instantiation185, 175, 176  ⊢  
  : , : , :
169theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
170instantiation177, 178, 179  ⊢  
  : , :
171instantiation180, 181  ⊢  
  :
172theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
173theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
174theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
175theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
176theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
177theorem  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
178instantiation185, 186, 182  ⊢  
  : , : , :
179instantiation185, 183, 184  ⊢  
  : , : , :
180theorem  ⊢  
 proveit.numbers.negation.int_closure
181instantiation185, 186, 187  ⊢  
  : , : , :
182theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
183theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
184axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
185theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
186theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
187theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
*equality replacement requirements