let n, i be Element of NAT ; :: thesis: ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) )
set j = i div n;

per cases ( n <> 0 or n = 0 ) ;

suppose A1: n <> 0 ; :: thesis: ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) )

then i = (n * (i div n)) + (i mod n) by NAT_D:2;
then A2: ((2 * PI) * i) / n = (((2 * PI) * (n * (i div n))) + ((2 * PI) * (i mod n))) / n
.= (((2 * PI) * (n * (i div n))) / (n * 1)) + (((2 * PI) * (i mod n)) / n) by XCMPLX_1:63
.= ((((2 * PI) / n) * (n * (i div n))) / 1) + (((2 * PI) * (i mod n)) / n) by XCMPLX_1:84
.= (((2 * PI) * (1 / n)) * (n * (i div n))) + (((2 * PI) * (i mod n)) / n) by XCMPLX_1:100
.= ((2 * PI) * ((1 / n) * ((i div n) * n))) + (((2 * PI) * (i mod n)) / n)
.= ((2 * PI) * ((i div n) * 1)) + (((2 * PI) * (i mod n)) / n) by A1, XCMPLX_1:91
.= ((2 * PI) * (i div n)) + (((2 * PI) * (i mod n)) / n) ;
then A3: sin (((2 * PI) * i) / n) = ((sin (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) + ((cos (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS:80
.= ((sin . (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) + ((cos (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS:def 21
.= ((sin . (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) + ((cos . (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS:def 23
.= ((sin . 0) * (cos (((2 * PI) * (i mod n)) / n))) + ((cos . (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS2:10
.= ((sin . 0) * (cos (((2 * PI) * (i mod n)) / n))) + ((cos . 0) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS2:11
.= sin (((2 * PI) * (i mod n)) / n) by SIN_COS:33 ;
cos (((2 * PI) * i) / n) = ((cos (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) - ((sin (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by A2, SIN_COS:80
.= ((cos . (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) - ((sin (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS:def 23
.= ((cos . (((2 * PI) * (i div n)) + 0)) * (cos (((2 * PI) * (i mod n)) / n))) - ((sin . (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS:def 21
.= ((cos . 0) * (cos (((2 * PI) * (i mod n)) / n))) - ((sin . (((2 * PI) * (i div n)) + 0)) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS2:11
.= ((cos . 0) * (cos (((2 * PI) * (i mod n)) / n))) - ((sin . 0) * (sin (((2 * PI) * (i mod n)) / n))) by SIN_COS2:10
.= cos (((2 * PI) * (i mod n)) / n) by SIN_COS:33 ;
hence ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) ) by A3; :: thesis: verum

end;

suppose A4: n = 0 ; :: thesis: ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) )

then ((2 * PI) * i) / n = 0 by XCMPLX_1:49;
hence ( cos (((2 * PI) * i) / n) = cos (((2 * PI) * (i mod n)) / n) & sin (((2 * PI) * i) / n) = sin (((2 * PI) * (i mod n)) / n) ) by A4, XCMPLX_1:49; :: thesis: verum

end;

end;