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  ⊢  
  : , : , :
1reference84  ⊢  
2instantiation89, 4  ⊢  
  : , : , :
3instantiation84, 5, 6  ⊢  
  : , : , :
4modus ponens7, 8  ⊢  
5instantiation89, 9  ⊢  
  : , : , :
6instantiation10, 11  ⊢  
  : , :
7instantiation12, 151  ⊢  
  : , : , : , : , : , :
8generalization13  ⊢  
9modus ponens14, 15  ⊢  
10theorem  ⊢  
 proveit.logic.equality.equals_reversal
11instantiation16, 111, 32  ⊢  
  : , :
12axiom  ⊢  
 proveit.core_expr_types.lambda_maps.lambda_substitution
13instantiation17, 18  ⊢  
  : , : , :
14instantiation19, 151  ⊢  
  : , : , : , : , : , : , :
15generalization20  ⊢  
16modus ponens21, 22  ⊢  
17axiom  ⊢  
 proveit.core_expr_types.conditionals.conditional_substitution
18deduction23  ⊢  
19theorem  ⊢  
 proveit.core_expr_types.lambda_maps.general_lambda_substitution
20instantiation84, 24, 25,  ⊢  
  : , : , :
21instantiation26, 175, 151, 110  ⊢  
  : , : , : , : , : , :
22generalization27  ⊢  
23instantiation109, 175, 170, 110, 28, 111, 33, 32, 34,  ⊢  
  : , : , : , : , : , :
24instantiation29, 110, 175, 111, 33, 32, 34,  ⊢  
  : , : , : , : , : , : , :
25instantiation30, 175, 170, 110, 31, 111, 32, 33, 34,  ⊢  
  : , : , : , : , : , :
26theorem  ⊢  
 proveit.numbers.multiplication.distribute_through_summation
27instantiation123, 33, 34,  ⊢  
  : , :
28instantiation126  ⊢  
  : , :
29theorem  ⊢  
 proveit.numbers.multiplication.leftward_commutation
30theorem  ⊢  
 proveit.numbers.multiplication.association
31instantiation126  ⊢  
  : , :
32instantiation60, 35, 36, 37  ⊢  
  : , :
33instantiation42, 39, 38  ⊢  
  : , :
34instantiation42, 39, 40,  ⊢  
  : , :
35instantiation173, 136, 41  ⊢  
  : , : , :
36instantiation42, 119, 43  ⊢  
  : , :
37instantiation44, 45, 46  ⊢  
  : , : , :
38instantiation95, 47, 48  ⊢  
  : , : , :
39instantiation173, 136, 49  ⊢  
  : , : , :
40instantiation50, 51,  ⊢  
  :
41instantiation173, 147, 52  ⊢  
  : , : , :
42theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
43instantiation60, 92, 119, 67  ⊢  
  : , :
44theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
45instantiation53, 130, 54  ⊢  
  : , :
46instantiation89, 55  ⊢  
  : , : , :
47instantiation123, 98, 56  ⊢  
  : , :
48instantiation84, 57, 58  ⊢  
  : , : , :
49instantiation173, 139, 59  ⊢  
  : , : , :
50theorem  ⊢  
 proveit.numbers.negation.complex_closure
51instantiation60, 61, 62, 63,  ⊢  
  : , :
52instantiation173, 154, 169  ⊢  
  : , : , :
53theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
54instantiation173, 64, 65  ⊢  
  : , : , :
55instantiation66, 92, 119, 67, 68*  ⊢  
  : , :
56instantiation95, 69, 70  ⊢  
  : , : , :
57instantiation109, 175, 99, 110, 71, 111, 98, 124, 94, 125  ⊢  
  : , : , : , : , : , :
58instantiation109, 110, 170, 99, 111, 100, 71, 119, 114, 124, 94, 125  ⊢  
  : , : , : , : , : , :
59theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
60theorem  ⊢  
 proveit.numbers.division.div_complex_closure
61instantiation95, 72, 73,  ⊢  
  : , : , :
62instantiation173, 136, 74  ⊢  
  : , : , :
63instantiation78, 75  ⊢  
  :
64theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational_nonzero
65instantiation76, 135, 77  ⊢  
  : , :
66theorem  ⊢  
 proveit.numbers.division.div_as_mult
67instantiation78, 153  ⊢  
  :
68instantiation84, 79, 80  ⊢  
  : , : , :
69instantiation123, 81, 125  ⊢  
  : , :
70instantiation109, 110, 170, 175, 111, 82, 124, 94, 125  ⊢  
  : , : , : , : , : , :
71instantiation115  ⊢  
  : , : , :
72instantiation123, 98, 83,  ⊢  
  : , :
73instantiation84, 85, 86,  ⊢  
  : , : , :
74instantiation173, 147, 87  ⊢  
  : , : , :
