# 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
: , : , :
1reference5
2instantiation31, 4
: , : , :
3instantiation5, 6, 7
: , : , :
4instantiation31, 8
: , : , :
5axiom
proveit.logic.equality.equals_transitivity
6instantiation9, 12, 93, 90, 14, 10, 15, 39, 48
: , : , : , : , : , :
7instantiation11, 90, 93, 12, 13, 14, 15, 39, 48, 16*
: , : , : , : , : , :
8instantiation17, 18, 19, 20
: , : , : , :
9theorem
10instantiation21
: , :
11theorem
12axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
13instantiation21
: , :
14theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
15instantiation22, 23, 24
: , :
16instantiation25, 26, 27
: , : , :
17theorem
proveit.logic.equality.four_chain_transitivity
18instantiation31, 28
: , : , :
19instantiation29, 30
: , :
20instantiation31, 32
: , : , :
21theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
22theorem
proveit.numbers.multiplication.mult_complex_closure_bin
23instantiation33, 48, 34, 35
: , :
24instantiation91, 70, 36
: , : , :
25theorem
proveit.logic.equality.sub_right_side_into
26instantiation37, 48, 61, 38
: , : , :
27instantiation40, 48, 39
: , :
28instantiation40, 41, 42
: , :
29theorem
proveit.logic.equality.equals_reversal
30instantiation43, 61, 55, 54, 50
: , : , :
31axiom
proveit.logic.equality.substitution
32instantiation44, 45, 46
: , :
33theorem
proveit.numbers.division.div_complex_closure
34instantiation47, 61, 48
: , :
35instantiation49, 50, 51
: , : , :
36instantiation91, 80, 52
: , : , :
37theorem
38theorem
39instantiation91, 70, 53
: , : , :
40theorem
41instantiation91, 70, 54
: , : , :
42instantiation91, 70, 55
: , : , :
43theorem
proveit.numbers.exponentiation.product_of_real_powers
44theorem
proveit.numbers.exponentiation.neg_power_as_div
45instantiation91, 56, 57
: , : , :
46theorem
proveit.numbers.numerals.decimals.posnat1
47theorem
proveit.numbers.exponentiation.exp_complex_closure
48instantiation91, 70, 58
: , : , :
49theorem
proveit.logic.equality.sub_left_side_into
50instantiation59, 87
:
51instantiation60, 61
:
52instantiation91, 88, 62
: , : , :
53instantiation91, 80, 63
: , : , :
54instantiation64, 65, 83
: , : , :
55instantiation91, 80, 66
: , : , :
56theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
57instantiation91, 67, 68
: , : , :
58instantiation91, 80, 69
: , : , :
59theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
60theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
61instantiation91, 70, 71
: , : , :
62instantiation72, 89, 73
: , :
63instantiation91, 88, 74
: , : , :
64theorem
proveit.logic.sets.inclusion.unfold_subset_eq
65instantiation75, 76
: , :
66instantiation91, 88, 77
: , : , :
67theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
68instantiation91, 78, 79
: , : , :
69instantiation91, 88, 85
: , : , :
70theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
71instantiation91, 80, 81
: , : , :
72theorem
proveit.numbers.exponentiation.exp_int_closure
73instantiation91, 82, 83
: , : , :
74instantiation84, 89
:
75theorem
proveit.logic.sets.inclusion.relax_proper_subset
76theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
77instantiation84, 85
:
78theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
79instantiation91, 86, 87
: , : , :
80theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
81instantiation91, 88, 89
: , : , :
82theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
83axiom
proveit.physics.quantum.QPE._t_in_natural_pos
84theorem
proveit.numbers.negation.int_closure
85instantiation91, 92, 90
: , : , :
86theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
87theorem
proveit.numbers.numerals.decimals.posnat2
88theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
89instantiation91, 92, 93
: , : , :
90theorem
proveit.numbers.numerals.decimals.nat1
91theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
92theorem
proveit.numbers.number_sets.integers.nat_within_int
93theorem
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements