let th be real number ; :: thesis: ( th < 0 implies ( 0 < exp_R . th & exp_R . th <= 1 ) )
assume th < 0 ; :: thesis: ( 0 < exp_R . th & exp_R . th <= 1 )
then A1: exp_R . (- th) >= 1 by Th57;
X: (exp_R . (- th)) * (exp_R . th) = exp_R . ((- th) + th) by Lm15
.= 1 by Lm16 ;
then A2: exp_R . th = 1 / (exp_R . (- th)) by XCMPLX_1:74;
thus 0 < exp_R . th by A1, X; :: thesis: exp_R . th <= 1
thus exp_R . th <= 1 by A1, A2, XREAL_1:213; :: thesis: verum