:: SIN_COS2 semantic presentation begin theorem Th1: :: SIN_COS2:1 for p, r being real number st p >= 0 & r >= 0 holds p + r >= 2 * (sqrt (p * r)) proof let p, r be real number ; ::_thesis: ( p >= 0 & r >= 0 implies p + r >= 2 * (sqrt (p * r)) ) assume that A1: p >= 0 and A2: r >= 0 ; ::_thesis: p + r >= 2 * (sqrt (p * r)) A3: ((sqrt p) - (sqrt r)) ^2 >= 0 by XREAL_1:63; ((sqrt p) - (sqrt r)) ^2 = (((sqrt p) ^2) - ((2 * (sqrt p)) * (sqrt r))) + ((sqrt r) ^2) .= (p - ((2 * (sqrt p)) * (sqrt r))) + ((sqrt r) ^2) by A1, SQUARE_1:def_2 .= (p - ((2 * (sqrt p)) * (sqrt r))) + r by A2, SQUARE_1:def_2 .= (p + r) - ((2 * (sqrt p)) * (sqrt r)) ; then 0 + ((2 * (sqrt p)) * (sqrt r)) <= p + r by A3, XREAL_1:19; then 2 * ((sqrt p) * (sqrt r)) <= p + r ; hence p + r >= 2 * (sqrt (p * r)) by A1, A2, SQUARE_1:29; ::_thesis: verum end; theorem :: SIN_COS2:2 sin | ].0,(PI / 2).[ is increasing proof for th being Real st th in ].0,(PI / 2).[ holds 0 < diff (sin,th) proof let th be Real; ::_thesis: ( th in ].0,(PI / 2).[ implies 0 < diff (sin,th) ) assume th in ].0,(PI / 2).[ ; ::_thesis: 0 < diff (sin,th) then cos . th > 0 by SIN_COS:80; hence 0 < diff (sin,th) by SIN_COS:68; ::_thesis: verum end; hence sin | ].0,(PI / 2).[ is increasing by FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:68; ::_thesis: verum end; Lm1: for th being real number st th in ].0,(PI / 2).[ holds 0 < sin . th proof let th be real number ; ::_thesis: ( th in ].0,(PI / 2).[ implies 0 < sin . th ) assume A1: th in ].0,(PI / 2).[ ; ::_thesis: 0 < sin . th then th < PI / 2 by XXREAL_1:4; then - th > - (PI / 2) by XREAL_1:24; then A2: (- th) + (PI / 2) > (- (PI / 2)) + (PI / 2) by XREAL_1:6; 0 < th by A1, XXREAL_1:4; then 0 - th < 0 ; then (- th) + (PI / 2) < 0 + (PI / 2) by XREAL_1:6; then (PI / 2) - th in ].0,(PI / 2).[ by A2, XXREAL_1:4; then cos . ((PI / 2) - th) > 0 by SIN_COS:80; hence 0 < sin . th by SIN_COS:78; ::_thesis: verum end; theorem :: SIN_COS2:3 sin | ].(PI / 2),PI.[ is decreasing proof for th1 being Real st th1 in ].(PI / 2),PI.[ holds 0 > diff (sin,th1) proof let th1 be Real; ::_thesis: ( th1 in ].(PI / 2),PI.[ implies 0 > diff (sin,th1) ) assume A1: th1 in ].(PI / 2),PI.[ ; ::_thesis: 0 > diff (sin,th1) then th1 < PI by XXREAL_1:4; then A2: th1 - (PI / 2) < PI - (PI / 2) by XREAL_1:9; PI / 2 < th1 by A1, XXREAL_1:4; then (PI / 2) - (PI / 2) < th1 - (PI / 2) by XREAL_1:9; then th1 - (PI / 2) in ].0,(PI / 2).[ by A2, XXREAL_1:4; then sin . (th1 - (PI / 2)) > 0 by Lm1; then A3: 0 - (sin . (th1 - (PI / 2))) < 0 ; diff (sin,th1) = cos . ((PI / 2) + (th1 - (PI / 2))) by SIN_COS:68 .= - (sin . (th1 - (PI / 2))) by SIN_COS:78 ; hence 0 > diff (sin,th1) by A3; ::_thesis: verum end; hence sin | ].(PI / 2),PI.[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:68; ::_thesis: verum end; theorem :: SIN_COS2:4 cos | ].0,(PI / 2).[ is decreasing proof for th being Real st th in ].0,(PI / 2).[ holds diff (cos,th) < 0 proof let th be Real; ::_thesis: ( th in ].0,(PI / 2).[ implies diff (cos,th) < 0 ) assume th in ].0,(PI / 2).[ ; ::_thesis: diff (cos,th) < 0 then 0 < sin . th by Lm1; then ( diff (cos,th) = - (sin . th) & 0 - (sin . th) < 0 ) by SIN_COS:67; hence diff (cos,th) < 0 ; ::_thesis: verum end; hence cos | ].0,(PI / 2).[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:67; ::_thesis: verum end; theorem :: SIN_COS2:5 cos | ].(PI / 2),PI.[ is decreasing proof for th being Real st th in ].(PI / 2),PI.[ holds diff (cos,th) < 0 proof let th be Real; ::_thesis: ( th in ].(PI / 2),PI.[ implies diff (cos,th) < 0 ) assume A1: th in ].(PI / 2),PI.[ ; ::_thesis: diff (cos,th) < 0 then th < PI by XXREAL_1:4; then A2: th - (PI / 2) < PI - (PI / 2) by XREAL_1:9; PI / 2 < th by A1, XXREAL_1:4; then (PI / 2) - (PI / 2) < th - (PI / 2) by XREAL_1:9; then th - (PI / 2) in ].0,(PI / 2).[ by A2, XXREAL_1:4; then cos . (th - (PI / 2)) > 0 by SIN_COS:80; then A3: 0 - (cos . (th - (PI / 2))) < 0 ; diff (cos,th) = - (sin . ((PI / 2) + (th - (PI / 2)))) by SIN_COS:67 .= - (cos . (th - (PI / 2))) by SIN_COS:78 ; hence diff (cos,th) < 0 by A3; ::_thesis: verum end; hence cos | ].(PI / 2),PI.[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:67; ::_thesis: verum end; theorem :: SIN_COS2:6 sin | ].PI,((3 / 2) * PI).[ is decreasing proof for th being Real st th in ].PI,((3 / 2) * PI).[ holds diff (sin,th) < 0 proof let th be Real; ::_thesis: ( th in ].PI,((3 / 2) * PI).[ implies diff (sin,th) < 0 ) assume A1: th in ].PI,((3 / 2) * PI).[ ; ::_thesis: diff (sin,th) < 0 th < (3 / 2) * PI by A1, XXREAL_1:4; then A2: th - PI < ((3 / 2) * PI) - PI by XREAL_1:9; PI < th by A1, XXREAL_1:4; then PI - PI < th - PI by XREAL_1:9; then th - PI in ].0,(PI / 2).[ by A2, XXREAL_1:4; then cos . (th - PI) > 0 by SIN_COS:80; then A3: 0 - (cos . (th - PI)) < 0 ; diff (sin,th) = cos . (PI + (th - PI)) by SIN_COS:68 .= - (cos . (th - PI)) by SIN_COS:78 ; hence diff (sin,th) < 0 by A3; ::_thesis: verum end; hence sin | ].PI,((3 / 2) * PI).[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:68; ::_thesis: verum end; theorem :: SIN_COS2:7 sin | ].((3 / 2) * PI),(2 * PI).[ is increasing proof for th being Real st th in ].((3 / 2) * PI),(2 * PI).[ holds diff (sin,th) > 0 proof let th be Real; ::_thesis: ( th in ].((3 / 2) * PI),(2 * PI).[ implies diff (sin,th) > 0 ) assume A1: th in ].((3 / 2) * PI),(2 * PI).[ ; ::_thesis: diff (sin,th) > 0 th < 2 * PI by A1, XXREAL_1:4; then A2: th - ((3 / 2) * PI) < (2 * PI) - ((3 / 2) * PI) by XREAL_1:9; A3: diff (sin,th) = cos . (PI + ((PI / 2) + (th - ((3 / 2) * PI)))) by SIN_COS:68 .= - (cos . ((PI / 2) + (th - ((3 / 2) * PI)))) by SIN_COS:78 .= - (- (sin . (th - ((3 / 2) * PI)))) by SIN_COS:78 .= sin . (th - ((3 / 2) * PI)) ; (3 / 2) * PI < th by A1, XXREAL_1:4; then ((3 / 2) * PI) - ((3 / 2) * PI) < th - ((3 / 2) * PI) by XREAL_1:9; then th - ((3 / 2) * PI) in ].0,(PI / 2).[ by A2, XXREAL_1:4; hence diff (sin,th) > 0 by A3, Lm1; ::_thesis: verum end; hence sin | ].((3 / 2) * PI),(2 * PI).[ is increasing by FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:68; ::_thesis: verum end; theorem :: SIN_COS2:8 cos | ].PI,((3 / 2) * PI).[ is increasing proof for th being Real st th in ].PI,((3 / 2) * PI).[ holds diff (cos,th) > 0 proof let th be Real; ::_thesis: ( th in ].PI,((3 / 2) * PI).[ implies diff (cos,th) > 0 ) assume A1: th in ].PI,((3 / 2) * PI).[ ; ::_thesis: diff (cos,th) > 0 th < (3 / 2) * PI by A1, XXREAL_1:4; then A2: th - PI < ((3 / 2) * PI) - PI by XREAL_1:9; A3: diff (cos,th) = - (sin . (PI + (th - PI))) by SIN_COS:67 .= - (- (sin . (th - PI))) by SIN_COS:78 .= sin . (th - PI) ; PI < th by A1, XXREAL_1:4; then PI - PI < th - PI by XREAL_1:9; then th - PI in ].0,(PI / 2).[ by A2, XXREAL_1:4; hence diff (cos,th) > 0 by A3, Lm1; ::_thesis: verum end; hence cos | ].PI,((3 / 2) * PI).[ is increasing by FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:67; ::_thesis: verum end; theorem :: SIN_COS2:9 cos | ].((3 / 2) * PI),(2 * PI).[ is increasing proof for th being Real st th in ].((3 / 2) * PI),(2 * PI).[ holds diff (cos,th) > 0 proof let th be Real; ::_thesis: ( th in ].((3 / 2) * PI),(2 * PI).[ implies diff (cos,th) > 0 ) assume A1: th in ].((3 / 2) * PI),(2 * PI).[ ; ::_thesis: diff (cos,th) > 0 th < 2 * PI by A1, XXREAL_1:4; then A2: th - ((3 / 2) * PI) < (2 * PI) - ((3 / 2) * PI) by XREAL_1:9; A3: diff (cos,th) = - (sin . (PI + ((PI / 2) + (th - ((3 / 2) * PI))))) by SIN_COS:67 .= - (- (sin . ((PI / 2) + (th - ((3 / 2) * PI))))) by SIN_COS:78 .= cos . (th - ((3 / 2) * PI)) by SIN_COS:78 ; (3 / 2) * PI < th by A1, XXREAL_1:4; then ((3 / 2) * PI) - ((3 / 2) * PI) < th - ((3 / 2) * PI) by XREAL_1:9; then th - ((3 / 2) * PI) in ].0,(PI / 2).[ by A2, XXREAL_1:4; hence diff (cos,th) > 0 by A3, SIN_COS:80; ::_thesis: verum end; hence cos | ].((3 / 2) * PI),(2 * PI).[ is increasing by FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:67; ::_thesis: verum end; theorem :: SIN_COS2:10 for th being real number for n being Nat holds sin . th = sin . (((2 * PI) * n) + th) proof let th be real number ; ::_thesis: for n being Nat holds sin . th = sin . (((2 * PI) * n) + th) defpred S1[ Nat] means for th being real number holds sin . th = sin . (((2 * PI) * \$1) + th); let n be Nat; ::_thesis: sin . th = sin . (((2 * PI) * n) + th) A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: for th being real number holds sin . th = sin . (((2 * PI) * n) + th) ; ::_thesis: S1[n + 1] for th being real number holds sin . th = sin . (((2 * PI) * (n + 1)) + th) proof let th be real number ; ::_thesis: sin . th = sin . (((2 * PI) * (n + 1)) + th) sin . (((2 * PI) * (n + 1)) + th) = sin . ((((2 * PI) * n) + th) + (2 * PI)) .= sin . (((2 * PI) * n) + th) by SIN_COS:78 .= sin . th by A2 ; hence sin . th = sin . (((2 * PI) * (n + 1)) + th) ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence sin . th = sin . (((2 * PI) * n) + th) ; ::_thesis: verum end; theorem :: SIN_COS2:11 for th being real number for n being Nat holds cos . th = cos . (((2 * PI) * n) + th) proof let th be real number ; ::_thesis: for n being Nat holds cos . th = cos . (((2 * PI) * n) + th) defpred S1[ Nat] means for th being real number holds cos . th = cos . (((2 * PI) * \$1) + th); let n be Nat; ::_thesis: cos . th = cos . (((2 * PI) * n) + th) A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: for th being real number holds cos . th = cos . (((2 * PI) * n) + th) ; ::_thesis: S1[n + 1] for th being real number holds cos . th = cos . (((2 * PI) * (n + 1)) + th) proof let th be real number ; ::_thesis: cos . th = cos . (((2 * PI) * (n + 1)) + th) cos . (((2 * PI) * (n + 1)) + th) = cos . ((((2 * PI) * n) + th) + (2 * PI)) .= cos . (((2 * PI) * n) + th) by SIN_COS:78 .= cos . th by A2 ; hence cos . th = cos . (((2 * PI) * (n + 1)) + th) ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence cos . th = cos . (((2 * PI) * n) + th) ; ::_thesis: verum end; 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 proof deffunc H1( Real) -> Element of REAL = ((exp_R . \$1) - (exp_R . (- \$1))) / 2; consider f being Function of REAL,REAL such that A1: for d being Element of REAL holds f . d = H1(d) from FUNCT_2:sch_4(); take f ; ::_thesis: for d being real number holds f . d = ((exp_R . d) - (exp_R . (- d))) / 2 let d be real number ; ::_thesis: f . d = ((exp_R . d) - (exp_R . (- d))) / 2 d is Real by XREAL_0:def_1; hence f . d = ((exp_R . d) - (exp_R . (- d))) / 2 by A1; ::_thesis: verum end; 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 proof let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for d being real number holds f1 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ) & ( for d being real number holds f2 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ) implies f1 = f2 ) assume A2: for d being real number holds f1 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ; ::_thesis: ( ex d being real number st not f2 . d = ((exp_R . d) - (exp_R . (- d))) / 2 or f1 = f2 ) assume A3: for d being real number holds f2 . d = ((exp_R . d) - (exp_R . (- d))) / 2 ; ::_thesis: f1 = f2 for d being Element of REAL holds f1 . d = f2 . d proof let d be Element of REAL ; ::_thesis: f1 . d = f2 . d thus f1 . d = ((exp_R . d) - (exp_R . (- d))) / 2 by A2 .= f2 . d by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; 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 proof deffunc H1( Real) -> Element of REAL = ((exp_R . \$1) + (exp_R . (- \$1))) / 2; consider f being Function of REAL,REAL such that A1: for d being Element of REAL holds f . d = H1(d) from FUNCT_2:sch_4(); take f ; ::_thesis: for d being real number holds f . d = ((exp_R . d) + (exp_R . (- d))) / 2 let d be real number ; ::_thesis: f . d = ((exp_R . d) + (exp_R . (- d))) / 2 d is Real by XREAL_0:def_1; hence f . d = ((exp_R . d) + (exp_R . (- d))) / 2 by A1; ::_thesis: verum end; 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 proof let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for d being real number holds f1 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ) & ( for d being real number holds f2 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ) implies f1 = f2 ) assume A2: for d being real number holds f1 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ; ::_thesis: ( ex d being real number st not f2 . d = ((exp_R . d) + (exp_R . (- d))) / 2 or f1 = f2 ) assume A3: for d being real number holds f2 . d = ((exp_R . d) + (exp_R . (- d))) / 2 ; ::_thesis: f1 = f2 for d being Element of REAL holds f1 . d = f2 . d proof let d be Element of REAL ; ::_thesis: f1 . d = f2 . d thus f1 . d = ((exp_R . d) + (exp_R . (- d))) / 2 by A2 .= f2 . d by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; 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))) proof deffunc H1( Real) -> Element of REAL = ((exp_R . \$1) - (exp_R . (- \$1))) / ((exp_R . \$1) + (exp_R . (- \$1))); consider f being Function of REAL,REAL such that A1: for d being Element of REAL holds f . d = H1(d) from FUNCT_2:sch_4(); take f ; ::_thesis: for d being real number holds f . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) let d be real number ; ::_thesis: f . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) d is Real by XREAL_0:def_1; hence f . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) by A1; ::_thesis: verum end; 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 proof let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for d being real number holds f1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ) & ( for d being real number holds f2 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ) implies f1 = f2 ) assume A2: for d being real number holds f1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ; ::_thesis: ( ex d being real number st not f2 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) or f1 = f2 ) assume A3: for d being real number holds f2 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) ; ::_thesis: f1 = f2 for d being Element of REAL holds f1 . d = f2 . d proof let d be Element of REAL ; ::_thesis: f1 . d = f2 . d thus f1 . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) by A2 .= f2 . d by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; 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) proof let p, q be real number ; ::_thesis: exp_R . (p + q) = (exp_R . p) * (exp_R . q) exp_R . (p + q) = exp_R (p + q) by SIN_COS:def_23 .= (exp_R p) * (exp_R q) by SIN_COS:50 .= (exp_R . p) * (exp_R q) by SIN_COS:def_23 .= (exp_R . p) * (exp_R . q) by SIN_COS:def_23 ; hence exp_R . (p + q) = (exp_R . p) * (exp_R . q) ; ::_thesis: verum end; 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 ) proof let p be real number ; ::_thesis: ( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 ) A1: (sinh . p) * (sinh . p) = (((exp_R . p) - (exp_R . (- p))) / 2) * (sinh . p) by Def1 .= (((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2) by Def1 .= (((((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / (2 * 2) .= ((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + (exp_R . ((- p) + (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) - 1) - 1) + (exp_R . ((- p) + (- p)))) / 4 by Th12, Th13 ; (cosh . p) * (cosh . p) = (((exp_R . p) + (exp_R . (- p))) / 2) * (cosh . p) by Def3 .= (((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2) by Def3 .= (((((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / (2 * 2) .= ((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + (exp_R . ((- p) + (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) + 1) + 1) + (exp_R . ((- p) + (- p)))) / 4 by Th12, Th13 .= (((exp_R . (p + p)) + 2) + (exp_R . ((- p) + (- p)))) / 4 ; hence ( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 ) by A1; ::_thesis: verum end; Lm2: for p, r being real number holds cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) proof let p, r be real number ; ::_thesis: cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) = ((((exp_R . p) + (exp_R . (- p))) / 2) * (cosh . r)) + ((sinh . p) * (sinh . r)) by Def3 .= ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((sinh . p) * (sinh . r)) by Def3 .= ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((((exp_R . p) - (exp_R . (- p))) / 2) * (sinh . r)) by Def1 .= ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) - (exp_R . (- r))) / 2)) by Def1 .= ((2 * ((exp_R . p) * (exp_R . r))) + (2 * ((exp_R . (- p)) * (exp_R . (- r))))) / 4 .= ((2 * (exp_R . (p + r))) + (2 * ((exp_R . (- p)) * (exp_R . (- r))))) / 4 by Th12 .= ((2 * (exp_R . (p + r))) + (2 * (exp_R . ((- p) + (- r))))) / 4 by Th12 .= ((exp_R . (p + r)) + (exp_R . (- (p + r)))) / 2 .= cosh . (p + r) by Def3 ; hence cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) ; ::_thesis: verum end; Lm3: for p, r being real number holds sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) proof let p, r be real number ; ::_thesis: sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) = ((((exp_R . p) - (exp_R . (- p))) / 2) * (cosh . r)) + ((cosh . p) * (sinh . r)) by Def1 .= ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((cosh . p) * (sinh . r)) by Def3 .= ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((((exp_R . p) + (exp_R . (- p))) / 2) * (sinh . r)) by Def3 .= ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . r) - (exp_R . (- r))) / 2)) by Def1 .= ((2 * ((exp_R . p) * (exp_R . r))) + (2 * (- ((exp_R . (- p)) * (exp_R . (- r)))))) / 4 .= ((2 * (exp_R . (p + r))) + (2 * (- ((exp_R . (- p)) * (exp_R . (- r)))))) / 4 by Th12 .= ((2 * (exp_R . (p + r))) + (2 * (- (exp_R . ((- p) + (- r)))))) / 4 by Th12 .= ((exp_R . (p + r)) - (exp_R . (- (p + r)))) / 2 .= sinh . (p + r) by Def1 ; hence sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) ; ::_thesis: verum end; theorem Th15: :: SIN_COS2:15 for p being real number holds ( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 ) proof let p be real number ; ::_thesis: ( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 ) ( exp_R . p > 0 & exp_R . (- p) > 0 ) by SIN_COS:54; then A1: ((exp_R . p) + (exp_R . (- p))) / 2 > 0 by XREAL_1:139; cosh . 0 = ((exp_R . 0) + (exp_R . (- 0))) / 2 by Def3 .= 1 by SIN_COS:51, SIN_COS:def_23 ; hence ( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 ) by A1, Def3; ::_thesis: verum end; theorem Th16: :: SIN_COS2:16 sinh . 0 = 0 proof sinh . 0 = ((exp_R . 0) - (exp_R . (- 0))) / 2 by Def1 .= 0 ; hence sinh . 0 = 0 ; ::_thesis: verum end; theorem Th17: :: SIN_COS2:17 for p being real number holds tanh . p = (sinh . p) / (cosh . p) proof let p be real number ; ::_thesis: tanh . p = (sinh . p) / (cosh . p) (sinh . p) / (cosh . p) = (((exp_R . p) - (exp_R . (- p))) / 2) / (cosh . p) by Def1 .= (((exp_R . p) - (exp_R . (- p))) / 2) / (((exp_R . p) + (exp_R . (- p))) / 2) by Def3 .= ((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) by XCMPLX_1:55 .= tanh . p by Def5 ; hence tanh . p = (sinh . p) / (cosh . p) ; ::_thesis: verum end; 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))) proof let r, q, p, a1 be real number ; ::_thesis: ( r <> 0 & q <> 0 implies ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) ) assume that A1: r <> 0 and A2: q <> 0 ; ::_thesis: ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = (((p * q) + (r * a1)) / (r * q)) / (((r * q) + (p * a1)) / (r * q)) by A1, A2, XCMPLX_1:6, XCMPLX_1:55 .= (((p * q) / (r * q)) + ((r * a1) / (r * q))) / (((r * q) + (p * a1)) / (r * q)) by XCMPLX_1:62 .= (((p * q) / (r * q)) + ((r * a1) / (r * q))) / (((r * q) / (r * q)) + ((p * a1) / (r * q))) by XCMPLX_1:62 .= ((p / r) + ((a1 * r) / (q * r))) / (((r * q) / (r * q)) + ((p * a1) / (r * q))) by A2, XCMPLX_1:91 .= ((p / r) + (a1 / q)) / (((r * q) / (r * q)) + ((p * a1) / (r * q))) by A1, XCMPLX_1:91 .= ((p / r) + (a1 / q)) / (1 + ((p * a1) / (r * q))) by A1, A2, XCMPLX_1:6, XCMPLX_1:60 .= ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) by XCMPLX_1:76 ; hence ((p * q) + (r * a1)) / ((r * q) + (p * a1)) = ((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))) ; ::_thesis: verum end; Lm5: for p, r being real number holds tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) proof let p, r be real number ; ::_thesis: tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) A1: ( cosh . r <> 0 & cosh . p <> 0 ) by Th15; tanh . (p + r) = (sinh . (p + r)) / (cosh . (p + r)) by Th17 .= (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / (cosh . (p + r)) by Lm3 .= (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / (((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))) by Lm2 .= (((sinh . p) / (cosh . p)) + ((sinh . r) / (cosh . r))) / (1 + (((sinh . p) / (cosh . p)) * ((sinh . r) / (cosh . r)))) by A1, Lm4 .= ((tanh . p) + ((sinh . r) / (cosh . r))) / (1 + (((sinh . p) / (cosh . p)) * ((sinh . r) / (cosh . r)))) by Th17 .= ((tanh . p) + (tanh . r)) / (1 + (((sinh . p) / (cosh . p)) * ((sinh . r) / (cosh . r)))) by Th17 .= ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * ((sinh . r) / (cosh . r)))) by Th17 .= ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) by Th17 ; hence tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) ; ::_thesis: verum end; 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) ) proof let p be real number ; ::_thesis: ( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) ) A1: (cosh . p) ^2 = (((exp_R . p) + (exp_R . (- p))) / 2) * (cosh . p) by Def3 .= (((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2) by Def3 .= (((((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 .= ((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + (exp_R . (p + (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12 .= (((exp_R . (2 * p)) + (2 * (exp_R . 0))) + (exp_R . ((- p) + (- p)))) / 4 .= (((exp_R . (2 * p)) + (2 * 1)) + (exp_R . (- (2 * p)))) / 4 by SIN_COS:51, SIN_COS:def_23 .= ((1 / 2) * (((exp_R . (2 * p)) + (exp_R . (- (2 * p)))) / 2)) + ((1 * 2) / (2 * 2)) .= ((1 / 2) * (cosh . (2 * p))) + ((1 / 2) * ((2 * 1) / 2)) by Def3 .= (1 / 2) * ((cosh . (2 * p)) + 1) ; (sinh . p) ^2 = (((exp_R . p) - (exp_R . (- p))) / 2) * (sinh . p) by Def1 .= (((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2) by Def1 .= (((((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 .= ((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12 .= ((((exp_R . (p + p)) + (- (exp_R . (p + (- p))))) - (exp_R . (p + (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12 .= (((exp_R . (2 * p)) + (2 * (- (exp_R . 0)))) + (exp_R . ((- p) + (- p)))) / 4 .= (((exp_R . (2 * p)) + (2 * (- 1))) + (exp_R . (- (2 * p)))) / 4 by SIN_COS:51, SIN_COS:def_23 .= ((1 / 2) * (((exp_R . (2 * p)) + (exp_R . (- (2 * p)))) / 2)) + (((- 1) * 2) / (2 * 2)) .= ((1 / 2) * (cosh . (2 * p))) + ((1 / 2) * ((2 * (- 1)) / 2)) by Def3 .= (1 / 2) * ((cosh . (2 * p)) - 1) ; hence ( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) ) by A1; ::_thesis: verum end; Lm6: for p being real number holds ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 ) proof let p be real number ; ::_thesis: ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 ) A1: 2 * ((cosh . p) ^2) = 2 * ((1 / 2) * ((cosh . (2 * p)) + 1)) by Th18 .= (cosh . (2 * p)) + 1 ; (2 * (sinh . p)) * (cosh . p) = (2 * (((exp_R . p) - (exp_R . (- p))) / 2)) * (cosh . p) by Def1 .= (2 * (((exp_R . p) - (exp_R . (- p))) / 2)) * (((exp_R . p) + (exp_R . (- p))) / 2) by Def3 .= (2 / 4) * (((exp_R . p) ^2) - ((exp_R . (- p)) ^2)) .= (2 / 4) * ((exp_R . (p + p)) - ((exp_R . (- p)) * (exp_R . (- p)))) by Th12 .= (2 / 4) * ((exp_R . (2 * p)) - (exp_R . ((- p) + (- p)))) by Th12 .= (((exp_R . (2 * p)) - (exp_R . (- (2 * p)))) / 2) * 1 .= sinh . (2 * p) by Def1 ; hence ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 ) by A1; ::_thesis: verum end; theorem Th19: :: SIN_COS2:19 for p being real number holds ( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) ) proof let p be real number ; ::_thesis: ( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) ) A1: cosh . (- p) = ((exp_R . (- p)) + (exp_R . (- (- p)))) / 2 by Def3 .= cosh . p by Def3 ; A2: sinh . (- p) = ((exp_R . (- p)) - (exp_R . (- (- p)))) / 2 by Def1 .= - (((exp_R . p) - (exp_R . (- p))) / 2) .= - (sinh . p) by Def1 ; then tanh . (- p) = (- (sinh . p)) / (cosh . (- p)) by Th17 .= - ((sinh . p) / (cosh . p)) by A1, XCMPLX_1:187 .= - (tanh . p) by Th17 ; hence ( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) ) by A1, A2; ::_thesis: verum end; Lm7: for p, r being real number holds cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r)) proof let p, r be real number ; ::_thesis: cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r)) cosh . (p - r) = cosh . (p + (- r)) .= ((cosh . p) * (cosh . (- r))) + ((sinh . p) * (sinh . (- r))) by Lm2 .= ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . (- r))) by Th19 .= ((cosh . p) * (cosh . r)) + ((sinh . p) * (- (sinh . r))) by Th19 .= ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r)) ; hence cosh . (p - r) = ((cosh . p) * (cosh . r)) - ((sinh . p) * (sinh . r)) ; ::_thesis: verum end; 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)) proof let p, r be real number ; ::_thesis: sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) sinh . (p - r) = sinh . (p + (- r)) .= ((sinh . p) * (cosh . (- r))) + ((cosh . p) * (sinh . (- r))) by Lm3 .= ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . (- r))) by Th19 .= ((sinh . p) * (cosh . r)) + ((cosh . p) * (- (sinh . r))) by Th19 .= ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) ; hence sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) ; ::_thesis: verum end; 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))) proof let p, r be real number ; ::_thesis: tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) tanh . (p - r) = tanh . (p + (- r)) .= ((tanh . p) + (tanh . (- r))) / (1 + ((tanh . p) * (tanh . (- r)))) by Lm5 .= ((tanh . p) + (- (tanh . r))) / (1 + ((tanh . p) * (tanh . (- r)))) by Th19 .= ((tanh . p) - (tanh . r)) / (1 + ((tanh . p) * (- (tanh . r)))) by Th19 .= ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) ; hence tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) ; ::_thesis: verum end; 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)) ) proof let p be real number ; ::_thesis: ( 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)) ) tanh . (2 * p) = tanh . (p + p) .= ((tanh . p) + (tanh . p)) / (1 + ((tanh . p) * (tanh . p))) by Lm5 .= (2 * (tanh . p)) / (1 + ((tanh . p) ^2)) ; hence ( 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)) ) by Lm6; ::_thesis: verum end; 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) ) proof let p, q be real number ; ::_thesis: ( ((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) ) A1: (sinh . (p + q)) * (sinh . (p - q)) = (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (sinh . (p + (- q))) by Lm3 .= (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (((sinh . p) * (cosh . (- q))) + ((cosh . p) * (sinh . (- q)))) by Lm3 .= (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . (- q)))) by Th19 .= (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (((sinh . p) * (cosh . q)) + ((cosh . p) * (- (sinh . q)))) by Th19 .= (((sinh . p) ^2) * ((cosh . q) ^2)) - (((sinh . q) ^2) * ((cosh . p) ^2)) ; then A2: (sinh . (p + q)) * (sinh . (p - q)) = (((cosh . q) ^2) * (- (((cosh . p) ^2) - ((sinh . p) ^2)))) + ((((cosh . p) ^2) * ((cosh . q) ^2)) + (- (((sinh . q) ^2) * ((cosh . p) ^2)))) .= (((cosh . q) ^2) * (- 1)) + (((cosh . p) ^2) * (((cosh . q) ^2) - ((sinh . q) ^2))) by Th14 .= (((cosh . q) ^2) * (- 1)) + (((cosh . p) ^2) * 1) by Th14 .= ((cosh . p) ^2) - ((cosh . q) ^2) ; (sinh . (p + q)) * (sinh . (p - q)) = ((((sinh . p) ^2) * (((cosh . q) ^2) - ((sinh . q) ^2))) + (((sinh . q) ^2) * ((sinh . p) ^2))) - (((sinh . q) ^2) * ((cosh . p) ^2)) by A1 .= ((((sinh . p) ^2) * 1) + (((sinh . p) ^2) * ((sinh . q) ^2))) - (((sinh . q) ^2) * ((cosh . p) ^2)) by Th14 .= ((sinh . p) ^2) + (((sinh . q) ^2) * (- (((cosh . p) ^2) - ((sinh . p) ^2)))) .= ((sinh . p) ^2) + (((sinh . q) ^2) * (- 1)) by Th14 .= ((sinh . p) ^2) - ((sinh . q) ^2) ; hence ( ((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) ) by A2; ::_thesis: verum end; 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) ) proof let p, q be real number ; ::_thesis: ( ((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) ) A1: (cosh . (p + q)) * (cosh . (p - q)) = (((cosh . p) * (cosh . q)) + ((sinh . p) * (sinh . q))) * (cosh . (p + (- q))) by Lm2 .= (((cosh . p) * (cosh . q)) + ((sinh . p) * (sinh . q))) * (((cosh . p) * (cosh . (- q))) + ((sinh . p) * (sinh . (- q)))) by Lm2 .= (((((cosh . p) * (cosh . q)) * ((cosh . p) * (cosh . (- q)))) + (((cosh . p) * (cosh . q)) * ((sinh . p) * (sinh . (- q))))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . (- q))))) + (((sinh . p) * (sinh . q)) * ((sinh . p) * (sinh . (- q)))) .= (((((cosh . p) * (cosh . q)) * ((cosh . p) * (cosh . q))) + (((cosh . p) * (cosh . q)) * ((sinh . (- q)) * (sinh . p)))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . (- q))))) + (((sinh . p) * (sinh . q)) * ((sinh . (- q)) * (sinh . p))) by Th19 .= (((((cosh . p) * (cosh . q)) ^2) + (((sinh . (- q)) * (sinh . p)) * ((cosh . p) * (cosh . q)))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . q)))) + (((sinh . (- q)) * (sinh . p)) * ((sinh . p) * (sinh . q))) by Th19 .= (((((cosh . p) * (cosh . q)) ^2) + (((- (sinh . q)) * (sinh . p)) * ((cosh . p) * (cosh . q)))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . q)))) + (((sinh . (- q)) * (sinh . p)) * ((sinh . p) * (sinh . q))) by Th19 .= ((((cosh . p) * (cosh . q)) ^2) + 0) + ((((- 1) * (sinh . q)) * (sinh . p)) * ((sinh . p) * (sinh . q))) by Th19 .= (((cosh . p) ^2) * ((cosh . q) ^2)) - (((sinh . q) ^2) * ((sinh . p) ^2)) ; then A2: (cosh . (p + q)) * (cosh . (p - q)) = ((((cosh . p) ^2) * (((cosh . q) ^2) - ((sinh . q) ^2))) + (((cosh . p) ^2) * ((sinh . q) ^2))) + (- (((sinh . q) ^2) * ((sinh . p) ^2))) .= ((((cosh . p) ^2) * 1) + (((cosh . p) ^2) * ((sinh . q) ^2))) + (- (((sinh . q) ^2) * ((sinh . p) ^2))) by Th14 .= ((cosh . p) ^2) + (((sinh . q) ^2) * (((cosh . p) ^2) - ((sinh . p) ^2))) .= ((cosh . p) ^2) + (((sinh . q) ^2) * 1) by Th14 .= ((cosh . p) ^2) + ((sinh . q) ^2) ; (cosh . (p + q)) * (cosh . (p - q)) = (((cosh . q) ^2) * (((cosh . p) ^2) - ((sinh . p) ^2))) + ((((cosh . q) ^2) * ((sinh . p) ^2)) + (- (((sinh . p) ^2) * ((sinh . q) ^2)))) by A1 .= (((cosh . q) ^2) * 1) + ((((cosh . q) ^2) * ((sinh . p) ^2)) - (((sinh . p) ^2) * ((sinh . q) ^2))) by Th14 .= ((cosh . q) ^2) + (((sinh . p) ^2) * (((cosh . q) ^2) - ((sinh . q) ^2))) .= ((cosh . q) ^2) + (((sinh . p) ^2) * 1) by Th14 .= ((cosh . q) ^2) + ((sinh . p) ^2) ; hence ( ((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) ) by A2; ::_thesis: verum end; 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))) ) proof let p, r be real number ; ::_thesis: ( (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))) ) A1: (2 * (sinh . ((p / 2) - (r / 2)))) * (cosh . ((p / 2) + (r / 2))) = (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) - ((cosh . (p / 2)) * (sinh . (r / 2))))) * (cosh . ((p / 2) + (r / 2))) by Lm8 .= (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) - ((cosh . (p / 2)) * (sinh . (r / 2))))) * (((cosh . (p / 2)) * (cosh . (r / 2))) + ((sinh . (p / 2)) * (sinh . (r / 2)))) by Lm2 .= 2 * (((((cosh . (r / 2)) * (sinh . (r / 2))) * (- (((cosh . (p / 2)) ^2) - ((sinh . (p / 2)) ^2)))) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2)))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2)))) .= 2 * (((((cosh . (r / 2)) * (sinh . (r / 2))) * (- 1)) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2)))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2)))) by Th14 .= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * (((cosh . (r / 2)) ^2) - ((sinh . (r / 2)) ^2))) + ((- 1) * ((cosh . (r / 2)) * (sinh . (r / 2))))) .= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * 1) + ((- 1) * ((cosh . (r / 2)) * (sinh . (r / 2))))) by Th14 .= ((2 * (sinh . (p / 2))) * (cosh . (p / 2))) - (2 * ((sinh . (r / 2)) * (cosh . (r / 2)))) .= (sinh . (2 * (p / 2))) - ((2 * (sinh . (r / 2))) * (cosh . (r / 2))) by Lm6 .= (sinh . p) - (sinh . (2 * (r / 2))) by Lm6 .= (sinh . p) - (sinh . r) ; (2 * (sinh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) = (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) + ((cosh . (p / 2)) * (sinh . (r / 2))))) * (cosh . ((p / 2) - (r / 2))) by Lm3 .= (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) + ((cosh . (p / 2)) * (sinh . (r / 2))))) * (((cosh . (p / 2)) * (cosh . (r / 2))) - ((sinh . (p / 2)) * (sinh . (r / 2)))) by Lm7 .= 2 * (((((sinh . (r / 2)) * (cosh . (r / 2))) * (((cosh . (p / 2)) ^2) - ((sinh . (p / 2)) ^2))) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2)))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2)))) .= 2 * (((((sinh . (r / 2)) * (cosh . (r / 2))) * 1) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2)))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2)))) by Th14 .= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * (((cosh . (r / 2)) ^2) - ((sinh . (r / 2)) ^2))) + ((sinh . (r / 2)) * (cosh . (r / 2)))) .= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * 1) + ((sinh . (r / 2)) * (cosh . (r / 2)))) by Th14 .= ((2 * (sinh . (p / 2))) * (cosh . (p / 2))) + (2 * ((sinh . (r / 2)) * (cosh . (r / 2)))) .= (sinh . (2 * (p / 2))) + ((2 * (sinh . (r / 2))) * (cosh . (r / 2))) by Lm6 .= (sinh . p) + (sinh . (2 * (r / 2))) by Lm6 .= (sinh . p) + (sinh . r) ; hence ( (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))) ) by A1; ::_thesis: verum end; 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))) ) proof let p, r be real number ; ::_thesis: ( (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))) ) A1: (2 * (sinh . ((p / 2) - (r / 2)))) * (sinh . ((p / 2) + (r / 2))) = 2 * ((sinh . ((p / 2) - (r / 2))) * (sinh . ((p / 2) + (r / 2)))) .= 2 * (((cosh . (p / 2)) ^2) - ((cosh . (r / 2)) ^2)) by Th24 .= 2 * (((1 / 2) * ((cosh . (2 * (p / 2))) + 1)) - ((cosh . (r / 2)) ^2)) by Th18 .= 2 * (((1 / 2) * ((cosh . p) + 1)) - ((1 / 2) * ((cosh . (2 * (r / 2))) + 1))) by Th18 .= (cosh . p) - (cosh . r) ; (2 * (cosh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) = 2 * ((cosh . ((p / 2) + (r / 2))) * (cosh . ((p / 2) - (r / 2)))) .= 2 * (((sinh . (p / 2)) ^2) + ((cosh . (r / 2)) ^2)) by Th25 .= 2 * (((1 / 2) * ((cosh . (2 * (p / 2))) - 1)) + ((cosh . (r / 2)) ^2)) by Th18 .= 2 * (((1 / 2) * ((cosh . p) - 1)) + ((1 / 2) * ((cosh . (2 * (r / 2))) + 1))) by Th18 .= (cosh . r) + (cosh . p) ; hence ( (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))) ) by A1; ::_thesis: verum end; 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)) ) proof let p, r be real number ; ::_thesis: ( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) ) A1: (sinh . (p - r)) / ((cosh . p) * (cosh . r)) = (((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))) / ((cosh . p) * (cosh . r)) by Lm8 .= (((sinh . p) * (cosh . r)) / ((cosh . p) * (cosh . r))) - (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by XCMPLX_1:120 .= ((sinh . p) / (cosh . p)) - (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by Th15, XCMPLX_1:91 .= ((sinh . p) / (cosh . p)) - ((sinh . r) / (cosh . r)) by Th15, XCMPLX_1:91 .= (tanh . p) - ((sinh . r) / (cosh . r)) by Th17 .= (tanh . p) - (tanh . r) by Th17 ; (sinh . (p + r)) / ((cosh . p) * (cosh . r)) = (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / ((cosh . p) * (cosh . r)) by Lm3 .= (((sinh . p) * (cosh . r)) / ((cosh . p) * (cosh . r))) + (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by XCMPLX_1:62 .= ((sinh . p) / (cosh . p)) + (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by Th15, XCMPLX_1:91 .= ((sinh . p) / (cosh . p)) + ((sinh . r) / (cosh . r)) by Th15, XCMPLX_1:91 .= (tanh . p) + ((sinh . r) / (cosh . r)) by Th17 .= (tanh . p) + (tanh . r) by Th17 ; hence ( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) ) by A1; ::_thesis: verum end; 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)) proof let p be real number ; ::_thesis: for n being Element of NAT holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p)) let n be Element of NAT ; ::_thesis: ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p)) defpred S1[ Nat] means for p being real number holds ((cosh . p) + (sinh . p)) |^ \$1 = (cosh . (\$1 * p)) + (sinh . (\$1 * p)); A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: for p being real number holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p)) ; ::_thesis: S1[n + 1] for p being real number holds ((cosh . p) + (sinh . p)) |^ (n + 1) = (cosh . ((n + 1) * p)) + (sinh . ((n + 1) * p)) proof let p be real number ; ::_thesis: ((cosh . p) + (sinh . p)) |^ (n + 1) = (cosh . ((n + 1) * p)) + (sinh . ((n + 1) * p)) A3: ((cosh . (n * p)) * (cosh . p)) + ((sinh . (n * p)) * (sinh . p)) = ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (cosh . p)) + ((sinh . (n * p)) * (sinh . p)) by Def3 .= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2)) + ((sinh . (n * p)) * (sinh . p)) by Def3 .= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2)) + ((((exp_R . (n * p)) - (exp_R . (- (n * p)))) / 2) * (sinh . p)) by Def1 .= ((((exp_R . (n * p)) / 2) + ((exp_R . (- (n * p))) / 2)) * (((exp_R . p) / 2) + ((exp_R . (- p)) / 2))) + ((((exp_R . (n * p)) / 2) - ((exp_R . (- (n * p))) / 2)) * (((exp_R . p) - (exp_R . (- p))) / 2)) by Def1 .= (2 * (((exp_R . (n * p)) * (exp_R . p)) / (2 * 2))) + (2 * (((exp_R . (- (n * p))) / 2) * ((exp_R . (- p)) / 2))) .= (2 * ((exp_R . ((p * n) + (p * 1))) / (2 * 2))) + (2 * (((exp_R . (- (n * p))) * (exp_R . (- p))) / (2 * 2))) by Th12 .= (2 * ((exp_R . (p * (n + 1))) / (2 * 2))) + (2 * ((exp_R . ((- (n * p)) + (- p))) / (2 * 2))) by Th12 .= ((exp_R . (p * (n + 1))) + (exp_R . (- (p * (n + 1))))) / 2 .= cosh . (p * (n + 1)) by Def3 ; A4: ((cosh . (n * p)) * (sinh . p)) + ((sinh . (n * p)) * (cosh . p)) = ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (sinh . p)) + ((sinh . (n * p)) * (cosh . p)) by Def3 .= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2)) + ((sinh . (n * p)) * (cosh . p)) by Def1 .= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2)) + ((((exp_R . (n * p)) - (exp_R . (- (n * p)))) / 2) * (cosh . p)) by Def1 .= ((((((exp_R . (n * p)) / 2) * ((exp_R . p) / 2)) - (((exp_R . (n * p)) / 2) * ((exp_R . (- p)) / 2))) + (((exp_R . (- (n * p))) / 2) * ((exp_R . p) / 2))) - (((exp_R . (- (n * p))) / 2) * ((exp_R . (- p)) / 2))) + ((((exp_R . (n * p)) - (exp_R . (- (n * p)))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2)) by Def3 .= (2 * (((exp_R . (n * p)) * (exp_R . p)) / 4)) + (2 * (- (((exp_R . (- (n * p))) * (exp_R . (- p))) / (2 * 2)))) .= (2 * ((exp_R . ((n * p) + p)) / 4)) + (2 * (- (((exp_R . (- (n * p))) * (exp_R . (- p))) / 4))) by Th12 .= (2 * ((exp_R . ((n * p) + p)) / 4)) + (2 * (- ((exp_R . ((- (n * p)) + (- p))) / 4))) by Th12 .= ((exp_R . (p * (n + 1))) - (exp_R . (- (p * (n + 1))))) / 2 .= sinh . (p * (n + 1)) by Def1 ; ((cosh . p) + (sinh . p)) |^ (n + 1) = (((cosh . p) + (sinh . p)) |^ n) * ((cosh . p) + (sinh . p)) by NEWTON:6 .= ((cosh . (n * p)) + (sinh . (n * p))) * ((cosh . p) + (sinh . p)) by A2 .= (sinh . ((n + 1) * p)) + (cosh . ((n + 1) * p)) by A3, A4 ; hence ((cosh . p) + (sinh . p)) |^ (n + 1) = (cosh . ((n + 1) * p)) + (sinh . ((n + 1) * p)) ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A5: S1[ 0 ] by Th15, Th16, NEWTON:4; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A1); hence ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p)) ; ::_thesis: verum end; 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 proof let d be real number ; ::_thesis: compreal . d = (- 1) * d thus compreal . d = - d by BINOP_2:def_7 .= (- 1) * d ; ::_thesis: verum end; 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 ) proof reconsider f2 = REAL --> 0 as Function of REAL,REAL ; deffunc H1( Real) -> Element of REAL = - \$1; let f be PartFunc of REAL,REAL; ::_thesis: ( f = compreal implies for p being real number holds ( f is_differentiable_in p & diff (f,p) = - 1 ) ) assume A1: f = compreal ; ::_thesis: for p being real number holds ( f is_differentiable_in p & diff (f,p) = - 1 ) let p be real number ; ::_thesis: ( f is_differentiable_in p & diff (f,p) = - 1 ) consider f1 being Function of REAL,REAL such that A2: for p being Element of REAL holds f1 . p = H1(p) from FUNCT_2:sch_4(); A3: dom f2 = REAL by FUNCOP_1:13; for hy1 being non-zero 0 -convergent Real_Sequence holds ( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 ) proof let hy1 be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 ) A4: for n being Nat holds ((hy1 ") (#) (f2 /* hy1)) . n = 0 proof let n be Nat; ::_thesis: ((hy1 ") (#) (f2 /* hy1)) . n = 0 A5: rng hy1 c= dom f2 by A3; A6: n in NAT by ORDINAL1:def_12; then ((hy1 ") (#) (f2 /* hy1)) . n = ((hy1 ") . n) * ((f2 /* hy1) . n) by SEQ_1:8 .= ((hy1 . n) ") * ((f2 /* hy1) . n) by VALUED_1:10 ; then ((hy1 ") (#) (f2 /* hy1)) . n = ((hy1 . n) ") * (f2 . (hy1 . n)) by A6, A5, FUNCT_2:108 .= ((hy1 . n) ") * 0 by FUNCOP_1:7 .= 0 ; hence ((hy1 ") (#) (f2 /* hy1)) . n = 0 ; ::_thesis: verum end; then A7: (hy1 ") (#) (f2 /* hy1) is constant by VALUED_0:def_18; for n being Element of NAT holds lim ((hy1 ") (#) (f2 /* hy1)) = 0 proof let n be Element of NAT ; ::_thesis: lim ((hy1 ") (#) (f2 /* hy1)) = 0 lim ((hy1 ") (#) (f2 /* hy1)) = ((hy1 ") (#) (f2 /* hy1)) . n by A7, SEQ_4:26 .= 0 by A4 ; hence lim ((hy1 ") (#) (f2 /* hy1)) = 0 ; ::_thesis: verum end; hence ( (hy1 ") (#) (f2 /* hy1) is convergent & lim ((hy1 ") (#) (f2 /* hy1)) = 0 ) by A7; ::_thesis: verum end; then A8: f2 is RestFunc by FDIFF_1:def_2; A9: ex N being Neighbourhood of p st ( N c= dom compreal & ( for r being Real st r in N holds (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) ) proof take ].(p - 1),(p + 1).[ ; ::_thesis: ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom compreal & ( for r being Real st r in ].(p - 1),(p + 1).[ holds (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) ) for r being real number st r in ].(p - 1),(p + 1).[ holds (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) proof let r be real number ; ::_thesis: ( r in ].(p - 1),(p + 1).[ implies (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) A10: for d being real number holds f2 . d = 0 proof let d be real number ; ::_thesis: f2 . d = 0 d is Real by XREAL_0:def_1; hence f2 . d = 0 by FUNCOP_1:7; ::_thesis: verum end; A11: for p being real number holds f1 . p = - p proof let p be real number ; ::_thesis: f1 . p = - p p is Real by XREAL_0:def_1; hence f1 . p = - p by A2; ::_thesis: verum end; (compreal . r) - (compreal . p) = ((- 1) * r) - (compreal . p) by Lm10 .= (((- 1) * r) - ((- 1) * p)) + 0 by Lm10 .= (- (r - p)) + (f2 . (r - p)) by A10 .= (f1 . (r - p)) + (f2 . (r - p)) by A11 ; hence ( r in ].(p - 1),(p + 1).[ implies (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) ; ::_thesis: verum end; hence ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom compreal & ( for r being Real st r in ].(p - 1),(p + 1).[ holds (compreal . r) - (compreal . p) = (f1 . (r - p)) + (f2 . (r - p)) ) ) by Lm11, RCOMP_1:def_6; ::_thesis: verum end; for p being Real holds f1 . p = (- 1) * p proof let p be Real; ::_thesis: f1 . p = (- 1) * p f1 . p = - p by A2; hence f1 . p = (- 1) * p ; ::_thesis: verum end; then A12: f1 is LinearFunc by FDIFF_1:def_3; then f is_differentiable_in p by A1, A8, A9, FDIFF_1:def_4; then diff (f,p) = f1 . 1 by A1, A12, A8, A9, FDIFF_1:def_5 .= - 1 by A2 ; hence ( f is_differentiable_in p & diff (f,p) = - 1 ) by A1, A12, A8, A9, FDIFF_1:def_4; ::_thesis: verum end; 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)) ) proof let p be real number ; ::_thesis: 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)) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f = compreal implies ( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) ) ) assume A1: f = compreal ; ::_thesis: ( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) ) A2: ( p is Real & exp_R is_differentiable_in f . p ) by SIN_COS:65, XREAL_0:def_1; A3: f is_differentiable_in p by A1, Lm12; then diff ((exp_R * f),p) = (diff (exp_R,(f . p))) * (diff (f,p)) by A2, FDIFF_2:13 .= (diff (exp_R,(f . p))) * (- 1) by A1, Lm12 .= (exp_R . (f . p)) * (- 1) by SIN_COS:65 ; hence ( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) ) by A2, A3, FDIFF_2:13; ::_thesis: verum end; 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 proof let p be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f = compreal holds exp_R . ((- 1) * p) = (exp_R * f) . p let f be PartFunc of REAL,REAL; ::_thesis: ( f = compreal implies exp_R . ((- 1) * p) = (exp_R * f) . p ) A1: p is Real by XREAL_0:def_1; assume A2: f = compreal ; ::_thesis: exp_R . ((- 1) * p) = (exp_R * f) . p then exp_R . ((- 1) * p) = exp_R . (f . p) by Lm10 .= (exp_R * f) . p by A2, A1, FUNCT_2:15 ; hence exp_R . ((- 1) * p) = (exp_R * f) . p ; ::_thesis: verum end; 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)) ) proof let p be real number ; ::_thesis: 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)) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f = compreal implies ( 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)) ) ) A1: ( p is Real & exp_R is_differentiable_in p ) by SIN_COS:65, XREAL_0:def_1; assume A2: f = compreal ; ::_thesis: ( 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)) ) then A3: exp_R * f is_differentiable_in p by Lm13; then A4: diff ((exp_R + (exp_R * f)),p) = (diff (exp_R,p)) + (diff ((exp_R * f),p)) by A1, FDIFF_1:13 .= (exp_R . p) + (diff ((exp_R * f),p)) by SIN_COS:65 .= (exp_R . p) + ((- 1) * (exp_R . (f . p))) by A2, Lm13 .= (exp_R . p) + ((- 1) * (exp_R . ((- 1) * p))) by A2, Lm10 .= (exp_R . p) - (exp_R . (- p)) ; diff ((exp_R - (exp_R * f)),p) = (diff (exp_R,p)) - (diff ((exp_R * f),p)) by A1, A3, FDIFF_1:14 .= (exp_R . p) - (diff ((exp_R * f),p)) by SIN_COS:65 .= (exp_R . p) - ((- 1) * (exp_R . (f . p))) by A2, Lm13 .= (exp_R . p) - ((- 1) * (exp_R . ((- 1) * p))) by A2, Lm10 .= (exp_R . p) + (exp_R . (- p)) ; hence ( 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)) ) by A1, A3, A4, FDIFF_1:13, FDIFF_1:14; ::_thesis: verum end; 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)) ) proof let p be real number ; ::_thesis: 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)) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f = compreal implies ( (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)) ) ) assume f = compreal ; ::_thesis: ( (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)) ) then ( p is Real & exp_R - (exp_R * f) is_differentiable_in p ) by Lm15, XREAL_0:def_1; hence ( (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)) ) by FDIFF_1:15; ::_thesis: verum end; 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 proof let p be real number ; ::_thesis: for ff being PartFunc of REAL,REAL st ff = compreal holds sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p A1: p is Real by XREAL_0:def_1; let ff be PartFunc of REAL,REAL; ::_thesis: ( ff = compreal implies sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p ) assume A2: ff = compreal ; ::_thesis: sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p A3: ( dom (exp_R - (exp_R * ff)) = (dom exp_R) /\ (dom (exp_R * ff)) & dom (exp_R * ff) = REAL ) by A2, FUNCT_2:def_1, VALUED_1:12; A4: dom ((1 / 2) (#) (exp_R - (exp_R * ff))) = REAL by A2, FUNCT_2:def_1; sinh . p = ((exp_R . p) - (exp_R . (- p))) / 2 by Def1 .= (1 / 2) * ((exp_R . p) - (exp_R . ((- 1) * p))) .= (1 / 2) * ((exp_R . p) - ((exp_R * ff) . p)) by A2, Lm14 .= (1 / 2) * ((exp_R - (exp_R * ff)) . p) by A1, A3, SIN_COS:47, VALUED_1:13 .= ((1 / 2) (#) (exp_R - (exp_R * ff))) . p by A1, A4, VALUED_1:def_5 ; hence sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p ; ::_thesis: verum end; Lm18: for ff being PartFunc of REAL,REAL st ff = compreal holds sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) proof let ff be PartFunc of REAL,REAL; ::_thesis: ( ff = compreal implies sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) ) assume ff = compreal ; ::_thesis: sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) then A1: ( REAL = dom ((1 / 2) (#) (exp_R - (exp_R * ff))) & ( for p being Element of REAL st p in REAL holds sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p ) ) by Lm17, FUNCT_2:def_1; REAL = dom sinh by FUNCT_2:def_1; hence sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th31: :: SIN_COS2:31 for p being real number holds ( sinh is_differentiable_in p & diff (sinh,p) = cosh . p ) proof let p be real number ; ::_thesis: ( sinh is_differentiable_in p & diff (sinh,p) = cosh . p ) set ff = compreal ; A1: sinh = (1 / 2) (#) (exp_R - (exp_R * compreal)) by Lm18; diff (sinh,p) = diff (((1 / 2) (#) (exp_R - (exp_R * compreal))),p) by Lm18 .= (1 / 2) * (diff ((exp_R - (exp_R * compreal)),p)) by Lm16 .= (1 / 2) * ((exp_R . p) + (exp_R . (- p))) by Lm15 .= ((exp_R . p) + (exp_R . (- p))) / 2 .= cosh . p by Def3 ; hence ( sinh is_differentiable_in p & diff (sinh,p) = cosh . p ) by A1, Lm16; ::_thesis: verum end; 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)) ) proof let p be real number ; ::_thesis: 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)) ) let ff be PartFunc of REAL,REAL; ::_thesis: ( ff = compreal implies ( (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)) ) ) assume ff = compreal ; ::_thesis: ( (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)) ) then ( p is Real & exp_R + (exp_R * ff) is_differentiable_in p ) by Lm15, XREAL_0:def_1; hence ( (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)) ) by FDIFF_1:15; ::_thesis: verum end; 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 proof let p be real number ; ::_thesis: for ff being PartFunc of REAL,REAL st ff = compreal holds cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p A1: p is Real by XREAL_0:def_1; let ff be PartFunc of REAL,REAL; ::_thesis: ( ff = compreal implies cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p ) assume A2: ff = compreal ; ::_thesis: cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p A3: ( dom (exp_R + (exp_R * ff)) = (dom exp_R) /\ (dom (exp_R * ff)) & dom (exp_R * ff) = REAL ) by A2, FUNCT_2:def_1, VALUED_1:def_1; A4: dom ((1 / 2) (#) (exp_R + (exp_R * ff))) = REAL by A2, FUNCT_2:def_1; cosh . p = ((exp_R . p) + (exp_R . (- p))) / 2 by Def3 .= (1 / 2) * ((exp_R . p) + (exp_R . ((- 1) * p))) .= (1 / 2) * ((exp_R . p) + ((exp_R * ff) . p)) by A2, Lm14 .= (1 / 2) * ((exp_R + (exp_R * ff)) . p) by A1, A3, SIN_COS:47, VALUED_1:def_1 .= ((1 / 2) (#) (exp_R + (exp_R * ff))) . p by A1, A4, VALUED_1:def_5 ; hence cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p ; ::_thesis: verum end; Lm21: for ff being PartFunc of REAL,REAL st ff = compreal holds cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) proof let ff be PartFunc of REAL,REAL; ::_thesis: ( ff = compreal implies cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) ) assume ff = compreal ; ::_thesis: cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) then A1: ( REAL = dom ((1 / 2) (#) (exp_R + (exp_R * ff))) & ( for p being Element of REAL st p in REAL holds cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p ) ) by Lm20, FUNCT_2:def_1; REAL = dom cosh by FUNCT_2:def_1; hence cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th32: :: SIN_COS2:32 for p being real number holds ( cosh is_differentiable_in p & diff (cosh,p) = sinh . p ) proof let p be real number ; ::_thesis: ( cosh is_differentiable_in p & diff (cosh,p) = sinh . p ) reconsider ff = compreal as PartFunc of REAL,REAL ; A1: cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) by Lm21; diff (cosh,p) = diff (((1 / 2) (#) (exp_R + (exp_R * ff))),p) by Lm21 .= (1 / 2) * (diff ((exp_R + (exp_R * ff)),p)) by Lm19 .= (1 / 2) * ((exp_R . p) - (exp_R . (- p))) by Lm15 .= ((exp_R . p) - (exp_R . (- p))) / 2 .= sinh . p by Def1 ; hence ( cosh is_differentiable_in p & diff (cosh,p) = sinh . p ) by A1, Lm19; ::_thesis: verum end; Lm22: for p being real number holds ( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) ) proof let p be real number ; ::_thesis: ( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) ) A1: ( p is Real & cosh . p <> 0 ) by Th15, XREAL_0:def_1; A2: ( sinh is_differentiable_in p & cosh is_differentiable_in p ) by Th31, Th32; then diff ((sinh / cosh),p) = (((diff (sinh,p)) * (cosh . p)) - ((diff (cosh,p)) * (sinh . p))) / ((cosh . p) ^2) by A1, FDIFF_2:14 .= (((cosh . p) * (cosh . p)) - ((diff (cosh,p)) * (sinh . p))) / ((cosh . p) ^2) by Th31 .= (((cosh . p) ^2) - ((sinh . p) * (sinh . p))) / ((cosh . p) ^2) by Th32 .= 1 / ((cosh . p) ^2) by Th14 ; hence ( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) ) by A1, A2, FDIFF_2:14; ::_thesis: verum end; Lm23: tanh = sinh / cosh proof not 0 in rng cosh proof assume 0 in rng cosh ; ::_thesis: contradiction then ex p being Real st ( p in dom cosh & 0 = cosh . p ) by PARTFUN1:3; hence contradiction by Th15; ::_thesis: verum end; then A1: ( dom (sinh / cosh) = (dom sinh) /\ ((dom cosh) \ (cosh " {0})) & cosh " {0} = {} ) by FUNCT_1:72, RFUNCT_1:def_1; for p being Element of REAL st p in REAL holds tanh . p = (sinh / cosh) . p proof let p be real number ; ::_thesis: ( p is Element of REAL & p in REAL implies tanh . p = (sinh / cosh) . p ) p is Real by XREAL_0:def_1; then (sinh / cosh) . p = (sinh . p) * ((cosh . p) ") by A1, Th30, RFUNCT_1:def_1 .= (sinh . p) / (cosh . p) by XCMPLX_0:def_9 .= tanh . p by Th17 ; hence ( p is Element of REAL & p in REAL implies tanh . p = (sinh / cosh) . p ) ; ::_thesis: verum end; hence tanh = sinh / cosh by A1, Th30, PARTFUN1:5; ::_thesis: verum end; 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 ) proof let p be real number ; ::_thesis: ( sinh is_differentiable_on REAL & diff (sinh,p) = cosh . p ) A1: ( [#] REAL is open Subset of REAL & REAL c= dom sinh ) by FUNCT_2:def_1; for p being Real st p in REAL holds sinh is_differentiable_in p by Th31; hence ( sinh is_differentiable_on REAL & diff (sinh,p) = cosh . p ) by A1, Th31, FDIFF_1:9; ::_thesis: verum end; theorem Th35: :: SIN_COS2:35 for p being real number holds ( cosh is_differentiable_on REAL & diff (cosh,p) = sinh . p ) proof let p be real number ; ::_thesis: ( cosh is_differentiable_on REAL & diff (cosh,p) = sinh . p ) A1: ( [#] REAL is open Subset of REAL & REAL c= dom cosh ) by FUNCT_2:def_1; for r being Real st r in REAL holds cosh is_differentiable_in r by Th32; hence ( cosh is_differentiable_on REAL & diff (cosh,p) = sinh . p ) by A1, Th32, FDIFF_1:9; ::_thesis: verum end; theorem Th36: :: SIN_COS2:36 for p being real number holds ( tanh is_differentiable_on REAL & diff (tanh,p) = 1 / ((cosh . p) ^2) ) proof let p be real number ; ::_thesis: ( tanh is_differentiable_on REAL & diff (tanh,p) = 1 / ((cosh . p) ^2) ) ( [#] REAL is open Subset of REAL & ( for p being Real st p in REAL holds tanh is_differentiable_in p ) ) by Lm22, Lm23; hence ( tanh is_differentiable_on REAL & diff (tanh,p) = 1 / ((cosh . p) ^2) ) by Lm22, Lm23, Th30, FDIFF_1:9; ::_thesis: verum end; Lm24: for p being real number holds (exp_R . p) + (exp_R . (- p)) >= 2 proof let p be real number ; ::_thesis: (exp_R . p) + (exp_R . (- p)) >= 2 A1: ( exp_R . p >= 0 & exp_R . (- p) >= 0 ) by SIN_COS:54; 2 * (sqrt ((exp_R . p) * (exp_R . (- p)))) = 2 * (sqrt (exp_R . (p + (- p)))) by Th12 .= 2 * 1 by SIN_COS:51, SIN_COS:def_23, SQUARE_1:18 ; hence (exp_R . p) + (exp_R . (- p)) >= 2 by A1, Th1; ::_thesis: verum end; theorem :: SIN_COS2:37 for p being real number holds cosh . p >= 1 proof let p be real number ; ::_thesis: cosh . p >= 1 ((exp_R . p) + (exp_R . (- p))) / 2 >= 2 / 2 by Lm24, XREAL_1:72; hence cosh . p >= 1 by Def3; ::_thesis: verum end; 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 ) proof let p be real number ; ::_thesis: ( tanh . p < 1 & tanh . p > - 1 ) A1: ( exp_R . p > 0 & exp_R . (- p) > 0 ) by SIN_COS:54; thus tanh . p < 1 ::_thesis: tanh . p > - 1 proof assume tanh . p >= 1 ; ::_thesis: contradiction then A2: ((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) >= 1 by Def5; ( exp_R . p > 0 & exp_R . (- p) > 0 ) by SIN_COS:54; then A3: (((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) = (exp_R . p) - (exp_R . (- p)) by XCMPLX_1:87; (exp_R . p) + (exp_R . (- p)) >= 2 by Lm24; then (((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) >= 1 * ((exp_R . p) + (exp_R . (- p))) by A2, XREAL_1:64; then ((exp_R . p) - (exp_R . (- p))) - (exp_R . p) >= ((exp_R . p) + (exp_R . (- p))) - (exp_R . p) by A3, XREAL_1:9; then A4: (- (exp_R . (- p))) + (exp_R . (- p)) >= (exp_R . (- p)) + (exp_R . (- p)) by XREAL_1:6; exp_R . (- p) > 0 by SIN_COS:54; hence contradiction by A4; ::_thesis: verum end; assume tanh . p <= - 1 ; ::_thesis: contradiction then A5: ((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) <= - 1 by Def5; (exp_R . p) + (exp_R . (- p)) >= 2 by Lm24; then (((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) <= (- 1) * ((exp_R . p) + (exp_R . (- p))) by A5, XREAL_1:64; then (exp_R . p) - (exp_R . (- p)) <= - ((exp_R . p) + (exp_R . (- p))) by A1, XCMPLX_1:87; then A6: ((exp_R . p) - (exp_R . (- p))) + (exp_R . (- p)) <= ((- (exp_R . p)) + (- (exp_R . (- p)))) + (exp_R . (- p)) by XREAL_1:6; exp_R . p > 0 by SIN_COS:54; hence contradiction by A6; ::_thesis: verum end;