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, 4, 5  ⊢  
  : , : , : , :
1theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_ket_in_QmultCodomain
2reference16  ⊢  
3reference17  ⊢  
4instantiation15, 16, 17, 6  ⊢  
  : , : , :
5modus ponens7, 8  ⊢  
6instantiation9, 16, 17, 10, 11  ⊢  
  : , : , : , : , :
7instantiation12, 13, 22  ⊢  
  : , : , : , : , : , :
8generalization14  ⊢  
9theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_op_is_op
10instantiation15, 16, 17, 18  ⊢  
  : , : , :
11instantiation19, 37, 20  ⊢  
  : , : , :
12theorem  ⊢  
 proveit.linear_algebra.addition.summation_closure
13theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
14instantiation21, 22, 23, 24  ⊢  
  : , : , : , :
15theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_is_linmap
16instantiation25, 37  ⊢  
  :
17theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
18instantiation26, 95, 27  ⊢  
  : , :
19theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_matrix_is_linmap
20instantiation28, 29, 30  ⊢  
  : , : , :
21theorem  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
22instantiation31, 37  ⊢  
  :
23instantiation32, 33, 34  ⊢  
  : , :
24instantiation35, 95, 81  ⊢  
  : , :
25theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
26theorem  ⊢  
 proveit.physics.quantum.algebra.num_bra_is_lin_map
27assumption  ⊢  
28theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
29instantiation36, 37  ⊢  
  :
30instantiation38, 95  ⊢  
  :
31theorem  ⊢  
 proveit.linear_algebra.complex_vec_set_is_vec_space
32theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
33instantiation96, 71, 39  ⊢  
  : , : , :
34instantiation48, 40, 41  ⊢  
  : , : , :
35theorem  ⊢  
 proveit.physics.quantum.algebra.num_ket_in_register_space
36theorem  ⊢  
 proveit.linear_algebra.matrices.unitaries_are_matrices
37instantiation42, 93, 90  ⊢  
  : , :
38theorem  ⊢  
 proveit.physics.quantum.QFT.invFT_is_unitary
39instantiation96, 76, 43  ⊢  
  : , : , :
40instantiation64, 51, 44  ⊢  
  : , :
41instantiation45, 46, 47  ⊢  
  : , : , :
42theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
43theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
44instantiation48, 49, 50  ⊢  
  : , : , :
45axiom  ⊢  
 proveit.logic.equality.equals_transitivity
46instantiation56, 98, 52, 57, 54, 58, 51, 65, 66, 60  ⊢  
  : , : , : , : , : , :
47instantiation56, 57, 93, 52, 58, 53, 54, 61, 62, 65, 66, 60  ⊢  
  : , : , : , : , : , :
48theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
49instantiation64, 55, 60  ⊢  
  : , :
50instantiation56, 57, 93, 98, 58, 59, 65, 66, 60  ⊢  
  : , : , : , : , : , :
51instantiation64, 61, 62  ⊢  
  : , :
52theorem  ⊢  
 proveit.numbers.numerals.decimals.nat3
53instantiation67  ⊢  
  : , :
54instantiation63  ⊢  
  : , : , :
55instantiation64, 65, 66  ⊢  
  : , :
56theorem  ⊢  
 proveit.numbers.multiplication.disassociation
57axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
58theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
59instantiation67  ⊢  
  : , :
60instantiation96, 71, 68  ⊢  
  : , : , :
61instantiation96, 71, 69  ⊢  
  : , : , :
62instantiation96, 71, 70  ⊢  
  : , : , :
63theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
64theorem  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
65theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
66instantiation96, 71, 72  ⊢  
  : , : , :
67theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
68instantiation96, 74, 73  ⊢  
  : , : , :
69instantiation96, 74, 75  ⊢  
  : , : , :
70instantiation96, 76, 77  ⊢  
  : , : , :
71theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
72theorem  ⊢  
 proveit.physics.quantum.QPE._phase_is_real
73instantiation96, 79, 78  ⊢  
  : , : , :
74theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
75instantiation96, 79, 89  ⊢  
  : , : , :
76theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
77theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
78instantiation96, 80, 81  ⊢  
  : , : , :
79theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
80instantiation82, 83, 84  ⊢  
  : , :
81assumption  ⊢  
82theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
83theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
84instantiation85, 86, 87  ⊢  
  : , :
85theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
86instantiation88, 89, 90  ⊢  
  : , :
87instantiation91, 92  ⊢  
  :
88theorem  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
89instantiation96, 97, 93  ⊢  
  : , : , :
90instantiation96, 94, 95  ⊢  
  : , : , :
91theorem  ⊢  
 proveit.numbers.negation.int_closure
92instantiation96, 97, 98  ⊢  
  : , : , :
93theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
94theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
95axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
96theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
97theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
98theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1