# 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, 8, 9
: , : , : , : , : , :
1theorem
2axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
3reference69
4reference61
5theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
6instantiation10
: , :
7reference19
8instantiation67, 47, 11
: , : , :
9instantiation12, 13, 14, 15, 32, 16
: , :
10theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
11instantiation67, 54, 17
: , : , :
12theorem
13theorem
proveit.numbers.numerals.decimals.nat3
14instantiation18
: , : , :
15instantiation20, 19
:
16instantiation20, 21
:
17instantiation67, 62, 60
: , : , :
18theorem
proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
19instantiation22, 23, 24
: , :
20theorem
proveit.numbers.negation.complex_closure
21instantiation67, 47, 25
: , : , :
22theorem
proveit.numbers.multiplication.mult_complex_closure_bin
23instantiation26, 32, 27, 28
: , :
24instantiation67, 47, 29
: , : , :
25instantiation67, 54, 30
: , : , :
26theorem
proveit.numbers.division.div_complex_closure
27instantiation31, 42, 32
: , :
28instantiation33, 34, 35
: , : , :
29instantiation67, 54, 36
: , : , :
30instantiation67, 62, 37
: , : , :
31theorem
proveit.numbers.exponentiation.exp_complex_closure
32instantiation67, 47, 38
: , : , :
33theorem
proveit.logic.equality.sub_left_side_into
34instantiation39, 40
:
35instantiation41, 42
:
36instantiation67, 62, 43
: , : , :
37instantiation67, 44, 45
: , : , :
38instantiation67, 54, 46
: , : , :
39theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
40theorem
proveit.numbers.numerals.decimals.posnat2
41theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
42instantiation67, 47, 48
: , : , :
43instantiation49, 66, 50
: , :
44instantiation51, 53, 52
: , :
45assumption
46instantiation67, 62, 53
: , : , :
47theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
48instantiation67, 54, 55
: , : , :
49theorem
proveit.numbers.exponentiation.exp_int_closure
50instantiation67, 56, 57
: , : , :
51theorem
proveit.numbers.number_sets.integers.int_interval_within_int
52instantiation58, 59, 60
: , :
53instantiation67, 68, 61
: , : , :
54theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
55instantiation67, 62, 66
: , : , :
56theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
57axiom
proveit.physics.quantum.QPE._t_in_natural_pos
58theorem
59instantiation67, 63, 64
: , : , :
60instantiation65, 66
:
61theorem
proveit.numbers.numerals.decimals.nat1
62theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
63theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
64theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
65theorem
proveit.numbers.negation.int_closure
66instantiation67, 68, 69
: , : , :
67theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
68theorem
proveit.numbers.number_sets.integers.nat_within_int
69theorem
proveit.numbers.numerals.decimals.nat2