let k be Nat; sec is (2 * PI) * (k + 1) -periodic
defpred S1[ Nat] means sec is (2 * PI) * ($1 + 1) -periodic ;
A1:
S1[ 0 ]
by Lm7;
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
sec is
(2 * PI) * (k + 1) -periodic
;
S1[k + 1]
sec is
(2 * PI) * ((k + 1) + 1) -periodic
proof
for
x being
Real st
x in dom sec holds
(
x + ((2 * PI) * ((k + 1) + 1)) in dom sec &
x - ((2 * PI) * ((k + 1) + 1)) in dom sec &
sec . x = sec . (x + ((2 * PI) * ((k + 1) + 1))) )
proof
let x be
Real;
( x in dom sec implies ( x + ((2 * PI) * ((k + 1) + 1)) in dom sec & x - ((2 * PI) * ((k + 1) + 1)) in dom sec & sec . x = sec . (x + ((2 * PI) * ((k + 1) + 1))) ) )
assume
x in dom sec
;
( x + ((2 * PI) * ((k + 1) + 1)) in dom sec & x - ((2 * PI) * ((k + 1) + 1)) in dom sec & sec . x = sec . (x + ((2 * PI) * ((k + 1) + 1))) )
then A4:
(
x + ((2 * PI) * (k + 1)) in dom sec &
x - ((2 * PI) * (k + 1)) in dom sec &
sec . x = sec . (x + ((2 * PI) * (k + 1))) )
by A3, Th1;
then
(
x + ((2 * PI) * (k + 1)) in (dom cos) \ (cos " {0}) &
x - ((2 * PI) * (k + 1)) in (dom cos) \ (cos " {0}) )
by RFUNCT_1:def 2;
then
(
x + ((2 * PI) * (k + 1)) in dom cos & not
x + ((2 * PI) * (k + 1)) in cos " {0} &
x - ((2 * PI) * (k + 1)) in dom cos & not
x - ((2 * PI) * (k + 1)) in cos " {0} )
by XBOOLE_0:def 5;
then A5:
( not
cos . (x + ((2 * PI) * (k + 1))) in {0} & not
cos . (x - ((2 * PI) * (k + 1))) in {0} )
by FUNCT_1:def 7;
then
cos . (x + ((2 * PI) * (k + 1))) <> 0
by TARSKI:def 1;
then
cos . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) <> 0
by SIN_COS:78;
then
not
cos . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) in {0}
by TARSKI:def 1;
then
(
(x + ((2 * PI) * (k + 1))) + (2 * PI) in dom cos & not
(x + ((2 * PI) * (k + 1))) + (2 * PI) in cos " {0} )
by FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;
then A6:
x + ((2 * PI) * ((k + 1) + 1)) in (dom cos) \ (cos " {0})
by XBOOLE_0:def 5;
x - ((2 * PI) * ((k + 1) + 1)) in dom cos
by SIN_COS:24, XREAL_0:def 1;
then
cos . (x - ((2 * PI) * ((k + 1) + 1))) = cos . ((x - ((2 * PI) * ((k + 1) + 1))) + (2 * PI))
by Lm3;
then
(
x - ((2 * PI) * ((k + 1) + 1)) in dom cos & not
x - ((2 * PI) * ((k + 1) + 1)) in cos " {0} )
by A5, FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;
then A7:
x - ((2 * PI) * ((k + 1) + 1)) in (dom cos) \ (cos " {0})
by XBOOLE_0:def 5;
then
(
x + ((2 * PI) * ((k + 1) + 1)) in dom sec &
x - ((2 * PI) * ((k + 1) + 1)) in dom sec )
by A6, RFUNCT_1:def 2;
then sec . (x + ((2 * PI) * ((k + 1) + 1))) =
(cos . ((x + ((2 * PI) * (k + 1))) + (2 * PI))) "
by RFUNCT_1:def 2
.=
(cos . (x + ((2 * PI) * (k + 1)))) "
by SIN_COS:78
.=
sec . x
by A4, RFUNCT_1:def 2
;
hence
(
x + ((2 * PI) * ((k + 1) + 1)) in dom sec &
x - ((2 * PI) * ((k + 1) + 1)) in dom sec &
sec . x = sec . (x + ((2 * PI) * ((k + 1) + 1))) )
by A6, A7, RFUNCT_1:def 2;
verum
end;
hence
sec is
(2 * PI) * ((k + 1) + 1) -periodic
by Th1;
verum
end;
hence
S1[
k + 1]
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
hence
sec is (2 * PI) * (k + 1) -periodic
; verum