let n, i be 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:62
.= ((((2 * PI) / n) * (n * (i div n))) / 1) + (((2 * PI) * (i mod n)) / n) by XCMPLX_1:83
.= (((2 * PI) * (1 / n)) * (n * (i div n))) + (((2 * PI) * (i mod n)) / n) by XCMPLX_1:99
.= ((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:90
.= ((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:75
.= ((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 17
.= ((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 19
.= ((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:30 ;
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:75
.= ((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 19
.= ((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 17
.= ((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:30 ;
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;