# 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
2instantiation37, 4
: , : , :
3instantiation5, 6, 7
: , : , :
4instantiation37, 8
: , : , :
5axiom
proveit.logic.equality.equals_transitivity
6instantiation9, 101, 10, 14, 11, 15, 21, 17, 53, 12
: , : , : , : , : , :
7instantiation13, 14, 104, 15, 16, 21, 17, 53, 18
: , : , : , : , : , : , : , :
8instantiation37, 19
: , : , :
9theorem
10theorem
proveit.numbers.numerals.decimals.nat3
11instantiation20
: , : , :
12instantiation23, 21
:
13theorem
14axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
15theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
16instantiation22
: , :
17instantiation23, 24
:
18instantiation25
:
19instantiation26, 27, 28, 29
: , : , : , :
20theorem
proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
21instantiation102, 77, 30
: , : , :
22theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
23theorem
proveit.numbers.negation.complex_closure
24instantiation31, 32, 33
: , :
25axiom
proveit.logic.equality.equals_reflexivity
26theorem
proveit.logic.equality.four_chain_transitivity
27instantiation37, 34
: , : , :
28instantiation35, 36
: , :
29instantiation37, 38
: , : , :
30instantiation102, 89, 39
: , : , :
31theorem
proveit.numbers.multiplication.mult_complex_closure_bin
32instantiation40, 53, 41, 42
: , :
33instantiation102, 77, 43
: , : , :
34instantiation44, 45, 46
: , :
35theorem
proveit.logic.equality.equals_reversal
36instantiation47, 67, 59, 58, 55
: , : , :
37axiom
proveit.logic.equality.substitution
38instantiation48, 49, 50
: , :
39instantiation102, 99, 51
: , : , :
40theorem
proveit.numbers.division.div_complex_closure
41instantiation52, 67, 53
: , :
42instantiation54, 55, 56
: , : , :
43instantiation102, 89, 57
: , : , :
44theorem
45instantiation102, 77, 58
: , : , :
46instantiation102, 77, 59
: , : , :
47theorem
proveit.numbers.exponentiation.product_of_real_powers
48theorem
proveit.numbers.exponentiation.neg_power_as_div
49instantiation102, 60, 61
: , : , :
50theorem
proveit.numbers.numerals.decimals.posnat1
51instantiation102, 62, 63
: , : , :
52theorem
proveit.numbers.exponentiation.exp_complex_closure
53instantiation102, 77, 64
: , : , :
54theorem
proveit.logic.equality.sub_left_side_into
55instantiation65, 95
:
56instantiation66, 67
:
57instantiation102, 99, 68
: , : , :
58instantiation69, 70, 92
: , : , :
59instantiation102, 89, 71
: , : , :
60theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
61instantiation102, 72, 73
: , : , :
62instantiation74, 93, 75
: , :
63assumption
64instantiation102, 89, 76
: , : , :
65theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
66theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
67instantiation102, 77, 78
: , : , :
68instantiation79, 100, 80
: , :
69theorem
proveit.logic.sets.inclusion.unfold_subset_eq
70instantiation81, 82
: , :
71instantiation102, 99, 83
: , : , :
72theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
73instantiation102, 84, 85
: , : , :
74theorem
proveit.numbers.number_sets.integers.int_interval_within_int
75instantiation86, 87, 88
: , :
76instantiation102, 99, 93
: , : , :
77theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
78instantiation102, 89, 90
: , : , :
79theorem
proveit.numbers.exponentiation.exp_int_closure
80instantiation102, 91, 92
: , : , :
81theorem
proveit.logic.sets.inclusion.relax_proper_subset
82theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
83instantiation98, 93
:
84theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
85instantiation102, 94, 95
: , : , :
86theorem
87instantiation102, 96, 97
: , : , :
88instantiation98, 100
:
89theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
90instantiation102, 99, 100
: , : , :
91theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
92axiom
proveit.physics.quantum.QPE._t_in_natural_pos
93instantiation102, 103, 101
: , : , :
94theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
95theorem
proveit.numbers.numerals.decimals.posnat2
96theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
97theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
98theorem
proveit.numbers.negation.int_closure
99theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
100instantiation102, 103, 104
: , : , :
101theorem
proveit.numbers.numerals.decimals.nat1
102theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
103theorem
proveit.numbers.number_sets.integers.nat_within_int
104theorem
proveit.numbers.numerals.decimals.nat2