let p be Real; :: 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