75instantiation88, 170, 167  ⊢  
  : , :
76theorem  ⊢  
 proveit.numbers.multiplication.mult_rational_pos_closure_bin
77instantiation173, 152, 172  ⊢  
  : , : , :
78theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
79instantiation89, 90  ⊢  
  : , : , :
80instantiation91, 92, 93  ⊢  
  : , :
81instantiation123, 124, 94  ⊢  
  : , :
82instantiation126  ⊢  
  : , :
83instantiation95, 96, 97,  ⊢  
  : , : , :
84axiom  ⊢  
 proveit.logic.equality.equals_transitivity
85instantiation109, 175, 99, 110, 101, 111, 98, 124, 125, 113,  ⊢  
  : , : , : , : , : , :
86instantiation109, 110, 170, 99, 111, 100, 101, 119, 114, 124, 125, 113,  ⊢  
  : , : , : , : , : , :
87instantiation173, 154, 163  ⊢  
  : , : , :
88theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
89axiom  ⊢  
 proveit.logic.equality.substitution
90instantiation102, 103, 151, 104*  ⊢  
  : , :
91theorem  ⊢  
 proveit.numbers.multiplication.commutation
92instantiation173, 136, 105  ⊢  
  : , : , :
93instantiation173, 136, 106  ⊢  
  : , : , :
94instantiation173, 136, 107  ⊢  
  : , : , :
95theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
96instantiation123, 108, 113,  ⊢  
  : , :
97instantiation109, 110, 170, 175, 111, 112, 124, 125, 113,  ⊢  
  : , : , : , : , : , :
98instantiation123, 119, 114  ⊢  
  : , :
99theorem  ⊢  
 proveit.numbers.numerals.decimals.nat3
100instantiation126  ⊢  
  : , :
101instantiation115  ⊢  
  : , : , :
102theorem  ⊢  
 proveit.numbers.exponentiation.neg_power_as_div
103instantiation173, 116, 117  ⊢  
  : , : , :
104instantiation118, 119  ⊢  
  :
105instantiation120, 121, 172  ⊢  
  : , : , :
106instantiation173, 147, 122  ⊢  
  : , : , :
107theorem  ⊢  
 proveit.physics.quantum.QPE._phase_is_real
108instantiation123, 124, 125  ⊢  
  : , :
109theorem  ⊢  
 proveit.numbers.multiplication.disassociation
110axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
111theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
112instantiation126  ⊢  
  : , :
113instantiation173, 136, 127  ⊢  
  : , : , :
114instantiation173, 136, 128  ⊢  
  : , : , :
115theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
116theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
117instantiation173, 129, 130  ⊢  
  : , : , :
118theorem  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
119instantiation173, 136, 131  ⊢  
  : , : , :
120theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
121instantiation132, 133  ⊢  
  : , :
122instantiation173, 134, 135  ⊢  
  : , : , :
123theorem  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
124theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
125instantiation173, 136, 137  ⊢  
  : , : , :
126theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
127instantiation173, 147, 138  ⊢  
  : , : , :
128instantiation173, 139, 140  ⊢  
  : , : , :
129theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
130instantiation173, 141, 142  ⊢  
  : , : , :
131instantiation173, 147, 143  ⊢  
  : , : , :
132theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
133theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
134theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
135instantiation144, 145, 146  ⊢  
  : , :
136theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
137instantiation173, 147, 148  ⊢  
  : , : , :
138instantiation173, 154, 149  ⊢  
  : , : , :
139theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
140theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
141theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
142instantiation173, 150, 153  ⊢  
  : , : , :
143instantiation173, 154, 166  ⊢  
  : , : , :
144theorem  ⊢  
 proveit.numbers.division.div_rational_pos_closure
145instantiation173, 152, 151  ⊢  
  : , : , :
146instantiation173, 152, 153  ⊢  
  : , : , :
147theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
148instantiation173, 154, 155  ⊢  
  : , : , :
149instantiation173, 157, 156  ⊢  
  : , : , :
150theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
151theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
152theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
153theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
154theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
155instantiation173, 157, 158  ⊢  
  : , : , :
156assumption  ⊢  
157instantiation159, 160, 161  ⊢  
  : , :
158assumption  ⊢  
159theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
160theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
161instantiation162, 163, 164  ⊢  
  : , :
162theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
163instantiation165, 166, 167  ⊢  
  : , :
164instantiation168, 169  ⊢  
  :
165theorem  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
166instantiation173, 174, 170  ⊢  
  : , : , :
167instantiation173, 171, 172  ⊢  
  : , : , :
168theorem  ⊢  
 proveit.numbers.negation.int_closure
169instantiation173, 174, 175  ⊢  
  : , : , :
170theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
171theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
172axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
173theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
174theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
175theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
*equality replacement requirements