# 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
: , : , :
1reference32
2instantiation6, 3, 4
: , : , :
3instantiation32, 5
: , : , :
4instantiation6, 7, 8
: , : , :
5instantiation32, 9
: , : , :
6axiom
proveit.logic.equality.equals_transitivity
7instantiation10, 13, 94, 91, 15, 11, 16, 40, 49
: , : , : , : , : , :
8instantiation12, 91, 94, 13, 14, 15, 16, 40, 49, 17*
: , : , : , : , : , :
9instantiation18, 19, 20, 21
: , : , : , :
10theorem
11instantiation22
: , :
12theorem
13axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
14instantiation22
: , :
15theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
16instantiation23, 24, 25
: , :
17instantiation26, 27, 28
: , : , :
18theorem
proveit.logic.equality.four_chain_transitivity
19instantiation32, 29
: , : , :
20instantiation30, 31
: , :
21instantiation32, 33
: , : , :
22theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
23theorem
proveit.numbers.multiplication.mult_complex_closure_bin
24instantiation34, 49, 35, 36
: , :
25instantiation92, 71, 37
: , : , :
26theorem
proveit.logic.equality.sub_right_side_into
27instantiation38, 49, 62, 39
: , : , :
28instantiation41, 49, 40
: , :
29instantiation41, 42, 43
: , :
30theorem
proveit.logic.equality.equals_reversal
31instantiation44, 62, 56, 55, 51
: , : , :
32axiom
proveit.logic.equality.substitution
33instantiation45, 46, 47
: , :
34theorem
proveit.numbers.division.div_complex_closure
35instantiation48, 62, 49
: , :
36instantiation50, 51, 52
: , : , :
37instantiation92, 81, 53
: , : , :
38theorem
39theorem
40instantiation92, 71, 54
: , : , :
41theorem
42instantiation92, 71, 55
: , : , :
43instantiation92, 71, 56
: , : , :
44theorem
proveit.numbers.exponentiation.product_of_real_powers
45theorem
proveit.numbers.exponentiation.neg_power_as_div
46instantiation92, 57, 58
: , : , :
47theorem
proveit.numbers.numerals.decimals.posnat1
48theorem
proveit.numbers.exponentiation.exp_complex_closure
49instantiation92, 71, 59
: , : , :
50theorem
proveit.logic.equality.sub_left_side_into
51instantiation60, 88
:
52instantiation61, 62
:
53instantiation92, 89, 63
: , : , :
54instantiation92, 81, 64
: , : , :
55instantiation65, 66, 84
: , : , :
56instantiation92, 81, 67
: , : , :
57theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
58instantiation92, 68, 69
: , : , :
59instantiation92, 81, 70
: , : , :
60theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
61theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
62instantiation92, 71, 72
: , : , :
63instantiation73, 90, 74
: , :
64instantiation92, 89, 75
: , : , :
65theorem
proveit.logic.sets.inclusion.unfold_subset_eq
66instantiation76, 77
: , :
67instantiation92, 89, 78
: , : , :
68theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
69instantiation92, 79, 80
: , : , :
70instantiation92, 89, 86
: , : , :
71theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
72instantiation92, 81, 82
: , : , :
73theorem
proveit.numbers.exponentiation.exp_int_closure
74instantiation92, 83, 84
: , : , :
75instantiation85, 90
:
76theorem
proveit.logic.sets.inclusion.relax_proper_subset
77theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
78instantiation85, 86
:
79theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
80instantiation92, 87, 88
: , : , :
81theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
82instantiation92, 89, 90
: , : , :
83theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
84axiom
proveit.physics.quantum.QPE._t_in_natural_pos
85theorem
proveit.numbers.negation.int_closure
86instantiation92, 93, 91
: , : , :
87theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
88theorem
proveit.numbers.numerals.decimals.posnat2
89theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
90instantiation92, 93, 94
: , : , :
91theorem
proveit.numbers.numerals.decimals.nat1
92theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
93theorem
proveit.numbers.number_sets.integers.nat_within_int
94theorem
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements