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  ⊢  
  : , : , :
1reference50  ⊢  
2instantiation8, 6, 7  ⊢  
  : , :
3instantiation8, 10, 11  ⊢  
  : , :
4instantiation8, 10, 12  ⊢  
  : , :
5instantiation9, 10, 11, 12, 13, 14  ⊢  
  : , : , :
6instantiation189, 170, 15  ⊢  
  : , : , :
7instantiation46, 161, 16, 17  ⊢  
  : , :
8theorem  ⊢  
 proveit.numbers.multiplication.mult_real_closure_bin
9theorem  ⊢  
 proveit.numbers.multiplication.weak_bound_via_right_factor_bound
10instantiation189, 170, 18  ⊢  
  : , : , :
11modus ponens19, 20  ⊢  
12instantiation46, 161, 123, 21  ⊢  
  : , :
13instantiation22, 23, 24  ⊢  
  : , : , :
14instantiation58, 25  ⊢  
  : , :
15instantiation189, 28, 26  ⊢  
  : , : , :
16instantiation63, 123, 191  ⊢  
  : , :
17instantiation65, 27, 67  ⊢  
  : , :
18instantiation189, 28, 43  ⊢  
  : , : , :
19instantiation29  ⊢  
  : , : , :
20generalization30  ⊢  
21instantiation31, 147  ⊢  
  :
22theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less_eq
23instantiation32, 33, 34, 152, 139, 35, 36, 37*  ⊢  
  : , : , : , :
24instantiation38, 39, 40, 41  ⊢  
  : , :
25instantiation42, 43  ⊢  
  :
26instantiation59, 60, 44  ⊢  
  : , :
27instantiation189, 79, 45  ⊢  
  : , : , :
28theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
29theorem  ⊢  
 proveit.numbers.summation.summation_real_closure
30instantiation46, 161, 47, 48,  ⊢  
  : , :
31theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
32theorem  ⊢  
 proveit.numbers.summation.integral_upper_bound_of_sum
33theorem  ⊢  
 proveit.numbers.functions.one_over_x_sqrd_in_mon_dec_fxns
34instantiation154, 49  ⊢  
  : , :
35instantiation50, 161, 123, 95, 96, 87*  ⊢  
  : , : , :
36instantiation51, 52  ⊢  
  : , : , :
37instantiation97, 53, 54  ⊢  
  : , : , :
38theorem  ⊢  
 proveit.numbers.integration.boundedInvSqrdIntegral
39instantiation189, 55, 56  ⊢  
  : , : , :
40instantiation81, 106, 57  ⊢  
  :
41instantiation58, 75  ⊢  
  : , :
42theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
43instantiation59, 60, 61  ⊢  
  : , :
44instantiation189, 76, 62  ⊢  
  : , : , :
45instantiation189, 89, 147  ⊢  
  : , : , :
46theorem  ⊢  
 proveit.numbers.division.div_real_closure
47instantiation63, 64, 191,  ⊢  
  : , :
48instantiation65, 66, 67,  ⊢  
  : , :
49theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
50theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
51theorem  ⊢  
 proveit.logic.sets.inclusion.fold_subset_eq
52generalization68  ⊢  
53instantiation110, 113, 191, 181, 115, 69, 72, 150, 70  ⊢  
  : , : , : , : , : , :
54instantiation71, 150, 72, 73  ⊢  
  : , : , :
55theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
56instantiation189, 76, 147  ⊢  
  : , : , :
57instantiation74, 159, 75  ⊢  
  : , : , :
58theorem  ⊢  
 proveit.numbers.ordering.relax_less
59theorem  ⊢  
 proveit.numbers.division.div_rational_pos_closure
60instantiation189, 76, 174  ⊢  
  : , : , :
61instantiation189, 76, 90  ⊢  
  : , : , :
62theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat4
63theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
64instantiation189, 170, 77,  ⊢  
  : , : , :
65theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
66instantiation189, 79, 78,  ⊢  
  : , : , :
67instantiation189, 79, 80  ⊢  
  : , : , :
68instantiation81, 82, 83,  ⊢  
  :
69instantiation127  ⊢  
  : , :
70instantiation84, 150  ⊢  
  :
71theorem  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_23
72instantiation189, 160, 123  ⊢  
  : , : , :
73instantiation85  ⊢  
  :
74axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
75instantiation135, 86, 87  ⊢  
  : , : , :
76theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
77instantiation189, 177, 100,  ⊢  
  : , : , :
78instantiation189, 89, 88,  ⊢  
  : , : , :
79theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
80instantiation189, 89, 90  ⊢  
  : , : , :
81theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
82instantiation91, 105, 106, 107,  ⊢  
  : , : , :
83instantiation167, 92, 93,  ⊢  
  : , : , :
84theorem  ⊢  
 proveit.numbers.negation.complex_closure
85axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
86instantiation94, 123, 95, 161, 96, 168  ⊢  
  : , : , :
87instantiation97, 98, 99  ⊢  
  : , : , :
88instantiation158, 100, 101,  ⊢  
  :
89theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
90theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
91theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_cc__is__real
92instantiation102, 103  ⊢  
  : , :
93instantiation104, 105, 106, 107,  ⊢  
  : , : , :
94theorem  ⊢  
 proveit.numbers.ordering.less_eq_add_right_strong
95instantiation189, 170, 108  ⊢  
  : , : , :
96instantiation109, 179, 180, 176  ⊢  
  : , : , :
97axiom  ⊢  
 proveit.logic.equality.equals_transitivity
98instantiation110, 113, 191, 181, 115, 111, 116, 145, 150  ⊢  
  : , : , : , : , : , :
99instantiation112, 181, 191, 113, 114, 115, 116, 145, 150, 117*  ⊢  
  : , : , : , : , : , :
100instantiation189, 118, 133,  ⊢  
  : , : , :
101instantiation167, 119, 120,  ⊢  
  : , : , :
102theorem  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
103instantiation121, 161, 122, 123, 159, 124*  ⊢  
  : , : , :
104theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_cc_lower_bound
105instantiation189, 170, 125  ⊢  
  : , : , :
106instantiation189, 170, 126  ⊢  
  : , : , :
107assumption  ⊢  
108instantiation189, 177, 180  ⊢  
  : , : , :
109theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
110theorem  ⊢  
 proveit.numbers.addition.disassociation
111instantiation127  ⊢  
  : , :
112theorem  ⊢  
 proveit.numbers.addition.association
113axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
114instantiation127  ⊢  
  : , :
115theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
116instantiation189, 160, 128  ⊢  
  : , : , :
117instantiation135, 129, 130  ⊢  
  : , : , :
118instantiation178, 152, 139  ⊢  
  : , :
119instantiation131, 132  ⊢  
  :
120instantiation175, 152, 139, 133,  ⊢  
  : , : , :
121theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
122theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
123instantiation189, 170, 134  ⊢  
  : , : , :
124instantiation135, 136, 137  ⊢  
  : , : , :
125instantiation189, 177, 138  ⊢  
  : , : , :
126instantiation189, 177, 139  ⊢  
  : , : , :
127theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
128instantiation140, 141, 186  ⊢  
  : , : , :
129instantiation142, 150, 143, 144  ⊢  
  : , : , :
130instantiation149, 150, 145  ⊢  
  : , :
131theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
132instantiation146, 147, 174  ⊢  
  : , :
133assumption  ⊢  
134instantiation189, 177, 162  ⊢  
  : , : , :
135theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
136instantiation148, 150  ⊢  
  :
137instantiation149, 150, 151  ⊢  
  : , :
138instantiation182, 152, 153  ⊢  
  : , :
139instantiation182, 183, 153  ⊢  
  : , :
140theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
141instantiation154, 155  ⊢  
  : , :
142theorem  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add_reversed
143instantiation189, 160, 156  ⊢  
  : , : , :
144theorem  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
145instantiation189, 160, 157  ⊢  
  : , : , :
146theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
147instantiation158, 162, 159  ⊢  
  :
148theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
149theorem  ⊢  
 proveit.numbers.addition.commutation
150instantiation189, 160, 161  ⊢  
  : , : , :
151theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
152instantiation182, 162, 179  ⊢  
  : , :
153instantiation189, 163, 164  ⊢  
  : , : , :
154theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
155theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
156instantiation189, 170, 165  ⊢  
  : , : , :
157instantiation189, 170, 166  ⊢  
  : , : , :
158theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
159instantiation167, 168, 169  ⊢  
  : , : , :
160theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
161instantiation189, 170, 171  ⊢  
  : , : , :
162instantiation189, 172, 176  ⊢  
  : , : , :
163theorem  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_int
164instantiation173, 174  ⊢  
  :
165instantiation189, 177, 188  ⊢  
  : , : , :
166instantiation189, 177, 184  ⊢  
  : , : , :
167theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
168theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
169instantiation175, 179, 180, 176  ⊢  
  : , : , :
170theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
171instantiation189, 177, 179  ⊢  
  : , : , :
172instantiation178, 179, 180  ⊢  
  : , :
173theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
174theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
175theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
176assumption  ⊢  
177theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
178theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
179instantiation189, 190, 181  ⊢  
  : , : , :
180instantiation182, 183, 184  ⊢  
  : , :
181theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
182theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
183instantiation189, 185, 186  ⊢  
  : , : , :
184instantiation187, 188  ⊢  
  :
185theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
186theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
187theorem  ⊢  
 proveit.numbers.negation.int_closure
188instantiation189, 190, 191  ⊢  
  : , : , :
189theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
190theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
191theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements