Theory "transc"

Signature

Definitions

atn

|- ∀y. atn y = @x. -(pi / 2) < x ∧ x < pi / 2 ∧ (tan x = y)

acs

|- ∀y. acs y = @x. 0 ≤ x ∧ x ≤ pi ∧ (cos x = y)

asn

|- ∀y. asn y = @x. -(pi / 2) ≤ x ∧ x ≤ pi / 2 ∧ (sin x = y)

tan

|- ∀x. tan x = sin x / cos x

pi

|- pi = 2 * @x. 0 ≤ x ∧ x ≤ 2 ∧ (cos x = 0)

sqrt

|- ∀x. sqrt x = root 2 x

root

|- ∀n x. root n x = @u. (0 < x ⇒ 0 < u) ∧ (u pow n = x)

exp

|- ∀x. exp x = suminf (λn. (λn. inv (&FACT n)) n * x pow n)

cos

|- ∀x.
     cos x =
     suminf
       (λn.
          (λn. if EVEN n then -1 pow (n DIV 2) / &FACT n else 0) n * x pow n)

sin

|- ∀x.
     sin x =
     suminf
       (λn.
          (λn. if EVEN n then 0 else -1 pow ((n − 1) DIV 2) / &FACT n) n *
          x pow n)

ln

|- ∀x. ln x = @u. exp u = x

division

|- ∀a b D.
     division (a,b) D ⇔
     (D 0 = a) ∧ ∃N. (∀n. n < N ⇒ D n < D (SUC n)) ∧ ∀n. n ≥ N ⇒ (D n = b)

dsize

|- ∀D. dsize D = @N. (∀n. n < N ⇒ D n < D (SUC n)) ∧ ∀n. n ≥ N ⇒ (D n = D N)

tdiv

|- ∀a b D p.
     tdiv (a,b) (D,p) ⇔ division (a,b) D ∧ ∀n. D n ≤ p n ∧ p n ≤ D (SUC n)

gauge

|- ∀E g. gauge E g ⇔ ∀x. E x ⇒ 0 < g x

fine

|- ∀g D p. fine g (D,p) ⇔ ∀n. n < dsize D ⇒ D (SUC n) − D n < g (p n)

rsum

|- ∀D p f. rsum (D,p) f = sum (0,dsize D) (λn. f (p n) * (D (SUC n) − D n))

Dint

|- ∀a b f k.
     Dint (a,b) f k ⇔
     ∀e.
       0 < e ⇒
       ∃g.
         gauge (λx. a ≤ x ∧ x ≤ b) g ∧
         ∀D p. tdiv (a,b) (D,p) ∧ fine g (D,p) ⇒ abs (rsum (D,p) f − k) < e

rpow_def

|- ∀a b. a rpow b = exp (b * ln a)

Theorems

SIN_COS_SQRT

|- ∀x. 0 ≤ sin x ⇒ (sin x = sqrt (1 − cos x pow 2))

COS_SIN_SQRT

|- ∀x. 0 ≤ cos x ⇒ (cos x = sqrt (1 − sin x pow 2))

SIN_ACS_NZ

|- ∀x. -1 < x ∧ x < 1 ⇒ sin (acs x) ≠ 0

COS_ASN_NZ

|- ∀x. -1 < x ∧ x < 1 ⇒ cos (asn x) ≠ 0

COS_ATN_NZ

|- ∀x. cos (atn x) ≠ 0

COS_SIN_SQ

|- ∀x. -(pi / 2) ≤ x ∧ x ≤ pi / 2 ⇒ (cos x = sqrt (1 − sin x pow 2))

SIN_COS_SQ

|- ∀x. 0 ≤ x ∧ x ≤ pi ⇒ (sin x = sqrt (1 − cos x pow 2))

TAN_SEC

|- ∀x. cos x ≠ 0 ⇒ (1 + tan x pow 2 = inv (cos x) pow 2)

TAN_ATN

|- ∀x. -(pi / 2) < x ∧ x < pi / 2 ⇒ (atn (tan x) = x)

ATN_BOUNDS

|- ∀y. -(pi / 2) < atn y ∧ atn y < pi / 2

ATN_TAN

|- ∀y. tan (atn y) = y

ATN

|- ∀y. -(pi / 2) < atn y ∧ atn y < pi / 2 ∧ (tan (atn y) = y)

COS_ACS

|- ∀x. 0 ≤ x ∧ x ≤ pi ⇒ (acs (cos x) = x)

ACS_BOUNDS_LT

|- ∀y. -1 < y ∧ y < 1 ⇒ 0 < acs y ∧ acs y < pi

ACS_BOUNDS

|- ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ 0 ≤ acs y ∧ acs y ≤ pi

ACS_COS

|- ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ (cos (acs y) = y)

ACS

|- ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ 0 ≤ acs y ∧ acs y ≤ pi ∧ (cos (acs y) = y)

SIN_ASN

|- ∀x. -(pi / 2) ≤ x ∧ x ≤ pi / 2 ⇒ (asn (sin x) = x)

ASN_BOUNDS_LT

|- ∀y. -1 < y ∧ y < 1 ⇒ -(pi / 2) < asn y ∧ asn y < pi / 2

ASN_BOUNDS

|- ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ -(pi / 2) ≤ asn y ∧ asn y ≤ pi / 2

ASN_SIN

|- ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ (sin (asn y) = y)

ASN

|- ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ -(pi / 2) ≤ asn y ∧ asn y ≤ pi / 2 ∧ (sin (asn y) = y)

TAN_TOTAL

|- ∀y. ∃!x. -(pi / 2) < x ∧ x < pi / 2 ∧ (tan x = y)

TAN_TOTAL_POS

|- ∀y. 0 ≤ y ⇒ ∃x. 0 ≤ x ∧ x < pi / 2 ∧ (tan x = y)

TAN_TOTAL_LEMMA

|- ∀y. 0 < y ⇒ ∃x. 0 < x ∧ x < pi / 2 ∧ y < tan x

DIFF_TAN

|- ∀x. cos x ≠ 0 ⇒ (tan diffl inv (cos x pow 2)) x

TAN_POS_PI2

|- ∀x. 0 < x ∧ x < pi / 2 ⇒ 0 < tan x

TAN_DOUBLE

|- ∀x.
     cos x ≠ 0 ∧ cos (2 * x) ≠ 0 ⇒
     (tan (2 * x) = 2 * tan x / (1 − tan x pow 2))

TAN_ADD

|- ∀x y.
     cos x ≠ 0 ∧ cos y ≠ 0 ∧ cos (x + y) ≠ 0 ⇒
     (tan (x + y) = (tan x + tan y) / (1 − tan x * tan y))

TAN_PERIODIC

|- ∀x. tan (x + 2 * pi) = tan x

TAN_NEG

|- ∀x. tan (-x) = -tan x

TAN_NPI

|- ∀n. tan (&n * pi) = 0

TAN_PI

|- tan pi = 0

TAN_0

|- tan 0 = 0

SIN_ZERO

|- ∀x.
     (sin x = 0) ⇔
     (∃n. EVEN n ∧ (x = &n * (pi / 2))) ∨ ∃n. EVEN n ∧ (x = -(&n * (pi / 2)))

COS_ZERO

|- ∀x.
     (cos x = 0) ⇔
     (∃n. ¬EVEN n ∧ (x = &n * (pi / 2))) ∨
     ∃n. ¬EVEN n ∧ (x = -(&n * (pi / 2)))

SIN_ZERO_LEMMA

|- ∀x. 0 ≤ x ∧ (sin x = 0) ⇒ ∃n. EVEN n ∧ (x = &n * (pi / 2))

COS_ZERO_LEMMA

|- ∀x. 0 ≤ x ∧ (cos x = 0) ⇒ ∃n. ¬EVEN n ∧ (x = &n * (pi / 2))

SIN_TOTAL

|- ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ ∃!x. -(pi / 2) ≤ x ∧ x ≤ pi / 2 ∧ (sin x = y)

COS_TOTAL

|- ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ ∃!x. 0 ≤ x ∧ x ≤ pi ∧ (cos x = y)

SIN_POS_PI_LE

|- ∀x. 0 ≤ x ∧ x ≤ pi ⇒ 0 ≤ sin x

SIN_POS_PI2_LE

|- ∀x. 0 ≤ x ∧ x ≤ pi / 2 ⇒ 0 ≤ sin x

COS_POS_PI_LE

|- ∀x. -(pi / 2) ≤ x ∧ x ≤ pi / 2 ⇒ 0 ≤ cos x

COS_POS_PI2_LE

|- ∀x. 0 ≤ x ∧ x ≤ pi / 2 ⇒ 0 ≤ cos x

SIN_POS_PI

|- ∀x. 0 < x ∧ x < pi ⇒ 0 < sin x

COS_POS_PI

|- ∀x. -(pi / 2) < x ∧ x < pi / 2 ⇒ 0 < cos x

COS_POS_PI2

|- ∀x. 0 < x ∧ x < pi / 2 ⇒ 0 < cos x

SIN_POS_PI2

|- ∀x. 0 < x ∧ x < pi / 2 ⇒ 0 < sin x

SIN_NPI

|- ∀n. sin (&n * pi) = 0

COS_NPI

|- ∀n. cos (&n * pi) = -1 pow n

COS_PERIODIC

|- ∀x. cos (x + 2 * pi) = cos x

SIN_PERIODIC

|- ∀x. sin (x + 2 * pi) = sin x

COS_PERIODIC_PI

|- ∀x. cos (x + pi) = -cos x

SIN_PERIODIC_PI

|- ∀x. sin (x + pi) = -sin x

COS_SIN

|- ∀x. cos x = sin (pi / 2 − x)

SIN_COS

|- ∀x. sin x = cos (pi / 2 − x)

SIN_PI

|- sin pi = 0

COS_PI

|- cos pi = -1

SIN_PI2

|- sin (pi / 2) = 1

PI_POS

|- 0 < pi

PI2_BOUNDS

|- 0 < pi / 2 ∧ pi / 2 < 2

COS_PI2

|- cos (pi / 2) = 0

PI2

|- pi / 2 = @x. 0 ≤ x ∧ x ≤ 2 ∧ (cos x = 0)

COS_ISZERO

|- ∃!x. 0 ≤ x ∧ x ≤ 2 ∧ (cos x = 0)

COS_2

|- cos 2 < 0

COS_PAIRED

|- ∀x. (λn. -1 pow n / &FACT (2 * n) * x pow (2 * n)) sums cos x

SIN_POS

|- ∀x. 0 < x ∧ x < 2 ⇒ 0 < sin x

SIN_PAIRED

|- ∀x. (λn. -1 pow n / &FACT (2 * n + 1) * x pow (2 * n + 1)) sums sin x

COS_DOUBLE

|- ∀x. cos (2 * x) = cos x pow 2 − sin x pow 2

SIN_DOUBLE

|- ∀x. sin (2 * x) = 2 * (sin x * cos x)

COS_NEG

|- ∀x. cos (-x) = cos x

SIN_NEG

|- ∀x. sin (-x) = -sin x

COS_ADD

|- ∀x y. cos (x + y) = cos x * cos y − sin x * sin y

SIN_ADD

|- ∀x y. sin (x + y) = sin x * cos y + cos x * sin y

SIN_COS_NEG

|- ∀x. (sin (-x) + sin x) pow 2 + (cos (-x) − cos x) pow 2 = 0

SIN_COS_ADD

|- ∀x y.
     (sin (x + y) − (sin x * cos y + cos x * sin y)) pow 2 +
     (cos (x + y) − (cos x * cos y − sin x * sin y)) pow 2 =
     0

COS_BOUNDS

|- ∀x. -1 ≤ cos x ∧ cos x ≤ 1

COS_BOUND

|- ∀x. abs (cos x) ≤ 1

