# 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, 8, 9, 10*
: , : , : , : , : , :
1theorem
2axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
3reference50
4reference40
5theorem
proveit.core_expr_types.tuples.tuple_len_0_typical_eq
6instantiation11
: , :
7reference23
8reference22
9instantiation12, 13
:
10instantiation14, 15, 16
: , : , :
11theorem
proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
12theorem
proveit.numbers.negation.complex_closure
13instantiation48, 27, 17
: , : , :
14theorem
proveit.logic.equality.sub_right_side_into
15instantiation18, 22, 19, 20
: , : , :
16instantiation21, 22, 23
: , :
17instantiation48, 32, 24
: , : , :
18theorem
19instantiation48, 27, 25
: , : , :
20theorem
21theorem
22instantiation48, 27, 26
: , : , :
23instantiation48, 27, 28
: , : , :
24instantiation48, 36, 29
: , : , :
25instantiation48, 32, 30
: , : , :
26instantiation48, 32, 31
: , : , :
27theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
28instantiation48, 32, 33
: , : , :
29instantiation48, 34, 35
: , : , :
30instantiation48, 36, 47
: , : , :
31instantiation48, 36, 38
: , : , :
32theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
33instantiation48, 36, 43
: , : , :
34instantiation37, 38, 39
: , :
35assumption
36theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
37theorem
proveit.numbers.number_sets.integers.int_interval_within_int
38instantiation48, 49, 40
: , : , :
39instantiation41, 42, 43
: , :
40theorem
proveit.numbers.numerals.decimals.nat1
41theorem
42instantiation48, 44, 45
: , : , :
43instantiation46, 47
:
44theorem
proveit.numbers.number_sets.integers.nat_pos_within_int
45theorem
proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
46theorem
proveit.numbers.negation.int_closure
47instantiation48, 49, 50
: , : , :
48theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
49theorem
proveit.numbers.number_sets.integers.nat_within_int
50theorem
proveit.numbers.numerals.decimals.nat2
*equality replacement requirements