let x be Real; :: thesis: (exp_R x) + (exp_R (- x)) >= 2
exp_R . x >= 0 by SIN_COS:54;
then A1: exp_R x >= 0 by SIN_COS:def 23;
exp_R . (- x) >= 0 by SIN_COS:54;
then A2: exp_R (- x) >= 0 by SIN_COS:def 23;
2 * (sqrt ((exp_R x) * (exp_R (- x)))) = 2 * (sqrt ((exp_R x) * (exp_R . (- x)))) by SIN_COS:def 23
.= 2 * (sqrt ((exp_R . x) * (exp_R . (- x)))) by SIN_COS:def 23
.= 2 * (sqrt (exp_R . (x + (- x)))) by SIN_COS2:12
.= 2 * 1 by SIN_COS:51, SIN_COS:def 23, SQUARE_1:18 ;
hence (exp_R x) + (exp_R (- x)) >= 2 by A1, A2, SIN_COS2:1; :: thesis: verum