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  ⊢  
  : , :
1reference45  ⊢  
2modus ponens4, 5  ⊢  
3modus ponens6, 7  ⊢  
4instantiation9  ⊢  
  : , : , :
5generalization8  ⊢  
6instantiation9  ⊢  
  : , : , :
7generalization10  ⊢  
8instantiation13, 95, 11, 12,  ⊢  
  : , :
9theorem  ⊢  
 proveit.numbers.summation.summation_real_closure
10instantiation13, 95, 14, 15,  ⊢  
  : , :
11instantiation17, 23, 112,  ⊢  
  : , :
12instantiation18, 16,  ⊢  
  :
13theorem  ⊢  
 proveit.numbers.division.div_real_closure
14instantiation17, 38, 112,  ⊢  
  : , :
15instantiation18, 19,  ⊢  
  :
16instantiation110, 21, 20,  ⊢  
  : , : , :
17theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
18theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
19instantiation110, 21, 22,  ⊢  
  : , : , :
20instantiation25, 23, 24,  ⊢  
  :
21theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
22instantiation25, 38, 26,  ⊢  
  :
23instantiation110, 98, 27,  ⊢  
  : , : , :
24instantiation28, 33, 29, 30,  ⊢  
  : , :
25theorem  ⊢  
 proveit.numbers.exponentiation.sqrd_pos_closure
26instantiation31, 32,  ⊢  
  : , :
27instantiation110, 103, 33,  ⊢  
  : , : , :
28theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq_int
29theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
30instantiation34, 35, 36,  ⊢  
  : , : , :
31theorem  ⊢  
 proveit.logic.equality.not_equals_symmetry
32instantiation37, 73, 38, 39,  ⊢  
  : , :
33instantiation110, 40, 42,  ⊢  
  : , : , :
34theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
35instantiation41, 50, 51, 42,  ⊢  
  : , : , :
36instantiation43, 44  ⊢  
  :
37theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq
38instantiation45, 46, 47,  ⊢  
  : , :
39instantiation48, 49,  ⊢  
  : , :
40instantiation96, 50, 51  ⊢  
  : , :
41theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
42assumption  ⊢  
43theorem  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
44instantiation52, 53  ⊢  
  :
45theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
46instantiation110, 98, 54,  ⊢  
  : , : , :
47instantiation55, 56  ⊢  
  :
48theorem  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
49instantiation57, 58, 59,  ⊢  
  : , : , :
50instantiation100, 60, 104  ⊢  
  : , :
51instantiation107, 78  ⊢  
  :
52theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
53instantiation61, 62, 63  ⊢  
  : , :
54instantiation110, 103, 64,  ⊢  
  : , : , :
55theorem  ⊢  
 proveit.numbers.negation.real_closure
56instantiation65, 73, 95, 67  ⊢  
  : , : , :
57axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
58instantiation66, 73, 95, 67  ⊢  
  : , : , :
59instantiation80, 68, 69,  ⊢  
  : , : , :
60instantiation107, 101  ⊢  
  :
61theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
62instantiation70, 86, 75  ⊢  
  :
63theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
64instantiation110, 71, 77,  ⊢  
  : , : , :
65theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
66theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
67theorem  ⊢  
 proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
68instantiation72, 95, 73, 74, 75, 76*  ⊢  
  : , : , :
69instantiation87, 78, 101, 77,  ⊢  
  : , : , :
70theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
71instantiation96, 78, 101  ⊢  
  : , :
72theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
73theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
74instantiation110, 98, 79  ⊢  
  : , : , :
75instantiation80, 81, 82  ⊢  
  : , : , :
76instantiation83, 84, 85  ⊢  
  : , : , :
77assumption  ⊢  
78instantiation100, 86, 104  ⊢  
  : , :
79instantiation110, 103, 86  ⊢  
  : , : , :
80theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
81theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
82instantiation87, 104, 97, 93  ⊢  
  : , : , :
83theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
84instantiation88, 90  ⊢  
  :
85instantiation89, 90, 91  ⊢  
  : , :
86instantiation110, 92, 93  ⊢  
  : , : , :
87theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
88theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
89theorem  ⊢  
 proveit.numbers.addition.commutation
90instantiation110, 94, 95  ⊢  
  : , : , :
91theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
92instantiation96, 104, 97  ⊢  
  : , :
93assumption  ⊢  
94theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
95instantiation110, 98, 99  ⊢  
  : , : , :
96theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
97instantiation100, 101, 102  ⊢  
  : , :
98theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
99instantiation110, 103, 104  ⊢  
  : , : , :
100theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
101instantiation110, 105, 106  ⊢  
  : , : , :
102instantiation107, 108  ⊢  
  :
103theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
104instantiation110, 111, 109  ⊢  
  : , : , :
105theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
106theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
107theorem  ⊢  
 proveit.numbers.negation.int_closure
108instantiation110, 111, 112  ⊢  
  : , : , :
109theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
110theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
111theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
112theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements