# 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
: , : , :
1reference16
2instantiation16, 4, 5
: , : , :
3instantiation16, 6, 7
: , : , :
4instantiation49, 8
: , : , :
5instantiation49, 9
: , : , :
6instantiation16, 10, 11
: , : , :
7instantiation12, 28, 125, 117, 30, 13, 34, 82, 43, 14*
: , : , : , : , : , :
8instantiation49, 25
: , : , :
9instantiation49, 15
: , : , :
10instantiation16, 17, 18
: , : , :
11instantiation19, 28, 117, 125, 30, 20, 52, 34, 82, 43, 21
: , : , : , : , : , : , : , :
12theorem
13instantiation44
: , :
14instantiation22, 23, 24
: , : , :
15instantiation49, 25
: , : , :
16axiom
proveit.logic.equality.equals_transitivity
17instantiation27, 28, 125, 117, 30, 29, 52, 34, 26
: , : , : , : , : , :
18instantiation27, 125, 40, 28, 29, 41, 30, 52, 34, 42, 82, 43
: , : , : , : , : , :
19theorem
20instantiation44
: , :
21instantiation31
:
22theorem
proveit.logic.equality.sub_right_side_into
23instantiation32, 82, 96, 33
: , : , :
24instantiation56, 82, 34
: , :
25instantiation35, 36, 37, 38
: , : , : , :
26instantiation39, 40, 41, 42, 82, 43
: , :
27theorem
28axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
29instantiation44
: , :
30theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
31axiom
proveit.logic.equality.equals_reflexivity
32theorem
33theorem
34instantiation123, 103, 45
: , : , :
35theorem
proveit.logic.equality.four_chain_transitivity
36instantiation49, 46
: , : , :
37instantiation47, 48
: , :
38instantiation49, 50
: , : , :
39theorem
40theorem
proveit.numbers.numerals.decimals.nat3
41instantiation51
: , : , :
42instantiation53, 52
:
43instantiation53, 54
:
44theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
45instantiation123, 110, 55
: , : , :
46instantiation56, 57, 58
: , :
47theorem
proveit.logic.equality.equals_reversal
48instantiation59, 96, 68, 67, 84
: , : , :
49axiom
proveit.logic.equality.substitution
50instantiation60, 61, 62
: , :
51theorem
proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
52instantiation63, 64, 65
: , :
53theorem
proveit.numbers.negation.complex_closure
54instantiation123, 103, 66
: , : , :
55instantiation123, 118, 116
: , : , :
56theorem
57instantiation123, 103, 67
: , : , :
58instantiation123, 103, 68
: , : , :
59theorem
proveit.numbers.exponentiation.product_of_real_powers
60theorem
proveit.numbers.exponentiation.neg_power_as_div
61instantiation123, 69, 70
: , : , :
62theorem
proveit.numbers.numerals.decimals.posnat1
63theorem
proveit.numbers.multiplication.mult_complex_closure_bin
64instantiation71, 82, 72, 73
: , :
65instantiation123, 103, 74
: , : , :
66instantiation123, 110, 75
: , : , :
67instantiation76, 77, 113
: , : , :
68instantiation123, 110, 78
: , : , :
69theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
70instantiation123, 79, 80
: , : , :
71theorem
proveit.numbers.division.div_complex_closure
72instantiation81, 96, 82
: , :
73instantiation83, 84, 85
: , : , :
74instantiation123, 110, 86
: , : , :
75instantiation123, 118, 87
: , : , :
76theorem
proveit.logic.sets.inclusion.unfold_subset_eq
77instantiation88, 89
: , :
78instantiation123, 118, 90
: , : , :
79theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
80instantiation123, 91, 92
: , : , :
81theorem
proveit.numbers.exponentiation.exp_complex_closure
82instantiation123, 103, 93
: , : , :
83theorem
proveit.logic.equality.sub_left_side_into
84instantiation94, 101
:
85instantiation95, 96
:
86instantiation123, 118, 97
: , : , :
87instantiation123, 98, 99
: , : , :
88theorem
proveit.logic.sets.inclusion.relax_proper_subset
89theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
90instantiation121, 109
:
91theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
92instantiation123, 100, 101
: , : , :
93instantiation123, 110, 102
: , : , :
94theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
95theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
96instantiation123, 103, 104
: , : , :
97instantiation105, 122, 106
: , :
98instantiation107, 109, 108
: , :
99assumption
100theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
101theorem
proveit.numbers.numerals.decimals.posnat2
102instantiation123, 118, 109
: , : , :
103theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
104instantiation123, 110, 111
: , : , :
105theorem
proveit.numbers.exponentiation.exp_int_closure
106instantiation123, 112, 113
: , : , :
107theorem
proveit.numbers.number_sets.integers.int_interval_within_int
108instantiation114, 115, 116
: , :
109instantiation123, 124, 117
: , : , :
110theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
111instantiation123, 118, 122
: , : , :
112theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
113axiom
proveit.physics.quantum.QPE._t_in_natural_pos
114theorem
115instantiation123, 119, 120
: , : , :
116instantiation121, 122
:
117theorem
proveit.numbers.numerals.decimals.nat1
118theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
119theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
120theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
121theorem
proveit.numbers.negation.int_closure
122instantiation123, 124, 125
: , : , :
123theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
124theorem
proveit.numbers.number_sets.integers.nat_within_int
125theorem
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements