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_complex_closure
2instantiation24, 6, 7, 8  ⊢  
  : , :
3reference10  ⊢  
4reference11  ⊢  
5instantiation9, 10, 11, 12  ⊢  
  : , : , :
6instantiation83, 64, 13  ⊢  
  : , : , :
7instantiation14, 57, 15  ⊢  
  : , :
8instantiation16, 17, 18  ⊢  
  : , : , :
9theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_is_linmap
10instantiation19, 20  ⊢  
  :
11theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
12instantiation21, 60, 22  ⊢  
  : , :
13instantiation83, 72, 23  ⊢  
  : , : , :
14theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
15instantiation24, 47, 57, 34  ⊢  
  : , :
16theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
17instantiation25, 63, 26  ⊢  
  : , :
18instantiation44, 27  ⊢  
  : , : , :
19theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
20instantiation28, 85, 29  ⊢  
  : , :
21theorem  ⊢  
 proveit.physics.quantum.algebra.num_bra_is_lin_map
22assumption  ⊢  
23instantiation83, 78, 30  ⊢  
  : , : , :
24theorem  ⊢  
 proveit.numbers.division.div_complex_closure
25theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
26instantiation83, 31, 32  ⊢  
  : , : , :
27instantiation33, 47, 57, 34, 35*  ⊢  
  : , :
28theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
29instantiation83, 36, 60  ⊢  
  : , : , :
30instantiation83, 84, 37  ⊢  
  : , : , :
31theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
32instantiation38, 69, 39  ⊢  
  : , :
33theorem  ⊢  
 proveit.numbers.division.div_as_mult
34instantiation40, 82  ⊢  
  :
35instantiation41, 42, 43  ⊢  
  : , : , :
36theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
37theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
38theorem  ⊢  
 proveit.numbers.multiplication.mult_rational_pos_closure_bin
39instantiation83, 81, 60  ⊢  
  : , : , :
40theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
41axiom  ⊢  
 proveit.logic.equality.equals_transitivity
42instantiation44, 45  ⊢  
  : , : , :
43instantiation46, 47, 48  ⊢  
  : , :
44axiom  ⊢  
 proveit.logic.equality.substitution
45instantiation49, 50, 80, 51*  ⊢  
  : , :
46theorem  ⊢  
 proveit.numbers.multiplication.commutation
47instantiation83, 64, 52  ⊢  
  : , : , :
48instantiation83, 64, 53  ⊢  
  : , : , :
49theorem  ⊢  
 proveit.numbers.exponentiation.neg_power_as_div
50instantiation83, 54, 55  ⊢  
  : , : , :
51instantiation56, 57  ⊢  
  :
52instantiation58, 59, 60  ⊢  
  : , : , :
53instantiation83, 72, 61  ⊢  
  : , : , :
54theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
55instantiation83, 62, 63  ⊢  
  : , : , :
56theorem  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
57instantiation83, 64, 65  ⊢  
  : , : , :
58theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
59instantiation66, 67  ⊢  
  : , :
60axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
61instantiation83, 68, 69  ⊢  
  : , : , :
62theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
63instantiation83, 70, 71  ⊢  
  : , : , :
64theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
65instantiation83, 72, 73  ⊢  
  : , : , :
66theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
67theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
68theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
69instantiation74, 75, 76  ⊢  
  : , :
70theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
71instantiation83, 77, 82  ⊢  
  : , : , :
72theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
73instantiation83, 78, 79  ⊢  
  : , : , :
74theorem  ⊢  
 proveit.numbers.division.div_rational_pos_closure
75instantiation83, 81, 80  ⊢  
  : , : , :
76instantiation83, 81, 82  ⊢  
  : , : , :
77theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
78theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
79instantiation83, 84, 85  ⊢  
  : , : , :
80theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
81theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
82theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
83theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
84theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
85theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements