Theory "transc"

Parents powser

Signature

Constant	Type
Dint	:complex -> (real -> real) -> real -> bool
acs	:real -> real
asn	:real -> real
atn	:real -> real
cos	:real -> real
division	:complex -> (num -> real) -> bool
dsize	:(num -> real) -> num
exp	:real -> real
fine	:(real -> real) -> (num -> real) set_relation$reln
gauge	:(real -> bool) -> (real -> real) -> bool
ln	:real -> real
pi	:real
root	:num -> real -> real
rpow	:real -> real -> real
rsum	:(num -> real) # (num -> real) -> (real -> real) -> real
sin	:real -> real
sqrt	:real -> real
tan	:real -> real
tdiv	:complex -> (num -> real) set_relation$reln

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. (&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 = (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 (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 x⁻¹ = (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) x⁻¹ = (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. (&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. (&FACT n)⁻¹) = (λn. (&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. (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) = (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 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 x⁻¹) x

DIFF_ASN_LEMMA

⊢ ∀x. -1 < x ∧ x < 1 ⇒ (asn diffl (cos (asn x))⁻¹) x

DIFF_ASN

⊢ ∀x. -1 < x ∧ x < 1 ⇒ (asn diffl (sqrt (1 − x pow 2))⁻¹) x

DIFF_ACS_LEMMA

⊢ ∀x. -1 < x ∧ x < 1 ⇒ (acs diffl (-sin (acs x))⁻¹) x

DIFF_ACS

⊢ ∀x. -1 < x ∧ x < 1 ⇒ (acs diffl -(sqrt (1 − x pow 2))⁻¹) x

DIFF_ATN

⊢ ∀x. (atn diffl (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 ((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 ⇒ a⁻¹ rpow b = (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