Theory: transc

Parents

• powser

Types

Constants

• acs  :real -> real
• asn  :real -> real
• atn  :real -> real
• cos  :real -> real
• exp  :real -> real
• tan  :real -> real
• sin  :real -> real
• ln  :real -> real
• pi  :real
• Dint  :real # real -> (real -> real) -> real -> bool
• fine  :(real -> real) -> (num -> real) # (num -> real) -> bool
• division  :real # real -> (num -> real) -> bool
• gauge  :(real -> bool) -> (real -> real) -> bool
• dsize  :(num -> real) -> num
• tdiv  :real # real -> (num -> real) # (num -> real) -> bool
• root  :num -> real -> real
• rsum  :(num -> real) # (num -> real) -> (real -> real) -> real
• sqrt  :real -> real

Definitions

cos

|- !x.
     cos x =
     suminf
       (\n.
          (\n. (if EVEN n then ~1 pow (n DIV 2) / & (FACT n) else 0)) n *
          x pow 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

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. inv (& (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)

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

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 pow 2 - sin x pow 2

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

COS_SIN_SQRT

|- !x. 0 <= cos x ==> (cos x = sqrt (1 - sin x pow 2))

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 ~inv (sqrt (1 - x pow 2))) x

DIFF_ACS_LEMMA

|- !x. ~1 < x /\ x < 1 ==> (acs diffl inv ~sin (acs x)) x

DIFF_ASN

|- !x. ~1 < x /\ x < 1 ==> (asn diffl inv (sqrt (1 - x pow 2))) x

DIFF_ASN_LEMMA

|- !x. ~1 < x /\ x < 1 ==> (asn diffl inv (cos (asn x))) x

DIFF_ATN

|- !x. (atn diffl inv (1 + x pow 2)) 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)

DIFF_COS

|- !x. (cos diffl ~sin x) x

DIFF_EXP

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

DIFF_LN

|- !x. 0 < x ==> (ln diffl inv x) x

DIFF_LN_COMPOSITE

|- !g m x.
     (g diffl m) x /\ 0 < g x ==> ((\x. ln (g x)) diffl (inv (g x) * m)) x

DIFF_SIN

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

DIFF_TAN

|- !x. ~(cos x = 0) ==> (tan diffl inv (cos x pow 2)) 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. inv (& (FACT n))) n * x pow n) sums exp x

EXP_FDIFF

|- diffs (\n. inv (& (FACT n))) = (\n. inv (& (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 = inv (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))

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

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)

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 pow 2) = 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) (inv x) = inv (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)

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 pow 2 + cos x pow 2 = 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)) pow 2 +
     (cos (x + y) - (cos x * cos y - sin x * sin y)) pow 2 =
     0

SIN_COS_NEG

|- !x. (sin ~x + sin x) pow 2 + (cos ~x - cos x) pow 2 = 0

SIN_COS_SQ

|- !x. 0 <= x /\ x <= pi ==> (sin x = sqrt (1 - cos x pow 2))

SIN_COS_SQRT

|- !x. 0 <= sin x ==> (sin x = sqrt (1 - cos x pow 2))

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 pow 2 = 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 (inv x) = inv (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 pow 2 = x) ==> (sqrt x = y)

SQRT_POW2

|- !x. (sqrt x pow 2 = x) = 0 <= x

SQRT_POW_2

|- !x. 0 <= x ==> (sqrt x pow 2 = 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 pow 2))

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 pow 2 = inv (cos x) pow 2)

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)