Theory transc

⊢ ∀y. acosh y = @x. 0 ≤ x ∧ cosh x = y

⊢ ∀y. acoth y = @x. x ≠ 0 ∧ coth x = y

⊢ ∀y. acs y = @x. 0 ≤ x ∧ x ≤ pi ∧ cos x = y

⊢ ∀y. acsch y = @x. x ≠ 0 ∧ csch x = y

⊢ ∀y. asech y = @x. 0 ≤ x ∧ sech x = y

⊢ ∀y. asinh y = @x. sinh x = y

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

⊢ ∀y. atanh y = @x. tanh x = y

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

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

⊢ ∀x. cosh x = (exp x + exp (-x)) / 2

⊢ ∀x. coth x = 1 / tanh x

⊢ ∀x. csch x = 1 / sinh x

⊢ ∀x. lg x = logr 2 x

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

⊢ ∀a x. logr a x = ln x / ln a

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

⊢ (∀a b. 0 < a ⇒ a powr b = exp (b * ln a)) ∧ (∀b. 0 < b ⇒ 0 powr b = 0) ∧
  (∀a n. a powr &n = a pow n) ∧ ∀a n. a powr -&n = (a pow n)⁻¹

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

⊢ ∀x. sech x = 1 / cosh x

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

⊢ ∀x. sinh x = (exp x − exp (-x)) / 2

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

⊢ ∀x. tanh x = sinh x / cosh x

⊢ acosh 1 = 0

⊢ ∀x. 0 ≤ x ⇒ acosh (cosh x) = x

⊢ ∀x. x ≤ 0 ⇒ acosh (cosh x) = -x

⊢ ∀x. 1 ≤ x ⇒ acosh x = ln (x + sqrt (x² − 1))

⊢ ∀x y. 1 ≤ x ∧ x ≤ y ⇒ acosh x ≤ acosh y

⊢ ∀x y. 1 ≤ x ∧ x < y ⇒ acosh x < acosh y

⊢ ∀x. 1 < x ⇒ acosh x ≠ 0

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

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

⊢ ∀x y. (y < -1 ∨ 1 < x) ∧ x ≤ y ⇒ acoth y ≤ acoth x

⊢ ∀x y. (y < -1 ∨ 1 < x) ∧ x < y ⇒ acoth y < acoth x

⊢ ∀x. x ≠ 0 ⇒ acoth (coth x) = x

⊢ ∀x. x < -1 ∨ 1 < x ⇒ acoth x = atanh x⁻¹

⊢ ∀x. x < -1 ∨ 1 < x ⇒ acoth x = ln ((x + 1) / (x − 1)) / 2

⊢ ∀x. x < -1 ∨ 1 < x ⇒ acoth (-x) = -acoth x

⊢ ∀x. x < -1 ⇒ acoth x < 0

⊢ ∀x. x < -1 ∨ 1 < x ⇒ acoth x ≠ 0

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

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

⊢ ∀x y. (y < 0 ∨ 0 < x) ∧ x ≤ y ⇒ acsch y ≤ acsch x

⊢ ∀x y. (y < 0 ∨ 0 < x) ∧ x < y ⇒ acsch y < acsch x

⊢ ∀x. x ≠ 0 ⇒ acsch (csch x) = x

⊢ ∀x. x ≠ 0 ⇒ acsch x = asinh x⁻¹

⊢ ∀x. x ≠ 0 ⇒ acsch x = ln (x⁻¹ + sqrt (x⁻¹ ² + 1))

⊢ ∀x. x ≠ 0 ⇒ acsch (-x) = -acsch x

⊢ ∀x. x < 0 ⇒ acsch x < 0

⊢ ∀x. x ≠ 0 ⇒ acsch x ≠ 0

⊢ ∀x. 0 < x ⇒ 0 < acsch x

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

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

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

⊢ ∀s x n.
    s HAS_SIZE n ∧ n ≠ 0 ∧ (∀i. i ∈ s ⇒ 0 ≤ x i) ⇒
    product s x ≤ (sum s x / &n) pow n

⊢ ∀x y u v.
    0 < x ∧ 0 < y ∧ 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1 ⇒
    x powr u * y powr v ≤ u * x + v * y

⊢ ∀a x s.
    FINITE s ∧ sum s a = 1 ∧ (∀i. i ∈ s ⇒ 0 ≤ a i ∧ 0 < x i) ⇒
    product s (λi. x i powr a i) ≤ sum s (λi. a i * x i)

⊢ ∀s x n.
    s HAS_SIZE n ∧ n ≠ 0 ∧ (∀i. i ∈ s ⇒ 0 ≤ x i) ⇒
    root n (product s x) ≤ sum s x / &n

⊢ ∀s x n.
    s HAS_SIZE n ∧ n ≠ 0 ∧ (∀i. i ∈ s ⇒ 0 < x i) ⇒
    product s (λi. x i powr (1 / &n)) ≤ sum s (λi. x i / &n)

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ sqrt (x * y) ≤ (x + y) / 2

⊢ asech 1 = 0

⊢ ∀x y. 0 < x ∧ y ≤ 1 ∧ x ≤ y ⇒ asech y ≤ asech x

⊢ ∀x y. 0 < x ∧ y ≤ 1 ∧ x < y ⇒ asech y < asech x

⊢ ∀x. 0 < x ∧ x ≤ 1 ⇒ asech x = acosh x⁻¹

⊢ ∀x. 0 < x ∧ x ≤ 1 ⇒ asech x = ln (x⁻¹ + sqrt (x⁻¹ ² − 1))

⊢ ∀x. 0 < x ∧ x < 1 ⇒ asech x ≠ 0

⊢ ∀x. 0 < x ∧ x ≤ 1 ⇒ 0 ≤ asech x

⊢ ∀x. 0 < x ∧ x < 1 ⇒ 0 < asech x

⊢ ∀x. 0 ≤ x ⇒ asech (sech x) = x

⊢ ∀x. x ≤ 0 ⇒ asech (sech x) = -x

⊢ asinh 0 = 0

⊢ ∀x. asinh x = ln (x + sqrt (x² + 1))

⊢ ∀x y. x ≤ y ⇒ asinh x ≤ asinh y

⊢ ∀x y. x < y ⇒ asinh x < asinh y

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

⊢ ∀x. x ≤ 0 ⇒ asinh x ≤ 0

⊢ ∀x. x < 0 ⇒ asinh x < 0

⊢ ∀x. asinh x ≠ 0 ⇔ x ≠ 0

⊢ ∀x. 0 ≤ x ⇒ 0 ≤ asinh x

⊢ ∀x. 0 < x ⇒ 0 < asinh x

⊢ ∀x. asinh (sinh x) = x

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

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

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

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

⊢ atanh 0 = 0

⊢ ∀x. -1 < x ∧ x < 1 ⇒ atanh x = ln ((1 + x) / (1 − x)) / 2

⊢ ∀x y. -1 < x ∧ y < 1 ∧ x ≤ y ⇒ atanh x ≤ atanh y

⊢ ∀x y. -1 < x ∧ y < 1 ∧ x < y ⇒ atanh x < atanh y

⊢ ∀x. -1 < x ∧ x < 1 ⇒ atanh (-x) = -atanh x

⊢ ∀x. -1 < x ∧ x ≤ 0 ⇒ atanh x ≤ 0

⊢ ∀x. -1 < x ∧ x < 0 ⇒ atanh x < 0

⊢ ∀x. -1 < x ∧ x ≠ 0 ∧ x < 1 ⇒ atanh x ≠ 0

⊢ ∀x. 0 ≤ x ∧ x < 1 ⇒ 0 ≤ atanh x

⊢ ∀x. 0 < x ∧ x < 1 ⇒ 0 < atanh x

⊢ ∀x. atanh (tanh x) = x

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

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

⊢ ∀y. tan (atn y) = y

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

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

⊢ cosh 0 = 1

⊢ ∀x. 1 ≤ x ⇒ cosh (acosh x) = x

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

⊢ ∀x y. x < y ∧ y ≤ 0 ⇒ cosh y < cosh x

⊢ ∀x. cosh (asinh x) = sqrt (x² + 1)

⊢ ∀x. 1 ≤ cosh x

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

⊢ ∀x y. 0 ≤ x ∧ x < y ⇒ cosh x < cosh y

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

⊢ ∀x. cosh x ≠ 0

⊢ ∀x. 0 < cosh x

⊢ ∀x. (cosh x)² − (sinh x)² = 1

⊢ cos 0 = 1

⊢ cos 2 < 0

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

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

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

⊢ ∀x. cos (atn x) ≠ 0

⊢ ∀x. abs (cos x) ≤ 1

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

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

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

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

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

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

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

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

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

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

⊢ cos pi = -1

⊢ cos (pi / 2) = 0

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

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

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

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

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

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

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

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

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

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

⊢ ∀x. x < -1 ∨ 1 < x ⇒ coth (acoth x) = x

⊢ ∀x y. (y < 0 ∨ 0 < x) ∧ x ≤ y ⇒ coth y ≤ coth x

⊢ ∀x y. (y < 0 ∨ 0 < x) ∧ x < y ⇒ coth y < coth x

⊢ ∀x. x ≠ 0 ⇒ coth x < -1 ∨ 1 < coth x

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

⊢ ∀x. x < 0 ⇒ coth x < 0

⊢ ∀x. x ≠ 0 ⇒ coth x ≠ 0

⊢ ∀x. 0 < x ⇒ 0 < coth x

⊢ ∀x. x ≠ 0 ⇒ (coth x)² − (csch x)² = 1

⊢ csch 0 = 0

⊢ ∀x. x ≠ 0 ⇒ csch (acsch x) = x

⊢ ∀x y. (y < 0 ∨ 0 < x) ∧ x ≤ y ⇒ csch y ≤ csch x

⊢ ∀x y. (y < 0 ∨ 0 < x) ∧ x < y ⇒ csch y < csch x

⊢ ∀x. x ≠ 0 ⇒ csch x ≠ 0

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

⊢ ∀x. x < 0 ⇒ csch x < 0

⊢ ∀x. x ≠ 0 ⇒ csch x ≠ 0

⊢ ∀x. 0 < x ⇒ 0 < csch x

⊢ ∀x. 1 < x ⇒ (acosh diffl (sqrt (x² − 1))⁻¹) x

⊢ ∀x. x < -1 ∨ 1 < x ⇒ (acoth diffl (1 − x²)⁻¹) x

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

⊢ ∀x. x ≠ 0 ⇒ (acsch diffl -(abs x * sqrt (1 + x²))⁻¹) x

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

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

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

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

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

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

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

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

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

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

⊢ ∀x. (cosh diffl sinh x) x

⊢ ∀x. x ≠ 0 ⇒ (coth diffl (1 − (coth x)²)) x

⊢ ∀x. x ≠ 0 ⇒ (csch diffl -(coth x * csch x)) x

⊢ ∀x. (exp diffl exp x) x

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

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

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

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

⊢ ∀x. (sech diffl -(tanh x * sech x)) x

⊢ ∀x. (sin diffl cos x) x

⊢ ∀x. (sinh diffl cosh x) x

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

⊢ ∀x. (tanh diffl (1 − (tanh x)²)) x

⊢ exp 0 = 1

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

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

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

⊢ ∀n x. 1 < n ⇒ exp (x / &n) = root n (exp x)

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

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

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

⊢ ∀x. 1 + x ≤ exp x

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

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

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

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

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

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

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

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

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

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

⊢ ∀x. exp x ≠ 0

⊢ ∀x. 0 ≤ exp x

⊢ ∀x. 0 < exp x

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

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

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

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

⊢ ln 1 = 0

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

⊢ ∀x. 0 < x ⇒ ln x = 2 * atanh ((x − 1) / (x + 1))

⊢ ∀x. ln (exp x) = x

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

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

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

⊢ ∀x. 2 ≤ x ⇒ ln x < x / 2

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

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

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

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

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

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

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

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

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

⊢ ∀f s.
    FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒
    ln (product s f) = sum s (λx. ln (f x))

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

⊢ ∀x y b. 0 < x ∧ 0 < y ∧ 1 < b ⇒ (logr b x ≤ logr b y ⇔ x ≤ y)

⊢ ∀x y b. 0 < x ∧ x ≤ y ∧ 1 ≤ b ⇒ logr b x ≤ logr b y

⊢ ∀x y b. 0 < x ∧ 0 < y ∧ 1 < b ⇒ (logr b x < logr b y ⇔ x < y)

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀f h n.
    0 < h ∧ 0 < n ∧ (∀t. 0 ≤ t ∧ t ≤ h ⇒ higher_differentiable n f t) ⇒
    ∃t. 0 < t ∧ t < h ∧
        f h =
        SIGMA (λm. diffn m f 0 / &FACT m * h pow m) (count n) +
        diffn n f t / &FACT n * h pow n

⊢ ∀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

⊢ ∀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

⊢ ∀x n.
    0 < x ∧ x < 1 ∧ 0 < n ⇒
    ∃t. 0 < t ∧ t < x ∧
        -ln (1 − x) =
        sum (0,n) (λm. x pow m / &m) + x pow n / (&n * (1 − t) pow n)

⊢ ∀x n.
    0 < x ∧ 0 < n ⇒
    ∃t. 0 < t ∧ t < x ∧
        ln (1 + x) =
        sum (0,n) (λm. -1 pow SUC m * x pow m / &m) +
        -1 pow SUC n * x pow n / (&n * (1 + t) pow n)

⊢ ∀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

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

⊢ ∀a. 1 powr a = 1

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

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

⊢ 0 < pi

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

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

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

⊢ ∀x. 0 ≤ x ∧ x ≤ 2⁻¹ ⇒ exp x ≤ 1 + 2 * x

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

⊢ ∀n x. n ≠ 0 ∧ 0 < x ⇒ root n x = x powr (&n)⁻¹

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀n f s.
    FINITE s ∧ n ≠ 0 ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒
    root n (product s f) = product s (λi. root n (f i))

⊢ ∀a. a powr 0 = 1

⊢ ∀a. a powr 1 = a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ sech 0 = 1

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

⊢ ∀x y. 0 ≤ x ∧ x < y ⇒ sech y < sech x

⊢ ∀x. 0 < x ∧ x ≤ 1 ⇒ sech (asech x) = x

⊢ ∀x. 0 < sech x ∧ sech x ≤ 1

⊢ ∀x y. x < y ∧ y ≤ 0 ⇒ sech x < sech y

⊢ ∀x y. x < y ∧ y ≤ 0 ⇒ sech x < sech y

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

⊢ ∀x. sech x ≠ 0

⊢ ∀x. 0 < sech x

⊢ ∀x. (sech x)² + (tanh x)² = 1

⊢ sinh 0 = 0

⊢ ∀x. 1 < x ⇒ sinh (acosh x) = sqrt (x² − 1)

⊢ ∀x. sinh (asinh x) = x

⊢ ∀x y. x ≤ y ⇒ sinh x ≤ sinh y

⊢ ∀x y. x < y ⇒ sinh x < sinh y

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

⊢ ∀x. x ≤ 0 ⇒ sinh x ≤ 0

⊢ ∀x. x < 0 ⇒ sinh x < 0

⊢ ∀x. sinh x ≠ 0 ⇔ x ≠ 0

⊢ ∀x. 0 ≤ x ⇒ 0 ≤ sinh x

⊢ ∀x. 0 < x ⇒ 0 < sinh x

⊢ sin 0 = 0

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

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

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

⊢ ∀x. abs (sin x) ≤ 1

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

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

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

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

⊢ ∀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

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

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

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

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

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

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

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

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

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

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

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

⊢ sin pi = 0

⊢ sin (pi / 2) = 1

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

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

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

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

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

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

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

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

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

⊢ ∀x. 0 < x ⇒ sqrt x = x powr 2⁻¹

⊢ tanh 0 = 0

⊢ ∀x. -1 < x ∧ x < 1 ⇒ tanh (atanh x) = x

⊢ ∀x. -1 < tanh x ∧ tanh x < 1

⊢ ∀x y. x ≤ y ⇒ tanh x ≤ tanh y

⊢ ∀x y. x < y ⇒ tanh x < tanh y

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

⊢ ∀x. x ≤ 0 ⇒ tanh x ≤ 0

⊢ ∀x. x < 0 ⇒ tanh x < 0

⊢ ∀x. tanh x ≠ 0 ⇔ x ≠ 0

⊢ ∀x. 0 ≤ x ⇒ 0 ≤ tanh x

⊢ ∀x. 0 < x ⇒ 0 < tanh x

⊢ tan 0 = 0

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

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

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

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

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

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

⊢ tan pi = 0

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

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

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

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

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

⊢ ∀f a x n.
    a < x ∧ 0 < n ∧ (∀t. a ≤ t ∧ t ≤ x ⇒ higher_differentiable n f t) ⇒
    ∃t. a < t ∧ t < x ∧
        f x =
        SIGMA (λm. diffn m f a / &FACT m * (x − a) pow m) (count n) +
        diffn n f t / &FACT n * (x − a) pow n

⊢ ∀f a x n.
    0 < n ∧ a ≠ x ∧
    (∀t. min a x ≤ t ∧ t ≤ max a x ⇒ higher_differentiable n f t) ⇒
    ∃t. min a x < t ∧ t < max a x ∧
        f x =
        SIGMA (λm. diffn m f a / &FACT m * (x − a) pow m) (count n) +
        diffn n f t / &FACT n * (x − a) pow n

⊢ ∀f a x n.
    x < a ∧ 0 < n ∧ (∀t. x ≤ t ∧ t ≤ a ⇒ higher_differentiable n f t) ⇒
    ∃t. x < t ∧ t < a ∧
        f x =
        SIGMA (λm. diffn m f a / &FACT m * (x − a) pow m) (count n) +
        diffn n f t / &FACT n * (x − a) pow n

⊢ ∀a b p q.
    0 < a ∧ 0 < b ∧ 0 < p ∧ 0 < q ∧ p⁻¹ + q⁻¹ = 1 ⇒
    a * b ≤ a powr p / p + b powr q / q

⊢ ∀x. coth x = cosh x / sinh x

⊢ ∀n x. diffn n exp = exp

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

⊢ exp ∈ convex_fn

⊢ ∀n x. higher_differentiable n exp x

⊢ lg 1 = 0

⊢ lg 2 = 1

⊢ ∀x. 0 < x ⇒ lg x⁻¹ = -lg x

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

⊢ ∀x. x ≠ 0 ∧ 0 ≤ x ⇒ (lg x ≠ 0 ⇔ x ≠ 1)

⊢ ∀n. lg (2 pow n) = &n

⊢ ∀b. logr b 1 = 0

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

⊢ ∀b x. 0 < x ⇒ logr b x⁻¹ = -logr b x

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

⊢ ∀x. 0 < x ⇒ -lg x = lg x⁻¹

⊢ ∀b x. 0 < x ⇒ -logr b x = logr b x⁻¹

⊢ lg ∈ pos_concave_fn

⊢ ln ∈ pos_concave_fn

⊢ ∀b. 1 ≤ b ⇒ logr b ∈ pos_concave_fn

⊢ realinv ∈ pos_convex_fn

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

⊢ ∀x. sqrt x = root 2 x

⊢ ∀x. tanh x = (exp x − exp (-x)) / (exp x + exp (-x))

⊢ ∀x. tanh x = (exp (2 * x) − 1) / (exp (2 * x) + 1)