# 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, 5, 6*, 7*
: , : , :
1theorem
2reference12
3reference48
4instantiation71, 72, 42
: , : , :
5instantiation8, 42
:
6instantiation51, 37, 9
: , :
7instantiation13, 10, 11
: , : , :
8theorem
proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
9instantiation91, 65, 12
: , : , :
10instantiation13, 14, 15
: , : , :
11instantiation16, 17, 18
: , :
12instantiation91, 75, 19
: , : , :
13axiom
proveit.logic.equality.equals_transitivity
14instantiation46, 26
: , : , :
15instantiation46, 20
: , : , :
16theorem
17instantiation21, 22, 23
: , :
18instantiation24
:
19instantiation91, 82, 25
: , : , :
20instantiation46, 26
: , : , :
21theorem
proveit.numbers.multiplication.mult_complex_closure_bin
22instantiation27, 37, 28, 29
: , :
23instantiation91, 65, 30
: , : , :
24axiom
proveit.logic.equality.equals_reflexivity
25instantiation86, 31
:
26instantiation32, 33, 34, 35
: , : , : , :
27theorem
proveit.numbers.division.div_complex_closure
28instantiation36, 55, 37
: , :
29instantiation38, 56, 39
: , : , :
30instantiation91, 75, 40
: , : , :
31instantiation91, 41, 42
: , : , :
32theorem
proveit.logic.equality.four_chain_transitivity
33instantiation46, 43
: , : , :
34instantiation44, 45
: , :
35instantiation46, 47
: , : , :
36theorem
proveit.numbers.exponentiation.exp_complex_closure
37instantiation91, 65, 48
: , : , :
38theorem
proveit.logic.equality.sub_left_side_into
39instantiation49, 55
:
40instantiation91, 82, 50
: , : , :
41theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
42theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
43instantiation51, 52, 53
: , :
44theorem
proveit.logic.equality.equals_reversal
45instantiation54, 55, 64, 63, 56
: , : , :
46axiom
proveit.logic.equality.substitution
47instantiation57, 58, 59
: , :
48instantiation91, 75, 60
: , : , :
49theorem
proveit.numbers.exponentiation.complex_x_to_first_power_is_x
50instantiation61, 83, 62
: , :
51theorem
52instantiation91, 65, 63
: , : , :
53instantiation91, 65, 64
: , : , :
54theorem
proveit.numbers.exponentiation.product_of_real_powers
55instantiation91, 65, 66
: , : , :
56instantiation67, 90
:
57theorem
proveit.numbers.exponentiation.neg_power_as_div
58instantiation91, 68, 69
: , : , :
59theorem
proveit.numbers.numerals.decimals.posnat1
60instantiation91, 82, 87
: , : , :
61theorem
proveit.numbers.exponentiation.exp_int_closure
62instantiation91, 70, 73
: , : , :
63instantiation71, 72, 73
: , : , :
64instantiation91, 75, 74
: , : , :
65theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
66instantiation91, 75, 76
: , : , :
67theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
68theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
69instantiation91, 77, 78
: , : , :
70theorem
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
71theorem
proveit.logic.sets.inclusion.unfold_subset_eq
72instantiation79, 80
: , :
73axiom
proveit.physics.quantum.QPE._t_in_natural_pos
74instantiation91, 82, 81
: , : , :
75theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
76instantiation91, 82, 83
: , : , :
77theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
78instantiation91, 84, 85
: , : , :
79theorem
proveit.logic.sets.inclusion.relax_proper_subset
80theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
81instantiation86, 87
:
82theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
83instantiation91, 92, 88
: , : , :
84theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
85instantiation91, 89, 90
: , : , :
86theorem
proveit.numbers.negation.int_closure
87instantiation91, 92, 93
: , : , :
88theorem
proveit.numbers.numerals.decimals.nat2
89theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
90theorem
proveit.numbers.numerals.decimals.posnat2
91theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
92theorem
proveit.numbers.number_sets.integers.nat_within_int
93theorem
proveit.numbers.numerals.decimals.nat1
*equality replacement requirements