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  ⊢  
  : , :
1reference15  ⊢  
2instantiation75, 3, 4, 5  ⊢  
  : , : , : , :
3instantiation58, 102, 6, 7, 8*  ⊢  
  : , :
4instantiation128, 9  ⊢  
  : , : , :
5instantiation15, 10  ⊢  
  : , :
6instantiation164, 151, 11  ⊢  
  : , : , :
7instantiation81, 12  ⊢  
  :
8instantiation115, 13, 14  ⊢  
  : , : , :
9instantiation15, 16  ⊢  
  : , :
10instantiation115, 17, 18  ⊢  
  : , : , :
11instantiation164, 157, 19  ⊢  
  : , : , :
12instantiation20, 166, 36  ⊢  
  : , :
13instantiation128, 21  ⊢  
  : , : , :
14instantiation141, 22  ⊢  
  :
15theorem  ⊢  
 proveit.logic.equality.equals_reversal
16instantiation23, 85, 142, 24*  ⊢  
  : , :
17instantiation128, 25  ⊢  
  : , : , :
18instantiation67, 142, 26, 152, 68  ⊢  
  : , : , :
19instantiation164, 162, 27  ⊢  
  : , : , :
20theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
21instantiation67, 142, 125, 106, 68, 28*  ⊢  
  : , : , :
22instantiation70, 142, 29  ⊢  
  : , :
23theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_left
24instantiation75, 30, 31, 38  ⊢  
  : , : , : , :
25instantiation115, 32, 33  ⊢  
  : , : , :
26instantiation34, 98  ⊢  
  :
27instantiation35, 163, 36  ⊢  
  : , :
28instantiation37, 112, 102, 38*  ⊢  
  : , :
29instantiation84, 112  ⊢  
  :
30instantiation94, 108, 166, 153, 110, 109, 111, 112, 142  ⊢  
  : , : , : , : , : , :
31instantiation115, 39, 40  ⊢  
  : , : , :
32instantiation128, 41  ⊢  
  : , : , :
33instantiation58, 102, 42, 43, 44*  ⊢  
  : , :
34theorem  ⊢  
 proveit.numbers.negation.real_closure
35theorem  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
36instantiation164, 45, 150  ⊢  
  : , : , :
37theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_right
38instantiation131, 112  ⊢  
  :
39instantiation46, 108, 166, 110, 47, 111, 112, 142  ⊢  
  : , : , : , : , : , : , :
40instantiation115, 48, 49  ⊢  
  : , : , :
41instantiation128, 50  ⊢  
  : , : , :
42instantiation70, 142, 85  ⊢  
  : , :
43instantiation51, 121, 52  ⊢  
  : , :
44instantiation115, 53, 54  ⊢  
  : , : , :
45theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
46theorem  ⊢  
 proveit.numbers.multiplication.rightward_commutation
47instantiation123  ⊢  
  : , :
48instantiation55, 153, 166, 108, 56, 110, 112, 142, 111  ⊢  
  : , : , : , : , : , :
49instantiation128, 57  ⊢  
  : , : , :
50instantiation58, 112, 142, 68, 59*  ⊢  
  : , :
51theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
52instantiation164, 60, 126  ⊢  
  : , : , :
53instantiation128, 61  ⊢  
  : , : , :
54instantiation141, 62  ⊢  
  :
55theorem  ⊢  
 proveit.numbers.multiplication.association
56instantiation123  ⊢  
  : , :
57instantiation72, 63, 64  ⊢  
  : , : , :
58theorem  ⊢  
 proveit.numbers.division.div_as_mult
59instantiation115, 65, 66  ⊢  
  : , : , :
60theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
61instantiation67, 142, 98, 106, 68, 69*  ⊢  
  : , : , :
62instantiation70, 142, 71  ⊢  
  : , :
63instantiation72, 73, 74  ⊢  
  : , : , :
64instantiation75, 76, 77, 78  ⊢  
  : , : , : , :
65instantiation128, 79  ⊢  
  : , : , :
66instantiation80, 112, 111  ⊢  
  : , :
67theorem  ⊢  
 proveit.numbers.exponentiation.real_power_of_real_power
68instantiation81, 161  ⊢  
  :
69instantiation115, 82, 83  ⊢  
  : , : , :
70theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
71instantiation84, 85  ⊢  
  :
72theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
73instantiation86, 102, 92, 87  ⊢  
  : , : , : , : , :
74instantiation115, 88, 89  ⊢  
  : , : , :
75theorem  ⊢  
 proveit.logic.equality.four_chain_transitivity
76instantiation128, 90  ⊢  
  : , : , :
