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  ⊢  
  : , : , :
1theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
2instantiation4, 20, 21, 5, 6  ⊢  
  : , : , : , :
3instantiation7, 8, 9  ⊢  
  : , : , :
4theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_ket_is_ket
5instantiation19, 20, 21, 10  ⊢  
  : , : , :
6modus ponens11, 12  ⊢  
7axiom  ⊢  
 proveit.physics.quantum.algebra.multi_qmult_def
8theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
9instantiation71  ⊢  
  : , :
10instantiation13, 20, 21, 14, 15  ⊢  
  : , : , : , : , :
11instantiation16, 17, 26  ⊢  
  : , : , : , : , : , :
12generalization18  ⊢  
13theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_op_is_op
14instantiation19, 20, 21, 22  ⊢  
  : , : , :
15instantiation23, 41, 24  ⊢  
  : , : , :
16theorem  ⊢  
 proveit.linear_algebra.addition.summation_closure
17theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
18instantiation25, 26, 27, 28  ⊢  
  : , : , : , :
19theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_is_linmap
20instantiation29, 41  ⊢  
  :
21theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
22instantiation30, 99, 31  ⊢  
  : , :
23theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_matrix_is_linmap
24instantiation32, 33, 34  ⊢  
  : , : , :
25theorem  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
26instantiation35, 41  ⊢  
  :
27instantiation36, 37, 38  ⊢  
  : , :
28instantiation39, 99, 85  ⊢  
  : , :
29theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
30theorem  ⊢  
 proveit.physics.quantum.algebra.num_bra_is_lin_map
31assumption  ⊢  
32theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
33instantiation40, 41  ⊢  
  :
34instantiation42, 99  ⊢  
  :
35theorem  ⊢  
 proveit.linear_algebra.complex_vec_set_is_vec_space
36theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
37instantiation100, 75, 43  ⊢  
  : , : , :
38instantiation52, 44, 45  ⊢  
  : , : , :
39theorem  ⊢  
 proveit.physics.quantum.algebra.num_ket_in_register_space
40theorem  ⊢  
 proveit.linear_algebra.matrices.unitaries_are_matrices
41instantiation46, 97, 94  ⊢  
  : , :
42theorem  ⊢  
 proveit.physics.quantum.QFT.invFT_is_unitary
43instantiation100, 80, 47  ⊢  
  : , : , :
44instantiation68, 55, 48  ⊢  
  : , :
45instantiation49, 50, 51  ⊢  
  : , : , :
46theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
47theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
48instantiation52, 53, 54  ⊢  
  : , : , :
49axiom  ⊢  
 proveit.logic.equality.equals_transitivity
50instantiation60, 102, 56, 61, 58, 62, 55, 69, 70, 64  ⊢  
  : , : , : , : , : , :
51instantiation60, 61, 97, 56, 62, 57, 58, 65, 66, 69, 70, 64  ⊢  
  : , : , : , : , : , :
52theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
53instantiation68, 59, 64  ⊢  
  : , :
54instantiation60, 61, 97, 102, 62, 63, 69, 70, 64  ⊢  
  : , : , : , : , : , :
55instantiation68, 65, 66  ⊢  
  : , :
56theorem  ⊢  
 proveit.numbers.numerals.decimals.nat3
57instantiation71  ⊢  
  : , :
58instantiation67  ⊢  
  : , : , :
59instantiation68, 69, 70  ⊢  
  : , :
60theorem  ⊢  
 proveit.numbers.multiplication.disassociation
61axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
62theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
63instantiation71  ⊢  
  : , :
64instantiation100, 75, 72  ⊢  
  : , : , :
65instantiation100, 75, 73  ⊢  
  : , : , :
66instantiation100, 75, 74  ⊢  
  : , : , :
67theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
68theorem  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
69theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
70instantiation100, 75, 76  ⊢  
  : , : , :
71theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
72instantiation100, 78, 77  ⊢  
  : , : , :
73instantiation100, 78, 79  ⊢  
  : , : , :
74instantiation100, 80, 81  ⊢  
  : , : , :
75theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
76theorem  ⊢  
 proveit.physics.quantum.QPE._phase_is_real
77instantiation100, 83, 82  ⊢  
  : , : , :
78theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
79instantiation100, 83, 93  ⊢  
  : , : , :
80theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
81theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
82instantiation100, 84, 85  ⊢  
  : , : , :
83theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
84instantiation86, 87, 88  ⊢  
  : , :
85assumption  ⊢  
86theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
87theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
88instantiation89, 90, 91  ⊢  
  : , :
89theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
90instantiation92, 93, 94  ⊢  
  : , :
91instantiation95, 96  ⊢  
  :
92theorem  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
93instantiation100, 101, 97  ⊢  
  : , : , :
94instantiation100, 98, 99  ⊢  
  : , : , :
95theorem  ⊢  
 proveit.numbers.negation.int_closure
96instantiation100, 101, 102  ⊢  
  : , : , :
97theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
98theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
99axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
100theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
101theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
102theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1