:: Properties of Trigonometric Function :: by Takashi Mitsuishi and Yuguang Yang :: :: Received March 13, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin theorem Th1: :: SIN_COS2:1 for p, r being real number st p >= 0 & r >= 0 holds p + r >= 2 * (sqrt (p * r)) proofend; theorem :: SIN_COS2:2 sin | ].0,(PI / 2).[ is increasing proofend; Lm1: for th being real number st th in ].0,(PI / 2).[ holds 0 < sin . th proofend; theorem :: SIN_COS2:3 sin | ].(PI / 2),PI.[ is decreasing proofend; theorem :: SIN_COS2:4 cos | ].0,(PI / 2).[ is decreasing proofend; theorem :: SIN_COS2:5 cos | ].(PI / 2),PI.[ is decreasing proofend; theorem :: SIN_COS2:6 sin | ].PI,((3 / 2) * PI).[ is decreasing proofend; theorem :: SIN_COS2:7 sin | ].((3 / 2) * PI),(2 * PI).[ is increasing proofend; theorem :: SIN_COS2:8 cos | ].PI,((3 / 2) * PI).[ is increasing proofend; theorem :: SIN_COS2:9 cos | ].((3 / 2) * PI),(2 * PI).[ is increasing proofend; theorem :: SIN_COS2:10 for th being real number for n being Nat holds sin . th = sin . (((2 * PI) * n) + th) proofend; theorem :: SIN_COS2:11 for th being real number for n being Nat holds cos . th = cos . (((2 * PI) * n) + th) proofend; begin definition func sinh -> Function of REAL,REAL means :Def1: :: SIN_COS2:def 1 for d being real number holds it . d = ((exp_R . d) - (exp_R . (- d))) / 2; existence ex b1 being Function of REAL,REAL st for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / 2 proofend; uniqueness for b1, b2 being Function of REAL,REAL st ( for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ) & ( for d being real number holds b2 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines sinh SIN_COS2:def_1_:_ for b1 being Function of REAL,REAL holds ( b1 = sinh iff for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- 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 -> Function of REAL,REAL means :Def3: :: SIN_COS2:def 3 for d being real number holds it . d = ((exp_R . d) + (exp_R . (- d))) / 2; existence ex b1 being Function of REAL,REAL st for d being real number holds b1 . d = ((exp_R . d) + (exp_R . (- d))) / 2 proofend; uniqueness for b1, b2 being Function of REAL,REAL st ( for d being real number holds b1 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ) & ( for d being real number holds b2 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines cosh SIN_COS2:def_3_:_ for b1 being Function of REAL,REAL holds ( b1 = cosh iff for d being real number holds b1 . d = ((exp_R . d) + (exp_R . (- 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 -> Function of REAL,REAL means :Def5: :: SIN_COS2:def 5 for d being real number holds it . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))); existence ex b1 being Function of REAL,REAL st for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) proofend; uniqueness for b1, b2 being Function of REAL,REAL st ( for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ) & ( for d being real number holds b2 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines tanh SIN_COS2:def_5_:_ for b1 being Function of REAL,REAL holds ( b1 = tanh iff for d being real number holds b1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- 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 for p, q being real number holds exp_R . (p + q) = (exp_R . p) * (exp_R . q) proofend; theorem Th13: :: SIN_COS2:13 exp_R . 0 = 1 by SIN_COS:51, SIN_COS:def_23; theorem Th14: :: SIN_COS2:14 for p being real number holds ( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 ) proofend; Lm2: for p, r being real number holds cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) proofend; Lm3: for p, r being real number holds sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) proofend; theorem Th15: :: SIN_COS2:15 for p being real number holds ( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 ) proofend; theorem Th16: :: SIN_COS2:16 sinh . 0 = 0 proofend; theorem Th17: :: SIN_COS2:17 for p being real number holds tanh . p = (sinh . p) / (cosh . p) proofend; Lm4: for r, q, p, a1 being real number st r <> 0 & q <> 0 holds ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) proofend; Lm5: for p, r being real number holds tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) proofend; theorem Th18: :: SIN_COS2:18 for p being real number holds ( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) ) proofend; Lm6: for p being real number holds ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 ) proofend; theorem Th19: :: SIN_COS2:19 for p being real number holds ( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) ) proofend; Lm7: for p, r being real number holds cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r)) proofend; theorem :: SIN_COS2:20 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 Lm2, Lm7; Lm8: for p, r being real number holds sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) proofend; theorem :: SIN_COS2:21 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 Lm3, Lm8; Lm9: for p, r being real number holds tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) proofend; theorem :: SIN_COS2:22 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 Lm5, Lm9; theorem :: SIN_COS2:23 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)) ) proofend; theorem Th24: :: SIN_COS2:24 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) ) proofend; theorem Th25: :: SIN_COS2:25 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) ) proofend; theorem :: SIN_COS2:26 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))) ) proofend; theorem :: SIN_COS2:27 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))) ) proofend; theorem :: SIN_COS2:28 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)) ) proofend; theorem :: SIN_COS2:29 for p being real number for n being Element of NAT holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p)) proofend; theorem Th30: :: SIN_COS2:30 ( dom sinh = REAL & dom cosh = REAL & dom tanh = REAL ) by FUNCT_2:def_1; Lm10: for d being real number holds compreal . d = (- 1) * d proofend; Lm11: dom compreal = REAL by FUNCT_2:def_1; Lm12: 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 ) proofend; Lm13: for p being real number for f being PartFunc of REAL,REAL st f = compreal holds ( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) ) proofend; Lm14: for p being real number for f being PartFunc of REAL,REAL st f = compreal holds exp_R . ((- 1) * p) = (exp_R * f) . p proofend; Lm15: for p being real number for f being PartFunc of REAL,REAL st f = compreal holds ( exp_R - (exp_R * f) is_differentiable_in p & exp_R + (exp_R * f) is_differentiable_in p & diff ((exp_R - (exp_R * f)),p) = (exp_R . p) + (exp_R . (- p)) & diff ((exp_R + (exp_R * f)),p) = (exp_R . p) - (exp_R . (- p)) ) proofend; Lm16: for p being real number for f being PartFunc of REAL,REAL st f = compreal holds ( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R - (exp_R * f))),p) = (1 / 2) * (diff ((exp_R - (exp_R * f)),p)) ) proofend; Lm17: for p being real number for ff being PartFunc of REAL,REAL st ff = compreal holds sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p proofend; Lm18: for ff being PartFunc of REAL,REAL st ff = compreal holds sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) proofend; theorem Th31: :: SIN_COS2:31 for p being real number holds ( sinh is_differentiable_in p & diff (sinh,p) = cosh . p ) proofend; Lm19: for p being real number for ff being PartFunc of REAL,REAL st ff = compreal holds ( (1 / 2) (#) (exp_R + (exp_R * ff)) is_differentiable_in p & diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) = (1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) ) proofend; Lm20: for p being real number for ff being PartFunc of REAL,REAL st ff = compreal holds cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p proofend; Lm21: for ff being PartFunc of REAL,REAL st ff = compreal holds cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) proofend; theorem Th32: :: SIN_COS2:32 for p being real number holds ( cosh is_differentiable_in p & diff (cosh,p) = sinh . p ) proofend; Lm22: for p being real number holds ( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) ) proofend; Lm23: tanh = sinh / cosh proofend; theorem :: SIN_COS2:33 for p being real number holds ( tanh is_differentiable_in p & diff (tanh,p) = 1 / ((cosh . p) ^2) ) by Lm22, Lm23; theorem Th34: :: SIN_COS2:34 for p being real number holds ( sinh is_differentiable_on REAL & diff (sinh,p) = cosh . p ) proofend; theorem Th35: :: SIN_COS2:35 for p being real number holds ( cosh is_differentiable_on REAL & diff (cosh,p) = sinh . p ) proofend; theorem Th36: :: SIN_COS2:36 for p being real number holds ( tanh is_differentiable_on REAL & diff (tanh,p) = 1 / ((cosh . p) ^2) ) proofend; Lm24: for p being real number holds (exp_R . p) + (exp_R . (- p)) >= 2 proofend; theorem :: SIN_COS2:37 for p being real number holds cosh . p >= 1 proofend; theorem :: SIN_COS2:38 for p being real number holds sinh is_continuous_in p by Th31, FDIFF_1:24; theorem :: SIN_COS2:39 for p being real number holds cosh is_continuous_in p by Th32, FDIFF_1:24; theorem :: SIN_COS2:40 for p being real number holds tanh is_continuous_in p by Lm22, Lm23, FDIFF_1:24; theorem :: SIN_COS2:41 sinh | REAL is continuous by Th34, FDIFF_1:25; theorem :: SIN_COS2:42 cosh | REAL is continuous by Th35, FDIFF_1:25; theorem :: SIN_COS2:43 tanh | REAL is continuous by Th36, FDIFF_1:25; theorem :: SIN_COS2:44 for p being real number holds ( tanh . p < 1 & tanh . p > - 1 ) proofend;