let x be Real; :: thesis: ( x <> 0 implies ( sinh x <> 0 & tanh x <> 0 ) )

A1: exp_R x > 0 by SIN_COS:55;

assume x <> 0 ; :: thesis: ( sinh x <> 0 & tanh x <> 0 )

then 1 / (exp_R x) <> exp_R x by A1, SIN_COS7:29, XCMPLX_1:199;

then ((exp_R x) - (exp_R (- x))) / 2 <> 0 by TAYLOR_1:4;

then A2: sinh x <> 0 by Lm2;

cosh x <> 0 by Lm1;

then (sinh x) / (cosh x) <> 0 by A2, XCMPLX_1:50;

hence ( sinh x <> 0 & tanh x <> 0 ) by Th1; :: thesis: verum

A1: exp_R x > 0 by SIN_COS:55;

assume x <> 0 ; :: thesis: ( sinh x <> 0 & tanh x <> 0 )

then 1 / (exp_R x) <> exp_R x by A1, SIN_COS7:29, XCMPLX_1:199;

then ((exp_R x) - (exp_R (- x))) / 2 <> 0 by TAYLOR_1:4;

then A2: sinh x <> 0 by Lm2;

cosh x <> 0 by Lm1;

then (sinh x) / (cosh x) <> 0 by A2, XCMPLX_1:50;

hence ( sinh x <> 0 & tanh x <> 0 ) by Th1; :: thesis: verum