let th be Real; :: 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 Th51;
A2: (exp_R . (- th)) * (exp_R . th) = exp_R . ((- th) + th) by Lm10
.= 1 by Lm11 ;
then A3: exp_R . th = 1 / (exp_R . (- th)) by XCMPLX_1:73;
thus 0 < exp_R . th by A1, A2; :: thesis: exp_R . th <= 1
thus exp_R . th <= 1 by A1, A3, XREAL_1:211; :: thesis: verum