let x be real number ; :: thesis: ( x <> 0 implies ( sinh x <> 0 & tanh x <> 0 ) )
assume A1: x <> 0 ; :: thesis: ( sinh x <> 0 & tanh x <> 0 )
A2: cosh x <> 0 by Lm1;
exp_R x > 0 by SIN_COS:60;
then 1 / (exp_R x) <> exp_R x by A1, SIN_COS7:29, XCMPLX_1:200;
then ((exp_R x) - (exp_R (- x))) / 2 <> 0 by TAYLOR_1:4;
then sinh x <> 0 by Lm2;
then (sinh x) / (cosh x) <> 0 by A2, XCMPLX_1:50;
hence ( sinh x <> 0 & tanh x <> 0 ) by Th1; :: thesis: verum