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
0generalization1  ⊢  
1instantiation471, 2, 3  ⊢  
  : , : , :
2instantiation79, 4, 5  ⊢  
  : , : , :
3instantiation243, 527, 6, 7, 8, 9  ⊢  
  : , : , : , :
4instantiation79, 10, 11  ⊢  
  : , : , :
5instantiation147, 12, 13, 14, 15  ⊢  
  : , : , :
6instantiation461  ⊢  
  : , :
7instantiation461  ⊢  
  : , :
8instantiation205, 16  ⊢  
  : , :
9instantiation205, 17  ⊢  
  : , :
10instantiation18, 516  ⊢  
  :
11instantiation471, 19, 20, 21*  ⊢  
  : , : , :
12instantiation22, 179, 204  ⊢  
  : , :
13instantiation22, 175, 314  ⊢  
  : , :
14instantiation22, 175, 23  ⊢  
  : , :
15instantiation114, 175, 314, 23, 24, 25  ⊢  
  : , : , :
16instantiation29, 26, 27, 28  ⊢  
  : , : , : , :
17instantiation29, 30, 31, 32  ⊢  
  : , : , : , :
18theorem  ⊢  
 proveit.physics.quantum.QPE._failure_upper_bound_lemma
19instantiation471, 33, 34  ⊢  
  : , : , :
20instantiation35, 499, 481, 133  ⊢  
  : , : , : , :
21instantiation406, 36, 37  ⊢  
  : , : , :
22theorem  ⊢  
 proveit.numbers.multiplication.mult_real_closure_bin
23instantiation371, 495, 458, 224  ⊢  
  : , :
24instantiation79, 38, 39  ⊢  
  : , : , :
25instantiation402, 40  ⊢  
  : , :
26instantiation110, 485, 41, 42, 43*  ⊢  
  : , :
27instantiation325  ⊢  
  :
28instantiation205, 44  ⊢  
  : , :
29theorem  ⊢  
 proveit.logic.equality.four_chain_transitivity
30instantiation110, 485, 45, 46, 47*  ⊢  
  : , :
31instantiation325  ⊢  
  :
32instantiation205, 48  ⊢  
  : , :
33instantiation471, 49, 50  ⊢  
  : , : , :
34instantiation51, 453, 454, 52*, 53*, 54*  ⊢  
  : , : , : , :
35theorem  ⊢  
 proveit.numbers.summation.sum_split_first
36instantiation234, 55  ⊢  
  : , : , :
37instantiation239, 517, 527, 446, 56, 447, 144, 57, 163, 58*  ⊢  
  : , : , : , : , : , :
38instantiation59, 60, 61, 480, 481, 62, 63, 83*  ⊢  
  : , : , : , :
39instantiation64, 65, 66, 67  ⊢  
  : , :
40instantiation194, 262  ⊢  
  :
41instantiation93, 463, 226  ⊢  
  : , :
42instantiation73, 527, 68, 249, 69  ⊢  
  : , :
43instantiation406, 70, 71  ⊢  
  : , : , :
44instantiation234, 72  ⊢  
  : , : , :
45instantiation93, 286, 140  ⊢  
  : , :
46instantiation73, 527, 74, 177, 75  ⊢  
  : , :
47instantiation406, 76, 77  ⊢  
  : , : , :
48instantiation234, 78  ⊢  
  : , : , :
49instantiation79, 80, 81  ⊢  
  : , : , :
50instantiation82, 480, 519, 493, 83*, 84*  ⊢  
  : , : , : , : , :
51theorem  ⊢  
 proveit.numbers.summation.index_negate
52instantiation280, 85  ⊢  
  :
53instantiation86, 87, 485, 88*  ⊢  
  : , :
54instantiation89, 90, 517, 267*,  ⊢  
  : , :
55instantiation406, 91, 92  ⊢  
  : , : , :
56instantiation461  ⊢  
  : , :
57instantiation93, 463, 283  ⊢  
  : , :
58instantiation406, 94, 95  ⊢  
  : , : , :
59theorem  ⊢  
 proveit.numbers.summation.integral_upper_bound_of_sum
60theorem  ⊢  
 proveit.numbers.functions.one_over_x_sqrd_in_mon_dec_fxns
61instantiation496, 96  ⊢  
  : , :
62instantiation147, 495, 458, 215, 216, 173*  ⊢  
  : , : , :
63instantiation97, 98  ⊢  
  : , : , :
64theorem  ⊢  
 proveit.numbers.integration.boundedInvSqrdIntegral
65instantiation525, 330, 99  ⊢  
  : , : , :
66instantiation169, 253, 100  ⊢  
  :
67instantiation402, 133  ⊢  
  : , :
68instantiation461  ⊢  
  : , :
69instantiation525, 287, 101  ⊢  
  : , : , :
70instantiation234, 102  ⊢  
  : , : , :
71instantiation406, 103, 104  ⊢  
  : , : , :
72instantiation110, 485, 226, 224, 105*  ⊢  
  : , :
73theorem  ⊢  
 proveit.numbers.multiplication.mult_not_eq_zero
74instantiation461  ⊢  
  : , :
75instantiation106, 140, 238  ⊢  
  :
76instantiation234, 107  ⊢  
  : , : , :
77instantiation406, 108, 109  ⊢  
  : , : , :
78instantiation110, 485, 140, 238, 111*  ⊢  
  : , :
79theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less_eq
80instantiation114, 179, 112, 115, 113, 118  ⊢  
  : , : , :
81instantiation114, 179, 115, 116, 117, 118  ⊢  
  : , : , :
82theorem  ⊢  
 proveit.numbers.summation.index_shift
83instantiation406, 119, 120  ⊢  
  : , : , :
84instantiation406, 121, 122,  ⊢  
  : , : , :
85instantiation525, 494, 123  ⊢  
  : , : , :
86theorem  ⊢  
 proveit.numbers.negation.distribute_neg_through_binary_sum
87instantiation525, 494, 124  ⊢  
  : , : , :
88instantiation280, 260  ⊢  
  :
89theorem  ⊢  
 proveit.numbers.exponentiation.even_pow_is_even_fn
90instantiation525, 494, 391,  ⊢  
  : , : , :
91instantiation256, 517, 527, 446, 125, 447, 283, 163  ⊢  
  : , : , : , : , : , :
92instantiation406, 126, 127  ⊢  
  : , : , :
93theorem  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
94instantiation426, 517, 527, 446, 128, 447, 144, 463, 283  ⊢  
  : , : , : , : , : , :
95instantiation129, 446, 527, 517, 447, 130, 144, 463, 283, 131*  ⊢  
  : , : , : , : , : , :
96theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
97theorem  ⊢  
 proveit.logic.sets.inclusion.fold_subset_eq
98generalization132  ⊢  
99instantiation525, 349, 492  ⊢  
  : , : , :
100instantiation421, 500, 133  ⊢  
  : , : , :
101instantiation525, 316, 282  ⊢  
  : , : , :
102instantiation139, 463, 226, 386, 134, 224, 135*  ⊢  
  : , : , :
103instantiation426, 517, 527, 446, 136, 447, 485, 137, 138  ⊢  
  : , : , : , : , : , :
104instantiation445, 446, 527, 447, 136, 137, 138  ⊢  
  : , : , : , :
105instantiation285, 138  ⊢  
  :
106theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
107instantiation139, 286, 140, 386, 141, 238, 142*, 180*  ⊢  
  : , : , :
108instantiation426, 517, 527, 446, 143, 447, 485, 144, 181  ⊢  
  : , : , : , : , : , :
109instantiation445, 446, 527, 447, 143, 144, 181  ⊢  
  : , : , : , :
110theorem  ⊢  
 proveit.numbers.division.div_as_mult
111instantiation406, 145, 146  ⊢  
  : , : , :
112instantiation398, 148, 151  ⊢  
  : , :
113instantiation147, 151, 148, 150, 149  ⊢  
  : , : , :
114theorem  ⊢  
 proveit.numbers.multiplication.weak_bound_via_right_factor_bound
115instantiation398, 150, 151  ⊢  
  : , :
116instantiation398, 150, 152  ⊢  
  : , :
117instantiation343, 150, 151, 152, 153  ⊢  
  : , : , :
118instantiation402, 154  ⊢  
  : , :
119instantiation256, 446, 527, 517, 447, 155, 226, 485, 427  ⊢  
  : , : , : , : , : , :
120instantiation201, 485, 226, 203  ⊢  
  : , : , :
121instantiation234, 156  ⊢  
  : , : , :
122instantiation406, 157, 158,  ⊢  
  : , : , :
123instantiation525, 503, 159  ⊢  
  : , : , :
124instantiation525, 503, 160  ⊢  
  : , : , :
125instantiation461  ⊢  
  : , :
126instantiation161, 517, 446, 447, 283, 163  ⊢  
  : , : , : , : , : , : , :
127instantiation258, 446, 527, 517, 447, 162, 283, 163, 164*  ⊢  
  : , : , : , : , : , :
128instantiation461  ⊢  
  : , :
129theorem  ⊢  
 proveit.numbers.multiplication.association
130instantiation461  ⊢  
  : , :
131instantiation165, 485, 463, 177, 166, 167*, 168*  ⊢  
  : , : , : , :
132instantiation169, 170, 171,  ⊢  
  :
133instantiation471, 172, 173  ⊢  
  : , : , :
134instantiation307, 432  ⊢  
  :
135instantiation176, 249, 510, 174*  ⊢  
  : , :
136instantiation461  ⊢  
  : , :
137instantiation525, 494, 175  ⊢  
  : , : , :
138instantiation462, 226, 427  ⊢  
  : , :
139theorem  ⊢  
 proveit.numbers.exponentiation.real_power_of_product
140instantiation525, 494, 237  ⊢  
  : , : , :
141instantiation307, 321  ⊢  
  :
142instantiation176, 177, 510, 178*  ⊢  
  : , :
143instantiation461  ⊢  
  : , :
144instantiation525, 494, 179  ⊢  
  : , : , :
145instantiation234, 180  ⊢  
  : , : , :
146instantiation285, 181  ⊢  
  :
147theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
148modus ponens182, 183  ⊢  
149modus ponens184, 185  ⊢  
150modus ponens186, 187  ⊢  
151modus ponens188, 189  ⊢  
152modus ponens190, 191  ⊢  
153modus ponens192, 193  ⊢  
154instantiation194, 265  ⊢  
  :
155instantiation461  ⊢  
  : , :
156instantiation195, 432, 196, 197, 198, 199  ⊢  
  : , : , :
157instantiation256, 446, 527, 517, 447, 200, 202, 485, 427,  ⊢  
  : , : , : , : , : , :
158instantiation201, 485, 202, 203,  ⊢  
  : , : , :
159instantiation525, 511, 480  ⊢  
  : , : , :
160instantiation525, 511, 469  ⊢  
  : , : , :
161theorem  ⊢  
 proveit.numbers.addition.leftward_commutation
162instantiation461  ⊢  
  : , :
163instantiation525, 494, 204  ⊢  
  : , : , :
164instantiation205, 206, 319*  ⊢  
  : , :
165theorem  ⊢  
 proveit.numbers.division.prod_of_fracs
166instantiation525, 287, 207  ⊢  
  : , : , :
167instantiation208, 463  ⊢  
  :
168instantiation406, 209, 210  ⊢  
  : , : , :
169theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
170instantiation211, 252, 253, 254,  ⊢  
  : , : , :
171instantiation506, 212, 213,  ⊢  
  : , : , :
172instantiation214, 458, 215, 495, 216, 507  ⊢  
  : , : , :
173instantiation406, 217, 218  ⊢  
  : , : , :
174instantiation221, 463  ⊢  
  :
175instantiation525, 503, 219  ⊢  
  : , : , :
176theorem  ⊢  
 proveit.numbers.exponentiation.neg_power_as_div
177instantiation525, 287, 220  ⊢  
  : , : , :
178instantiation221, 286  ⊢  
  :
179instantiation525, 503, 222  ⊢  
  : , : , :
180instantiation223, 226, 474, 386, 224, 225*  ⊢  
  : , : , :
181instantiation462, 226, 320  ⊢  
  : , :
182instantiation353  ⊢  
  : , : , :
183generalization227  ⊢  
184instantiation232  ⊢  
  : , : , :
185generalization228  ⊢  
186instantiation353  ⊢  
  : , : , :
187generalization229  ⊢  
188instantiation353  ⊢  
  : , : , :
189generalization230  ⊢  
190instantiation353  ⊢  
  : , : , :
191generalization231  ⊢  
192instantiation232  ⊢  
  : , : , :
193generalization233  ⊢  
194theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
195theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_eq_via_elem_eq
196instantiation461  ⊢  
  : , :
197instantiation461  ⊢  
  : , :
198instantiation234, 235  ⊢  
  : , : , :
199instantiation325  ⊢  
  :
200instantiation461  ⊢  
  : , :
201theorem  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_23
202instantiation525, 494, 236,  ⊢  
  : , : , :
203instantiation325  ⊢  
  :
204instantiation371, 495, 237, 238  ⊢  
  : , :
205theorem  ⊢  
 proveit.logic.equality.equals_reversal
206instantiation239, 446, 527, 517, 447, 240, 485, 283, 241*  ⊢  
  : , : , : , : , : , :
207instantiation525, 316, 242  ⊢  
  : , : , :
208theorem  ⊢  
 proveit.numbers.division.frac_one_denom
209instantiation243, 527, 244, 245, 246, 247  ⊢  
  : , : , : , :
210instantiation248, 249, 485, 267*, 250*  ⊢  
  : , : , :
211theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_cc__is__real
212instantiation423, 442  ⊢  
  : , :
213instantiation251, 252, 253, 254,  ⊢  
  : , : , :
214theorem  ⊢  
 proveit.numbers.ordering.less_eq_add_right_strong
215instantiation525, 503, 255  ⊢  
  : , : , :
216instantiation433, 514, 515, 516  ⊢  
  : , : , :
217instantiation256, 446, 527, 517, 447, 257, 260, 320, 485  ⊢  
  : , : , : , : , : , :
218instantiation258, 517, 527, 446, 259, 447, 260, 320, 485, 261*  ⊢  
  : , : , : , : , : , :
219instantiation525, 264, 262  ⊢  
  : , : , :
220instantiation525, 316, 263  ⊢  
  : , : , :
221theorem  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
222instantiation525, 264, 265  ⊢  
  : , : , :
223theorem  ⊢  
 proveit.numbers.exponentiation.real_power_of_real_power
224instantiation307, 492  ⊢  
  :
225instantiation266, 463, 485, 267*  ⊢  
  : , :
226instantiation525, 494, 458  ⊢  
  : , : , :
227instantiation371, 495, 268, 269,  ⊢  
  : , :
228instantiation270, 271, 326, 322, 272,  ⊢  
  : , : , :
229instantiation371, 495, 273, 274,  ⊢  
  : , :
230instantiation371, 495, 275, 276,  ⊢  
  : , :
231instantiation371, 495, 277, 278,  ⊢  
  : , :
232theorem  ⊢  
 proveit.numbers.summation.weak_summation_from_summands_bound
233instantiation402, 279,  ⊢  
  : , :
234axiom  ⊢  
 proveit.logic.equality.substitution
235instantiation280, 485  ⊢  
  :
236instantiation525, 503, 281,  ⊢  
  : , : , :
237instantiation390, 458, 527  ⊢  
  : , :
238instantiation392, 282, 394  ⊢  
  : , :
239theorem  ⊢  
 proveit.numbers.multiplication.distribute_through_sum
240instantiation461  ⊢  
  : , :
241instantiation285, 283  ⊢  
  :
242instantiation525, 411, 284  ⊢  
  : , : , :
243axiom  ⊢  
 proveit.core_expr_types.operations.operands_substitution
244instantiation461  ⊢  
  : , :
245instantiation461  ⊢  
  : , :
246instantiation285, 463  ⊢  
  :
247instantiation425, 286  ⊢  
  :
248theorem  ⊢  
 proveit.numbers.division.frac_cancel_left
249instantiation525, 287, 288  ⊢  
  : , : , :
250theorem  ⊢  
 proveit.numbers.numerals.decimals.mult_2_2
251theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_cc_lower_bound
252instantiation525, 503, 289  ⊢  
  : , : , :
253instantiation525, 503, 290  ⊢  
  : , : , :
254assumption  ⊢  
255instantiation525, 511, 515  ⊢  
  : , : , :
256theorem  ⊢  
 proveit.numbers.addition.disassociation
257instantiation461  ⊢  
  : , :
258theorem  ⊢  
 proveit.numbers.addition.association
259instantiation461  ⊢  
  : , :
260instantiation525, 494, 291  ⊢  
  : , : , :
261instantiation471, 292, 293  ⊢  
  : , : , :
262instantiation296, 329, 294  ⊢  
  : , :
263instantiation525, 411, 295  ⊢  
  : , : , :
264theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
265instantiation296, 329, 297  ⊢  
  : , :
266theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_right
267instantiation425, 463  ⊢  
  :
268instantiation390, 357, 527,  ⊢  
  : , :
269instantiation305, 298,  ⊢  
  :
270theorem  ⊢  
 proveit.numbers.division.weak_div_from_denom_bound__all_pos
271instantiation525, 299, 300  ⊢  
  : , : , :
272instantiation301, 474, 357, 378, 302, 303,  ⊢  
  : , : , :
273instantiation390, 378, 527,  ⊢  
  : , :
274instantiation305, 304,  ⊢  
  :
275instantiation390, 380, 527,  ⊢  
  : , :
276instantiation305, 306,  ⊢  
  :
277instantiation390, 333, 527,  ⊢  
  : , :
278instantiation307, 350,  ⊢  
  :
279instantiation308, 309, 310, 328, 311,  ⊢  
  : , : , :
280theorem  ⊢  
 proveit.numbers.negation.double_negation
281instantiation525, 511, 312,  ⊢  
  : , : , :
282instantiation525, 411, 313  ⊢  
  : , : , :
283instantiation525, 494, 314  ⊢  
  : , : , :
284instantiation525, 431, 510  ⊢  
  : , : , :
285theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
286instantiation525, 494, 315  ⊢  
  : , : , :
287theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
288instantiation525, 316, 394  ⊢  
  : , : , :
289instantiation525, 511, 317  ⊢  
  : , : , :
290instantiation525, 511, 481  ⊢  
  : , : , :
291instantiation488, 489, 522  ⊢  
  : , : , :
292instantiation318, 485, 463, 319  ⊢  
  : , : , :
293instantiation484, 485, 320  ⊢  
  : , :
294instantiation525, 349, 432  ⊢  
  : , : , :
295instantiation525, 431, 321  ⊢  
  : , : , :
296theorem  ⊢  
 proveit.numbers.division.div_rational_pos_closure
297instantiation525, 349, 321  ⊢  
  : , : , :
298instantiation525, 327, 322,  ⊢  
  : , : , :
299theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
300instantiation525, 323, 517  ⊢  
  : , : , :
301theorem  ⊢  
 proveit.numbers.exponentiation.exp_even_neg_base_lesseq
302instantiation351, 324, 395,  ⊢  
  : , :
303instantiation325  ⊢  
  :
304instantiation525, 327, 326,  ⊢  
  : , : , :
305theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
306instantiation525, 327, 328,  ⊢  
  : , : , :
307theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
308theorem  ⊢  
 proveit.numbers.division.strong_div_from_denom_bound__all_pos
309instantiation525, 330, 329  ⊢  
  : , : , :
310instantiation525, 330, 331,  ⊢  
  : , : , :
311instantiation332, 474, 333, 380, 334, 335,  ⊢  
  : , : , :
312instantiation525, 336, 337,  ⊢  
  : , : , :
313instantiation525, 431, 492  ⊢  
  : , : , :
314modus ponens338, 339  ⊢  
315instantiation525, 503, 340  ⊢  
  : , : , :
316theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
317instantiation518, 480, 493  ⊢  
  : , :
318theorem  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add_reversed
319theorem  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
320instantiation525, 494, 341  ⊢  
  : , : , :
321theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat4
322instantiation347, 357, 342,  ⊢  
  :
323theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
324instantiation343, 378, 400, 457, 344, 345*,  ⊢  
  : , : , :
325axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
326instantiation347, 378, 346,  ⊢  
  :
327theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
328instantiation347, 380, 348,  ⊢  
  :
329instantiation525, 349, 510  ⊢  
  : , : , :
330theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
331instantiation525, 349, 350,  ⊢  
  : , : , :
332theorem  ⊢  
 proveit.numbers.exponentiation.exp_pos_less
333instantiation398, 399, 386,  ⊢  
  : , :
334instantiation351, 384, 352,  ⊢  
  : , :
335instantiation478, 432  ⊢  
  :
336instantiation512, 499, 481  ⊢  
  : , :
337assumption  ⊢  
338instantiation353  ⊢  
  : , : , :
339generalization354  ⊢  
340instantiation525, 511, 355  ⊢  
  : , : , :
341instantiation525, 503, 356  ⊢  
  : , : , :
342instantiation379, 357, 457, 358,  ⊢  
  : , :
343theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_right_term_bound
344instantiation359, 386, 457, 420, 396, 360, 389*, 361*  ⊢  
  : , : , :
345instantiation483, 362,  ⊢  
  :
346instantiation363, 417, 364, 395,  ⊢  
  : , :
347theorem  ⊢  
 proveit.numbers.exponentiation.sqrd_pos_closure
348instantiation365, 366,  ⊢  
  : , :
349theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
350instantiation367, 368, 527,  ⊢  
  : , :
351theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
352instantiation369, 399, 386, 400, 370,  ⊢  
  : , : , :
353theorem  ⊢  
 proveit.numbers.summation.summation_real_closure
354instantiation371, 495, 372, 373,  ⊢  
  : , :
355instantiation525, 526, 374  ⊢  
  : , : , :
356instantiation525, 511, 520  ⊢  
  : , : , :
357instantiation398, 378, 400,  ⊢  
  : , :
358instantiation375, 376,  ⊢  
  : , :
359theorem  ⊢  
 proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound
360instantiation402, 387  ⊢  
  : , :
361instantiation377, 427  ⊢  
  :
362instantiation525, 494, 378,  ⊢  
  : , : , :
363theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq_int
364theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
365theorem  ⊢  
 proveit.logic.equality.not_equals_symmetry
366instantiation379, 457, 380, 381,  ⊢  
  : , :
367theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
368instantiation382, 383, 384,  ⊢  
  :
369theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_right_term_bound
370instantiation385, 386, 420, 495, 422, 387, 388*, 389*  ⊢  
  : , : , :
371theorem  ⊢  
 proveit.numbers.division.div_real_closure
372instantiation390, 391, 527,  ⊢  
  : , :
373instantiation392, 393, 394,  ⊢  
  : , :
374theorem  ⊢  
 proveit.numbers.numerals.decimals.nat4
375theorem  ⊢  
 proveit.numbers.addition.subtraction.neg_difference
376instantiation506, 395, 396,  ⊢  
  : , : , :
377theorem  ⊢  
 proveit.numbers.multiplication.mult_zero_right
378instantiation525, 503, 397,  ⊢  
  : , : , :
379theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq
380instantiation398, 399, 400,  ⊢  
  : , :
381instantiation423, 401,  ⊢  
  : , :
382theorem  ⊢  
 proveit.numbers.number_sets.integers.nonneg_int_is_natural
383instantiation518, 438, 493,  ⊢  
  : , :
384instantiation402, 403,  ⊢  
  : , :
385theorem  ⊢  
 proveit.numbers.multiplication.reversed_strong_bound_via_right_factor_bound
386instantiation419, 495  ⊢  
  :
387instantiation434, 502  ⊢  
  :
388instantiation404, 485, 405*  ⊢  
  : , :
389instantiation406, 407, 408  ⊢  
  : , : , :
390theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
391instantiation525, 503, 409,  ⊢  
  : , : , :
392theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
393instantiation525, 411, 410,  ⊢  
  : , : , :
394instantiation525, 411, 412  ⊢  
  : , : , :
395instantiation413, 414, 415,  ⊢  
  : , : , :
396instantiation416, 457, 495, 441  ⊢  
  : , : , :
397instantiation525, 511, 417,  ⊢  
  : , : , :
398theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
399instantiation525, 503, 418,  ⊢  
  : , : , :
400instantiation419, 420  ⊢  
  :
401instantiation421, 422, 424,  ⊢  
  : , : , :
402theorem  ⊢  
 proveit.numbers.ordering.relax_less
403instantiation423, 424,  ⊢  
  : , :
404theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_left
405instantiation425, 485  ⊢  
  :
406axiom  ⊢  
 proveit.logic.equality.equals_transitivity
407instantiation426, 517, 527, 446, 448, 447, 427, 449, 450  ⊢  
  : , : , : , : , : , :
408instantiation428, 446, 527, 447, 448, 485, 449, 450, 429*  ⊢  
  : , : , : , : , :
409instantiation525, 511, 451,  ⊢  
  : , : , :
410instantiation525, 431, 430,  ⊢  
  : , : , :
411theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
412instantiation525, 431, 432  ⊢  
  : , : , :
413theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
414instantiation433, 453, 454, 437,  ⊢  
  : , : , :
415instantiation434, 435  ⊢  
  :
416theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
417instantiation525, 436, 437,  ⊢  
  : , : , :
418instantiation525, 511, 438,  ⊢  
  : , : , :
419theorem  ⊢  
 proveit.numbers.negation.real_closure
420instantiation439, 457, 495, 441  ⊢  
  : , : , :
421axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
422instantiation440, 457, 495, 441  ⊢  
  : , : , :
423theorem  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
424instantiation506, 442, 443,  ⊢  
  : , : , :
425theorem  ⊢  
 proveit.numbers.multiplication.elim_one_right
426theorem  ⊢  
 proveit.numbers.multiplication.disassociation
427instantiation444, 485  ⊢  
  :
428theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_any
429instantiation445, 446, 527, 447, 448, 449, 450  ⊢  
  : , : , : , :
430instantiation498, 451, 452,  ⊢  
  :
431theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
432theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
433theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
434theorem  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
435instantiation509, 479  ⊢  
  :
436instantiation512, 453, 454  ⊢  
  : , :
437assumption  ⊢  
438instantiation525, 455, 460,  ⊢  
  : , : , :
439theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
440theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
441theorem  ⊢  
 proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
442instantiation456, 495, 457, 458, 500, 459*  ⊢  
  : , : , :
443instantiation513, 480, 519, 460,  ⊢  
  : , : , :
444theorem  ⊢  
 proveit.numbers.negation.complex_closure
445theorem  ⊢  
 proveit.numbers.multiplication.elim_one_any
446axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
447theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
448instantiation461  ⊢  
  : , :
449instantiation462, 463, 464  ⊢  
  : , :
450instantiation525, 494, 465  ⊢  
  : , : , :
451instantiation525, 466, 482,  ⊢  
  : , : , :
452instantiation506, 467, 468,  ⊢  
  : , : , :
453instantiation518, 469, 514  ⊢  
  : , :
454instantiation523, 480  ⊢  
  :
455instantiation512, 480, 519  ⊢  
  : , :
456theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
457theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
458instantiation525, 503, 470  ⊢  
  : , : , :
459instantiation471, 472, 473  ⊢  
  : , : , :
460assumption  ⊢  
461theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
462theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
463instantiation525, 494, 474  ⊢  
  : , : , :
464instantiation525, 494, 475  ⊢  
  : , : , :
465instantiation476, 477  ⊢  
  :
466instantiation512, 480, 481  ⊢  
  : , :
467instantiation478, 479  ⊢  
  :
468instantiation513, 480, 481, 482,  ⊢  
  : , : , :
469instantiation523, 519  ⊢  
  :
470instantiation525, 511, 499  ⊢  
  : , : , :
471theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
472instantiation483, 485  ⊢  
  :
473instantiation484, 485, 486  ⊢  
  : , :
474instantiation525, 503, 487  ⊢  
  : , : , :
475instantiation488, 489, 490  ⊢  
  : , : , :
476theorem  ⊢  
 proveit.physics.quantum.QPE._delta_b_is_real
477theorem  ⊢  
 proveit.physics.quantum.QPE._best_floor_is_int
478theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
479instantiation491, 492, 510  ⊢  
  : , :
480instantiation518, 499, 514  ⊢  
  : , :
481instantiation518, 519, 493  ⊢  
  : , :
482assumption  ⊢  
483theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
484theorem  ⊢  
 proveit.numbers.addition.commutation
485instantiation525, 494, 495  ⊢  
  : , : , :
486theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
487instantiation525, 511, 524  ⊢