let x be real number ; :: thesis: (exp_R x) + (exp_R (- x)) >= 2
exp_R . x >= 0 by SIN_COS:59;
then A1: exp_R x >= 0 by SIN_COS:def 27;
exp_R . (- x) >= 0 by SIN_COS:59;
then A2: exp_R (- x) >= 0 by SIN_COS:def 27;
2 * (sqrt ((exp_R x) * (exp_R (- x)))) = 2 * (sqrt ((exp_R x) * (exp_R . (- x)))) by SIN_COS:def 27
.= 2 * (sqrt ((exp_R . x) * (exp_R . (- x)))) by SIN_COS:def 27
.= 2 * (sqrt (exp_R . (x + (- x)))) by SIN_COS2:12
.= 2 * 1 by SIN_COS:56, SIN_COS:def 27, SQUARE_1:83 ;
hence (exp_R x) + (exp_R (- x)) >= 2 by A1, A2, SIN_COS2:1; :: thesis: verum