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, 4, 5, 6
: , :
1theorem
proveit.logic.booleans.conjunction.and_if_all
2theorem
proveit.numbers.numerals.decimals.nat3
3instantiation7
: , : , :
4instantiation8, 9, 10
: , : , :
5instantiation16, 131, 25, 11, 12, 13*
: , : , :
6instantiation14, 17, 15
: , :
7theorem
proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
8theorem
proveit.numbers.ordering.transitivity_less_eq_less_eq
9instantiation16, 43, 131, 17, 18, 19*, 20*
: , : , :
10instantiation21, 22
: , :
11instantiation23, 26, 131
: , :
12instantiation24, 25, 26, 131, 27, 28
: , : , :
13instantiation88, 29, 47, 30
: , : , : , :
14theorem
proveit.numbers.ordering.relax_equal_to_less_eq
15instantiation72
:
16theorem
17instantiation137, 138, 100
: , : , :
18instantiation31, 100
:
19instantiation113, 121, 32
: , :
20instantiation69, 33, 34
: , : , :
21theorem
proveit.numbers.ordering.relax_less
22instantiation35, 36
:
23theorem
24theorem
25instantiation164, 153, 37
: , : , :
26instantiation164, 153, 38
: , : , :
27instantiation39, 158, 75, 76
: , : , :
28instantiation40, 163
:
29instantiation69, 41, 42
: , : , :
30instantiation102, 77
: , :
31theorem
proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
32instantiation164, 143, 43
: , : , :
33instantiation69, 44, 45
: , : , :
34instantiation46, 84, 47
: , :
35theorem
proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
36instantiation48, 49, 119
: , :
37instantiation164, 161, 56
: , : , :
38instantiation164, 161, 75
: , : , :
39theorem
proveit.numbers.number_sets.integers.interval_upper_bound
40theorem
proveit.numbers.number_sets.natural_numbers.natural_lower_bound
41instantiation104, 50
: , : , :
42instantiation69, 51, 52
: , : , :
43instantiation164, 153, 53
: , : , :
44instantiation104, 77
: , : , :
45instantiation104, 54
: , : , :
46theorem
47instantiation72
:
48theorem
49instantiation55, 56, 57
:
50instantiation69, 58, 59
: , : , :
51instantiation78, 81, 166, 163, 83, 60, 84, 115, 121
: , : , : , : , : , :
52instantiation61, 121, 84, 62
: , : , :
53instantiation164, 161, 63
: , : , :
54instantiation104, 77
: , : , :
55theorem
proveit.numbers.number_sets.integers.pos_int_is_natural_pos
56instantiation164, 64, 76
: , : , :
57instantiation65, 66, 67
: , : , :
58instantiation104, 68
: , : , :
59instantiation69, 70, 71
: , : , :
60instantiation92
: , :
61theorem
62instantiation72
:
63instantiation157, 87
:
64instantiation73, 158, 75
: , :
65theorem
proveit.numbers.ordering.transitivity_less_less_eq
66theorem
proveit.numbers.numerals.decimals.less_0_1
67instantiation74, 158, 75, 76
: , : , :
68instantiation104, 77
: , : , :
69axiom
proveit.logic.equality.equals_transitivity
70instantiation78, 81, 166, 163, 83, 79, 84, 112, 121
: , : , : , : , : , :
71instantiation80, 163, 166, 81, 82, 83, 84, 112, 121, 85*
: , : , : , : , : , :
72axiom
proveit.logic.equality.equals_reflexivity
73theorem
proveit.numbers.number_sets.integers.int_interval_within_int
74theorem
proveit.numbers.number_sets.integers.interval_lower_bound
75instantiation86, 87, 147
: , :
76assumption
77instantiation88, 89, 90, 91
: , : , : , :
78theorem
79instantiation92
: , :
80theorem
81axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
82instantiation92
: , :
83theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
84instantiation93, 94, 95
: , :
85instantiation96, 97, 98
: , : , :
86theorem
87instantiation164, 99, 100
: , : , :
88theorem
proveit.logic.equality.four_chain_transitivity
89instantiation104, 101
: , : , :
90instantiation102, 103
: , :
91instantiation104, 105
: , : , :
92theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
93theorem
proveit.numbers.multiplication.mult_complex_closure_bin
94instantiation106, 121, 107, 108
: , :
95instantiation164, 143, 109
: , : , :
96theorem
proveit.logic.equality.sub_right_side_into
97instantiation110, 121, 134, 111
: , : , :
98instantiation113, 121, 112
: , :
99theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
100theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
101instantiation113, 114, 115
: , :
102theorem
proveit.logic.equality.equals_reversal
103instantiation116, 134, 128, 127, 123
: , : , :
104axiom
proveit.logic.equality.substitution
105instantiation117, 118, 119
: , :
106theorem
proveit.numbers.division.div_complex_closure
107instantiation120, 134, 121
: , :
108instantiation122, 123, 124
: , : , :
109instantiation164, 153, 125
: , : , :
110theorem
111theorem
112instantiation164, 143, 126
: , : , :
113theorem
114instantiation164, 143, 127
: , : , :
115instantiation164, 143, 128
: , : , :
116theorem
proveit.numbers.exponentiation.product_of_real_powers
117theorem
proveit.numbers.exponentiation.neg_power_as_div
118instantiation164, 129, 130
: , : , :
119theorem
proveit.numbers.numerals.decimals.posnat1
120theorem
proveit.numbers.exponentiation.exp_complex_closure
121instantiation164, 143, 131
: , : , :
122theorem
proveit.logic.equality.sub_left_side_into
123instantiation132, 160
:
124instantiation133, 134
:
125instantiation164, 161, 135
: , : , :
126instantiation164, 153, 136
: , : , :
127instantiation137, 138, 156
: , : , :
128instantiation164, 153, 139
: , : , :
129theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
130instantiation164, 140, 141
: , : , :
131instantiation164, 153, 142
: , : , :
132theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
133theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
134instantiation164, 143, 144
: , : , :
135instantiation145, 162, 146
: , :
136instantiation164, 161, 147
: , : , :
137theorem
proveit.logic.sets.inclusion.unfold_subset_eq
138instantiation148, 149
: , :
139instantiation164, 161, 150
: , : , :
140theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
141instantiation164, 151, 152
: , : , :
142instantiation164, 161, 158
: , : , :
143theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
144instantiation164, 153, 154
: , : , :
145theorem
proveit.numbers.exponentiation.exp_int_closure
146instantiation164, 155, 156
: , : , :
147instantiation157, 162
:
148theorem
proveit.logic.sets.inclusion.relax_proper_subset
149theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
150instantiation157, 158
:
151theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
152instantiation164, 159, 160
: , : , :
153theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
154instantiation164, 161, 162
: , : , :
155theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
156axiom
proveit.physics.quantum.QPE._t_in_natural_pos
157theorem
proveit.numbers.negation.int_closure
158instantiation164, 165, 163
: , : , :
159theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
160theorem
proveit.numbers.numerals.decimals.posnat2
161theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
162instantiation164, 165, 166
: , : , :
163theorem
proveit.numbers.numerals.decimals.nat1
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