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  ⊢  
  : , : , :
1axiom  ⊢  
 proveit.core_expr_types.conditionals.conditional_substitution
2deduction3  ⊢  
3instantiation82, 148, 143, 83, 4, 84, 5, 6, 7,  ⊢  
  : , : , : , : , : , :
4instantiation99  ⊢  
  : , :
5instantiation17, 12, 8  ⊢  
  : , :
6instantiation33, 9, 10, 11  ⊢  
  : , :
7instantiation17, 12, 13,  ⊢  
  : , :
8instantiation68, 14, 15  ⊢  
  : , : , :
9instantiation146, 109, 16  ⊢  
  : , : , :
10instantiation17, 92, 18  ⊢  
  : , :
11instantiation19, 20, 21  ⊢  
  : , : , :
12instantiation146, 109, 22  ⊢  
  : , : , :
13instantiation23, 24,  ⊢  
  :
14instantiation96, 71, 25  ⊢  
  : , :
15instantiation57, 26, 27  ⊢  
  : , : , :
16instantiation146, 120, 28  ⊢  
  : , : , :
17theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
18instantiation33, 66, 92, 43  ⊢  
  : , :
19theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
20instantiation29, 103, 30  ⊢  
  : , :
21instantiation63, 31  ⊢  
  : , : , :
22instantiation146, 112, 32  ⊢  
  : , : , :
23theorem  ⊢  
 proveit.numbers.negation.complex_closure
24instantiation33, 34, 35, 36,  ⊢  
  : , :
25instantiation68, 37, 38  ⊢  
  : , : , :
26instantiation82, 148, 72, 83, 39, 84, 71, 97, 62, 98  ⊢  
  : , : , : , : , : , :
27instantiation82, 83, 143, 72, 84, 73, 39, 92, 87, 97, 62, 98  ⊢  
  : , : , : , : , : , :
28instantiation146, 127, 142  ⊢  
  : , : , :
29theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
30instantiation146, 40, 41  ⊢  
  : , : , :
31instantiation42, 66, 92, 43, 44*  ⊢  
  : , :
32theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
33theorem  ⊢  
 proveit.numbers.division.div_complex_closure
34instantiation68, 45, 46,  ⊢  
  : , : , :
35instantiation146, 109, 47  ⊢  
  : , : , :
36instantiation53, 48  ⊢  
  :
37instantiation96, 49, 98  ⊢  
  : , :
38instantiation82, 83, 143, 148, 84, 50, 97, 62, 98  ⊢  
  : , : , : , : , : , :
39instantiation88  ⊢  
  : , : , :
40theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
41instantiation51, 108, 52  ⊢  
  : , :
42theorem  ⊢  
 proveit.numbers.division.div_as_mult
43instantiation53, 126  ⊢  
  :
44instantiation57, 54, 55  ⊢  
  : , : , :
45instantiation96, 71, 56,  ⊢  
  : , :
46instantiation57, 58, 59,  ⊢  
  : , : , :
47instantiation146, 120, 60  ⊢  
  : , : , :
48instantiation61, 143, 140  ⊢  
  : , :
49instantiation96, 97, 62  ⊢  
  : , :
50instantiation99  ⊢  
  : , :
51theorem  ⊢  
 proveit.numbers.multiplication.mult_rational_pos_closure_bin
52instantiation146, 125, 145  ⊢  
  : , : , :
53theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
54instantiation63, 64  ⊢  
  : , : , :
55instantiation65, 66, 67  ⊢  
  : , :
56instantiation68, 69, 70,  ⊢  
  : , : , :
57axiom  ⊢  
 proveit.logic.equality.equals_transitivity
58instantiation82, 148, 72, 83, 74, 84, 71, 97, 98, 86,  ⊢  
  : , : , : , : , : , :
59instantiation82, 83, 143, 72, 84, 73, 74, 92, 87, 97, 98, 86,  ⊢  
  : , : , : , : , : , :
