# 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
: , : , :
1reference276
2instantiation4, 11, 5, 6, 7, 25, 8*, 14*, 9*
: , : , : , : , : , : , : , :
3instantiation10, 11, 12, 13*, 14*, 15*
: , : , : , : , :
4theorem
proveit.statistics.prob_of_disjoint_events_is_prob_sum
5instantiation16, 368, 17, 24, 18
: , : , :
6instantiation291
:
7instantiation19, 279, 280, 296, 382, 20
: , : , : , :
8instantiation21, 22,  ⊢
:
9instantiation28, 384, 288, 290
: , : , : , : , :
10theorem
proveit.statistics.prob_of_all_as_sum
11theorem
proveit.physics.quantum.QPE._Omega_is_sample_space
12instantiation23, 24, 25
: , : , : , :
13instantiation26, 27,  ⊢
:
14instantiation28, 384, 288, 290
: , : , : , : , :
15instantiation28, 384, 288, 290
: , : , : , : , :
16theorem
proveit.logic.sets.unification.union_inclusion
17instantiation310
: , :
18instantiation34, 279, 296, 382, 29
: , : , : , :
19theorem
proveit.numbers.number_sets.integers.disjoint_intervals
20instantiation56, 306, 30, 59, 31, 41
: , :
21axiom
proveit.logic.booleans.eq_true_intro
22instantiation350, 32, 33,  ⊢
: , : , :
23theorem
proveit.logic.sets.functions.injections.subset_injection
24instantiation34, 279, 280, 382, 35
: , : , : , :
25instantiation36, 37
: , :
26theorem
proveit.physics.quantum.QPE._outcome_prob
27instantiation38, 242, 246,  ⊢
: , :
28theorem
proveit.core_expr_types.conditionals.true_condition_elimination
29instantiation56, 306, 39, 40, 41, 42
: , :
30instantiation318
: , : , :
31instantiation47, 268, 71, 43, 44, 45*, 46*
: , : , :
32instantiation47, 48, 210, 49, 50, 51*, 52*,  ⊢
: , : , :
33instantiation53, 54, 55*,  ⊢
:
34theorem
proveit.numbers.number_sets.integers.interval_subset_eq
35instantiation56, 306, 57, 58, 59, 60
: , :
36theorem
proveit.logic.booleans.conjunction.left_from_and
37instantiation61, 62
: , : , :
38theorem
proveit.physics.quantum.QPE._mod_add_closure
39instantiation318
: , : , :
40instantiation63, 64, 65
: , : , :
41instantiation99, 360, 333, 66, 67, 68*
: , : , :
42instantiation90, 100, 69
: , :
43instantiation283, 177, 371
: , :
44instantiation70, 71, 177, 371, 72, 73
: , : , :
45instantiation314, 74
: , :
46instantiation301, 75, 76, 77
: , : , : , :
47theorem
proveit.numbers.addition.strong_bound_via_left_term_bound
48instantiation283, 333, 78,  ⊢
: , :
49instantiation390, 377, 79
: , : , :
50instantiation80, 210, 81, 360, 212, 298,  ⊢
: , : , :
51instantiation270, 82, 83,  ⊢
: , : , :
52instantiation270, 84, 85,  ⊢
: , : , :
53theorem
proveit.physics.quantum.QPE._modabs_in_full_domain_simp
54instantiation86, 279, 382, 246, 87,  ⊢
: , : , :
55instantiation88, 89,  ⊢
:
56theorem
proveit.logic.booleans.conjunction.and_if_all
57instantiation318
: , : , :
58instantiation90, 91, 92
: , :
59instantiation99, 93, 333, 106, 107, 94*, 95*
: , : , :
60instantiation156, 96
: , :
61theorem
proveit.logic.sets.functions.bijections.membership_unfolding
62instantiation97, 98
: , : , :
63theorem
proveit.numbers.ordering.transitivity_less_eq_less_eq
64instantiation99, 168, 360, 100, 101, 102*, 103*
: , : , :
65instantiation156, 104
: , :
66instantiation283, 106, 360
: , :
67instantiation105, 333, 106, 360, 107, 108
: , : , :
68instantiation301, 109, 275, 110
: , : , : , :
69instantiation291
:
70theorem
proveit.numbers.ordering.less_add_right
71instantiation202, 371, 112
: , :
72instantiation111, 371, 112, 333, 282, 113
: , : , :
73instantiation143, 392
:
74instantiation301, 181, 114, 115
: , : , : , :
75instantiation287, 288, 392, 384, 290, 116, 149, 363, 251
: , : , : , : , : , :
76instantiation287, 392, 288, 116, 265, 290, 149, 363, 309, 325
: , : , : , : , : , :
77instantiation301, 117, 118, 119
: , : , : , :
78instantiation300, 210,  ⊢
:
79instantiation390, 385, 120
: , : , :
80theorem
proveit.numbers.ordering.less_eq_add_right_strong
81instantiation390, 377, 121
: , : , :
82instantiation287, 384, 392, 288, 153, 290, 184, 321, 155,  ⊢
: , : , : , : , : , :
83instantiation122, 184, 321, 123,  ⊢
: , : , :
84instantiation316, 124
: , : , :
85instantiation270, 125, 126,  ⊢
: , : , :
86theorem
proveit.numbers.number_sets.integers.in_interval
87instantiation165, 127, 128,  ⊢
: , :
88theorem
proveit.numbers.absolute_value.abs_neg_elim
89instantiation156, 186,  ⊢
: , :
90theorem
proveit.numbers.ordering.relax_equal_to_less_eq
91instantiation390, 377, 129
: , : , :
92instantiation291
:
93instantiation130, 306, 131, 168, 360, 284
: , :
94instantiation301, 132, 133, 134
: , : , : , :
95instantiation314, 135
: , :
96instantiation185, 213, 187
: , : , :
97theorem
proveit.logic.sets.functions.bijections.elim_domain_condition
98modus ponens136, 137
99theorem
proveit.numbers.addition.weak_bound_via_left_term_bound
100instantiation343, 344, 387
: , : , :
101instantiation138, 387
:
102instantiation323, 349, 139
: , :
103instantiation270, 140, 141
: , : , :
104instantiation214, 248
:
105theorem
proveit.numbers.ordering.less_eq_add_right
106instantiation390, 377, 142
: , : , :
107instantiation232, 376, 375, 366
: , : , :
108instantiation143, 384
:
109instantiation270, 144, 145
: , : , :
110instantiation314, 285
: , :
111theorem
proveit.numbers.multiplication.strong_bound_via_right_factor_bound
112theorem
proveit.numbers.number_sets.real_numbers.zero_is_real
113instantiation214, 368
:
114instantiation291
:
115instantiation314, 146
: , :
116instantiation310
: , :
117instantiation147, 384, 149, 363, 309, 325
: , : , : , : , : , : , :
118instantiation256, 288, 392, 290, 148, 228, 149, 309, 363, 325, 150*
: , : , : , : , : , :
119instantiation256, 384, 392, 288, 228, 290, 321, 363, 325, 229*
: , : , : , : , : , :
120instantiation381, 280, 376
: , :
121instantiation390, 385, 280
: , : , :
122theorem
proveit.numbers.addition.subtraction.add_cancel_triple_13
123instantiation291
:
124instantiation270, 151, 152
: , : , :
125instantiation287, 384, 392, 288, 153, 290, 309, 321, 155,  ⊢
: , : , : , : , : , :
126instantiation154, 321, 155, 267,  ⊢
: , : , :
127instantiation312, 279, 280, 262,  ⊢
: , : , :
128instantiation156, 157,  ⊢
: , :
129instantiation390, 385, 279
: , : , :
130theorem
proveit.numbers.addition.add_real_closure
131instantiation318
: , : , :
132instantiation270, 158, 159
: , : , :
133instantiation291
:
134instantiation314, 160
: , :
135instantiation301, 181, 161, 162
: , : , : , :
136instantiation163, 164*
: , : , : , : , : , :
137instantiation165, 166, 167
: , :
138theorem
proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
139instantiation390, 370, 168
: , : , :
140instantiation270, 169, 170
: , : , :
141instantiation171, 319, 275
: , :
142instantiation390, 385, 375
: , : , :
143theorem
proveit.numbers.number_sets.natural_numbers.natural_lower_bound
144instantiation316, 172
: , : , :
145instantiation270, 173, 174
: , : , :
146instantiation270, 175, 176
: , : , :
147theorem
proveit.numbers.addition.leftward_commutation
148instantiation310
: , :
149instantiation390, 370, 177
: , : , :
150instantiation270, 178, 179, 180*
: , : , :
151instantiation316, 181
: , : , :
152instantiation270, 182, 183
: , : , :
153instantiation310
: , :
154theorem
proveit.numbers.addition.subtraction.add_cancel_triple_21
155instantiation320, 184,  ⊢
:
156theorem
proveit.numbers.ordering.relax_less
157instantiation185, 186, 187,  ⊢
: , : , :
158instantiation316, 253
: , : , :
159instantiation270, 188, 189
: , : , :
160instantiation316, 269
: , : , :
161instantiation314, 190
: , :
162instantiation314, 191
: , :
163theorem
proveit.logic.sets.functions.bijections.bijection_transitivity
164instantiation316, 192
: , : , :
165theorem
proveit.logic.booleans.conjunction.and_if_both
166instantiation193, 194, 279, 382, 242
: , : , : , : , :
167theorem
proveit.physics.quantum.QPE._sample_space_bijection
168instantiation390, 377, 195
: , : , :
169instantiation316, 285
: , : , :
170instantiation316, 269
: , : , :
171theorem
proveit.numbers.addition.subtraction.add_cancel_basic
172instantiation270, 196, 197
: , : , :
173instantiation287, 288, 392, 384, 290, 198, 319, 325, 349
: , : , : , : , : , :
174instantiation208, 349, 319, 209
: , : , :
175instantiation316, 199
: , : , :
176instantiation270, 200, 201
: , : , :
177instantiation202, 371, 333
: , :
178instantiation316, 203
: , : , :
179instantiation314, 204
: , :
180instantiation270, 205, 206
: , : , :
181instantiation207, 321, 349
: , :
182instantiation287, 288, 392, 384, 290, 265, 309, 325, 349
: , : , : , : , : , :
183instantiation208, 349, 309, 209
: , : , :
184instantiation390, 370, 210,  ⊢
: , : , :
185axiom
proveit.numbers.ordering.transitivity_less_less
186instantiation211, 212, 213,  ⊢
: , : , :
187instantiation214, 387
:
188instantiation287, 384, 306, 288, 307, 290, 321, 308, 349, 309
: , : , : , : , : , :
189instantiation273, 288, 392, 290, 215, 321, 308, 349, 267
: , : , : , : , : , : , : , :
190instantiation245, 251, 321, 325, 216
: , : , :
191instantiation270, 217, 218
: , : , :
192instantiation314, 219
: , :
193theorem
proveit.numbers.modular.interval_left_shift_bijection
194instantiation220, 392, 373
: , :
195instantiation390, 385, 295
: , : , :
196instantiation316, 252
: , : , :
197instantiation270, 221, 222
: , : , :
198instantiation310
: , :
199instantiation223, 363
:
200instantiation287, 384, 392, 288, 265, 290, 224, 309, 325
: , : , : , : , : , :
201instantiation225, 288, 392, 290, 265, 309, 325
: , : , : , :
202theorem
proveit.numbers.multiplication.mult_real_closure_bin
203instantiation314, 226
: , :
204instantiation227, 288, 392, 384, 290, 228, 363, 325, 321
: , : , : , : , : , :
205instantiation316, 229
: , : , :
206instantiation230, 321
:
207theorem
proveit.numbers.negation.distribute_neg_through_binary_sum
208theorem
proveit.numbers.addition.subtraction.add_cancel_triple_32
209instantiation291
:
210instantiation390, 377, 231,  ⊢
: , : , :
211theorem
proveit.numbers.ordering.transitivity_less_eq_less
212instantiation232, 279, 280, 262,  ⊢
: , : , :
213instantiation233, 234
:
214theorem
proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
215instantiation310
: , :
216instantiation276, 235, 236
: , : , :
217instantiation270, 237, 238
: , : , :
218instantiation270, 239, 240
: , : , :
219instantiation241, 242, 243
: , :
220theorem
proveit.numbers.exponentiation.exp_natpos_closure
221instantiation287, 288, 392, 384, 290, 289, 319, 294, 349
: , : , : , : , : , :
222instantiation256, 384, 392, 288, 257, 290, 319, 294, 349, 258*
: , : , : , : , : , :
223theorem
proveit.numbers.multiplication.mult_zero_right
224theorem
proveit.numbers.number_sets.complex_numbers.zero_is_complex
225theorem
proveit.numbers.addition.elim_zero_any
226instantiation244, 321
:
227theorem
proveit.numbers.multiplication.distribute_through_sum
228instantiation310
: , :
229instantiation245, 349, 363, 293
: , : , :
230theorem
proveit.numbers.multiplication.elim_one_left
231instantiation390, 385, 246,  ⊢
: , : , :
232theorem
proveit.numbers.number_sets.integers.interval_upper_bound
233theorem
proveit.numbers.number_sets.integers.negative_if_in_neg_int
234instantiation247, 248
:
235instantiation270, 249, 250
: , : , :
236instantiation323, 321, 251
: , :
237instantiation316, 252
: , : , :
238instantiation316, 253
: , : , :
239instantiation270, 254, 255
: , : , :
240instantiation256, 288, 392, 384, 290, 257, 294, 349, 309, 258*
: , : , : , : , : , :
241axiom
proveit.physics.quantum.QPE._mod_add_def
242theorem
proveit.physics.quantum.QPE._best_floor_is_int
243instantiation390, 259, 260
: , : , :
244theorem
proveit.numbers.negation.mult_neg_one_left
245theorem
proveit.numbers.addition.subtraction.subtract_from_add
246instantiation390, 261, 262,  ⊢
: , : , :
247theorem
proveit.numbers.negation.int_neg_closure
248instantiation263, 264, 329
: , :
249instantiation287, 384, 392, 288, 265, 290, 321, 309, 325
: , : , : , : , : , :
250instantiation266, 321, 325, 267
: , : , :
251instantiation390, 370, 268
: , : , :
252instantiation316, 285
: , : , :
253instantiation316, 269
: , : , :
254instantiation270, 271, 272
: , : , :
255instantiation273, 288, 384, 392, 290, 274, 319, 294, 349, 309, 275
: , : , : , : , : , : , : , :
256theorem
proveit.numbers.addition.association
257instantiation310
: , :
258instantiation276, 277, 278
: , : , :
259instantiation374, 279, 382
: , :
260assumption
261instantiation374, 279, 280
: , :
262assumption
263theorem
proveit.numbers.addition.add_nat_pos_closure_bin
264instantiation281, 354, 282
:
265instantiation310
: , :
266theorem
proveit.numbers.addition.subtraction.add_cancel_triple_12
267instantiation291
:
268instantiation283, 284, 335
: , :
269instantiation316, 285
: , : , :
270axiom
proveit.logic.equality.equals_transitivity
271instantiation287, 288, 392, 384, 290, 289, 319, 294, 286
: , : , : , : , : , :
272instantiation287, 392, 306, 288, 289, 307, 290, 319, 294, 308, 349, 309
: , : , : , : , : , :
273theorem
proveit.numbers.addition.subtraction.add_cancel_general
274instantiation310
: , :
275instantiation291
:
276theorem
proveit.logic.equality.sub_right_side_into
277instantiation292, 349, 363, 293
: , : , :
278instantiation323, 349, 294
: , :
279instantiation381, 295, 376
: , :
280instantiation388, 296
:
281theorem
proveit.numbers.number_sets.integers.pos_int_is_natural_pos
282instantiation297, 298, 299
: , : , :
283theorem
proveit.numbers.addition.add_real_closure_bin
284instantiation300, 333
:
285instantiation301, 302, 303, 304
: , : , : , :
286instantiation305, 306, 307, 308, 349, 309
: , :
287theorem
proveit.numbers.addition.disassociation
288axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
289instantiation310
: , :
290theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
291axiom
proveit.logic.equality.equals_reflexivity
292theorem
proveit.numbers.addition.subtraction.subtract_from_add_reversed
293theorem
proveit.numbers.numerals.decimals.add_1_1
294instantiation390, 370, 311
: , : , :
295instantiation388, 382
:
296instantiation381, 354, 376
: , :
297theorem
proveit.numbers.ordering.transitivity_less_less_eq
298theorem
proveit.numbers.numerals.decimals.less_0_1
299instantiation312, 376, 375, 366
: , : , :
300theorem
proveit.numbers.negation.real_closure
301theorem
proveit.logic.equality.four_chain_transitivity
302instantiation316, 313
: , : , :
303instantiation314, 315
: , :
304instantiation316, 317
: , : , :
305theorem
proveit.numbers.addition.add_complex_closure
306theorem
proveit.numbers.numerals.decimals.nat3
307instantiation318
: , : , :
308instantiation320, 319
:
309instantiation320, 321
:
310theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
311instantiation390, 377, 322
: , : , :
312theorem
proveit.numbers.number_sets.integers.interval_lower_bound
313instantiation323, 324, 325
: , :
314theorem
proveit.logic.equality.equals_reversal
315instantiation326, 363, 335, 334, 351
: , : , :
316axiom
proveit.logic.equality.substitution
317instantiation327, 328, 329
: , :
318theorem
proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
319instantiation330, 331, 332
: , :
320theorem
proveit.numbers.negation.complex_closure
321instantiation390, 370, 333
: , : , :
322instantiation390, 385, 383
: , : , :
323theorem
proveit.numbers.addition.commutation
324instantiation390, 370, 334
: , : , :
325instantiation390, 370, 335
: , : , :
326theorem
proveit.numbers.exponentiation.product_of_real_powers
327theorem
proveit.numbers.exponentiation.neg_power_as_div
328instantiation390, 336, 337
: , : , :
329theorem
proveit.numbers.numerals.decimals.posnat1
330theorem
proveit.numbers.multiplication.mult_complex_closure_bin
331instantiation338, 349, 339, 340
: , :
332instantiation390, 370, 341
: , : , :
333instantiation390, 377, 342
: , : , :
334instantiation343, 344, 380
: , : , :
335instantiation390, 377, 345
: , : , :
336theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
337instantiation390, 346, 347
: , : , :
338theorem
proveit.numbers.division.div_complex_closure
339instantiation348, 363, 349
: , :
340instantiation350, 351, 352
: , : , :
341instantiation390, 377, 353
: , : , :
342instantiation390, 385, 354
: , : , :
343theorem
proveit.logic.sets.inclusion.unfold_subset_eq
344instantiation355, 356
: , :
345instantiation390, 385, 357
: , : , :
346theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
347instantiation390, 358, 359
: , : , :
348theorem
proveit.numbers.exponentiation.exp_complex_closure
349instantiation390, 370, 360
: , : , :
350theorem
proveit.logic.equality.sub_left_side_into
351instantiation361, 368
:
352instantiation362, 363
:
353instantiation390, 385, 364
: , : , :
354instantiation390, 365, 366
: , : , :
355theorem
proveit.logic.sets.inclusion.relax_proper_subset
356theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
357instantiation388, 376
:
358theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
359instantiation390, 367, 368
: , : , :
360instantiation390, 377, 369
: , : , :
361theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
362theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
363instantiation390, 370, 371
: , : , :
364instantiation372, 389, 373
: , :
365instantiation374, 376, 375
: , :
366assumption
367theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
368theorem
proveit.numbers.numerals.decimals.posnat2
369instantiation390, 385, 376
: , : , :
370theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
371instantiation390, 377, 378
: , : , :
372theorem
proveit.numbers.exponentiation.exp_int_closure
373instantiation390, 379, 380
: , : , :
374theorem
proveit.numbers.number_sets.integers.int_interval_within_int
375instantiation381, 382, 383
: , :
376instantiation390, 391, 384
: , : , :
377theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
378instantiation390, 385, 389
: , : , :
379theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
380axiom
proveit.physics.quantum.QPE._t_in_natural_pos
381theorem
proveit.numbers.addition.add_int_closure_bin
382instantiation390, 386, 387
: , : , :
383instantiation388, 389
:
384theorem
proveit.numbers.numerals.decimals.nat1
385theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
386theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
387theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
388theorem
proveit.numbers.negation.int_closure
389instantiation390, 391, 392
: , : , :
390theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
391theorem
proveit.numbers.number_sets.integers.nat_within_int
392theorem
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements