:: SIN_COS2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: ( 0 < PI / 2 & PI / 2 < PI & PI < (3 / 2) * PI & (3 / 2) * PI < 2 * PI )
proof end;

theorem Th1: :: SIN_COS2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, r being real number st p >= 0 & r >= 0 holds
p + r >= 2 * (sqrt (p * r))
proof end;

theorem :: SIN_COS2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
sin is_increasing_on ].0,(PI / 2).[
proof end;

Lm2: for th being real number st th in ].0,(PI / 2).[ holds
0 < sin . th
proof end;

theorem :: SIN_COS2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
sin is_decreasing_on ].(PI / 2),PI .[
proof end;

theorem :: SIN_COS2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
cos is_decreasing_on ].0,(PI / 2).[
proof end;

theorem :: SIN_COS2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
cos is_decreasing_on ].(PI / 2),PI .[
proof end;

theorem :: SIN_COS2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
sin is_decreasing_on ].PI ,((3 / 2) * PI ).[
proof end;

theorem :: SIN_COS2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
sin is_increasing_on ].((3 / 2) * PI ),(2 * PI ).[
proof end;

theorem :: SIN_COS2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
cos is_increasing_on ].PI ,((3 / 2) * PI ).[
proof end;

theorem :: SIN_COS2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
cos is_increasing_on ].((3 / 2) * PI ),(2 * PI ).[
proof end;

theorem :: SIN_COS2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th being real number
for n being Nat holds sin . th = sin . (((2 * PI ) * n) + th)
proof end;

theorem :: SIN_COS2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for th being real number
for n being Nat holds cos . th = cos . (((2 * PI ) * n) + th)
proof end;

definition
func sinh -> PartFunc of REAL , REAL means :Def1: :: SIN_COS2:def 1
( dom it = REAL & ( for d being real number holds it . d = ((exp . d) - (exp . (- d))) / 2 ) );
existence
ex b1 being PartFunc of REAL , REAL st
( dom b1 = REAL & ( for d being real number holds b1 . d = ((exp . d) - (exp . (- d))) / 2 ) )
proof end;
uniqueness
for b1, b2 being PartFunc of REAL , REAL st dom b1 = REAL & ( for d being real number holds b1 . d = ((exp . d) - (exp . (- d))) / 2 ) & dom b2 = REAL & ( for d being real number holds b2 . d = ((exp . d) - (exp . (- d))) / 2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines sinh SIN_COS2:def 1 :
for b1 being PartFunc of REAL , REAL holds
( b1 = sinh iff ( dom b1 = REAL & ( for d being real number holds b1 . d = ((exp . d) - (exp . (- d))) / 2 ) ) );

definition
let d be number ;
func sinh d -> set equals :: SIN_COS2:def 2
sinh . d;
coherence
sinh . d is set ;
end;

:: deftheorem defines sinh SIN_COS2:def 2 :
for d being number holds sinh d = sinh . d;

registration
let d be number ;
cluster sinh d -> real ;
coherence
sinh d is real ;
end;

definition
let d be number ;
:: original: sinh
redefine func sinh d -> Real;
coherence
sinh d is Real ;
end;

definition
func cosh -> PartFunc of REAL , REAL means :Def3: :: SIN_COS2:def 3
( dom it = REAL & ( for d being real number holds it . d = ((exp . d) + (exp . (- d))) / 2 ) );
existence
ex b1 being PartFunc of REAL , REAL st
( dom b1 = REAL & ( for d being real number holds b1 . d = ((exp . d) + (exp . (- d))) / 2 ) )
proof end;
uniqueness
for b1, b2 being PartFunc of REAL , REAL st dom b1 = REAL & ( for d being real number holds b1 . d = ((exp . d) + (exp . (- d))) / 2 ) & dom b2 = REAL & ( for d being real number holds b2 . d = ((exp . d) + (exp . (- d))) / 2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines cosh SIN_COS2:def 3 :
for b1 being PartFunc of REAL , REAL holds
( b1 = cosh iff ( dom b1 = REAL & ( for d being real number holds b1 . d = ((exp . d) + (exp . (- d))) / 2 ) ) );

definition
let d be number ;
func cosh d -> set equals :: SIN_COS2:def 4
cosh . d;
coherence
cosh . d is set ;
end;

:: deftheorem defines cosh SIN_COS2:def 4 :
for d being number holds cosh d = cosh . d;

registration
let d be number ;
cluster cosh d -> real ;
coherence
cosh d is real ;
end;

definition
let d be number ;
:: original: cosh
redefine func cosh d -> Real;
coherence
cosh d is Real ;
end;

definition
func tanh -> PartFunc of REAL , REAL means :Def5: :: SIN_COS2:def 5
( dom it = REAL & ( for d being real number holds it . d = ((exp . d) - (exp . (- d))) / ((exp . d) + (exp . (- d))) ) );
existence
ex b1 being PartFunc of REAL , REAL st
( dom b1 = REAL & ( for d being real number holds b1 . d = ((exp . d) - (exp . (- d))) / ((exp . d) + (exp . (- d))) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of REAL , REAL st dom b1 = REAL & ( for d being real number holds b1 . d = ((exp . d) - (exp . (- d))) / ((exp . d) + (exp . (- d))) ) & dom b2 = REAL & ( for d being real number holds b2 . d = ((exp . d) - (exp . (- d))) / ((exp . d) + (exp . (- d))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines tanh SIN_COS2:def 5 :
for b1 being PartFunc of REAL , REAL holds
( b1 = tanh iff ( dom b1 = REAL & ( for d being real number holds b1 . d = ((exp . d) - (exp . (- d))) / ((exp . d) + (exp . (- d))) ) ) );

definition
let d be number ;
func tanh d -> set equals :: SIN_COS2:def 6
tanh . d;
coherence
tanh . d is set ;
end;

:: deftheorem defines tanh SIN_COS2:def 6 :
for d being number holds tanh d = tanh . d;

registration
let d be number ;
cluster tanh d -> real ;
coherence
tanh d is real ;
end;

definition
let d be number ;
:: original: tanh
redefine func tanh d -> Real;
coherence
tanh d is Real ;
end;

theorem Th12: :: SIN_COS2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being real number holds exp . (p + q) = (exp . p) * (exp . q)
proof end;

theorem Th13: :: SIN_COS2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
exp . 0 = 1 by SIN_COS:56, SIN_COS:def 27;

theorem Th14: :: SIN_COS2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( ((cosh . p) ^2 ) - ((sinh . p) ^2 ) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 )
proof end;

Lm3: for p, r being real number holds cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))
proof end;

Lm4: for p, r being real number holds sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))
proof end;

theorem Th15: :: SIN_COS2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 )
proof end;

theorem Th16: :: SIN_COS2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
sinh . 0 = 0
proof end;

theorem Th17: :: SIN_COS2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds tanh . p = (sinh . p) / (cosh . p)
proof end;

Lm5: for r, q, p, a1 being real number st r <> 0 & q <> 0 & (r * q) + (p * a1) <> 0 holds
((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q)))
proof end;

Lm6: for p, r being real number holds tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r)))
proof end;

theorem Th18: :: SIN_COS2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) )
proof end;

Lm7: for p being real number holds
( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2 )) - 1 )
proof end;

theorem Th19: :: SIN_COS2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) )
proof end;

Lm8: for p, r being real number holds cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r))
proof end;

theorem :: SIN_COS2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, r being real number holds
( cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) & cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r)) ) by Lm3, Lm8;

Lm9: for p, r being real number holds sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))
proof end;

theorem :: SIN_COS2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, r being real number holds
( sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) & sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) ) by Lm4, Lm9;

Lm10: for p, r being real number holds tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r)))
proof end;

theorem :: SIN_COS2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, r being real number holds
( tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) & tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) ) by Lm6, Lm10;

theorem :: SIN_COS2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2 )) - 1 & tanh . (2 * p) = (2 * (tanh . p)) / (1 + ((tanh . p) ^2 )) )
proof end;

theorem Th24: :: SIN_COS2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being real number holds
( ((sinh . p) ^2 ) - ((sinh . q) ^2 ) = (sinh . (p + q)) * (sinh . (p - q)) & (sinh . (p + q)) * (sinh . (p - q)) = ((cosh . p) ^2 ) - ((cosh . q) ^2 ) & ((sinh . p) ^2 ) - ((sinh . q) ^2 ) = ((cosh . p) ^2 ) - ((cosh . q) ^2 ) )
proof end;

theorem Th25: :: SIN_COS2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being real number holds
( ((sinh . p) ^2 ) + ((cosh . q) ^2 ) = (cosh . (p + q)) * (cosh . (p - q)) & (cosh . (p + q)) * (cosh . (p - q)) = ((cosh . p) ^2 ) + ((sinh . q) ^2 ) & ((sinh . p) ^2 ) + ((cosh . q) ^2 ) = ((cosh . p) ^2 ) + ((sinh . q) ^2 ) )
proof end;

theorem :: SIN_COS2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, r being real number holds
( (sinh . p) + (sinh . r) = (2 * (sinh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (sinh . p) - (sinh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (cosh . ((p / 2) + (r / 2))) )
proof end;

theorem :: SIN_COS2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, r being real number holds
( (cosh . p) + (cosh . r) = (2 * (cosh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (cosh . p) - (cosh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (sinh . ((p / 2) + (r / 2))) )
proof end;

theorem :: SIN_COS2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, r being real number holds
( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) )
proof end;

theorem :: SIN_COS2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number
for n being Nat holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p))
proof end;

registration
cluster sinh -> total ;
coherence
sinh is total
proof end;
cluster cosh -> total ;
coherence
cosh is total
proof end;
cluster tanh -> total ;
coherence
tanh is total
proof end;
end;

theorem Th30: :: SIN_COS2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( dom sinh = REAL & dom cosh = REAL & dom tanh = REAL ) by Def1, Def3, Def5;

Lm11: for d being real number holds compreal . d = (- 1) * d
proof end;

Lm12: ( dom compreal = REAL & rng compreal c= REAL )
by FUNCT_2:def 1, RELSET_1:12;

Lm13: for f being PartFunc of REAL , REAL st f = compreal holds
for p being real number holds
( f is_differentiable_in p & diff f,p = - 1 )
proof end;

Lm14: for p being real number
for f being PartFunc of REAL , REAL st f = compreal holds
( exp * f is_differentiable_in p & diff (exp * f),p = (- 1) * (exp . (f . p)) )
proof end;

Lm15: for p being real number
for f being PartFunc of REAL , REAL st f = compreal holds
exp . ((- 1) * p) = (exp * f) . p
proof end;

Lm16: for p being real number
for f being PartFunc of REAL , REAL st f = compreal holds
( exp - (exp * f) is_differentiable_in p & exp + (exp * f) is_differentiable_in p & diff (exp - (exp * f)),p = (exp . p) + (exp . (- p)) & diff (exp + (exp * f)),p = (exp . p) - (exp . (- p)) )
proof end;

Lm17: for p being real number
for f being PartFunc of REAL , REAL st f = compreal holds
( (1 / 2) (#) (exp - (exp * f)) is_differentiable_in p & diff ((1 / 2) (#) (exp - (exp * f))),p = (1 / 2) * (diff (exp - (exp * f)),p) )
proof end;

Lm18: for p being real number
for ff being PartFunc of REAL , REAL st ff = compreal holds
sinh . p = ((1 / 2) (#) (exp - (exp * ff))) . p
proof end;

Lm19: for ff being PartFunc of REAL , REAL st ff = compreal holds
sinh = (1 / 2) (#) (exp - (exp * ff))
proof end;

theorem Th31: :: SIN_COS2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( sinh is_differentiable_in p & diff sinh ,p = cosh . p )
proof end;

Lm20: for p being real number
for ff being PartFunc of REAL , REAL st ff = compreal holds
( (1 / 2) (#) (exp + (exp * ff)) is_differentiable_in p & diff ((1 / 2) (#) (exp + (exp * ff))),p = (1 / 2) * (diff (exp + (exp * ff)),p) )
proof end;

Lm21: for p being real number
for ff being PartFunc of REAL , REAL st ff = compreal holds
cosh . p = ((1 / 2) (#) (exp + (exp * ff))) . p
proof end;

Lm22: for ff being PartFunc of REAL , REAL st ff = compreal holds
cosh = (1 / 2) (#) (exp + (exp * ff))
proof end;

theorem Th32: :: SIN_COS2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( cosh is_differentiable_in p & diff cosh ,p = sinh . p )
proof end;

Lm23: for p being real number holds
( sinh / cosh is_differentiable_in p & diff (sinh / cosh ),p = 1 / ((cosh . p) ^2 ) )
proof end;

Lm24: tanh = sinh / cosh
proof end;

theorem :: SIN_COS2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( tanh is_differentiable_in p & diff tanh ,p = 1 / ((cosh . p) ^2 ) ) by Lm23, Lm24;

theorem Th34: :: SIN_COS2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( sinh is_differentiable_on REAL & diff sinh ,p = cosh . p )
proof end;

theorem Th35: :: SIN_COS2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( cosh is_differentiable_on REAL & diff cosh ,p = sinh . p )
proof end;

theorem Th36: :: SIN_COS2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( tanh is_differentiable_on REAL & diff tanh ,p = 1 / ((cosh . p) ^2 ) )
proof end;

Lm25: for p being real number holds (exp . p) + (exp . (- p)) >= 2
proof end;

theorem :: SIN_COS2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds cosh . p >= 1
proof end;

theorem :: SIN_COS2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds sinh is_continuous_in p
proof end;

theorem :: SIN_COS2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds cosh is_continuous_in p
proof end;

theorem :: SIN_COS2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds tanh is_continuous_in p
proof end;

theorem :: SIN_COS2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
sinh is_continuous_on REAL by Th34, FDIFF_1:33;

theorem :: SIN_COS2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
cosh is_continuous_on REAL by Th35, FDIFF_1:33;

theorem :: SIN_COS2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
tanh is_continuous_on REAL by Th36, FDIFF_1:33;

theorem :: SIN_COS2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number holds
( tanh . p < 1 & tanh . p > - 1 )
proof end;