sin_cos2.miz



    begin

    reserve p,q,r,th,th1 for Real;

    reserve n for Nat;

    theorem :: SIN_COS2:1

    

     Th1: p >= 0 & r >= 0 implies (p + r) >= (2 * ( sqrt (p * r)))

    proof

      assume that

       A1: p >= 0 and

       A2: r >= 0 ;

      

       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 thesis by A1, A2, SQUARE_1: 29;

    end;

    theorem :: SIN_COS2:2

    ( sin | ]. 0 , ( PI / 2).[) is increasing

    proof

      for th st th in ]. 0 , ( PI / 2).[ holds 0 < ( diff ( sin ,th))

      proof

        let th;

        assume th in ]. 0 , ( PI / 2).[;

        then ( cos . th) > 0 by SIN_COS: 80;

        hence thesis by SIN_COS: 68;

      end;

      hence thesis by FDIFF_1: 26, ROLLE: 9, SIN_COS: 24, SIN_COS: 68;

    end;

    

     Lm1: for th st th in ]. 0 , ( PI / 2).[ holds 0 < ( sin . th)

    proof

      let th;

      assume

       A1: th in ]. 0 , ( PI / 2).[;

      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 thesis by SIN_COS: 78;

    end;

    theorem :: SIN_COS2:3

    ( sin | ].( PI / 2), PI .[) is decreasing

    proof

      for th1 st th1 in ].( PI / 2), PI .[ holds 0 > ( diff ( sin ,th1))

      proof

        let th1;

        assume

         A1: th1 in ].( PI / 2), PI .[;

        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 thesis by A3;

      end;

      hence thesis by FDIFF_1: 26, ROLLE: 10, SIN_COS: 24, SIN_COS: 68;

    end;

    theorem :: SIN_COS2:4

    ( cos | ]. 0 , ( PI / 2).[) is decreasing

    proof

      for th st th in ]. 0 , ( PI / 2).[ holds ( diff ( cos ,th)) < 0

      proof

        let th;

        assume th in ]. 0 , ( PI / 2).[;

        then 0 < ( sin . th) by Lm1;

        then ( diff ( cos ,th)) = ( - ( sin . th)) & ( 0 - ( sin . th)) < 0 by SIN_COS: 67;

        hence thesis;

      end;

      hence thesis by FDIFF_1: 26, ROLLE: 10, SIN_COS: 24, SIN_COS: 67;

    end;

    theorem :: SIN_COS2:5

    ( cos | ].( PI / 2), PI .[) is decreasing

    proof

      for th st th in ].( PI / 2), PI .[ holds ( diff ( cos ,th)) < 0

      proof

        let th;

        assume

         A1: th in ].( PI / 2), PI .[;

        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 thesis by A3;

      end;

      hence thesis by FDIFF_1: 26, ROLLE: 10, SIN_COS: 24, SIN_COS: 67;

    end;

    theorem :: SIN_COS2:6

    ( sin | ]. PI , ((3 / 2) * PI ).[) is decreasing

    proof

      for th st th in ]. PI , ((3 / 2) * PI ).[ holds ( diff ( sin ,th)) < 0

      proof

        let th such that

         A1: th in ]. PI , ((3 / 2) * PI ).[;

        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 thesis by A3;

      end;

      hence thesis by FDIFF_1: 26, ROLLE: 10, SIN_COS: 24, SIN_COS: 68;

    end;

    theorem :: SIN_COS2:7

    ( sin | ].((3 / 2) * PI ), (2 * PI ).[) is increasing

    proof

      for th st th in ].((3 / 2) * PI ), (2 * PI ).[ holds ( diff ( sin ,th)) > 0

      proof

        let th such that

         A1: th in ].((3 / 2) * PI ), (2 * PI ).[;

        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 thesis by A3, Lm1;

      end;

      hence thesis by FDIFF_1: 26, ROLLE: 9, SIN_COS: 24, SIN_COS: 68;

    end;

    theorem :: SIN_COS2:8

    ( cos | ]. PI , ((3 / 2) * PI ).[) is increasing

    proof

      for th st th in ]. PI , ((3 / 2) * PI ).[ holds ( diff ( cos ,th)) > 0

      proof

        let th such that

         A1: th in ]. PI , ((3 / 2) * PI ).[;

        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 thesis by A3, Lm1;

      end;

      hence thesis by FDIFF_1: 26, ROLLE: 9, SIN_COS: 24, SIN_COS: 67;

    end;

    theorem :: SIN_COS2:9

    ( cos | ].((3 / 2) * PI ), (2 * PI ).[) is increasing

    proof

      for th st th in ].((3 / 2) * PI ), (2 * PI ).[ holds ( diff ( cos ,th)) > 0

      proof

        let th such that

         A1: th in ].((3 / 2) * PI ), (2 * PI ).[;

        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 thesis by A3, SIN_COS: 80;

      end;

      hence thesis by FDIFF_1: 26, ROLLE: 9, SIN_COS: 24, SIN_COS: 67;

    end;

    theorem :: SIN_COS2:10

    for n be Nat holds ( sin . th) = ( sin . (((2 * PI ) * n) + th))

    proof

      defpred X[ Nat] means for th holds ( sin . th) = ( sin . (((2 * PI ) * $1) + th));

      let n be Nat;

      

       A1: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let n be Nat such that

         A2: for th holds ( sin . th) = ( sin . (((2 * PI ) * n) + th));

        for th holds ( sin . th) = ( sin . (((2 * PI ) * (n + 1)) + th))

        proof

          let 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 thesis;

        end;

        hence thesis;

      end;

      

       A3: X[ 0 ];

      for n be Nat holds X[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: SIN_COS2:11

    for n be Nat holds ( cos . th) = ( cos . (((2 * PI ) * n) + th))

    proof

      defpred X[ Nat] means for th holds ( cos . th) = ( cos . (((2 * PI ) * $1) + th));

      let n be Nat;

      

       A1: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let n be Nat such that

         A2: for th holds ( cos . th) = ( cos . (((2 * PI ) * n) + th));

        for th holds ( cos . th) = ( cos . (((2 * PI ) * (n + 1)) + th))

        proof

          let 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 thesis;

        end;

        hence thesis;

      end;

      

       A3: X[ 0 ];

      for n be Nat holds X[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    begin

    definition

      :: SIN_COS2:def1

      func sinh -> Function of REAL , REAL means

      : Def1: for d be Real holds (it . d) = ((( exp_R . d) - ( exp_R . ( - d))) / 2);

      existence

      proof

        deffunc U( Real) = ( In (((( exp_R . $1) - ( exp_R . ( - $1))) / 2), REAL ));

        consider f be Function of REAL , REAL such that

         A1: for d be Element of REAL holds (f . d) = U(d) from FUNCT_2:sch 4;

        take f;

        let d be Real;

        d in REAL by XREAL_0:def 1;

        then (f . d) = U(d) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of REAL , REAL ;

        assume

         A2: for d be Real holds (f1 . d) = ((( exp_R . d) - ( exp_R . ( - d))) / 2);

        assume

         A3: for d be Real holds (f2 . d) = ((( exp_R . d) - ( exp_R . ( - d))) / 2);

        for d be Element of REAL holds (f1 . d) = (f2 . d)

        proof

          let d be Element of REAL ;

          

          thus (f1 . d) = ((( exp_R . d) - ( exp_R . ( - d))) / 2) by A2

          .= (f2 . d) by A3;

        end;

        hence f1 = f2 by FUNCT_2: 63;

      end;

    end

    definition

      let d be object;

      :: SIN_COS2:def2

      func sinh (d) -> number equals ( sinh . d);

      coherence ;

    end

    registration

      let d be object;

      cluster ( sinh d) -> real;

      coherence ;

    end

    definition

      :: SIN_COS2:def3

      func cosh -> Function of REAL , REAL means

      : Def3: for d be Real holds (it . d) = ((( exp_R . d) + ( exp_R . ( - d))) / 2);

      existence

      proof

        deffunc U( Real) = ( In (((( exp_R . $1) + ( exp_R . ( - $1))) / 2), REAL ));

        consider f be Function of REAL , REAL such that

         A1: for d be Element of REAL holds (f . d) = U(d) from FUNCT_2:sch 4;

        take f;

        let d be Real;

        d in REAL by XREAL_0:def 1;

        then (f . d) = U(d) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of REAL , REAL ;

        assume

         A2: for d be Real holds (f1 . d) = ((( exp_R . d) + ( exp_R . ( - d))) / 2);

        assume

         A3: for d be Real holds (f2 . d) = ((( exp_R . d) + ( exp_R . ( - d))) / 2);

        for d be Element of REAL holds (f1 . d) = (f2 . d)

        proof

          let d be Element of REAL ;

          

          thus (f1 . d) = ((( exp_R . d) + ( exp_R . ( - d))) / 2) by A2

          .= (f2 . d) by A3;

        end;

        hence f1 = f2 by FUNCT_2: 63;

      end;

    end

    definition

      let d be object;

      :: SIN_COS2:def4

      func cosh (d) -> number equals ( cosh . d);

      coherence ;

    end

    registration

      let d be object;

      cluster ( cosh d) -> real;

      coherence ;

    end

    definition

      :: SIN_COS2:def5

      func tanh -> Function of REAL , REAL means

      : Def5: for d be Real holds (it . d) = ((( exp_R . d) - ( exp_R . ( - d))) / (( exp_R . d) + ( exp_R . ( - d))));

      existence

      proof

        deffunc U( Real) = ( In (((( exp_R . $1) - ( exp_R . ( - $1))) / (( exp_R . $1) + ( exp_R . ( - $1)))), REAL ));

        consider f be Function of REAL , REAL such that

         A1: for d be Element of REAL holds (f . d) = U(d) from FUNCT_2:sch 4;

        take f;

        let d be Real;

        d in REAL by XREAL_0:def 1;

        then (f . d) = U(d) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of REAL , REAL ;

        assume

         A2: for d be Real holds (f1 . d) = ((( exp_R . d) - ( exp_R . ( - d))) / (( exp_R . d) + ( exp_R . ( - d))));

        assume

         A3: for d be Real holds (f2 . d) = ((( exp_R . d) - ( exp_R . ( - d))) / (( exp_R . d) + ( exp_R . ( - d))));

        for d be Element of REAL holds (f1 . d) = (f2 . d)

        proof

          let d be Element of REAL ;

          

          thus (f1 . d) = ((( exp_R . d) - ( exp_R . ( - d))) / (( exp_R . d) + ( exp_R . ( - d)))) by A2

          .= (f2 . d) by A3;

        end;

        hence f1 = f2 by FUNCT_2: 63;

      end;

    end

    definition

      let d be object;

      :: SIN_COS2:def6

      func tanh (d) -> number equals ( tanh . d);

      coherence ;

    end

    registration

      let d be object;

      cluster ( tanh d) -> real;

      coherence ;

    end

    theorem :: SIN_COS2:12

    

     Th12: ( exp_R . (p + q)) = (( exp_R . p) * ( exp_R . q))

    proof

      ( 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 thesis;

    end;

    theorem :: SIN_COS2:13

    

     Th13: ( exp_R . 0 ) = 1 by SIN_COS: 51, SIN_COS:def 23;

    theorem :: SIN_COS2:14

    

     Th14: ((( cosh . p) ^2 ) - (( sinh . p) ^2 )) = 1 & ((( cosh . p) * ( cosh . p)) - (( sinh . p) * ( sinh . p))) = 1

    proof

      

       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 thesis by A1;

    end;

    

     Lm2: ( cosh . (p + r)) = ((( cosh . p) * ( cosh . r)) + (( sinh . p) * ( sinh . r)))

    proof

      ((( 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 thesis;

    end;

    

     Lm3: ( sinh . (p + r)) = ((( sinh . p) * ( cosh . r)) + (( cosh . p) * ( sinh . r)))

    proof

      ((( 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 thesis;

    end;

    theorem :: SIN_COS2:15

    

     Th15: ( cosh . p) <> 0 & ( cosh . p) > 0 & ( cosh . 0 ) = 1

    proof

      ( 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 thesis by A1, Def3;

    end;

    theorem :: SIN_COS2:16

    

     Th16: ( sinh . 0 ) = 0

    proof

      ( sinh . 0 ) = ((( exp_R . 0 ) - ( exp_R . ( - 0 ))) / 2) by Def1

      .= 0 ;

      hence thesis;

    end;

    theorem :: SIN_COS2:17

    

     Th17: ( tanh . p) = (( sinh . p) / ( cosh . p))

    proof

      (( 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 thesis;

    end;

    

     Lm4: for a1 be Real holds r <> 0 & q <> 0 implies (((p * q) + (r * a1)) / ((r * q) + (p * a1))) = (((p / r) + (a1 / q)) / (1 + ((p / r) * (a1 / q))))

    proof

      let a1 be Real;

      assume that

       A1: r <> 0 and

       A2: q <> 0 ;

      (((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 thesis;

    end;

    

     Lm5: ( tanh . (p + r)) = ((( tanh . p) + ( tanh . r)) / (1 + (( tanh . p) * ( tanh . r))))

    proof

      

       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 thesis;

    end;

    theorem :: SIN_COS2:18

    

     Th18: (( sinh . p) ^2 ) = ((1 / 2) * (( cosh . (2 * p)) - 1)) & (( cosh . p) ^2 ) = ((1 / 2) * (( cosh . (2 * p)) + 1))

    proof

      

       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 thesis by A1;

    end;

    

     Lm6: ( sinh . (2 * p)) = ((2 * ( sinh . p)) * ( cosh . p)) & ( cosh . (2 * p)) = ((2 * (( cosh . p) ^2 )) - 1)

    proof

      

       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 thesis by A1;

    end;

    theorem :: SIN_COS2:19

    

     Th19: ( cosh . ( - p)) = ( cosh . p) & ( sinh . ( - p)) = ( - ( sinh . p)) & ( tanh . ( - p)) = ( - ( tanh . p))

    proof

      

       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 thesis by A1, A2;

    end;

    

     Lm7: ( cosh . (p - r)) = ((( cosh . p) * ( cosh . r)) - (( sinh . p) * ( sinh . r)))

    proof

      ( 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 thesis;

    end;

    theorem :: SIN_COS2:20

    ( 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: ( sinh . (p - r)) = ((( sinh . p) * ( cosh . r)) - (( cosh . p) * ( sinh . r)))

    proof

      ( 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 thesis;

    end;

    theorem :: SIN_COS2:21

    ( 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: ( tanh . (p - r)) = ((( tanh . p) - ( tanh . r)) / (1 - (( tanh . p) * ( tanh . r))))

    proof

      ( 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 thesis;

    end;

    theorem :: SIN_COS2:22

    ( 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

    ( 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

      ( 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 thesis by Lm6;

    end;

    theorem :: SIN_COS2:24

    

     Th24: ((( 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

      

       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 thesis by A2;

    end;

    theorem :: SIN_COS2:25

    

     Th25: ((( 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

      

       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 thesis by A2;

    end;

    theorem :: SIN_COS2:26

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

      

       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 thesis by A1;

    end;

    theorem :: SIN_COS2:27

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

      

       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 thesis by A1;

    end;

    theorem :: SIN_COS2:28

    (( tanh . p) + ( tanh . r)) = (( sinh . (p + r)) / (( cosh . p) * ( cosh . r))) & (( tanh . p) - ( tanh . r)) = (( sinh . (p - r)) / (( cosh . p) * ( cosh . r)))

    proof

      

       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 thesis by A1;

    end;

    theorem :: SIN_COS2:29

    ((( cosh . p) + ( sinh . p)) |^ n) = (( cosh . (n * p)) + ( sinh . (n * p)))

    proof

      defpred X[ Nat] means for p holds ((( cosh . p) + ( sinh . p)) |^ $1) = (( cosh . ($1 * p)) + ( sinh . ($1 * p)));

      

       A1: for n st X[n] holds X[(n + 1)]

      proof

        let n such that

         A2: for p holds ((( cosh . p) + ( sinh . p)) |^ n) = (( cosh . (n * p)) + ( sinh . (n * p)));

        for p holds ((( cosh . p) + ( sinh . p)) |^ (n + 1)) = (( cosh . ((n + 1) * p)) + ( sinh . ((n + 1) * p)))

        proof

          let 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 thesis;

        end;

        hence thesis;

      end;

      

       A5: X[ 0 ] by Th15, Th16, NEWTON: 4;

      for n holds X[n] from NAT_1:sch 2( A5, A1);

      hence thesis;

    end;

    theorem :: SIN_COS2:30

    

     Th30: ( dom sinh ) = REAL & ( dom cosh ) = REAL & ( dom tanh ) = REAL by FUNCT_2:def 1;

    

     Lm10: for d be Real holds ( compreal . d) = (( - 1) * d)

    proof

      let d be Real;

      

      thus ( compreal . d) = ( - d) by BINOP_2:def 7

      .= (( - 1) * d);

    end;

    

     Lm11: ( dom compreal ) = REAL by FUNCT_2:def 1;

    

     Lm12: for f be PartFunc of REAL , REAL st f = compreal holds for p holds f is_differentiable_in p & ( diff (f,p)) = ( - 1)

    proof

      reconsider f2 = ( REAL --> ( In ( 0 , REAL ))) as Function of REAL , REAL ;

      deffunc U( Real) = ( In (( - $1), REAL ));

      let f be PartFunc of REAL , REAL such that

       A1: f = compreal ;

      let p;

      consider f1 be Function of REAL , REAL such that

       A2: for p be Element of REAL holds (f1 . p) = U(p) from FUNCT_2:sch 4;

      

       A3: ( dom f2) = REAL by FUNCOP_1: 13;

      for hy1 be 0 -convergent non-zero Real_Sequence holds ((hy1 " ) (#) (f2 /* hy1)) is convergent & ( lim ((hy1 " ) (#) (f2 /* hy1))) = 0

      proof

        let hy1 be 0 -convergent non-zero Real_Sequence;

        

         A4: for n be Nat holds (((hy1 " ) (#) (f2 /* hy1)) . n) = ( In ( 0 , REAL ))

        proof

          let n be Nat;

          

           A5: ( rng hy1) c= ( dom f2) by A3;

          

           A6: n in NAT by ORDINAL1:def 12;

          (((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 thesis;

        end;

        then

         A7: ((hy1 " ) (#) (f2 /* hy1)) is constant by VALUED_0:def 18;

        for n holds ( lim ((hy1 " ) (#) (f2 /* hy1))) = 0

        proof

          let n;

          ( lim ((hy1 " ) (#) (f2 /* hy1))) = (((hy1 " ) (#) (f2 /* hy1)) . n) by A7, SEQ_4: 26

          .= 0 by A4;

          hence thesis;

        end;

        hence thesis by A7;

      end;

      then

       A8: f2 is RestFunc by FDIFF_1:def 2;

      

       A9: ex N be Neighbourhood of p st N c= ( dom compreal ) & for r st r in N holds (( compreal . r) - ( compreal . p)) = ((f1 . (r - p)) + (f2 . (r - p)))

      proof

        take ].(p - 1), (p + 1).[;

        for r st r in ].(p - 1), (p + 1).[ holds (( compreal . r) - ( compreal . p)) = ((f1 . (r - p)) + (f2 . (r - p)))

        proof

          let r;

          

           A10: for d be Real holds (f2 . d) = 0 by XREAL_0:def 1, FUNCOP_1: 7;

          

           A11: for p be Real holds (f1 . p) = ( - p)

          proof

            let p be Real;

            p in REAL by XREAL_0:def 1;

            then (f1 . p) = U(p) by A2;

            hence thesis;

          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 thesis;

        end;

        hence thesis by Lm11, RCOMP_1:def 6;

      end;

      reconsider pp = p as Real;

      

       A12: 1 in REAL by XREAL_0:def 1;

      for p holds (f1 . p) = (( - 1) * p)

      proof

        let p;

        reconsider pp = p as Element of REAL by XREAL_0:def 1;

        (f1 . p) = U(pp) by A2;

        hence thesis;

      end;

      then

       A13: f1 is LinearFunc by FDIFF_1:def 3;

      then f is_differentiable_in pp by A1, A8, A9, FDIFF_1:def 4;

      

      then ( diff (f,pp)) = (f1 . 1) by A1, A13, A8, A9, FDIFF_1:def 5

      .= U() by A2, A12;

      hence thesis by A1, A13, A8, A9, FDIFF_1:def 4;

    end;

    

     Lm13: for f be 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 f be PartFunc of REAL , REAL such that

       A1: f = compreal ;

      

       A2: p is Real & exp_R is_differentiable_in (f . p) by SIN_COS: 65;

      

       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 thesis by A2, A3, FDIFF_2: 13;

    end;

    

     Lm14: for f be PartFunc of REAL , REAL st f = compreal holds ( exp_R . (( - 1) * p)) = (( exp_R * f) . p)

    proof

      let f be PartFunc of REAL , REAL ;

      

       A1: p in REAL by XREAL_0:def 1;

      assume

       A2: f = compreal ;

      

      then ( exp_R . (( - 1) * p)) = ( exp_R . (f . p)) by Lm10

      .= (( exp_R * f) . p) by A2, A1, FUNCT_2: 15;

      hence thesis;

    end;

    

     Lm15: for f be 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 f be PartFunc of REAL , REAL ;

      

       A1: p is Real & exp_R is_differentiable_in p by SIN_COS: 65;

      assume

       A2: f = compreal ;

      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 thesis by A1, A3, A4, FDIFF_1: 13, FDIFF_1: 14;

    end;

    

     Lm16: for f be 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 f be PartFunc of REAL , REAL ;

      assume f = compreal ;

      then p is Real & ( exp_R - ( exp_R * f)) is_differentiable_in p by Lm15;

      hence thesis by FDIFF_1: 15;

    end;

    

     Lm17: for ff be PartFunc of REAL , REAL st ff = compreal holds ( sinh . p) = (((1 / 2) (#) ( exp_R - ( exp_R * ff))) . p)

    proof

      

       A1: p in REAL by XREAL_0:def 1;

      let ff be PartFunc of REAL , REAL such that

       A2: ff = compreal ;

      

       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 thesis;

    end;

    

     Lm18: for ff be PartFunc of REAL , REAL st ff = compreal holds sinh = ((1 / 2) (#) ( exp_R - ( exp_R * ff)))

    proof

      let ff be PartFunc of REAL , REAL ;

      assume ff = compreal ;

      then

       A1: REAL = ( dom ((1 / 2) (#) ( exp_R - ( exp_R * ff)))) & for p be 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 thesis by A1, PARTFUN1: 5;

    end;

    theorem :: SIN_COS2:31

    

     Th31: sinh is_differentiable_in p & ( diff ( sinh ,p)) = ( cosh . p)

    proof

      set ff = compreal ;

      

       A1: sinh = ((1 / 2) (#) ( exp_R - ( exp_R * ff))) by Lm18;

      ( diff ( sinh ,p)) = ( diff (((1 / 2) (#) ( exp_R - ( exp_R * ff))),p)) by Lm18

      .= ((1 / 2) * ( diff (( exp_R - ( exp_R * ff)),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 thesis by A1, Lm16;

    end;

    

     Lm19: for ff be 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 ff be PartFunc of REAL , REAL ;

      assume ff = compreal ;

      then p is Real & ( exp_R + ( exp_R * ff)) is_differentiable_in p by Lm15;

      hence thesis by FDIFF_1: 15;

    end;

    

     Lm20: for ff be PartFunc of REAL , REAL st ff = compreal holds ( cosh . p) = (((1 / 2) (#) ( exp_R + ( exp_R * ff))) . p)

    proof

      

       A1: p in REAL by XREAL_0:def 1;

      let ff be PartFunc of REAL , REAL such that

       A2: ff = compreal ;

      

       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 thesis;

    end;

    

     Lm21: for ff be PartFunc of REAL , REAL st ff = compreal holds cosh = ((1 / 2) (#) ( exp_R + ( exp_R * ff)))

    proof

      let ff be PartFunc of REAL , REAL ;

      assume ff = compreal ;

      then

       A1: REAL = ( dom ((1 / 2) (#) ( exp_R + ( exp_R * ff)))) & for p be 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 thesis by A1, PARTFUN1: 5;

    end;

    theorem :: SIN_COS2:32

    

     Th32: cosh is_differentiable_in p & ( diff ( cosh ,p)) = ( sinh . p)

    proof

      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 thesis by A1, Lm19;

    end;

    

     Lm22: ( sinh / cosh ) is_differentiable_in p & ( diff (( sinh / cosh ),p)) = (1 / (( cosh . p) ^2 ))

    proof

      

       A1: p is Real & ( cosh . p) <> 0 by Th15;

      

       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 thesis by A1, A2, FDIFF_2: 14;

    end;

    

     Lm23: tanh = ( sinh / cosh )

    proof

       not 0 in ( rng cosh )

      proof

        assume 0 in ( rng cosh );

        then ex p be Element of REAL st p in ( dom cosh ) & 0 = ( cosh . p) by PARTFUN1: 3;

        hence contradiction by Th15;

      end;

      then

       A1: ( dom ( sinh / cosh )) = (( dom sinh ) /\ (( dom cosh ) \ ( cosh " { 0 }))) & ( cosh " { 0 }) = {} by FUNCT_1: 72, RFUNCT_1:def 1;

      for p be Element of REAL st p in REAL holds ( tanh . p) = (( sinh / cosh ) . p)

      proof

        let p;

        p in 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 thesis;

      end;

      hence thesis by A1, Th30, PARTFUN1: 5;

    end;

    theorem :: SIN_COS2:33

     tanh is_differentiable_in p & ( diff ( tanh ,p)) = (1 / (( cosh . p) ^2 )) by Lm22, Lm23;

    theorem :: SIN_COS2:34

    

     Th34: sinh is_differentiable_on REAL & ( diff ( sinh ,p)) = ( cosh . p)

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL & REAL c= ( dom sinh ) by FUNCT_2:def 1;

      for p st p in REAL holds sinh is_differentiable_in p by Th31;

      hence thesis by A1, Th31, FDIFF_1: 9;

    end;

    theorem :: SIN_COS2:35

    

     Th35: cosh is_differentiable_on REAL & ( diff ( cosh ,p)) = ( sinh . p)

    proof

      

       A1: ( [#] REAL ) is open Subset of REAL & REAL c= ( dom cosh ) by FUNCT_2:def 1;

      for r st r in REAL holds cosh is_differentiable_in r by Th32;

      hence thesis by A1, Th32, FDIFF_1: 9;

    end;

    theorem :: SIN_COS2:36

    

     Th36: tanh is_differentiable_on REAL & ( diff ( tanh ,p)) = (1 / (( cosh . p) ^2 ))

    proof

      ( [#] REAL ) is open Subset of REAL & for p st p in REAL holds tanh is_differentiable_in p by Lm22, Lm23;

      hence thesis by Lm22, Lm23, Th30, FDIFF_1: 9;

    end;

    

     Lm24: (( exp_R . p) + ( exp_R . ( - p))) >= 2

    proof

      

       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 thesis by A1, Th1;

    end;

    theorem :: SIN_COS2:37

    ( cosh . p) >= 1

    proof

      ((( exp_R . p) + ( exp_R . ( - p))) / 2) >= (2 / 2) by Lm24, XREAL_1: 72;

      hence thesis by Def3;

    end;

    theorem :: SIN_COS2:38

     sinh is_continuous_in p by Th31, FDIFF_1: 24;

    theorem :: SIN_COS2:39

     cosh is_continuous_in p by Th32, FDIFF_1: 24;

    theorem :: SIN_COS2:40

     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

    ( tanh . p) < 1 & ( tanh . p) > ( - 1)

    proof

      

       A1: ( exp_R . p) > 0 & ( exp_R . ( - p)) > 0 by SIN_COS: 54;

      thus ( tanh . p) < 1

      proof

        assume ( tanh . p) >= 1;

        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;

      end;

      assume ( tanh . p) <= ( - 1);

      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;

    end;