let c be Real; :: thesis: ( c < 0 implies exp_R c < 1 )
assume c < 0 ; :: thesis: exp_R c < 1
then ( exp_R c <= 1 & exp_R c <> 1 ) by SIN_COS:53, SIN_COS7:29;
hence exp_R c < 1 by XXREAL_0:1; :: thesis: verum