The Mathematica Journal
Departments
Feature Articles
Columns
New Products
New Publications
Classifieds
Calendar
News Bulletins
Mailbox
Letters
FAQ
Write Us
About the Journal
Staff and Contributors
Submissions
Subscriptions
Advertising
Back Issues
Home
Download this Issue

A Proof Generated by Theorema

Prove:

under the assumptions:

We assume

and show

Formula (1.1), by (Definition (limit:)), implies:

By (3), we can take an appropriate Skolem function such that

Formula (1.2), by (Definition (limit:)), implies:

By (5), we can take an appropriate Skolem function such that

Formula (2), using (Definition (limit:)), is implied by:

We assume

and show

We have to find such that

Formula (10), using (Definition (+:)), is implied by:

Formula (11), using (Lemma(|+|)), is implied by:

We have to find , and such that

Formula (13), using (6), is implied by:

which, using (4), is implied by:

which, using (Lemma (max)), is implied by:

Formula (14) is implied by:

Partially solving it, formula (15) is implied by:

Now,

can be solved for and by a call to Collins' CAD method yielding the solution

Let us take

Formula (16) is solved. Hence, we are done.


Copyright © 2001 Wolfram Media, Inc. All rights reserved.

[Article Index][Prev Page][Next Page]