let k be Nat; :: thesis: sin ^2 is PI * (k + 1) -periodic

defpred S_{1}[ Nat] means sin ^2 is PI * ($1 + 1) -periodic ;

A1: S_{1}[ 0 ]
by Lm20;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[n]
from NAT_1:sch 2(A1, A2);

hence sin ^2 is PI * (k + 1) -periodic ; :: thesis: verum

defpred S

A1: S

A2: for k being Nat st S

S

proof

for n being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: sin ^2 is PI * (k + 1) -periodic ; :: thesis: S_{1}[k + 1]

sin ^2 is PI * ((k + 1) + 1) -periodic_{1}[k + 1]
; :: thesis: verum

end;assume A3: sin ^2 is PI * (k + 1) -periodic ; :: thesis: S

sin ^2 is PI * ((k + 1) + 1) -periodic

proof

hence
S
for x being Real st x in dom (sin ^2) holds

( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) )

end;( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) )

proof

hence
sin ^2 is PI * ((k + 1) + 1) -periodic
by Th1; :: thesis: verum
let x be Real; :: thesis: ( x in dom (sin ^2) implies ( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) ) )

assume A4: x in dom (sin ^2) ; :: thesis: ( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) )

A5: ( x + (PI * ((k + 1) + 1)) in dom sin & x - (PI * ((k + 1) + 1)) in dom sin ) by SIN_COS:24, XREAL_0:def 1;

(sin ^2) . (x + (PI * ((k + 1) + 1))) = (sin . ((x + (PI * (k + 1))) + PI)) ^2 by VALUED_1:11

.= (- (sin . (x + (PI * (k + 1))))) ^2 by SIN_COS:78

.= (sin . (x + (PI * (k + 1)))) ^2

.= (sin ^2) . (x + (PI * (k + 1))) by VALUED_1:11 ;

hence ( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) ) by A3, A4, A5, VALUED_1:11; :: thesis: verum

end;assume A4: x in dom (sin ^2) ; :: thesis: ( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) )

A5: ( x + (PI * ((k + 1) + 1)) in dom sin & x - (PI * ((k + 1) + 1)) in dom sin ) by SIN_COS:24, XREAL_0:def 1;

(sin ^2) . (x + (PI * ((k + 1) + 1))) = (sin . ((x + (PI * (k + 1))) + PI)) ^2 by VALUED_1:11

.= (- (sin . (x + (PI * (k + 1))))) ^2 by SIN_COS:78

.= (sin . (x + (PI * (k + 1)))) ^2

.= (sin ^2) . (x + (PI * (k + 1))) by VALUED_1:11 ;

hence ( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) ) by A3, A4, A5, VALUED_1:11; :: thesis: verum

hence sin ^2 is PI * (k + 1) -periodic ; :: thesis: verum