SIN_BOUNDS

|- ∀x. -1 ≤ sin x ∧ sin x ≤ 1

SIN_BOUND

|- ∀x. abs (sin x) ≤ 1

SIN_CIRCLE

|- ∀x. sin x pow 2 + cos x pow 2 = 1

COS_0

|- cos 0 = 1

SIN_0

|- sin 0 = 0

SQRT_EQ

|- ∀x y. (x pow 2 = y) ∧ 0 ≤ x ⇒ (x = sqrt y)

REAL_DIV_SQRT

|- ∀x. 0 ≤ x ⇒ (x / sqrt x = sqrt x)

SQRT_EVEN_POW2

|- ∀n. EVEN n ⇒ (sqrt (2 pow n) = 2 pow (n DIV 2))

SQRT_MONO_LE

|- ∀x y. 0 ≤ x ∧ x ≤ y ⇒ sqrt x ≤ sqrt y

SQRT_DIV

|- ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ (sqrt (x / y) = sqrt x / sqrt y)

SQRT_INV

|- ∀x. 0 ≤ x ⇒ (sqrt (inv x) = inv (sqrt x))

SQRT_MUL

|- ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ (sqrt (x * y) = sqrt x * sqrt y)

SQRT_POS_UNIQ

|- ∀x y. 0 ≤ x ∧ 0 ≤ y ∧ (y pow 2 = x) ⇒ (sqrt x = y)

POW_2_SQRT

|- 0 ≤ x ⇒ (sqrt (x pow 2) = x)

SQRT_POW_2

|- ∀x. 0 ≤ x ⇒ (sqrt x pow 2 = x)

SQRT_POW2

|- ∀x. (sqrt x pow 2 = x) ⇔ 0 ≤ x

SQRT_POS_LE

|- ∀x. 0 ≤ x ⇒ 0 ≤ sqrt x

SQRT_POS_LT

|- ∀x. 0 < x ⇒ 0 < sqrt x

SQRT_1

|- sqrt 1 = 1

SQRT_0

|- sqrt 0 = 0

ROOT_MONO_LE

|- ∀x y. 0 ≤ x ∧ x ≤ y ⇒ root (SUC n) x ≤ root (SUC n) y

ROOT_DIV

|- ∀n x y.
     0 ≤ x ∧ 0 ≤ y ⇒ (root (SUC n) (x / y) = root (SUC n) x / root (SUC n) y)

ROOT_INV

|- ∀n x. 0 ≤ x ⇒ (root (SUC n) (inv x) = inv (root (SUC n) x))

ROOT_MUL

|- ∀n x y.
     0 ≤ x ∧ 0 ≤ y ⇒ (root (SUC n) (x * y) = root (SUC n) x * root (SUC n) y)

ROOT_POS_UNIQ

|- ∀n x y. 0 ≤ x ∧ 0 ≤ y ∧ (y pow SUC n = x) ⇒ (root (SUC n) x = y)

ROOT_POS

|- ∀n x. 0 ≤ x ⇒ 0 ≤ root (SUC n) x

POW_ROOT_POS

|- ∀n x. 0 ≤ x ⇒ (root (SUC n) (x pow SUC n) = x)

ROOT_POW_POS

|- ∀n x. 0 ≤ x ⇒ (root (SUC n) x pow SUC n = x)

ROOT_POS_LT

|- ∀n x. 0 < x ⇒ 0 < root (SUC n) x

ROOT_1

|- ∀n. root (SUC n) 1 = 1

ROOT_0

|- ∀n. root (SUC n) 0 = 0

ROOT_LN

|- ∀n x. 0 < x ⇒ (root (SUC n) x = exp (ln x / &SUC n))

ROOT_LT_LEMMA

|- ∀n x. 0 < x ⇒ (exp (ln x / &SUC n) pow SUC n = x)

EXP_CONVERGES

|- ∀x. (λn. (λn. inv (&FACT n)) n * x pow n) sums exp x

SIN_CONVERGES

|- ∀x.
     (λn.
        (λn. if EVEN n then 0 else -1 pow ((n − 1) DIV 2) / &FACT n) n *
        x pow n) sums sin x

COS_CONVERGES

|- ∀x.
     (λn.
        (λn. if EVEN n then -1 pow (n DIV 2) / &FACT n else 0) n *
        x pow n) sums cos x

EXP_FDIFF

|- diffs (λn. inv (&FACT n)) = (λn. inv (&FACT n))

SIN_FDIFF

|- diffs (λn. if EVEN n then 0 else -1 pow ((n − 1) DIV 2) / &FACT n) =
   (λn. if EVEN n then -1 pow (n DIV 2) / &FACT n else 0)

COS_FDIFF

|- diffs (λn. if EVEN n then -1 pow (n DIV 2) / &FACT n else 0) =
   (λn. -(λn. if EVEN n then 0 else -1 pow ((n − 1) DIV 2) / &FACT n) n)

SIN_NEGLEMMA

|- ∀x.
     -sin x =
     suminf
       (λn.
          -((λn. if EVEN n then 0 else -1 pow ((n − 1) DIV 2) / &FACT n) n *
            x pow n))

DIFF_EXP

|- ∀x. (exp diffl exp x) x

DIFF_SIN

|- ∀x. (sin diffl cos x) x

DIFF_COS

|- ∀x. (cos diffl -sin x) x

DIFF_COMPOSITE

|- ((f diffl l) x ∧ f x ≠ 0 ⇒ ((λx. inv (f x)) diffl -(l / f x pow 2)) x) ∧
   ((f diffl l) x ∧ (g diffl m) x ∧ g x ≠ 0 ⇒
    ((λx. f x / g x) diffl ((l * g x − m * f x) / g x pow 2)) x) ∧
   ((f diffl l) x ∧ (g diffl m) x ⇒ ((λx. f x + g x) diffl (l + m)) x) ∧
   ((f diffl l) x ∧ (g diffl m) x ⇒
    ((λx. f x * g x) diffl (l * g x + m * f x)) x) ∧
   ((f diffl l) x ∧ (g diffl m) x ⇒ ((λx. f x − g x) diffl (l − m)) x) ∧
   ((f diffl l) x ⇒ ((λx. -f x) diffl -l) x) ∧
   ((g diffl m) x ⇒ ((λx. g x pow n) diffl (&n * g x pow (n − 1) * m)) x) ∧
   ((g diffl m) x ⇒ ((λx. exp (g x)) diffl (exp (g x) * m)) x) ∧
   ((g diffl m) x ⇒ ((λx. sin (g x)) diffl (cos (g x) * m)) x) ∧
   ((g diffl m) x ⇒ ((λx. cos (g x)) diffl (-sin (g x) * m)) x)

EXP_0

|- exp 0 = 1

EXP_LE_X

|- ∀x. 0 ≤ x ⇒ 1 + x ≤ exp x

EXP_LT_1

|- ∀x. 0 < x ⇒ 1 < exp x

EXP_ADD_MUL

|- ∀x y. exp (x + y) * exp (-x) = exp y

EXP_NEG_MUL

|- ∀x. exp x * exp (-x) = 1

EXP_NEG_MUL2

|- ∀x. exp (-x) * exp x = 1

EXP_NEG

|- ∀x. exp (-x) = inv (exp x)

EXP_ADD

|- ∀x y. exp (x + y) = exp x * exp y

EXP_POS_LE

|- ∀x. 0 ≤ exp x

EXP_NZ

|- ∀x. exp x ≠ 0

EXP_POS_LT

|- ∀x. 0 < exp x

EXP_N

|- ∀n x. exp (&n * x) = exp x pow n

EXP_SUB

|- ∀x y. exp (x − y) = exp x / exp y

EXP_MONO_IMP

|- ∀x y. x < y ⇒ exp x < exp y

EXP_MONO_LT

|- ∀x y. exp x < exp y ⇔ x < y

EXP_MONO_LE

|- ∀x y. exp x ≤ exp y ⇔ x ≤ y

EXP_INJ

|- ∀x y. (exp x = exp y) ⇔ (x = y)

EXP_TOTAL_LEMMA

|- ∀y. 1 ≤ y ⇒ ∃x. 0 ≤ x ∧ x ≤ y − 1 ∧ (exp x = y)

EXP_TOTAL

|- ∀y. 0 < y ⇒ ∃x. exp x = y

LN_EXP

|- ∀x. ln (exp x) = x

EXP_LN

|- ∀x. (exp (ln x) = x) ⇔ 0 < x

LN_MUL

|- ∀x y. 0 < x ∧ 0 < y ⇒ (ln (x * y) = ln x + ln y)

LN_INJ

|- ∀x y. 0 < x ∧ 0 < y ⇒ ((ln x = ln y) ⇔ (x = y))

LN_1

|- ln 1 = 0

LN_INV

|- ∀x. 0 < x ⇒ (ln (inv x) = -ln x)

LN_DIV

|- ∀x y. 0 < x ∧ 0 < y ⇒ (ln (x / y) = ln x − ln y)

LN_MONO_LT

|- ∀x y. 0 < x ∧ 0 < y ⇒ (ln x < ln y ⇔ x < y)

LN_MONO_LE

|- ∀x y. 0 < x ∧ 0 < y ⇒ (ln x ≤ ln y ⇔ x ≤ y)

LN_POW

|- ∀n x. 0 < x ⇒ (ln (x pow n) = &n * ln x)

LN_LE

|- ∀x. 0 ≤ x ⇒ ln (1 + x) ≤ x

LN_LT_X

|- ∀x. 0 < x ⇒ ln x < x

LN_POS

|- ∀x. 1 ≤ x ⇒ 0 ≤ ln x

DIFF_LN

|- ∀x. 0 < x ⇒ (ln diffl inv x) x

DIFF_ASN_LEMMA

|- ∀x. -1 < x ∧ x < 1 ⇒ (asn diffl inv (cos (asn x))) x

DIFF_ASN

|- ∀x. -1 < x ∧ x < 1 ⇒ (asn diffl inv (sqrt (1 − x pow 2))) x

DIFF_ACS_LEMMA

|- ∀x. -1 < x ∧ x < 1 ⇒ (acs diffl inv (-sin (acs x))) x

DIFF_ACS

|- ∀x. -1 < x ∧ x < 1 ⇒ (acs diffl -inv (sqrt (1 − x pow 2))) x

DIFF_ATN

|- ∀x. (atn diffl inv (1 + x pow 2)) x

DIVISION_0

|- ∀a b. (a = b) ⇒ (dsize (λn. if n = 0 then a else b) = 0)

DIVISION_1

|- ∀a b. a < b ⇒ (dsize (λn. if n = 0 then a else b) = 1)

DIVISION_SINGLE

|- ∀a b. a ≤ b ⇒ division (a,b) (λn. if n = 0 then a else b)

DIVISION_LHS

|- ∀D a b. division (a,b) D ⇒ (D 0 = a)

DIVISION_THM

|- ∀D a b.
     division (a,b) D ⇔
     (D 0 = a) ∧ (∀n. n < dsize D ⇒ D n < D (SUC n)) ∧
     ∀n. n ≥ dsize D ⇒ (D n = b)

DIVISION_RHS

|- ∀D a b. division (a,b) D ⇒ (D (dsize D) = b)

DIVISION_LT_GEN

|- ∀D a b m n. division (a,b) D ∧ m < n ∧ n ≤ dsize D ⇒ D m < D n

DIVISION_LT

|- ∀D a b. division (a,b) D ⇒ ∀n. n < dsize D ⇒ D 0 < D (SUC n)

DIVISION_LE

|- ∀D a b. division (a,b) D ⇒ a ≤ b

DIVISION_GT

|- ∀D a b. division (a,b) D ⇒ ∀n. n < dsize D ⇒ D n < D (dsize D)

DIVISION_EQ

