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