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