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
0deduction1  ⊢  
1instantiation2, 3, 4,  ⊢  
  : , :
2theorem  ⊢  
 proveit.numbers.multiplication.commutation
3instantiation6, 7, 5  ⊢  
  : , :
4instantiation6, 7, 8,  ⊢  
  : , :
5instantiation39, 9, 10  ⊢  
  : , : , :
6theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
7instantiation91, 63, 11  ⊢  
  : , : , :
8instantiation12, 13,  ⊢  
  :
9instantiation56, 42, 14  ⊢  
  : , :
10instantiation33, 15, 16  ⊢  
  : , : , :
11instantiation91, 67, 17  ⊢  
  : , : , :
12theorem  ⊢  
 proveit.numbers.negation.complex_closure
13instantiation18, 19, 20, 21,  ⊢  
  : , :
14instantiation39, 22, 23  ⊢  
  : , : , :
15instantiation48, 93, 43, 49, 24, 50, 42, 57, 38, 58  ⊢  
  : , : , : , : , : , :
16instantiation48, 49, 88, 43, 50, 44, 24, 53, 54, 57, 38, 58  ⊢  
  : , : , : , : , : , :
17theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
18theorem  ⊢  
 proveit.numbers.division.div_complex_closure
19instantiation39, 25, 26,  ⊢  
  : , : , :
20instantiation91, 63, 27  ⊢  
  : , : , :
21instantiation28, 29  ⊢  
  :
22instantiation56, 30, 58  ⊢  
  : , :
23instantiation48, 49, 88, 93, 50, 31, 57, 38, 58  ⊢  
  : , : , : , : , : , :
24instantiation55  ⊢  
  : , : , :
25instantiation56, 42, 32,  ⊢  
  : , :
26instantiation33, 34, 35,  ⊢  
  : , : , :
27instantiation91, 69, 36  ⊢  
  : , : , :
28theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
29instantiation37, 88, 85  ⊢  
  : , :
30instantiation56, 57, 38  ⊢  
  : , :
31instantiation59  ⊢  
  : , :
32instantiation39, 40, 41,  ⊢  
  : , : , :
33axiom  ⊢  
 proveit.logic.equality.equals_transitivity
34instantiation48, 93, 43, 49, 45, 50, 42, 57, 58, 52,  ⊢  
  : , : , : , : , : , :
35instantiation48, 49, 88, 43, 50, 44, 45, 53, 54, 57, 58, 52,  ⊢  
  : , : , : , : , : , :
36instantiation91, 72, 81  ⊢  
  : , : , :
37theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
38instantiation91, 63, 46  ⊢  
  : , : , :
39theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
40instantiation56, 47, 52,  ⊢  
  : , :
41instantiation48, 49, 88, 93, 50, 51, 57, 58, 52,  ⊢  
  : , : , : , : , : , :
42instantiation56, 53, 54  ⊢  
  : , :
43theorem  ⊢  
 proveit.numbers.numerals.decimals.nat3
44instantiation59  ⊢  
  : , :
45instantiation55  ⊢  
  : , : , :
46theorem  ⊢  
 proveit.physics.quantum.QPE._phase_is_real
47instantiation56, 57, 58  ⊢  
  : , :
48theorem  ⊢  
 proveit.numbers.multiplication.disassociation
49axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
50theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
51instantiation59  ⊢  
  : , :
52instantiation91, 63, 60  ⊢  
  : , : , :
53instantiation91, 63, 61  ⊢  
  : , : , :
54instantiation91, 63, 62  ⊢  
  : , : , :
55theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
56theorem  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
57theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
58instantiation91, 63, 64  ⊢  
  : , : , :
59theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
60instantiation91, 69, 65  ⊢  
  : , : , :
61instantiation91, 69, 66  ⊢  
  : , : , :
62instantiation91, 67, 68  ⊢  
  : , : , :
63theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
64instantiation91, 69, 70  ⊢  
  : , : , :
65instantiation91, 72, 71  ⊢  
  : , : , :
66instantiation91, 72, 84  ⊢  
  : , : , :
67theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
68theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
69theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
70instantiation91, 72, 73  ⊢  
  : , : , :
71instantiation91, 75, 74  ⊢  
  : , : , :
72theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
73instantiation91, 75, 76  ⊢  
  : , : , :
74assumption  ⊢  
75instantiation77, 78, 79  ⊢  
  : , :
76assumption  ⊢  
77theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
78theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
79instantiation80, 81, 82  ⊢  
  : , :
80theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
81instantiation83, 84, 85  ⊢  
  : , :
82instantiation86, 87  ⊢  
  :
83theorem  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
84instantiation91, 92, 88  ⊢  
  : , : , :
85instantiation91, 89, 90  ⊢  
  : , : , :
86theorem  ⊢  
 proveit.numbers.negation.int_closure
87instantiation91, 92, 93  ⊢  
  : , : , :
88theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
89theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
90axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
91theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
92theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
93theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1