# 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*, 7*,  ⊢
: , : , :
1theorem
2instantiation8, 61, 9,  ⊢
: , :
3reference50,  ⊢
4instantiation87, 64, 10
: , : , :
5instantiation11, 50, 12, 53, 13, 14,  ⊢
: , : , :
6instantiation36, 15, 16,  ⊢
: , : , :
7instantiation36, 17, 18,  ⊢
: , : , :
8theorem
9instantiation19, 50,  ⊢
:
10instantiation87, 68, 20
: , : , :
11theorem
12instantiation87, 64, 21
: , : , :
13instantiation22, 69, 70, 67,  ⊢
: , : , :
14theorem
proveit.numbers.numerals.decimals.less_0_1
15instantiation41, 79, 89, 42, 30, 43, 39, 55, 32,  ⊢
: , : , : , : , : , :
16instantiation23, 39, 55, 24,  ⊢
: , : , :
17instantiation34, 25
: , : , :
18instantiation36, 26, 27,  ⊢
: , : , :
19theorem
proveit.numbers.negation.real_closure
20instantiation80, 70, 77
: , :
21instantiation87, 68, 70
: , : , :
22theorem
proveit.numbers.number_sets.integers.interval_upper_bound
23theorem
24instantiation56
:
25instantiation36, 28, 29
: , : , :
26instantiation41, 79, 89, 42, 30, 43, 48, 55, 32,  ⊢
: , : , : , : , : , :
27instantiation31, 55, 32, 33,  ⊢
: , : , :
28instantiation34, 35
: , : , :
29instantiation36, 37, 38
: , : , :
30instantiation51
: , :
31theorem
32instantiation54, 39,  ⊢
:
33instantiation56
:
34axiom
proveit.logic.equality.substitution
35instantiation40, 55, 47
: , :
36axiom
proveit.logic.equality.equals_transitivity
37instantiation41, 42, 89, 79, 43, 44, 48, 45, 47
: , : , : , : , : , :
38instantiation46, 47, 48, 49
: , : , :
39instantiation87, 60, 50,  ⊢
: , : , :
40theorem
proveit.numbers.negation.distribute_neg_through_binary_sum
41theorem
42axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
43theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
44instantiation51
: , :
45instantiation87, 60, 52
: , : , :
46theorem
47instantiation87, 60, 53
: , : , :
48instantiation54, 55
:
49instantiation56
:
50instantiation87, 64, 57,  ⊢
: , : , :
51theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
52instantiation87, 64, 58
: , : , :
53instantiation87, 64, 59
: , : , :
54theorem
proveit.numbers.negation.complex_closure
55instantiation87, 60, 61
: , : , :
56axiom
proveit.logic.equality.equals_reflexivity
57instantiation87, 68, 62,  ⊢
: , : , :
58instantiation87, 68, 63
: , : , :
59instantiation87, 68, 77
: , : , :
60theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
61instantiation87, 64, 65
: , : , :
62instantiation87, 66, 67,  ⊢
: , : , :
63instantiation85, 77
:
64theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
65instantiation87, 68, 73
: , : , :
66instantiation76, 69, 70
: , :
67assumption
68theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
69instantiation80, 71, 77
: , :
70instantiation85, 72
:
71instantiation85, 81
:
72instantiation80, 73, 77
: , :
73instantiation87, 74, 75
: , : , :
74instantiation76, 77, 78
: , :
75assumption
76theorem
proveit.numbers.number_sets.integers.int_interval_within_int
77instantiation87, 88, 79
: , : , :
78instantiation80, 81, 82
: , :
79theorem
proveit.numbers.numerals.decimals.nat1
80theorem
81instantiation87, 83, 84
: , : , :
82instantiation85, 86
:
83theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
84theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
85theorem
proveit.numbers.negation.int_closure
86instantiation87, 88, 89
: , : , :
87theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
88theorem
proveit.numbers.number_sets.integers.nat_within_int
89theorem
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements