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  ⊢  
  : , : , :
1axiom  ⊢  
 proveit.logic.equality.substitution
2instantiation3, 28, 4, 19, 5, 6, 7*, 8*  ⊢  
  : , : , :
3theorem  ⊢  
 proveit.numbers.exponentiation.real_power_of_product
4instantiation77, 51, 9  ⊢  
  : , : , :
5instantiation31, 57  ⊢  
  :
6instantiation10, 11, 12  ⊢  
  : , :
7instantiation13, 14, 15, 16*  ⊢  
  : , :
8instantiation17, 18, 52, 19, 20, 21*  ⊢  
  : , : , :
9instantiation22, 29, 79  ⊢  
  : , :
10theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
11instantiation77, 46, 23  ⊢  
  : , : , :
12instantiation77, 46, 24  ⊢  
  : , : , :
13theorem  ⊢  
 proveit.numbers.exponentiation.neg_power_as_div
14instantiation77, 25, 26  ⊢  
  : , : , :
15theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
16instantiation27, 28  ⊢  
  :
17theorem  ⊢  
 proveit.numbers.exponentiation.real_power_of_real_power
18instantiation77, 51, 29  ⊢  
  : , : , :
19instantiation30, 41  ⊢  
  :
20instantiation31, 35  ⊢  
  :
21instantiation32, 43, 33, 34*  ⊢  
  : , :
22theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
23instantiation77, 56, 35  ⊢  
  : , : , :
24instantiation77, 56, 36  ⊢  
  : , : , :
25theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
26instantiation77, 37, 38  ⊢  
  : , : , :
27theorem  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
28instantiation77, 51, 39  ⊢  
  : , : , :
29instantiation77, 60, 40  ⊢  
  : , : , :
30theorem  ⊢  
 proveit.numbers.negation.real_closure
31theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
32theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_right
33instantiation77, 51, 41  ⊢  
  : , : , :
34instantiation42, 43  ⊢  
  :
35instantiation44, 49, 45  ⊢  
  :
36theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
37theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
38instantiation77, 46, 47  ⊢  
  : , : , :
39instantiation77, 60, 48  ⊢  
  : , : , :
40instantiation77, 68, 49  ⊢  
  : , : , :
41instantiation77, 60, 50  ⊢  
  : , : , :
42theorem  ⊢  
 proveit.numbers.multiplication.elim_one_right
43instantiation77, 51, 52  ⊢  
  : , : , :
44theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
45instantiation53, 54, 55  ⊢  
  : , : , :
46theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
47instantiation77, 56, 57  ⊢  
  : , : , :
48instantiation77, 68, 58  ⊢  
  : , : , :
49instantiation77, 59, 63  ⊢  
  : , : , :
50instantiation77, 68, 66  ⊢  
  : , : , :
51theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
52instantiation77, 60, 61  ⊢  
  : , : , :
53theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
54theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
55instantiation62, 66, 67, 63  ⊢  
  : , : , :
56theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
57theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat4
58instantiation77, 78, 64  ⊢  
  : , : , :
59instantiation65, 66, 67  ⊢  
  : , :
60theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
61instantiation77, 68, 76  ⊢  
  : , : , :
62theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
63assumption  ⊢  
64theorem  ⊢  
 proveit.numbers.numerals.decimals.nat4
65theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
66instantiation77, 78, 69  ⊢  
  : , : , :
67instantiation70, 71, 72  ⊢  
  : , :
68theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
69theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
70theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
71instantiation77, 73, 74  ⊢  
  : , : , :
72instantiation75, 76  ⊢  
  :
73theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
74theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
75theorem  ⊢  
 proveit.numbers.negation.int_closure
76instantiation77, 78, 79  ⊢  
  : , : , :
77theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
78theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
79theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements