# 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
: , : , :
1reference4
2instantiation4, 5, 6
: , : , :
3instantiation7, 8, 9
: , :
4axiom
proveit.logic.equality.equals_transitivity
5instantiation32, 15
: , : , :
6instantiation32, 10
: , : , :
7theorem
8instantiation11, 12, 13
: , :
9instantiation14
:
10instantiation32, 15
: , : , :
11theorem
proveit.numbers.multiplication.mult_complex_closure_bin
12instantiation16, 25, 17, 18
: , :
13instantiation77, 51, 19
: , : , :
14axiom
proveit.logic.equality.equals_reflexivity
15instantiation20, 21, 22, 23
: , : , : , :
16theorem
proveit.numbers.division.div_complex_closure
17instantiation24, 41, 25
: , :
18instantiation26, 42, 27
: , : , :
19instantiation77, 61, 28
: , : , :
20theorem
proveit.logic.equality.four_chain_transitivity
21instantiation32, 29
: , : , :
22instantiation30, 31
: , :
23instantiation32, 33
: , : , :
24theorem
proveit.numbers.exponentiation.exp_complex_closure
25instantiation77, 51, 34
: , : , :
26theorem
proveit.logic.equality.sub_left_side_into
27instantiation35, 41
:
28instantiation77, 68, 36
: , : , :
29instantiation37, 38, 39
: , :
30theorem
proveit.logic.equality.equals_reversal
31instantiation40, 41, 50, 49, 42
: , : , :
32axiom
proveit.logic.equality.substitution
33instantiation43, 44, 45
: , :
34instantiation77, 61, 46
: , : , :
35theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
36instantiation47, 69, 48
: , :
37theorem
38instantiation77, 51, 49
: , : , :
39instantiation77, 51, 50
: , : , :
40theorem
proveit.numbers.exponentiation.product_of_real_powers
41instantiation77, 51, 52
: , : , :
42instantiation53, 76
:
43theorem
proveit.numbers.exponentiation.neg_power_as_div
44instantiation77, 54, 55
: , : , :
45theorem
proveit.numbers.numerals.decimals.posnat1
46instantiation77, 68, 73
: , : , :
47theorem
proveit.numbers.exponentiation.exp_int_closure
48instantiation77, 56, 59
: , : , :
49instantiation57, 58, 59
: , : , :
50instantiation77, 61, 60
: , : , :
51theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
52instantiation77, 61, 62
: , : , :
53theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
54theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
55instantiation77, 63, 64
: , : , :
56theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
57theorem
proveit.logic.sets.inclusion.unfold_subset_eq
58instantiation65, 66
: , :
59axiom
proveit.physics.quantum.QPE._t_in_natural_pos
60instantiation77, 68, 67
: , : , :
61theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
62instantiation77, 68, 69
: , : , :
63theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
64instantiation77, 70, 71
: , : , :
65theorem
proveit.logic.sets.inclusion.relax_proper_subset
66theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
67instantiation72, 73
:
68theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
69instantiation77, 78, 74
: , : , :
70theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
71instantiation77, 75, 76
: , : , :
72theorem
proveit.numbers.negation.int_closure
73instantiation77, 78, 79
: , : , :
74theorem
proveit.numbers.numerals.decimals.nat2
75theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
76theorem
proveit.numbers.numerals.decimals.posnat2
77theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
78theorem
proveit.numbers.number_sets.integers.nat_within_int
79theorem
proveit.numbers.numerals.decimals.nat1