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
: , : , :
1axiom
proveit.logic.equality.equals_transitivity
2instantiation15, 4
: , : , :
3instantiation15, 5
: , : , :
4instantiation15, 7
: , : , :
5instantiation15, 6
: , : , :
6instantiation15, 7
: , : , :
7instantiation8, 9, 10, 11
: , : , : , :
8theorem
proveit.logic.equality.four_chain_transitivity
9instantiation15, 12
: , : , :
10instantiation13, 14
: , :
11instantiation15, 16
: , : , :
12instantiation17, 18, 19
: , :
13theorem
proveit.logic.equality.equals_reversal
14instantiation20, 21, 27, 26, 22
: , : , :
15axiom
proveit.logic.equality.substitution
16instantiation23, 24, 25
: , :
17theorem
proveit.numbers.addition.commutation
18instantiation53, 28, 26
: , : , :
19instantiation53, 28, 27
: , : , :
20theorem
proveit.numbers.exponentiation.product_of_real_powers
21instantiation53, 28, 29
: , : , :
22instantiation30, 52
:
23theorem
proveit.numbers.exponentiation.neg_power_as_div
24instantiation53, 31, 32
: , : , :
25theorem
proveit.numbers.numerals.decimals.posnat1
26instantiation33, 34, 35
: , : , :
27instantiation53, 37, 36
: , : , :
28theorem
proveit.numbers.number_sets.complex_numbers.real_within_complex
29instantiation53, 37, 38
: , : , :
30theorem
proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
31theorem
proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
32instantiation53, 39, 40
: , : , :
33theorem
proveit.logic.sets.inclusion.unfold_subset_eq
34instantiation41, 42
: , :
35axiom
proveit.physics.quantum.QPE._t_in_natural_pos
36instantiation53, 44, 43
: , : , :
37theorem
proveit.numbers.number_sets.real_numbers.rational_within_real
38instantiation53, 44, 45
: , : , :
39theorem
proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
40instantiation53, 46, 47
: , : , :
41theorem
proveit.logic.sets.inclusion.relax_proper_subset
42theorem
proveit.numbers.number_sets.real_numbers.nat_pos_within_real
43instantiation48, 49
:
44theorem
proveit.numbers.number_sets.rational_numbers.int_within_rational
45instantiation53, 54, 50
: , : , :
46theorem
proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
47instantiation53, 51, 52
: , : , :
48theorem
proveit.numbers.negation.int_closure
49instantiation53, 54, 55
: , : , :
50theorem
proveit.numbers.numerals.decimals.nat2
51theorem
proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
52theorem
proveit.numbers.numerals.decimals.posnat2
53theorem
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
54theorem
proveit.numbers.number_sets.integers.nat_within_int
55theorem
proveit.numbers.numerals.decimals.nat1