let i be Integer; :: thesis: for x being Real holds (exp_R x) #R (1 / i) = exp_R (x / i)
let x be Real; :: thesis: (exp_R x) #R (1 / i) = exp_R (x / i)
set n = i;
per cases ( i <> 0 or i = 0 ) ;
suppose A1: i <> 0 ; :: thesis: (exp_R x) #R (1 / i) = exp_R (x / i)
then exp_R x = exp_R ((x / i) * i) by XCMPLX_1:87
.= (exp_R (x / i)) #R i by Lm2 ;
hence (exp_R x) #R (1 / i) = (exp_R (x / i)) #R (i * (1 / i)) by PREPOWER:91, SIN_COS:55
.= (exp_R (x / i)) #R 1 by A1, XCMPLX_1:106
.= exp_R (x / i) by PREPOWER:72, SIN_COS:55 ;
:: thesis: verum
end;
suppose A2: i = 0 ; :: thesis: (exp_R x) #R (1 / i) = exp_R (x / i)
(exp_R x) #R (1 / 0) = exp_R 0 by PREPOWER:71, SIN_COS:51, SIN_COS:55
.= exp_R (x / 0) by XCMPLX_1:49 ;
hence (exp_R x) #R (1 / i) = exp_R (x / i) by A2; :: thesis: verum
end;
end;