# 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
: , : , : , :
1theorem
proveit.logic.sets.functions.injections.subset_injection
2instantiation4, 125, 5, 154, 6
: , : , : , :
3instantiation7, 8
: , :
4theorem
proveit.numbers.number_sets.integers.interval_subset_eq
5instantiation138, 78, 188
: , :
6instantiation9, 10, 11, 12, 13, 14
: , :
7theorem
proveit.logic.booleans.conjunction.left_from_and
8instantiation15, 16
: , : , :
9theorem
proveit.logic.booleans.conjunction.and_if_all
10theorem
proveit.numbers.numerals.decimals.nat3
11instantiation17
: , : , :
12instantiation18, 19, 20
: , : , :
13instantiation28, 159, 37, 21, 22, 23*
: , : , :
14instantiation24, 29, 25
: , :
15theorem
proveit.logic.sets.functions.bijections.membership_unfolding
16instantiation26, 27
: , : , :
17theorem
proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
18theorem
proveit.numbers.ordering.transitivity_less_eq_less_eq
19instantiation28, 62, 159, 29, 30, 31*, 32*
: , : , :
20instantiation33, 34
: , :
21instantiation35, 38, 159
: , :
22instantiation36, 37, 38, 159, 39, 40
: , : , :
23instantiation113, 41, 66, 42
: , : , : , :
24theorem
proveit.numbers.ordering.relax_equal_to_less_eq
25instantiation95
:
26theorem
proveit.logic.sets.functions.bijections.elim_domain_condition
27modus ponens43, 44
28theorem
29instantiation167, 168, 166
: , : , :
30instantiation45, 166
:
31instantiation140, 148, 46
: , :
32instantiation92, 47, 48
: , : , :
33theorem
proveit.numbers.ordering.relax_less
34instantiation49, 50
:
35theorem
36theorem
37instantiation194, 183, 51
: , : , :
38instantiation194, 183, 52
: , : , :
39instantiation53, 188, 100, 101
: , : , :
40instantiation54, 193
:
41instantiation92, 55, 56
: , : , :
42instantiation127, 102
: , :
43instantiation57, 58*
: , : , : , : , : , :
44instantiation59, 60, 61
: , :
45theorem
proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
46instantiation194, 173, 62
: , : , :
47instantiation92, 63, 64
: , : , :
48instantiation65, 109, 66
: , :
49theorem
proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
50instantiation67, 68, 146
: , :
51instantiation194, 191, 78
: , : , :
52instantiation194, 191, 100
: , : , :
53theorem
proveit.numbers.number_sets.integers.interval_upper_bound
54theorem
proveit.numbers.number_sets.natural_numbers.natural_lower_bound
55instantiation129, 69
: , : , :
56instantiation92, 70, 71
: , : , :
57theorem
proveit.logic.sets.functions.bijections.bijection_transitivity
58instantiation129, 72
: , : , :
59theorem
proveit.logic.booleans.conjunction.and_if_both
60instantiation73, 74, 125, 154, 97
: , : , : , : , :
61theorem
proveit.physics.quantum.QPE._sample_space_bijection
62instantiation194, 183, 75
: , : , :
63instantiation129, 102
: , : , :
64instantiation129, 76
: , : , :
65theorem
66instantiation95
:
67theorem
68instantiation77, 78, 79
:
69instantiation92, 80, 81
: , : , :
70instantiation103, 106, 196, 193, 108, 82, 109, 142, 148
: , : , : , : , : , :
71instantiation83, 148, 109, 84
: , : , :
72instantiation127, 85
: , :
73theorem
proveit.numbers.modular.interval_left_shift_bijection
74instantiation86, 196, 176
: , :
75instantiation194, 191, 139
: , : , :
76instantiation129, 102
: , : , :
77theorem
proveit.numbers.number_sets.integers.pos_int_is_natural_pos
78instantiation194, 87, 101
: , : , :
79instantiation88, 89, 90
: , : , :
80instantiation129, 91
: , : , :
81instantiation92, 93, 94
: , : , :
82instantiation117
: , :
83theorem
84instantiation95
:
85instantiation96, 97, 98
: , :
86theorem
proveit.numbers.exponentiation.exp_natpos_closure
87instantiation124, 188, 100
: , :
88theorem
proveit.numbers.ordering.transitivity_less_less_eq
89theorem
proveit.numbers.numerals.decimals.less_0_1
90instantiation99, 188, 100, 101
: , : , :
91instantiation129, 102
: , : , :
92axiom
proveit.logic.equality.equals_transitivity
93instantiation103, 106, 196, 193, 108, 104, 109, 137, 148
: , : , : , : , : , :
94instantiation105, 193, 196, 106, 107, 108, 109, 137, 148, 110*
: , : , : , : , : , :
95axiom
proveit.logic.equality.equals_reflexivity
96axiom
97theorem
proveit.physics.quantum.QPE._best_floor_is_int
98instantiation194, 111, 112
: , : , :
99theorem
proveit.numbers.number_sets.integers.interval_lower_bound
100instantiation138, 154, 177
: , :
101assumption
102instantiation113, 114, 115, 116
: , : , : , :
103theorem
104instantiation117
: , :
105theorem
106axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
107instantiation117
: , :
108theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
109instantiation118, 119, 120
: , :
110instantiation121, 122, 123
: , : , :
111instantiation124, 125, 154
: , :
112assumption
113theorem
proveit.logic.equality.four_chain_transitivity
114instantiation129, 126
: , : , :
115instantiation127, 128
: , :
116instantiation129, 130
: , : , :
117theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
118theorem
proveit.numbers.multiplication.mult_complex_closure_bin
119instantiation131, 148, 132, 133
: , :
120instantiation194, 173, 134
: , : , :
121theorem
proveit.logic.equality.sub_right_side_into
122instantiation135, 148, 162, 136
: , : , :
123instantiation140, 148, 137
: , :
124theorem
proveit.numbers.number_sets.integers.int_interval_within_int
125instantiation138, 139, 188
: , :
126instantiation140, 141, 142
: , :
127theorem
proveit.logic.equality.equals_reversal
128instantiation143, 162, 156, 155, 150
: , : , :
129axiom
proveit.logic.equality.substitution
130instantiation144, 145, 146
: , :
131theorem
proveit.numbers.division.div_complex_closure
132instantiation147, 162, 148
: , :
133instantiation149, 150, 151
: , : , :
134instantiation194, 183, 152
: , : , :
135theorem
136theorem
137instantiation194, 173, 153
: , : , :
138theorem
139instantiation187, 154
:
140theorem
141instantiation194, 173, 155
: , : , :
142instantiation194, 173, 156
: , : , :
143theorem
proveit.numbers.exponentiation.product_of_real_powers
144theorem
proveit.numbers.exponentiation.neg_power_as_div
145instantiation194, 157, 158
: , : , :
146theorem
proveit.numbers.numerals.decimals.posnat1
147theorem
proveit.numbers.exponentiation.exp_complex_closure
148instantiation194, 173, 159
: , : , :
149theorem
proveit.logic.equality.sub_left_side_into
150instantiation160, 190
:
151instantiation161, 162
:
152instantiation194, 191, 163
: , : , :
153instantiation194, 183, 164
: , : , :
154instantiation194, 165, 166
: , : , :
155instantiation167, 168, 186
: , : , :
156instantiation194, 183, 169
: , : , :
157theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
158instantiation194, 170, 171
: , : , :
159instantiation194, 183, 172
: , : , :
160theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
161theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
162instantiation194, 173, 174
: , : , :
163instantiation175, 192, 176
: , :
164instantiation194, 191, 177
: , : , :
165theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
166theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
167theorem
proveit.logic.sets.inclusion.unfold_subset_eq
168instantiation178, 179
: , :
169instantiation194, 191, 180
: , : , :
170theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
171instantiation194, 181, 182
: , : , :
172instantiation194, 191, 188
: , : , :
173theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
174instantiation194, 183, 184
: , : , :
175theorem
proveit.numbers.exponentiation.exp_int_closure
176instantiation194, 185, 186
: , : , :
177instantiation187, 192
:
178theorem
proveit.logic.sets.inclusion.relax_proper_subset
179theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
180instantiation187, 188
:
181theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
182instantiation194, 189, 190
: , : , :
183theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
184instantiation194, 191, 192
: , : , :
185theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
186axiom
proveit.physics.quantum.QPE._t_in_natural_pos
187theorem
proveit.numbers.negation.int_closure
188instantiation194, 195, 193
: , : , :
189theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
190theorem
proveit.numbers.numerals.decimals.posnat2
191theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
192instantiation194, 195, 196
: , : , :
193theorem
proveit.numbers.numerals.decimals.nat1
194theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
195theorem
proveit.numbers.number_sets.integers.nat_within_int
196theorem
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements