logo

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*  ⊢  
  : , :
1theorem  ⊢  
 proveit.numbers.division.div_as_mult
2reference31  ⊢  
3instantiation53, 44, 6  ⊢  
  : , : , :
4instantiation28, 7  ⊢  
  :
5instantiation8, 9, 10  ⊢  
  : , : , :
6instantiation53, 42, 11  ⊢  
  : , : , :
7instantiation12, 52, 26  ⊢  
  : , :
8axiom  ⊢  
 proveit.logic.equality.equals_transitivity
9instantiation13, 14  ⊢  
  : , : , :
10instantiation15, 16  ⊢  
  :
11instantiation53, 47, 17  ⊢  
  : , : , :
12theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
13axiom  ⊢  
 proveit.logic.equality.substitution
14instantiation18, 23, 45, 19, 20, 21*  ⊢  
  : , : , :
15theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
16instantiation22, 23, 24  ⊢  
  : , :
17instantiation25, 46, 26  ⊢  
  : , :
18theorem  ⊢  
 proveit.numbers.exponentiation.real_power_of_real_power
19instantiation53, 42, 27  ⊢  
  : , : , :
20instantiation28, 29  ⊢  
  :
21instantiation30, 39, 31, 32*  ⊢  
  : , :
22theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
23instantiation53, 44, 33  ⊢  
  : , : , :
24instantiation34, 39  ⊢  
  :
25theorem  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
26instantiation53, 35, 51  ⊢  
  : , : , :
27instantiation53, 47, 36  ⊢  
  : , : , :
28theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
29theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
30theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_right
31instantiation53, 44, 37  ⊢  
  : , : , :
32instantiation38, 39  ⊢  
  :
33instantiation53, 42, 40  ⊢  
  : , : , :
34theorem  ⊢  
 proveit.numbers.negation.complex_closure
35theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
36instantiation41, 48  ⊢  
  :
37instantiation53, 42, 43  ⊢  
  : , : , :
38theorem  ⊢  
 proveit.numbers.multiplication.elim_one_right
39instantiation53, 44, 45  ⊢  
  : , : , :
40instantiation53, 47, 46  ⊢  
  : , : , :
41theorem  ⊢  
 proveit.numbers.negation.int_closure
42theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
43instantiation53, 47, 48  ⊢  
  : , : , :
44theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
45instantiation49, 50, 51  ⊢  
  : , : , :
46instantiation53, 54, 52  ⊢  
  : , : , :
47theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
48instantiation53, 54, 55  ⊢  
  : , : , :
49theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
50instantiation56, 57  ⊢  
  : , :
51axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
52theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
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
56theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
57theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements