Structure transcTheory
signature transcTheory =
sig
type thm = Thm.thm
(* Definitions *)
val acs : thm
val asn : thm
val atn : thm
val cos : thm
val lg_def : thm
val ln : thm
val logr_def : thm
val pi : thm
val root : thm
val rpow_def : thm
val sin : thm
val tan : thm
(* Theorems *)
val ACS : thm
val ACS_BOUNDS : thm
val ACS_BOUNDS_LT : thm
val ACS_COS : thm
val AGM : thm
val AGM_2 : thm
val AGM_GEN : thm
val AGM_ROOT : thm
val AGM_RPOW : thm
val AGM_SQRT : thm
val ASN : thm
val ASN_BOUNDS : thm
val ASN_BOUNDS_LT : thm
val ASN_SIN : thm
val ATN : thm
val ATN_BOUNDS : thm
val ATN_TAN : thm
val BASE_RPOW_LE : thm
val BASE_RPOW_LT : thm
val COS_0 : thm
val COS_2 : thm
val COS_ACS : thm
val COS_ADD : thm
val COS_ASN_NZ : thm
val COS_ATN_NZ : thm
val COS_BOUND : thm
val COS_BOUNDS : thm
val COS_CONVERGES : thm
val COS_DOUBLE : thm
val COS_FDIFF : thm
val COS_ISZERO : thm
val COS_NEG : thm
val COS_NPI : thm
val COS_PAIRED : thm
val COS_PERIODIC : thm
val COS_PERIODIC_PI : thm
val COS_PI : thm
val COS_PI2 : thm
val COS_POS_PI : thm
val COS_POS_PI2 : thm
val COS_POS_PI2_LE : thm
val COS_POS_PI_LE : thm
val COS_SIN : thm
val COS_SIN_SQ : thm
val COS_SIN_SQRT : thm
val COS_TOTAL : thm
val COS_ZERO : thm
val COS_ZERO_LEMMA : thm
val DIFF_ACS : thm
val DIFF_ACS_LEMMA : thm
val DIFF_ASN : thm
val DIFF_ASN_LEMMA : thm
val DIFF_ATN : thm
val DIFF_COMPOSITE : thm
val DIFF_COMPOSITE_EXP : thm
val DIFF_COS : thm
val DIFF_EXP : thm
val DIFF_LN : thm
val DIFF_LN_COMPOSITE : thm
val DIFF_LN_COMPOSITE' : thm
val DIFF_RPOW : thm
val DIFF_SIN : thm
val DIFF_TAN : thm
val EXP_0 : thm
val EXP_ADD : thm
val EXP_ADD_MUL : thm
val EXP_CONVERGES : thm
val EXP_FDIFF : thm
val EXP_INJ : thm
val EXP_LE_X : thm
val EXP_LE_X_FULL : thm
val EXP_LN : thm
val EXP_LT_1 : thm
val EXP_MONO_IMP : thm
val EXP_MONO_LE : thm
val EXP_MONO_LT : thm
val EXP_N : thm
val EXP_NEG : thm
val EXP_NEG_MUL : thm
val EXP_NEG_MUL2 : thm
val EXP_NZ : thm
val EXP_POS_LE : thm
val EXP_POS_LT : thm
val EXP_SUB : thm
val EXP_TOTAL : thm
val EXP_TOTAL_LEMMA : thm
val GEN_RPOW : thm
val LN_1 : thm
val LN_DIV : thm
val LN_EXP : thm
val LN_INJ : thm
val LN_INV : thm
val LN_LE : thm
val LN_LT_X : thm
val LN_MONO_LE : thm
val LN_MONO_LT : thm
val LN_MUL : thm
val LN_NEG : thm
val LN_NEG_LT : thm
val LN_POS : thm
val LN_POS_LT : thm
val LN_POW : thm
val LN_PRODUCT : thm
val LN_RPOW : thm
val LOGR_MONO_LE : thm
val LOGR_MONO_LE_IMP : thm
val LOGR_MONO_LT : thm
val MCLAURIN : thm
val MCLAURIN_ALL_LE : thm
val MCLAURIN_ALL_LT : thm
val MCLAURIN_EXP_LE : thm
val MCLAURIN_EXP_LT : thm
val MCLAURIN_LN_NEG : thm
val MCLAURIN_LN_POS : thm
val MCLAURIN_NEG : thm
val MCLAURIN_ZERO : thm
val ONE_RPOW : thm
val PI2 : thm
val PI2_BOUNDS : thm
val PI_POS : thm
val POW_ROOT_POS : thm
val REAL_DIV_SQRT : thm
val REAL_EXP_ADD : thm
val REAL_EXP_BOUND_LEMMA : thm
val REAL_ROOT_RPOW : thm
val ROOT_0 : thm
val ROOT_1 : thm
val ROOT_11 : thm
val ROOT_DIV : thm
val ROOT_INV : thm
val ROOT_LN : thm
val ROOT_LT_LEMMA : thm
val ROOT_MONO_LE : thm
val ROOT_MONO_LE_EQ : thm
val ROOT_MUL : thm
val ROOT_POS : thm
val ROOT_POS_LT : thm
val ROOT_POS_UNIQ : thm
val ROOT_POW_POS : thm
val ROOT_PRODUCT : thm
val RPOW_0 : thm
val RPOW_1 : thm
val RPOW_ADD : thm
val RPOW_ADD_MUL : thm
val RPOW_DIV : thm
val RPOW_DIV_BASE : thm
val RPOW_INV : thm
val RPOW_LE : thm
val RPOW_LT : thm
val RPOW_MUL : thm
val RPOW_NZ : thm
val RPOW_POS_LT : thm
val RPOW_RPOW : thm
val RPOW_SUB : thm
val RPOW_SUC_N : thm
val RPOW_UNIQ_BASE : thm
val RPOW_UNIQ_EXP : thm
val SIN_0 : thm
val SIN_ACS_NZ : thm
val SIN_ADD : thm
val SIN_ASN : thm
val SIN_BOUND : thm
val SIN_BOUNDS : thm
val SIN_CIRCLE : thm
val SIN_CONVERGES : thm
val SIN_COS : thm
val SIN_COS_ADD : thm
val SIN_COS_NEG : thm
val SIN_COS_SQ : thm
val SIN_COS_SQRT : thm
val SIN_DOUBLE : thm
val SIN_FDIFF : thm
val SIN_NEG : thm
val SIN_NEGLEMMA : thm
val SIN_NPI : thm
val SIN_PAIRED : thm
val SIN_PERIODIC : thm
val SIN_PERIODIC_PI : thm
val SIN_PI : thm
val SIN_PI2 : thm
val SIN_POS : thm
val SIN_POS_PI : thm
val SIN_POS_PI2 : thm
val SIN_POS_PI2_LE : thm
val SIN_POS_PI_LE : thm
val SIN_TOTAL : thm
val SIN_ZERO : thm
val SIN_ZERO_LEMMA : thm
val SQRT_EVEN_POW2 : thm
val SQRT_RPOW : thm
val TAN_0 : thm
val TAN_ADD : thm
val TAN_ATN : thm
val TAN_DOUBLE : thm
val TAN_NEG : thm
val TAN_NPI : thm
val TAN_PERIODIC : thm
val TAN_PI : thm
val TAN_POS_PI2 : thm
val TAN_SEC : thm
val TAN_TOTAL : thm
val TAN_TOTAL_LEMMA : thm
val TAN_TOTAL_POS : thm
val YOUNG_INEQUALITY : thm
val exp : thm
val exp_convex : thm
val lg_1 : thm
val lg_2 : thm
val lg_inv : thm
val lg_mul : thm
val lg_nonzero : thm
val lg_pow : thm
val logr_1 : thm
val logr_div : thm
val logr_inv : thm
val logr_mul : thm
val neg_lg : thm
val neg_logr : thm
val pos_concave_lg : thm
val pos_concave_ln : thm
val pos_concave_logr : thm
val pos_convex_inv : thm
val sqrt : thm
val transc_grammars : type_grammar.grammar * term_grammar.grammar
(*
[powser] Parent theory of "transc"
[acs] Definition
⊢ ∀y. acs y = @x. 0 ≤ x ∧ x ≤ pi ∧ cos x = y
[asn] Definition
⊢ ∀y. asn y = @x. -(pi / 2) ≤ x ∧ x ≤ pi / 2 ∧ sin x = y
[atn] Definition
⊢ ∀y. atn y = @x. -(pi / 2) < x ∧ x < pi / 2 ∧ tan x = y
[cos] Definition
⊢ ∀x. cos x =
suminf
(λn.
(λn. if EVEN n then -1 pow (n DIV 2) / &FACT n else 0) n *
x pow n)
[lg_def] Definition
⊢ ∀x. lg x = logr 2 x
[ln] Definition
⊢ ∀x. ln x = @u. exp u = x
[logr_def] Definition
⊢ ∀a x. logr a x = ln x / ln a
[pi] Definition
⊢ pi = 2 * @x. 0 ≤ x ∧ x ≤ 2 ∧ cos x = 0
[root] Definition
⊢ ∀n x. root n x = @u. (0 < x ⇒ 0 < u) ∧ u pow n = x
[rpow_def] Definition
⊢ ∀a b. a powr b = exp (b * ln a)
[sin] Definition
⊢ ∀x. sin x =
suminf
(λn.
(λn.
if EVEN n then 0
else -1 pow ((n − 1) DIV 2) / &FACT n) n * x pow n)
[tan] Definition
⊢ ∀x. tan x = sin x / cos x
[ACS] Theorem
⊢ ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ 0 ≤ acs y ∧ acs y ≤ pi ∧ cos (acs y) = y
[ACS_BOUNDS] Theorem
⊢ ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ 0 ≤ acs y ∧ acs y ≤ pi
[ACS_BOUNDS_LT] Theorem
⊢ ∀y. -1 < y ∧ y < 1 ⇒ 0 < acs y ∧ acs y < pi
[ACS_COS] Theorem
⊢ ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ cos (acs y) = y
[AGM] Theorem
⊢ ∀s x n.
s HAS_SIZE n ∧ n ≠ 0 ∧ (∀i. i ∈ s ⇒ 0 ≤ x i) ⇒
product s x ≤ (sum s x / &n) pow n
[AGM_2] Theorem
⊢ ∀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
[AGM_GEN] Theorem
⊢ ∀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)
[AGM_ROOT] Theorem
⊢ ∀s x n.
s HAS_SIZE n ∧ n ≠ 0 ∧ (∀i. i ∈ s ⇒ 0 ≤ x i) ⇒
root n (product s x) ≤ sum s x / &n
[AGM_RPOW] Theorem
⊢ ∀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)
[AGM_SQRT] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ sqrt (x * y) ≤ (x + y) / 2
[ASN] Theorem
⊢ ∀y. -1 ≤ y ∧ y ≤ 1 ⇒
-(pi / 2) ≤ asn y ∧ asn y ≤ pi / 2 ∧ sin (asn y) = y
[ASN_BOUNDS] Theorem
⊢ ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ -(pi / 2) ≤ asn y ∧ asn y ≤ pi / 2
[ASN_BOUNDS_LT] Theorem
⊢ ∀y. -1 < y ∧ y < 1 ⇒ -(pi / 2) < asn y ∧ asn y < pi / 2
[ASN_SIN] Theorem
⊢ ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ sin (asn y) = y
[ATN] Theorem
⊢ ∀y. -(pi / 2) < atn y ∧ atn y < pi / 2 ∧ tan (atn y) = y
[ATN_BOUNDS] Theorem
⊢ ∀y. -(pi / 2) < atn y ∧ atn y < pi / 2
[ATN_TAN] Theorem
⊢ ∀y. tan (atn y) = y
[BASE_RPOW_LE] Theorem
⊢ ∀a b c. 0 < a ∧ 0 < c ∧ 0 < b ⇒ (a powr b ≤ c powr b ⇔ a ≤ c)
[BASE_RPOW_LT] Theorem
⊢ ∀a b c. 0 < a ∧ 0 < c ∧ 0 < b ⇒ (a powr b < c powr b ⇔ a < c)
[COS_0] Theorem
⊢ cos 0 = 1
[COS_2] Theorem
⊢ cos 2 < 0
[COS_ACS] Theorem
⊢ ∀x. 0 ≤ x ∧ x ≤ pi ⇒ acs (cos x) = x
[COS_ADD] Theorem
⊢ ∀x y. cos (x + y) = cos x * cos y − sin x * sin y
[COS_ASN_NZ] Theorem
⊢ ∀x. -1 < x ∧ x < 1 ⇒ cos (asn x) ≠ 0
[COS_ATN_NZ] Theorem
⊢ ∀x. cos (atn x) ≠ 0
[COS_BOUND] Theorem
⊢ ∀x. abs (cos x) ≤ 1
[COS_BOUNDS] Theorem
⊢ ∀x. -1 ≤ cos x ∧ cos x ≤ 1
[COS_CONVERGES] Theorem
⊢ ∀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] Theorem
⊢ ∀x. cos (2 * x) = (cos x)² − (sin x)²
[COS_FDIFF] Theorem
⊢ 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] Theorem
⊢ ∃!x. 0 ≤ x ∧ x ≤ 2 ∧ cos x = 0
[COS_NEG] Theorem
⊢ ∀x. cos (-x) = cos x
[COS_NPI] Theorem
⊢ ∀n. cos (&n * pi) = -1 pow n
[COS_PAIRED] Theorem
⊢ ∀x. (λn. -1 pow n / &FACT (2 * n) * x pow (2 * n)) sums cos x
[COS_PERIODIC] Theorem
⊢ ∀x. cos (x + 2 * pi) = cos x
[COS_PERIODIC_PI] Theorem
⊢ ∀x. cos (x + pi) = -cos x
[COS_PI] Theorem
⊢ cos pi = -1
[COS_PI2] Theorem
⊢ cos (pi / 2) = 0
[COS_POS_PI] Theorem
⊢ ∀x. -(pi / 2) < x ∧ x < pi / 2 ⇒ 0 < cos x
[COS_POS_PI2] Theorem
⊢ ∀x. 0 < x ∧ x < pi / 2 ⇒ 0 < cos x
[COS_POS_PI2_LE] Theorem
⊢ ∀x. 0 ≤ x ∧ x ≤ pi / 2 ⇒ 0 ≤ cos x
[COS_POS_PI_LE] Theorem
⊢ ∀x. -(pi / 2) ≤ x ∧ x ≤ pi / 2 ⇒ 0 ≤ cos x
[COS_SIN] Theorem
⊢ ∀x. cos x = sin (pi / 2 − x)
[COS_SIN_SQ] Theorem
⊢ ∀x. -(pi / 2) ≤ x ∧ x ≤ pi / 2 ⇒ cos x = sqrt (1 − (sin x)²)
[COS_SIN_SQRT] Theorem
⊢ ∀x. 0 ≤ cos x ⇒ cos x = sqrt (1 − (sin x)²)
[COS_TOTAL] Theorem
⊢ ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ ∃!x. 0 ≤ x ∧ x ≤ pi ∧ cos x = y
[COS_ZERO] Theorem
⊢ ∀x. cos x = 0 ⇔
(∃n. ¬EVEN n ∧ x = &n * (pi / 2)) ∨
∃n. ¬EVEN n ∧ x = -(&n * (pi / 2))
[COS_ZERO_LEMMA] Theorem
⊢ ∀x. 0 ≤ x ∧ cos x = 0 ⇒ ∃n. ¬EVEN n ∧ x = &n * (pi / 2)
[DIFF_ACS] Theorem
⊢ ∀x. -1 < x ∧ x < 1 ⇒ (acs diffl -(sqrt (1 − x²))⁻¹) x
[DIFF_ACS_LEMMA] Theorem
⊢ ∀x. -1 < x ∧ x < 1 ⇒ (acs diffl (-sin (acs x))⁻¹) x
[DIFF_ASN] Theorem
⊢ ∀x. -1 < x ∧ x < 1 ⇒ (asn diffl (sqrt (1 − x²))⁻¹) x
[DIFF_ASN_LEMMA] Theorem
⊢ ∀x. -1 < x ∧ x < 1 ⇒ (asn diffl (cos (asn x))⁻¹) x
[DIFF_ATN] Theorem
⊢ ∀x. (atn diffl (1 + x²)⁻¹) x
[DIFF_COMPOSITE] Theorem
⊢ ((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] Theorem
⊢ ∀g m x. (g diffl m) x ⇒ ((λx. exp (g x)) diffl (exp (g x) * m)) x
[DIFF_COS] Theorem
⊢ ∀x. (cos diffl -sin x) x
[DIFF_EXP] Theorem
⊢ ∀x. (exp diffl exp x) x
[DIFF_LN] Theorem
⊢ ∀x. 0 < x ⇒ (ln diffl x⁻¹) x
[DIFF_LN_COMPOSITE] Theorem
⊢ ∀g m x.
(g diffl m) x ∧ 0 < g x ⇒ ((λx. ln (g x)) diffl ((g x)⁻¹ * m)) x
[DIFF_LN_COMPOSITE'] Theorem
⊢ (g diffl m) x ∧ 0 < g x ⇒ ((λx. ln (g x)) diffl ((g x)⁻¹ * m)) x
[DIFF_RPOW] Theorem
⊢ ∀x y. 0 < x ⇒ ((λx. x powr y) diffl (y * x powr (y − 1))) x
[DIFF_SIN] Theorem
⊢ ∀x. (sin diffl cos x) x
[DIFF_TAN] Theorem
⊢ ∀x. cos x ≠ 0 ⇒ (tan diffl (cos x)² ⁻¹) x
[EXP_0] Theorem
⊢ exp 0 = 1
[EXP_ADD] Theorem
⊢ ∀x y. exp (x + y) = exp x * exp y
[EXP_ADD_MUL] Theorem
⊢ ∀x y. exp (x + y) * exp (-x) = exp y
[EXP_CONVERGES] Theorem
⊢ ∀x. (λn. (λn. (&FACT n)⁻¹) n * x pow n) sums exp x
[EXP_FDIFF] Theorem
⊢ diffs (λn. (&FACT n)⁻¹) = (λn. (&FACT n)⁻¹)
[EXP_INJ] Theorem
⊢ ∀x y. exp x = exp y ⇔ x = y
[EXP_LE_X] Theorem
⊢ ∀x. 0 ≤ x ⇒ 1 + x ≤ exp x
[EXP_LE_X_FULL] Theorem
⊢ ∀x. 1 + x ≤ exp x
[EXP_LN] Theorem
⊢ ∀x. exp (ln x) = x ⇔ 0 < x
[EXP_LT_1] Theorem
⊢ ∀x. 0 < x ⇒ 1 < exp x
[EXP_MONO_IMP] Theorem
⊢ ∀x y. x < y ⇒ exp x < exp y
[EXP_MONO_LE] Theorem
⊢ ∀x y. exp x ≤ exp y ⇔ x ≤ y
[EXP_MONO_LT] Theorem
⊢ ∀x y. exp x < exp y ⇔ x < y
[EXP_N] Theorem
⊢ ∀n x. exp (&n * x) = exp x pow n
[EXP_NEG] Theorem
⊢ ∀x. exp (-x) = (exp x)⁻¹
[EXP_NEG_MUL] Theorem
⊢ ∀x. exp x * exp (-x) = 1
[EXP_NEG_MUL2] Theorem
⊢ ∀x. exp (-x) * exp x = 1
[EXP_NZ] Theorem
⊢ ∀x. exp x ≠ 0
[EXP_POS_LE] Theorem
⊢ ∀x. 0 ≤ exp x
[EXP_POS_LT] Theorem
⊢ ∀x. 0 < exp x
[EXP_SUB] Theorem
⊢ ∀x y. exp (x − y) = exp x / exp y
[EXP_TOTAL] Theorem
⊢ ∀y. 0 < y ⇒ ∃x. exp x = y
[EXP_TOTAL_LEMMA] Theorem
⊢ ∀y. 1 ≤ y ⇒ ∃x. 0 ≤ x ∧ x ≤ y − 1 ∧ exp x = y
[GEN_RPOW] Theorem
⊢ ∀a n. 0 < a ⇒ a pow n = a powr &n
[LN_1] Theorem
⊢ ln 1 = 0
[LN_DIV] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ ln (x / y) = ln x − ln y
[LN_EXP] Theorem
⊢ ∀x. ln (exp x) = x
[LN_INJ] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (ln x = ln y ⇔ x = y)
[LN_INV] Theorem
⊢ ∀x. 0 < x ⇒ ln x⁻¹ = -ln x
[LN_LE] Theorem
⊢ ∀x. 0 ≤ x ⇒ ln (1 + x) ≤ x
[LN_LT_X] Theorem
⊢ ∀x. 0 < x ⇒ ln x < x
[LN_MONO_LE] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (ln x ≤ ln y ⇔ x ≤ y)
[LN_MONO_LT] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (ln x < ln y ⇔ x < y)
[LN_MUL] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ ln (x * y) = ln x + ln y
[LN_NEG] Theorem
⊢ ∀x. 0 < x ∧ x ≤ 1 ⇒ ln x ≤ 0
[LN_NEG_LT] Theorem
⊢ ∀x. 0 < x ∧ x < 1 ⇒ ln x < 0
[LN_POS] Theorem
⊢ ∀x. 1 ≤ x ⇒ 0 ≤ ln x
[LN_POS_LT] Theorem
⊢ ∀x. 1 < x ⇒ 0 < ln x
[LN_POW] Theorem
⊢ ∀n x. 0 < x ⇒ ln (x pow n) = &n * ln x
[LN_PRODUCT] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒
ln (product s f) = sum s (λx. ln (f x))
[LN_RPOW] Theorem
⊢ ∀a b. 0 < a ⇒ ln (a powr b) = b * ln a
[LOGR_MONO_LE] Theorem
⊢ ∀x y b. 0 < x ∧ 0 < y ∧ 1 < b ⇒ (logr b x ≤ logr b y ⇔ x ≤ y)
[LOGR_MONO_LE_IMP] Theorem
⊢ ∀x y b. 0 < x ∧ x ≤ y ∧ 1 ≤ b ⇒ logr b x ≤ logr b y
[LOGR_MONO_LT] Theorem
⊢ ∀x y b. 0 < x ∧ 0 < y ∧ 1 < b ⇒ (logr b x < logr b y ⇔ x < y)
[MCLAURIN] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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] Theorem
⊢ ∀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_LN_NEG] Theorem
⊢ ∀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)
[MCLAURIN_LN_POS] Theorem
⊢ ∀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)
[MCLAURIN_NEG] Theorem
⊢ ∀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] Theorem
⊢ ∀diff n x.
x = 0 ∧ 0 < n ⇒
sum (0,n) (λm. diff m 0 / &FACT m * x pow m) = diff 0 0
[ONE_RPOW] Theorem
⊢ ∀a. 0 < a ⇒ 1 powr a = 1
[PI2] Theorem
⊢ pi / 2 = @x. 0 ≤ x ∧ x ≤ 2 ∧ cos x = 0
[PI2_BOUNDS] Theorem
⊢ 0 < pi / 2 ∧ pi / 2 < 2
[PI_POS] Theorem
⊢ 0 < pi
[POW_ROOT_POS] Theorem
⊢ ∀n x. 0 ≤ x ⇒ root (SUC n) (x pow SUC n) = x
[REAL_DIV_SQRT] Theorem
⊢ ∀x. 0 ≤ x ⇒ x / sqrt x = sqrt x
[REAL_EXP_ADD] Theorem
⊢ ∀x y. exp (x + y) = exp x * exp y
[REAL_EXP_BOUND_LEMMA] Theorem
⊢ ∀x. 0 ≤ x ∧ x ≤ 2⁻¹ ⇒ exp x ≤ 1 + 2 * x
[REAL_ROOT_RPOW] Theorem
⊢ ∀n x. n ≠ 0 ∧ 0 < x ⇒ root n x = x powr (&n)⁻¹
[ROOT_0] Theorem
⊢ ∀n. root (SUC n) 0 = 0
[ROOT_1] Theorem
⊢ ∀n. root (SUC n) 1 = 1
[ROOT_11] Theorem
⊢ ∀n x y. 0 ≤ x ∧ 0 ≤ y ∧ root (SUC n) x = root (SUC n) y ⇒ x = y
[ROOT_DIV] Theorem
⊢ ∀n x y.
0 ≤ x ∧ 0 ≤ y ⇒
root (SUC n) (x / y) = root (SUC n) x / root (SUC n) y
[ROOT_INV] Theorem
⊢ ∀n x. 0 ≤ x ⇒ root (SUC n) x⁻¹ = (root (SUC n) x)⁻¹
[ROOT_LN] Theorem
⊢ ∀n x. 0 < x ⇒ root (SUC n) x = exp (ln x / &SUC n)
[ROOT_LT_LEMMA] Theorem
⊢ ∀n x. 0 < x ⇒ exp (ln x / &SUC n) pow SUC n = x
[ROOT_MONO_LE] Theorem
⊢ ∀n x y. 0 ≤ x ∧ x ≤ y ⇒ root (SUC n) x ≤ root (SUC n) y
[ROOT_MONO_LE_EQ] Theorem
⊢ ∀n x y. 0 ≤ x ∧ 0 ≤ y ⇒ (root (SUC n) x ≤ root (SUC n) y ⇔ x ≤ y)
[ROOT_MUL] Theorem
⊢ ∀n x y.
0 ≤ x ∧ 0 ≤ y ⇒
root (SUC n) (x * y) = root (SUC n) x * root (SUC n) y
[ROOT_POS] Theorem
⊢ ∀n x. 0 ≤ x ⇒ 0 ≤ root (SUC n) x
[ROOT_POS_LT] Theorem
⊢ ∀n x. 0 < x ⇒ 0 < root (SUC n) x
[ROOT_POS_UNIQ] Theorem
⊢ ∀n x y. 0 ≤ x ∧ 0 ≤ y ∧ y pow SUC n = x ⇒ root (SUC n) x = y
[ROOT_POW_POS] Theorem
⊢ ∀n x. 0 ≤ x ⇒ root (SUC n) x pow SUC n = x
[ROOT_PRODUCT] Theorem
⊢ ∀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))
[RPOW_0] Theorem
⊢ ∀a. 0 < a ⇒ a powr 0 = 1
[RPOW_1] Theorem
⊢ ∀a. 0 < a ⇒ a powr 1 = a
[RPOW_ADD] Theorem
⊢ ∀a b c. a powr (b + c) = a powr b * a powr c
[RPOW_ADD_MUL] Theorem
⊢ ∀a b c. a powr (b + c) * a powr -b = a powr c
[RPOW_DIV] Theorem
⊢ ∀a b c. 0 < a ∧ 0 < b ⇒ (a / b) powr c = a powr c / b powr c
[RPOW_DIV_BASE] Theorem
⊢ ∀x t. 0 < x ⇒ x powr t / x = x powr (t − 1)
[RPOW_INV] Theorem
⊢ ∀a b. 0 < a ⇒ a⁻¹ powr b = (a powr b)⁻¹
[RPOW_LE] Theorem
⊢ ∀a b c. 1 < a ⇒ (a powr b ≤ a powr c ⇔ b ≤ c)
[RPOW_LT] Theorem
⊢ ∀a b c. 1 < a ⇒ (a powr b < a powr c ⇔ b < c)
[RPOW_MUL] Theorem
⊢ ∀a b c. 0 < a ∧ 0 < b ⇒ (a * b) powr c = a powr c * b powr c
[RPOW_NZ] Theorem
⊢ ∀a b. 0 ≠ a ⇒ a powr b ≠ 0
[RPOW_POS_LT] Theorem
⊢ ∀a b. 0 < a ⇒ 0 < a powr b
[RPOW_RPOW] Theorem
⊢ ∀a b c. 0 < a ⇒ (a powr b) powr c = a powr (b * c)
[RPOW_SUB] Theorem
⊢ ∀a b c. a powr (b − c) = a powr b / a powr c
[RPOW_SUC_N] Theorem
⊢ ∀a n. 0 < a ⇒ a powr (&n + 1) = a pow SUC n
[RPOW_UNIQ_BASE] Theorem
⊢ ∀a b c. 0 < a ∧ 0 < c ∧ 0 ≠ b ∧ a powr b = c powr b ⇒ a = c
[RPOW_UNIQ_EXP] Theorem
⊢ ∀a b c. 1 < a ∧ 0 < c ∧ 0 < b ∧ a powr b = a powr c ⇒ b = c
[SIN_0] Theorem
⊢ sin 0 = 0
[SIN_ACS_NZ] Theorem
⊢ ∀x. -1 < x ∧ x < 1 ⇒ sin (acs x) ≠ 0
[SIN_ADD] Theorem
⊢ ∀x y. sin (x + y) = sin x * cos y + cos x * sin y
[SIN_ASN] Theorem
⊢ ∀x. -(pi / 2) ≤ x ∧ x ≤ pi / 2 ⇒ asn (sin x) = x
[SIN_BOUND] Theorem
⊢ ∀x. abs (sin x) ≤ 1
[SIN_BOUNDS] Theorem
⊢ ∀x. -1 ≤ sin x ∧ sin x ≤ 1
[SIN_CIRCLE] Theorem
⊢ ∀x. (sin x)² + (cos x)² = 1
[SIN_CONVERGES] Theorem
⊢ ∀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] Theorem
⊢ ∀x. sin x = cos (pi / 2 − x)
[SIN_COS_ADD] Theorem
⊢ ∀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] Theorem
⊢ ∀x. (sin (-x) + sin x)² + (cos (-x) − cos x)² = 0
[SIN_COS_SQ] Theorem
⊢ ∀x. 0 ≤ x ∧ x ≤ pi ⇒ sin x = sqrt (1 − (cos x)²)
[SIN_COS_SQRT] Theorem
⊢ ∀x. 0 ≤ sin x ⇒ sin x = sqrt (1 − (cos x)²)
[SIN_DOUBLE] Theorem
⊢ ∀x. sin (2 * x) = 2 * (sin x * cos x)
[SIN_FDIFF] Theorem
⊢ 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] Theorem
⊢ ∀x. sin (-x) = -sin x
[SIN_NEGLEMMA] Theorem
⊢ ∀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] Theorem
⊢ ∀n. sin (&n * pi) = 0
[SIN_PAIRED] Theorem
⊢ ∀x. (λn. -1 pow n / &FACT (2 * n + 1) * x pow (2 * n + 1)) sums
sin x
[SIN_PERIODIC] Theorem
⊢ ∀x. sin (x + 2 * pi) = sin x
[SIN_PERIODIC_PI] Theorem
⊢ ∀x. sin (x + pi) = -sin x
[SIN_PI] Theorem
⊢ sin pi = 0
[SIN_PI2] Theorem
⊢ sin (pi / 2) = 1
[SIN_POS] Theorem
⊢ ∀x. 0 < x ∧ x < 2 ⇒ 0 < sin x
[SIN_POS_PI] Theorem
⊢ ∀x. 0 < x ∧ x < pi ⇒ 0 < sin x
[SIN_POS_PI2] Theorem
⊢ ∀x. 0 < x ∧ x < pi / 2 ⇒ 0 < sin x
[SIN_POS_PI2_LE] Theorem
⊢ ∀x. 0 ≤ x ∧ x ≤ pi / 2 ⇒ 0 ≤ sin x
[SIN_POS_PI_LE] Theorem
⊢ ∀x. 0 ≤ x ∧ x ≤ pi ⇒ 0 ≤ sin x
[SIN_TOTAL] Theorem
⊢ ∀y. -1 ≤ y ∧ y ≤ 1 ⇒ ∃!x. -(pi / 2) ≤ x ∧ x ≤ pi / 2 ∧ sin x = y
[SIN_ZERO] Theorem
⊢ ∀x. sin x = 0 ⇔
(∃n. EVEN n ∧ x = &n * (pi / 2)) ∨
∃n. EVEN n ∧ x = -(&n * (pi / 2))
[SIN_ZERO_LEMMA] Theorem
⊢ ∀x. 0 ≤ x ∧ sin x = 0 ⇒ ∃n. EVEN n ∧ x = &n * (pi / 2)
[SQRT_EVEN_POW2] Theorem
⊢ ∀n. EVEN n ⇒ sqrt (2 pow n) = 2 pow (n DIV 2)
[SQRT_RPOW] Theorem
⊢ ∀x. 0 < x ⇒ sqrt x = x powr 2⁻¹
[TAN_0] Theorem
⊢ tan 0 = 0
[TAN_ADD] Theorem
⊢ ∀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] Theorem
⊢ ∀x. -(pi / 2) < x ∧ x < pi / 2 ⇒ atn (tan x) = x
[TAN_DOUBLE] Theorem
⊢ ∀x. cos x ≠ 0 ∧ cos (2 * x) ≠ 0 ⇒
tan (2 * x) = 2 * tan x / (1 − (tan x)²)
[TAN_NEG] Theorem
⊢ ∀x. tan (-x) = -tan x
[TAN_NPI] Theorem
⊢ ∀n. tan (&n * pi) = 0
[TAN_PERIODIC] Theorem
⊢ ∀x. tan (x + 2 * pi) = tan x
[TAN_PI] Theorem
⊢ tan pi = 0
[TAN_POS_PI2] Theorem
⊢ ∀x. 0 < x ∧ x < pi / 2 ⇒ 0 < tan x
[TAN_SEC] Theorem
⊢ ∀x. cos x ≠ 0 ⇒ 1 + (tan x)² = (cos x)⁻¹ ²
[TAN_TOTAL] Theorem
⊢ ∀y. ∃!x. -(pi / 2) < x ∧ x < pi / 2 ∧ tan x = y
[TAN_TOTAL_LEMMA] Theorem
⊢ ∀y. 0 < y ⇒ ∃x. 0 < x ∧ x < pi / 2 ∧ y < tan x
[TAN_TOTAL_POS] Theorem
⊢ ∀y. 0 ≤ y ⇒ ∃x. 0 ≤ x ∧ x < pi / 2 ∧ tan x = y
[YOUNG_INEQUALITY] Theorem
⊢ ∀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
[exp] Theorem
⊢ ∀x. exp x = suminf (λn. (λn. (&FACT n)⁻¹) n * x pow n)
[exp_convex] Theorem
⊢ exp ∈ convex_fn
[lg_1] Theorem
⊢ lg 1 = 0
[lg_2] Theorem
⊢ lg 2 = 1
[lg_inv] Theorem
⊢ ∀x. 0 < x ⇒ lg x⁻¹ = -lg x
[lg_mul] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ lg (x * y) = lg x + lg y
[lg_nonzero] Theorem
⊢ ∀x. x ≠ 0 ∧ 0 ≤ x ⇒ (lg x ≠ 0 ⇔ x ≠ 1)
[lg_pow] Theorem
⊢ ∀n. lg (2 pow n) = &n
[logr_1] Theorem
⊢ ∀b. logr b 1 = 0
[logr_div] Theorem
⊢ ∀b x y. 0 < x ∧ 0 < y ⇒ logr b (x / y) = logr b x − logr b y
[logr_inv] Theorem
⊢ ∀b x. 0 < x ⇒ logr b x⁻¹ = -logr b x
[logr_mul] Theorem
⊢ ∀b x y. 0 < x ∧ 0 < y ⇒ logr b (x * y) = logr b x + logr b y
[neg_lg] Theorem
⊢ ∀x. 0 < x ⇒ -lg x = lg x⁻¹
[neg_logr] Theorem
⊢ ∀b x. 0 < x ⇒ -logr b x = logr b x⁻¹
[pos_concave_lg] Theorem
⊢ lg ∈ pos_concave_fn
[pos_concave_ln] Theorem
⊢ ln ∈ pos_concave_fn
[pos_concave_logr] Theorem
⊢ ∀b. 1 ≤ b ⇒ logr b ∈ pos_concave_fn
[pos_convex_inv] Theorem
⊢ realinv ∈ pos_convex_fn
[sqrt] Theorem
⊢ ∀x. sqrt x = root 2 x
*)
end
HOL 4, Trindemossen-1