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