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