|- ∀D a b. division (a,b) D ⇒ ((a = b) ⇔ (dsize D = 0))

DIVISION_LBOUND

|- ∀D a b. division (a,b) D ⇒ ∀r. a ≤ D r

DIVISION_LBOUND_LT

|- ∀D a b. division (a,b) D ∧ dsize D ≠ 0 ⇒ ∀n. a < D (SUC n)

DIVISION_UBOUND

|- ∀D a b. division (a,b) D ⇒ ∀r. D r ≤ b

DIVISION_UBOUND_LT

|- ∀D a b n. division (a,b) D ∧ n < dsize D ⇒ D n < b

DIVISION_APPEND

|- ∀a b c.
     (∃D1 p1. tdiv (a,b) (D1,p1) ∧ fine g (D1,p1)) ∧
     (∃D2 p2. tdiv (b,c) (D2,p2) ∧ fine g (D2,p2)) ⇒
     ∃D p. tdiv (a,c) (D,p) ∧ fine g (D,p)

DIVISION_EXISTS

|- ∀a b g.
     a ≤ b ∧ gauge (λx. a ≤ x ∧ x ≤ b) g ⇒
     ∃D p. tdiv (a,b) (D,p) ∧ fine g (D,p)

GAUGE_MIN

|- ∀E g1 g2.
     gauge E g1 ∧ gauge E g2 ⇒
     gauge E (λx. if g1 x < g2 x then g1 x else g2 x)

FINE_MIN

|- ∀g1 g2 D p.
     fine (λx. if g1 x < g2 x then g1 x else g2 x) (D,p) ⇒
     fine g1 (D,p) ∧ fine g2 (D,p)

DINT_UNIQ

|- ∀a b f k1 k2. a ≤ b ∧ Dint (a,b) f k1 ∧ Dint (a,b) f k2 ⇒ (k1 = k2)

INTEGRAL_NULL

|- ∀f a. Dint (a,a) f 0

FTC1

|- ∀f f' a b.
     a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ (f diffl f' x) x) ⇒
     Dint (a,b) f' (f b − f a)

MCLAURIN

|- ∀f diff h n.
     0 < h ∧ 0 < n ∧ (diff 0 = f) ∧
     (∀m t. m < n ∧ 0 ≤ t ∧ t ≤ h ⇒ (diff m diffl diff (SUC m) t) t) ⇒
     ∃t.
       0 < t ∧ t < h ∧
       (f h =
        sum (0,n) (λm. diff m 0 / &FACT m * h pow m) +
        diff n t / &FACT n * h pow n)

MCLAURIN_NEG

|- ∀f diff h n.
     h < 0 ∧ 0 < n ∧ (diff 0 = f) ∧
     (∀m t. m < n ∧ h ≤ t ∧ t ≤ 0 ⇒ (diff m diffl diff (SUC m) t) t) ⇒
     ∃t.
       h < t ∧ t < 0 ∧
       (f h =
        sum (0,n) (λm. diff m 0 / &FACT m * h pow m) +
        diff n t / &FACT n * h pow n)

MCLAURIN_ALL_LT

|- ∀f diff.
     (diff 0 = f) ∧ (∀m x. (diff m diffl diff (SUC m) x) x) ⇒
     ∀x n.
       x ≠ 0 ∧ 0 < n ⇒
       ∃t.
         0 < abs t ∧ abs t < abs x ∧
         (f x =
          sum (0,n) (λm. diff m 0 / &FACT m * x pow m) +
          diff n t / &FACT n * x pow n)

MCLAURIN_ZERO

|- ∀diff n x.
     (x = 0) ∧ 0 < n ⇒
     (sum (0,n) (λm. diff m 0 / &FACT m * x pow m) = diff 0 0)

MCLAURIN_ALL_LE

|- ∀f diff.
     (diff 0 = f) ∧ (∀m x. (diff m diffl diff (SUC m) x) x) ⇒
     ∀x n.
       ∃t.
         abs t ≤ abs x ∧
         (f x =
          sum (0,n) (λm. diff m 0 / &FACT m * x pow m) +
          diff n t / &FACT n * x pow n)

MCLAURIN_EXP_LT

|- ∀x n.
     x ≠ 0 ∧ 0 < n ⇒
     ∃t.
       0 < abs t ∧ abs t < abs x ∧
       (exp x = sum (0,n) (λm. x pow m / &FACT m) + exp t / &FACT n * x pow n)

MCLAURIN_EXP_LE

|- ∀x n.
     ∃t.
       abs t ≤ abs x ∧
       (exp x = sum (0,n) (λm. x pow m / &FACT m) + exp t / &FACT n * x pow n)

DIFF_LN_COMPOSITE

|- ∀g m x. (g diffl m) x ∧ 0 < g x ⇒ ((λx. ln (g x)) diffl (inv (g x) * m)) x

GEN_RPOW

|- ∀a n. 0 < a ⇒ (a pow n = a rpow &n)

RPOW_SUC_N

|- ∀a n. 0 < a ⇒ (a rpow (&n + 1) = a pow SUC n)

RPOW_0

|- ∀a. 0 < a ⇒ (a rpow 0 = 1)

RPOW_1

|- ∀a. 0 < a ⇒ (a rpow 1 = a)

ONE_RPOW

|- ∀a. 0 < a ⇒ (1 rpow a = 1)

RPOW_POS_LT

|- ∀a b. 0 < a ⇒ 0 < a rpow b

RPOW_NZ

|- ∀a b. 0 ≠ a ⇒ a rpow b ≠ 0

LN_RPOW

|- ∀a b. 0 < a ⇒ (ln (a rpow b) = b * ln a)

RPOW_ADD

|- ∀a b c. a rpow (b + c) = a rpow b * a rpow c

RPOW_ADD_MUL

|- ∀a b c. a rpow (b + c) * a rpow -b = a rpow c

RPOW_SUB

|- ∀a b c. a rpow (b − c) = a rpow b / a rpow c

RPOW_DIV

|- ∀a b c. 0 < a ∧ 0 < b ⇒ ((a / b) rpow c = a rpow c / b rpow c)

RPOW_INV

|- ∀a b. 0 < a ⇒ (inv a rpow b = inv (a rpow b))

RPOW_MUL

|- ∀a b c. 0 < a ∧ 0 < b ⇒ ((a * b) rpow c = a rpow c * b rpow c)

RPOW_RPOW

|- ∀a b c. 0 < a ⇒ ((a rpow b) rpow c = a rpow (b * c))

RPOW_LT

|- ∀a b c. 1 < a ⇒ (a rpow b < a rpow c ⇔ b < c)

RPOW_LE

|- ∀a b c. 1 < a ⇒ (a rpow b ≤ a rpow c ⇔ b ≤ c)

BASE_RPOW_LE

|- ∀a b c. 0 < a ∧ 0 < c ∧ 0 < b ⇒ (a rpow b ≤ c rpow b ⇔ a ≤ c)

BASE_RPOW_LT

|- ∀a b c. 0 < a ∧ 0 < c ∧ 0 < b ⇒ (a rpow b < c rpow b ⇔ a < c)

RPOW_UNIQ_BASE

|- ∀a b c. 0 < a ∧ 0 < c ∧ 0 ≠ b ∧ (a rpow b = c rpow b) ⇒ (a = c)

RPOW_UNIQ_EXP

|- ∀a b c. 1 < a ∧ 0 < c ∧ 0 < b ∧ (a rpow b = a rpow c) ⇒ (b = c)

RPOW_DIV_BASE

|- ∀x t. 0 < x ⇒ (x rpow t / x = x rpow (t − 1))

DIFF_COMPOSITE_EXP

|- ∀g m x. (g diffl m) x ⇒ ((λx. exp (g x)) diffl (exp (g x) * m)) x

DIFF_RPOW

|- ∀x y. 0 < x ⇒ ((λx. x rpow y) diffl (y * x rpow (y − 1))) x