60instantiation146, 127, 136  ⊢  
  : , : , :
61theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
62instantiation146, 109, 75  ⊢  
  : , : , :
63axiom  ⊢  
 proveit.logic.equality.substitution
64instantiation76, 77, 124, 78*  ⊢  
  : , :
65theorem  ⊢  
 proveit.numbers.multiplication.commutation
66instantiation146, 109, 79  ⊢  
  : , : , :
67instantiation146, 109, 80  ⊢  
  : , : , :
68theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
69instantiation96, 81, 86,  ⊢  
  : , :
70instantiation82, 83, 143, 148, 84, 85, 97, 98, 86,  ⊢  
  : , : , : , : , : , :
71instantiation96, 92, 87  ⊢  
  : , :
72theorem  ⊢  
 proveit.numbers.numerals.decimals.nat3
73instantiation99  ⊢  
  : , :
74instantiation88  ⊢  
  : , : , :
75theorem  ⊢  
 proveit.physics.quantum.QPE._phase_is_real
76theorem  ⊢  
 proveit.numbers.exponentiation.neg_power_as_div
77instantiation146, 89, 90  ⊢  
  : , : , :
78instantiation91, 92  ⊢  
  :
79instantiation93, 94, 145  ⊢  
  : , : , :
80instantiation146, 120, 95  ⊢  
  : , : , :
81instantiation96, 97, 98  ⊢  
  : , :
82theorem  ⊢  
 proveit.numbers.multiplication.disassociation
83axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
84theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
85instantiation99  ⊢  
  : , :
86instantiation146, 109, 100  ⊢  
  : , : , :
87instantiation146, 109, 101  ⊢  
  : , : , :
88theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
89theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
90instantiation146, 102, 103  ⊢  
  : , : , :
91theorem  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
92instantiation146, 109, 104  ⊢  
  : , : , :
93theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
94instantiation105, 106  ⊢  
  : , :
95instantiation146, 107, 108  ⊢  
  : , : , :
96theorem  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
97theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
98instantiation146, 109, 110  ⊢  
  : , : , :
99theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
100instantiation146, 120, 111  ⊢  
  : , : , :
101instantiation146, 112, 113  ⊢  
  : , : , :
102theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
103instantiation146, 114, 115  ⊢  
  : , : , :
104instantiation146, 120, 116  ⊢  
  : , : , :
105theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
106theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
107theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
108instantiation117, 118, 119  ⊢  
  : , :
109theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
110instantiation146, 120, 121  ⊢  
  : , : , :
111instantiation146, 127, 122  ⊢  
  : , : , :
112theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
113theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
114theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
115instantiation146, 123, 126  ⊢  
  : , : , :
116instantiation146, 127, 139  ⊢  
  : , : , :
117theorem  ⊢  
 proveit.numbers.division.div_rational_pos_closure
118instantiation146, 125, 124  ⊢  
  : , : , :
119instantiation146, 125, 126  ⊢  
  : , : , :
120theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
121instantiation146, 127, 128  ⊢  
  : , : , :
122instantiation146, 130, 129  ⊢  
  : , : , :
123theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
124theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
125theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
126theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
127theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
128instantiation146, 130, 131  ⊢  
  : , : , :
129assumption  ⊢  
130instantiation132, 133, 134  ⊢  
  : , :
131assumption  ⊢  
132theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
133theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
134instantiation135, 136, 137  ⊢  
  : , :
135theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
136instantiation138, 139, 140  ⊢  
  : , :
137instantiation141, 142  ⊢  
  :
138theorem  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
139instantiation146, 147, 143  ⊢  
  : , : , :
140instantiation146, 144, 145  ⊢  
  : , : , :
141theorem  ⊢  
 proveit.numbers.negation.int_closure
142instantiation146, 147, 148  ⊢  
  : , : , :
143theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
144theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
145axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
146theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
147theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
148theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
*equality replacement requirements