# 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
: , : , :
1reference9
2instantiation9, 4, 5
: , : , :
3instantiation6, 20, 87, 79, 22, 7, 27, 50, 32, 8*
: , : , : , : , : , :
4instantiation9, 10, 11
: , : , :
5instantiation12, 20, 79, 87, 22, 13, 36, 27, 50, 32, 14
: , : , : , : , : , : , : , :
6theorem
7instantiation33
: , :
8instantiation15, 16, 17
: , : , :
9axiom
proveit.logic.equality.equals_transitivity
10instantiation19, 20, 87, 79, 22, 21, 36, 27, 18
: , : , : , : , : , :
11instantiation19, 87, 29, 20, 21, 30, 22, 36, 27, 31, 50, 32
: , : , : , : , : , :
12theorem
13instantiation33
: , :
14instantiation23
:
15theorem
proveit.logic.equality.sub_right_side_into
16instantiation24, 50, 60, 25
: , : , :
17instantiation26, 50, 27
: , :
18instantiation28, 29, 30, 31, 50, 32
: , :
19theorem
20axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
21instantiation33
: , :
22theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
23axiom
proveit.logic.equality.equals_reflexivity
24theorem
25theorem
26theorem
27instantiation85, 65, 34
: , : , :
28theorem
29theorem
proveit.numbers.numerals.decimals.nat3
30instantiation35
: , : , :
31instantiation37, 36
:
32instantiation37, 38
:
33theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
34instantiation85, 72, 39
: , : , :
35theorem
proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
36instantiation40, 41, 42
: , :
37theorem
proveit.numbers.negation.complex_closure
38instantiation85, 65, 43
: , : , :
39instantiation85, 80, 78
: , : , :
40theorem
proveit.numbers.multiplication.mult_complex_closure_bin
41instantiation44, 50, 45, 46
: , :
42instantiation85, 65, 47
: , : , :
43instantiation85, 72, 48
: , : , :
44theorem
proveit.numbers.division.div_complex_closure
45instantiation49, 60, 50
: , :
46instantiation51, 52, 53
: , : , :
47instantiation85, 72, 54
: , : , :
48instantiation85, 80, 55
: , : , :
49theorem
proveit.numbers.exponentiation.exp_complex_closure
50instantiation85, 65, 56
: , : , :
51theorem
proveit.logic.equality.sub_left_side_into
52instantiation57, 58
:
53instantiation59, 60
:
54instantiation85, 80, 61
: , : , :
55instantiation85, 62, 63
: , : , :
56instantiation85, 72, 64
: , : , :
57theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
58theorem
proveit.numbers.numerals.decimals.posnat2
59theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
60instantiation85, 65, 66
: , : , :
61instantiation67, 84, 68
: , :
62instantiation69, 71, 70
: , :
63assumption
64instantiation85, 80, 71
: , : , :
65theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
66instantiation85, 72, 73
: , : , :
67theorem
proveit.numbers.exponentiation.exp_int_closure
68instantiation85, 74, 75
: , : , :
69theorem
proveit.numbers.number_sets.integers.int_interval_within_int
70instantiation76, 77, 78
: , :
71instantiation85, 86, 79
: , : , :
72theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
73instantiation85, 80, 84
: , : , :
74theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
75axiom
proveit.physics.quantum.QPE._t_in_natural_pos
76theorem
77instantiation85, 81, 82
: , : , :
78instantiation83, 84
:
79theorem
proveit.numbers.numerals.decimals.nat1
80theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
81theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
82theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
83theorem
proveit.numbers.negation.int_closure
84instantiation85, 86, 87
: , : , :
85theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
86theorem
proveit.numbers.number_sets.integers.nat_within_int
87theorem
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements