Theory "transc"

Parents powser

Signature

Constant	Type
Dint	:real # real -> (real -> real) -> real -> bool
acs	:real -> real
asn	:real -> real
atn	:real -> real
cos	:real -> real
division	:real # real -> (num -> real) -> bool
dsize	:(num -> real) -> num
exp	:real -> real
fine	:(real -> real) -> (num -> real) # (num -> real) -> bool
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	:real # real -> (num -> real) # (num -> real) -> bool

Definitions

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

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)

atn

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

cos

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

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)

exp

⊢ ∀x. exp x = suminf (λn. (λn. (&FACT n)⁻¹) n * x pow n)

fine

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

gauge

⊢ ∀E g. gauge E g ⇔ ∀x. E x ⇒ 0 < g x

ln

⊢ ∀x. ln x = @u. exp u = x

pi

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

root

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

rpow_def

⊢ ∀a b. a powr b = exp (b * ln a)

rsum

⊢ ∀D p f. rsum (D,p) f = sum (0,dsize D) (λn. f (p n) * (D (SUC n) − D 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)

sqrt

⊢ ∀x. sqrt x = root 2 x

tan

⊢ ∀x. tan x = sin x / cos x

tdiv

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

Theorems

ACS

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

ACS_BOUNDS

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

ACS_BOUNDS_LT

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

ACS_COS

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

ASN

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

ASN_BOUNDS

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

ASN_BOUNDS_LT

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

ASN_SIN

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

ATN

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

ATN_BOUNDS

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

ATN_TAN

⊢ ∀y. tan (atn y) = y

BASE_RPOW_LE

⊢ ∀a b c. 0 < a ∧ 0 < c ∧ 0 < b ⇒ (a powr b ≤ c powr b ⇔ a ≤ c)

BASE_RPOW_LT

⊢ ∀a b c. 0 < a ∧ 0 < c ∧ 0 < b ⇒ (a powr b < c powr b ⇔ a < c)

COS_0

⊢ cos 0 = 1

COS_2

⊢ cos 2 < 0

COS_ACS

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

COS_ADD

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

COS_ASN_NZ

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

COS_ATN_NZ

⊢ ∀x. cos (atn x) ≠ 0

COS_BOUND

⊢ ∀x. abs (cos x) ≤ 1

COS_BOUNDS

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

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

COS_DOUBLE

⊢ ∀x. cos (2 * x) = (cos x)² − (sin x)²

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)

COS_ISZERO

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

COS_NEG

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

COS_NPI

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

COS_PAIRED

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

COS_PERIODIC

⊢ ∀x. cos (x + 2 * pi) = cos x

COS_PERIODIC_PI

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

COS_PI

⊢ cos pi = -1

COS_PI2

⊢ cos (pi / 2) = 0

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

COS_POS_PI2_LE

⊢ ∀x. 0 ≤ x ∧ x ≤ pi / 2 ⇒ 0 ≤ cos x

COS_POS_PI_LE

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

COS_SIN

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

COS_SIN_SQ

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

COS_SIN_SQRT

⊢ ∀x. 0 ≤ cos x ⇒ (cos x = sqrt (1 − (sin x)²))

COS_TOTAL

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

COS_ZERO

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

COS_ZERO_LEMMA

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

DIFF_ACS

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

DIFF_ACS_LEMMA

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

DIFF_ASN

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

DIFF_ASN_LEMMA

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

DIFF_ATN

⊢ ∀x. (atn diffl (1 + x²)⁻¹) x

DIFF_COMPOSITE

⊢ ((f diffl l) x ∧ f x ≠ 0 ⇒ ((λx. (f x)⁻¹) diffl -(l / (f x)²)) 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)²)) 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)

DIFF_COMPOSITE_EXP

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

DIFF_COS

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

DIFF_EXP

⊢ ∀x. (exp diffl exp x) x

DIFF_LN

⊢ ∀x. 0 < x ⇒ (ln diffl x⁻¹) x

DIFF_LN_COMPOSITE

⊢ ∀g m x. (g diffl m) x ∧ 0 < g x ⇒ ((λx. ln (g x)) diffl ((g x)⁻¹ * m)) x

DIFF_RPOW

⊢ ∀x y. 0 < x ⇒ ((λx. x powr y) diffl (y * x powr (y − 1))) x

DIFF_SIN

⊢ ∀x. (sin diffl cos x) x

DIFF_TAN

⊢ ∀x. cos x ≠ 0 ⇒ (tan diffl (cos x)² ⁻¹) x

DINT_UNIQ

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

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_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_EQ

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

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)

DIVISION_GT

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

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_LE

⊢ ∀D a b. division (a,b) D ⇒ a ≤ b

DIVISION_LHS

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

DIVISION_LT

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

DIVISION_LT_GEN

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

DIVISION_RHS

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

DIVISION_SINGLE

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

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_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

EXP_0

⊢ exp 0 = 1

EXP_ADD

⊢ ∀x y. exp (x + y) = exp x * exp y

EXP_ADD_MUL

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

EXP_CONVERGES

⊢ ∀x. (λn. (λn. (&FACT n)⁻¹) n * x pow n) sums exp x

EXP_FDIFF

⊢ diffs (λn. (&FACT n)⁻¹) = (λn. (&FACT n)⁻¹)

EXP_INJ

⊢ ∀x y. (exp x = exp y) ⇔ (x = y)

EXP_LE_X

⊢ ∀x. 0 ≤ x ⇒ 1 + x ≤ exp x

EXP_LN

⊢ ∀x. (exp (ln x) = x) ⇔ 0 < x

EXP_LT_1

⊢ ∀x. 0 < x ⇒ 1 < exp x

EXP_MONO_IMP

⊢ ∀x y. x < y ⇒ exp x < exp y

EXP_MONO_LE

⊢ ∀x y. exp x ≤ exp y ⇔ x ≤ y

EXP_MONO_LT

⊢ ∀x y. exp x < exp y ⇔ x < y

EXP_N

⊢ ∀n x. exp (&n * x) = exp x pow n

EXP_NEG

⊢ ∀x. exp (-x) = (exp x)⁻¹

EXP_NEG_MUL

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

EXP_NEG_MUL2

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

EXP_NZ

⊢ ∀x. exp x ≠ 0

EXP_POS_LE

⊢ ∀x. 0 ≤ exp x

EXP_POS_LT

⊢ ∀x. 0 < exp x

EXP_SUB

⊢ ∀x y. exp (x − y) = exp x / exp y

EXP_TOTAL

⊢ ∀y. 0 < y ⇒ ∃x. exp x = y

EXP_TOTAL_LEMMA

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

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)

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)

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)

GEN_RPOW

⊢ ∀a n. 0 < a ⇒ (a pow n = a powr &n)

INTEGRAL_NULL

⊢ ∀f a. Dint (a,a) f 0

LN_1

⊢ ln 1 = 0

LN_DIV

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

LN_EXP

⊢ ∀x. ln (exp x) = x

LN_INJ

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

LN_INV

⊢ ∀x. 0 < x ⇒ (ln x⁻¹ = -ln x)

LN_LE

⊢ ∀x. 0 ≤ x ⇒ ln (1 + x) ≤ x

LN_LT_X

⊢ ∀x. 0 < x ⇒ ln x < x

LN_MONO_LE

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

LN_MONO_LT

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

LN_MUL

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

LN_POS

⊢ ∀x. 1 ≤ x ⇒ 0 ≤ ln x

LN_POW

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

LN_RPOW

⊢ ∀a b. 0 < a ⇒ (ln (a powr b) = b * ln 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_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_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_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)

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_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_ZERO

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

ONE_RPOW

⊢ ∀a. 0 < a ⇒ (1 powr a = 1)

PI2

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

PI2_BOUNDS

⊢ 0 < pi / 2 ∧ pi / 2 < 2

PI_POS

⊢ 0 < pi

POW_2_SQRT

⊢ 0 ≤ x ⇒ (sqrt x² = x)

POW_ROOT_POS

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

REAL_DIV_SQRT

⊢ ∀x. 0 ≤ x ⇒ (x / sqrt x = sqrt x)

ROOT_0

⊢ ∀n. root (SUC n) 0 = 0

ROOT_1

⊢ ∀n. root (SUC n) 1 = 1

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_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)

ROOT_MONO_LE

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

ROOT_MUL

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

ROOT_POS

⊢ ∀n x. 0 ≤ x ⇒ 0 ≤ root (SUC n) x

ROOT_POS_LT

⊢ ∀n x. 0 < x ⇒ 0 < root (SUC n) x

ROOT_POS_UNIQ

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

ROOT_POW_POS

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

RPOW_0

⊢ ∀a. 0 < a ⇒ (a powr 0 = 1)

RPOW_1

⊢ ∀a. 0 < a ⇒ (a powr 1 = a)

RPOW_ADD

⊢ ∀a b c. a powr (b + c) = a powr b * a powr c

RPOW_ADD_MUL

⊢ ∀a b c. a powr (b + c) * a powr -b = a powr c

RPOW_DIV

⊢ ∀a b c. 0 < a ∧ 0 < b ⇒ ((a / b) powr c = a powr c / b powr c)

RPOW_DIV_BASE

⊢ ∀x t. 0 < x ⇒ (x powr t / x = x powr (t − 1))

RPOW_INV

⊢ ∀a b. 0 < a ⇒ (a⁻¹ powr b = (a powr b)⁻¹)

RPOW_LE

⊢ ∀a b c. 1 < a ⇒ (a powr b ≤ a powr c ⇔ b ≤ c)

RPOW_LT

⊢ ∀a b c. 1 < a ⇒ (a powr b < a powr c ⇔ b < c)

RPOW_MUL

⊢ ∀a b c. 0 < a ∧ 0 < b ⇒ ((a * b) powr c = a powr c * b powr c)

RPOW_NZ

⊢ ∀a b. 0 ≠ a ⇒ a powr b ≠ 0

RPOW_POS_LT

⊢ ∀a b. 0 < a ⇒ 0 < a powr b

RPOW_RPOW

⊢ ∀a b c. 0 < a ⇒ ((a powr b) powr c = a powr (b * c))

RPOW_SUB

⊢ ∀a b c. a powr (b − c) = a powr b / a powr c

RPOW_SUC_N

⊢ ∀a n. 0 < a ⇒ (a powr (&n + 1) = a pow SUC n)

RPOW_UNIQ_BASE

⊢ ∀a b c. 0 < a ∧ 0 < c ∧ 0 ≠ b ∧ (a powr b = c powr b) ⇒ (a = c)

RPOW_UNIQ_EXP

⊢ ∀a b c. 1 < a ∧ 0 < c ∧ 0 < b ∧ (a powr b = a powr c) ⇒ (b = c)

SIN_0

⊢ sin 0 = 0

SIN_ACS_NZ

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

SIN_ADD

⊢ ∀x y. sin (x + y) = sin x * cos y + cos x * sin y

SIN_ASN

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

SIN_BOUND

⊢ ∀x. abs (sin x) ≤ 1

SIN_BOUNDS

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

SIN_CIRCLE

⊢ ∀x. (sin x)² + (cos x)² = 1

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

SIN_COS

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

SIN_COS_ADD

⊢ ∀x y.
    (sin (x + y) − (sin x * cos y + cos x * sin y))² +
    (cos (x + y) − (cos x * cos y − sin x * sin y))² = 0

SIN_COS_NEG

⊢ ∀x. (sin (-x) + sin x)² + (cos (-x) − cos x)² = 0

SIN_COS_SQ

⊢ ∀x. 0 ≤ x ∧ x ≤ pi ⇒ (sin x = sqrt (1 − (cos x)²))

SIN_COS_SQRT

⊢ ∀x. 0 ≤ sin x ⇒ (sin x = sqrt (1 − (cos x)²))

SIN_DOUBLE

⊢ ∀x. sin (2 * x) = 2 * (sin x * cos x)

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)

SIN_NEG

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

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))

SIN_NPI

⊢ ∀n. sin (&n * pi) = 0

SIN_PAIRED

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

SIN_PERIODIC

⊢ ∀x. sin (x + 2 * pi) = sin x

SIN_PERIODIC_PI

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

SIN_PI

⊢ sin pi = 0

SIN_PI2

⊢ sin (pi / 2) = 1

SIN_POS

⊢ ∀x. 0 < x ∧ x < 2 ⇒ 0 < sin x

SIN_POS_PI

⊢ ∀x. 0 < x ∧ x < pi ⇒ 0 < sin x

SIN_POS_PI2

⊢ ∀x. 0 < x ∧ x < pi / 2 ⇒ 0 < sin x

SIN_POS_PI2_LE

⊢ ∀x. 0 ≤ x ∧ x ≤ pi / 2 ⇒ 0 ≤ sin x

SIN_POS_PI_LE

⊢ ∀x. 0 ≤ x ∧ x ≤ pi ⇒ 0 ≤ sin x

SIN_TOTAL

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

SIN_ZERO

⊢ ∀x. (sin 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))

SQRT_0

⊢ sqrt 0 = 0

SQRT_1

⊢ sqrt 1 = 1

SQRT_DIV

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

SQRT_EQ

⊢ ∀x y. (x² = y) ∧ 0 ≤ x ⇒ (x = sqrt y)

SQRT_EVEN_POW2

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

SQRT_INV

⊢ ∀x. 0 ≤ x ⇒ (sqrt x⁻¹ = (sqrt x)⁻¹)

SQRT_MONO_LE

⊢ ∀x y. 0 ≤ x ∧ x ≤ y ⇒ sqrt x ≤ sqrt y

SQRT_MUL

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

SQRT_POS_LE

⊢ ∀x. 0 ≤ x ⇒ 0 ≤ sqrt x

SQRT_POS_LT

⊢ ∀x. 0 < x ⇒ 0 < sqrt x

SQRT_POS_UNIQ

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ∧ (y² = x) ⇒ (sqrt x = y)

SQRT_POW2

⊢ ∀x. ((sqrt x)² = x) ⇔ 0 ≤ x

SQRT_POW_2

⊢ ∀x. 0 ≤ x ⇒ ((sqrt x)² = x)

TAN_0

⊢ tan 0 = 0

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_ATN

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

TAN_DOUBLE

⊢ ∀x. cos x ≠ 0 ∧ cos (2 * x) ≠ 0 ⇒ (tan (2 * x) = 2 * tan x / (1 − (tan x)²))

TAN_NEG

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

TAN_NPI

⊢ ∀n. tan (&n * pi) = 0

TAN_PERIODIC

⊢ ∀x. tan (x + 2 * pi) = tan x

TAN_PI

⊢ tan pi = 0

TAN_POS_PI2

⊢ ∀x. 0 < x ∧ x < pi / 2 ⇒ 0 < tan x

TAN_SEC

⊢ ∀x. cos x ≠ 0 ⇒ (1 + (tan x)² = (cos x)⁻¹ ²)

TAN_TOTAL

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

TAN_TOTAL_LEMMA

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

TAN_TOTAL_POS

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