# 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
: , : , :
1reference13
2instantiation40, 4
: , : , :
3instantiation13, 5, 6
: , : , :
4instantiation13, 7, 8
: , : , :
5instantiation18, 21, 102, 99, 23, 9, 24, 51, 57
: , : , : , : , : , :
6instantiation10, 57, 24, 11
: , : , :
7instantiation40, 12
: , : , :
8instantiation13, 14, 15
: , : , :
9instantiation30
: , :
10theorem
11instantiation16
:
12instantiation40, 17
: , : , :
13axiom
proveit.logic.equality.equals_transitivity
14instantiation18, 21, 102, 99, 23, 19, 24, 48, 57
: , : , : , : , : , :
15instantiation20, 99, 102, 21, 22, 23, 24, 48, 57, 25*
: , : , : , : , : , :
16axiom
proveit.logic.equality.equals_reflexivity
17instantiation26, 27, 28, 29
: , : , : , :
18theorem
19instantiation30
: , :
20theorem
21axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
22instantiation30
: , :
23theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
24instantiation31, 32, 33
: , :
25instantiation34, 35, 36
: , : , :
26theorem
proveit.logic.equality.four_chain_transitivity
27instantiation40, 37
: , : , :
28instantiation38, 39
: , :
29instantiation40, 41
: , : , :
30theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
31theorem
proveit.numbers.multiplication.mult_complex_closure_bin
32instantiation42, 57, 43, 44
: , :
33instantiation100, 79, 45
: , : , :
34theorem
proveit.logic.equality.sub_right_side_into
35instantiation46, 57, 70, 47
: , : , :
36instantiation49, 57, 48
: , :
37instantiation49, 50, 51
: , :
38theorem
proveit.logic.equality.equals_reversal
39instantiation52, 70, 64, 63, 59
: , : , :
40axiom
proveit.logic.equality.substitution
41instantiation53, 54, 55
: , :
42theorem
proveit.numbers.division.div_complex_closure
43instantiation56, 70, 57
: , :
44instantiation58, 59, 60
: , : , :
45instantiation100, 89, 61
: , : , :
46theorem
47theorem
48instantiation100, 79, 62
: , : , :
49theorem
50instantiation100, 79, 63
: , : , :
51instantiation100, 79, 64
: , : , :
52theorem
proveit.numbers.exponentiation.product_of_real_powers
53theorem
proveit.numbers.exponentiation.neg_power_as_div
54instantiation100, 65, 66
: , : , :
55theorem
proveit.numbers.numerals.decimals.posnat1
56theorem
proveit.numbers.exponentiation.exp_complex_closure
57instantiation100, 79, 67
: , : , :
58theorem
proveit.logic.equality.sub_left_side_into
59instantiation68, 96
:
60instantiation69, 70
:
61instantiation100, 97, 71
: , : , :
62instantiation100, 89, 72
: , : , :
63instantiation73, 74, 92
: , : , :
64instantiation100, 89, 75
: , : , :
65theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
66instantiation100, 76, 77
: , : , :
67instantiation100, 89, 78
: , : , :
68theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
69theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
70instantiation100, 79, 80
: , : , :
71instantiation81, 98, 82
: , :
72instantiation100, 97, 83
: , : , :
73theorem
proveit.logic.sets.inclusion.unfold_subset_eq
74instantiation84, 85
: , :
75instantiation100, 97, 86
: , : , :
76theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
77instantiation100, 87, 88
: , : , :
78instantiation100, 97, 94
: , : , :
79theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
80instantiation100, 89, 90
: , : , :
81theorem
proveit.numbers.exponentiation.exp_int_closure
82instantiation100, 91, 92
: , : , :
83instantiation93, 98
:
84theorem
proveit.logic.sets.inclusion.relax_proper_subset
85theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
86instantiation93, 94
:
87theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
88instantiation100, 95, 96
: , : , :
89theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
90instantiation100, 97, 98
: , : , :
91theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
92axiom
proveit.physics.quantum.QPE._t_in_natural_pos
93theorem
proveit.numbers.negation.int_closure
94instantiation100, 101, 99
: , : , :
95theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
96theorem
proveit.numbers.numerals.decimals.posnat2
97theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
98instantiation100, 101, 102
: , : , :
99theorem
proveit.numbers.numerals.decimals.nat1
100theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
101theorem
proveit.numbers.number_sets.integers.nat_within_int
102theorem
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements