# 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
: , : , : , :
1reference29
2instantiation16, 5, 6
: , : , :
3instantiation19
:
4instantiation41, 20
: , :
5instantiation43, 7
: , : , :
6instantiation16, 8, 9
: , : , :
7instantiation16, 10, 11
: , : , :
8instantiation21, 24, 105, 102, 26, 12, 27, 54, 60
: , : , : , : , : , :
9instantiation13, 60, 27, 14
: , : , :
10instantiation43, 15
: , : , :
11instantiation16, 17, 18
: , : , :
12instantiation33
: , :
13theorem
proveit.numbers.addition.subtraction.add_cancel_triple_32
14instantiation19
:
15instantiation43, 20
: , : , :
16axiom
proveit.logic.equality.equals_transitivity
17instantiation21, 24, 105, 102, 26, 22, 27, 51, 60
: , : , : , : , : , :
18instantiation23, 102, 105, 24, 25, 26, 27, 51, 60, 28*
: , : , : , : , : , :
19axiom
proveit.logic.equality.equals_reflexivity
20instantiation29, 30, 31, 32
: , : , : , :
21theorem
proveit.numbers.addition.disassociation
22instantiation33
: , :
23theorem
proveit.numbers.addition.association
24axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
25instantiation33
: , :
26theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
27instantiation34, 35, 36
: , :
28instantiation37, 38, 39
: , : , :
29theorem
proveit.logic.equality.four_chain_transitivity
30instantiation43, 40
: , : , :
31instantiation41, 42
: , :
32instantiation43, 44
: , : , :
33theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
34theorem
proveit.numbers.multiplication.mult_complex_closure_bin
35instantiation45, 60, 46, 47
: , :
36instantiation103, 82, 48
: , : , :
37theorem
proveit.logic.equality.sub_right_side_into
38instantiation49, 60, 73, 50
: , : , :
39instantiation52, 60, 51
: , :
40instantiation52, 53, 54
: , :
41theorem
proveit.logic.equality.equals_reversal
42instantiation55, 73, 67, 66, 62
: , : , :
43axiom
proveit.logic.equality.substitution
44instantiation56, 57, 58
: , :
45theorem
proveit.numbers.division.div_complex_closure
46instantiation59, 73, 60
: , :
47instantiation61, 62, 63
: , : , :
48instantiation103, 92, 64
: , : , :
49theorem
proveit.numbers.addition.subtraction.subtract_from_add_reversed
50theorem
proveit.numbers.numerals.decimals.add_1_1
51instantiation103, 82, 65
: , : , :
52theorem
proveit.numbers.addition.commutation
53instantiation103, 82, 66
: , : , :
54instantiation103, 82, 67
: , : , :
55theorem
proveit.numbers.exponentiation.product_of_real_powers
56theorem
proveit.numbers.exponentiation.neg_power_as_div
57instantiation103, 68, 69
: , : , :
58theorem
proveit.numbers.numerals.decimals.posnat1
59theorem
proveit.numbers.exponentiation.exp_complex_closure
60instantiation103, 82, 70
: , : , :
61theorem
proveit.logic.equality.sub_left_side_into
62instantiation71, 99
:
63instantiation72, 73
:
64instantiation103, 100, 74
: , : , :
65instantiation103, 92, 75
: , : , :
66instantiation76, 77, 95
: , : , :
67instantiation103, 92, 78
: , : , :
68theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
69instantiation103, 79, 80
: , : , :
70instantiation103, 92, 81
: , : , :
71theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
72theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
73instantiation103, 82, 83
: , : , :
74instantiation84, 101, 85
: , :
75instantiation103, 100, 86
: , : , :
76theorem
proveit.logic.sets.inclusion.unfold_subset_eq
77instantiation87, 88
: , :
78instantiation103, 100, 89
: , : , :
79theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
80instantiation103, 90, 91
: , : , :
81instantiation103, 100, 97
: , : , :
82theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
83instantiation103, 92, 93
: , : , :
84theorem
proveit.numbers.exponentiation.exp_int_closure
85instantiation103, 94, 95
: , : , :
86instantiation96, 101
:
87theorem
proveit.logic.sets.inclusion.relax_proper_subset
88theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
89instantiation96, 97
:
90theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
91instantiation103, 98, 99
: , : , :
92theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
93instantiation103, 100, 101
: , : , :
94theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
95axiom
proveit.physics.quantum.QPE._t_in_natural_pos
96theorem
proveit.numbers.negation.int_closure
97instantiation103, 104, 102
: , : , :
98theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
99theorem
proveit.numbers.numerals.decimals.posnat2
100theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
101instantiation103, 104, 105
: , : , :
102theorem
proveit.numbers.numerals.decimals.nat1
103theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
104theorem
proveit.numbers.number_sets.integers.nat_within_int
105theorem
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements