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