77instantiation128, 90  ⊢  
  : , : , :
78instantiation131, 102  ⊢  
  :
79instantiation91, 92, 159, 93*  ⊢  
  : , :
80theorem  ⊢  
 proveit.numbers.multiplication.commutation
81theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
82instantiation94, 108, 166, 153, 110, 109, 111, 112, 95  ⊢  
  : , : , : , : , : , :
83instantiation96, 166, 108, 109, 110, 111, 112, 102, 97*  ⊢  
  : , : , : , : , :
84theorem  ⊢  
 proveit.numbers.negation.complex_closure
85instantiation164, 151, 98  ⊢  
  : , : , :
86theorem  ⊢  
 proveit.numbers.division.mult_frac_cancel_numer_left
87instantiation164, 103, 99  ⊢  
  : , : , :
88instantiation128, 100  ⊢  
  : , : , :
89instantiation128, 101  ⊢  
  : , : , :
90instantiation130, 102  ⊢  
  :
91theorem  ⊢  
 proveit.numbers.exponentiation.neg_power_as_div
92instantiation164, 103, 104  ⊢  
  : , : , :
93instantiation105, 142  ⊢  
  :
94theorem  ⊢  
 proveit.numbers.multiplication.disassociation
95instantiation164, 151, 106  ⊢  
  : , : , :
96theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_any
97instantiation107, 166, 108, 109, 110, 111, 112  ⊢  
  : , : , : , :
98instantiation164, 157, 113  ⊢  
  : , : , :
99instantiation164, 120, 114  ⊢  
  : , : , :
100instantiation115, 116, 117  ⊢  
  : , : , :
101instantiation128, 118  ⊢  
  : , : , :
102instantiation164, 151, 119  ⊢  
  : , : , :
103theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
104instantiation164, 120, 121  ⊢  
  : , : , :
105theorem  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
106instantiation164, 157, 122  ⊢  
  : , : , :
107theorem  ⊢  
 proveit.numbers.multiplication.elim_one_any
108axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
109instantiation123  ⊢  
  : , :
110theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
111instantiation164, 151, 124  ⊢  
  : , : , :
112instantiation164, 151, 125  ⊢  
  : , : , :
113instantiation164, 146, 126  ⊢  
  : , : , :
114instantiation164, 133, 127  ⊢  
  : , : , :
115axiom  ⊢  
 proveit.logic.equality.equals_transitivity
116instantiation128, 129  ⊢  
  : , : , :
117instantiation130, 142  ⊢  
  :
118instantiation131, 142  ⊢  
  :
119instantiation164, 157, 132  ⊢  
  : , : , :
120theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
121instantiation164, 133, 134  ⊢  
  : , : , :
122instantiation164, 162, 135  ⊢  
  : , : , :
123theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
124instantiation164, 157, 136  ⊢  
  : , : , :
125instantiation137, 138, 150  ⊢  
  : , : , :
126instantiation139, 147, 140  ⊢  
  : , :
127instantiation164, 143, 159  ⊢  
  : , : , :
128axiom  ⊢  
 proveit.logic.equality.substitution
129instantiation141, 142  ⊢  
  :
130theorem  ⊢  
 proveit.numbers.division.frac_one_denom
131theorem  ⊢  
 proveit.numbers.multiplication.elim_one_right
132instantiation164, 162, 145  ⊢  
  : , : , :
133theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
134instantiation164, 143, 161  ⊢  
  : , : , :
135instantiation144, 145  ⊢  
  :
136instantiation164, 146, 147  ⊢  
  : , : , :
137theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
138instantiation148, 149  ⊢  
  : , :
139theorem  ⊢  
 proveit.numbers.multiplication.mult_rational_pos_closure_bin
140instantiation164, 160, 150  ⊢  
  : , : , :
141theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
142instantiation164, 151, 152  ⊢  
  : , : , :
143theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
144theorem  ⊢  
 proveit.numbers.negation.int_closure
145instantiation164, 165, 153  ⊢  
  : , : , :
146theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
147instantiation154, 155, 156  ⊢  
  : , :
148theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
149theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
150axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
151theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
152instantiation164, 157, 158  ⊢  
  : , : , :
153theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
154theorem  ⊢  
 proveit.numbers.division.div_rational_pos_closure
155instantiation164, 160, 159  ⊢  
  : , : , :
156instantiation164, 160, 161  ⊢  
  : , : , :
157theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
158instantiation164, 162, 163  ⊢  
  : , : , :
159theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
160theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
161theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
162theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
163instantiation164, 165, 166  ⊢  
  : , : , :
164theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
165theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
166theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements