:: FUNCT_9 semantic presentation begin definition let t be real number ; let F be Function; attrF is t -periodic means :Def1: :: FUNCT_9:def 1 ( t <> 0 & ( for x being real number holds ( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) ) ); end; :: deftheorem Def1 defines -periodic FUNCT_9:def_1_:_ for t being real number for F being Function holds ( F is t -periodic iff ( t <> 0 & ( for x being real number holds ( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) ) ) ); definition let F be Function; attrF is periodic means :Def2: :: FUNCT_9:def 2 ex t being real number st F is t -periodic ; end; :: deftheorem Def2 defines periodic FUNCT_9:def_2_:_ for F being Function holds ( F is periodic iff ex t being real number st F is t -periodic ); theorem Th1: :: FUNCT_9:1 for t being real number for F being real-valued Function holds ( F is t -periodic iff ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) ) proof let t be real number ; ::_thesis: for F being real-valued Function holds ( F is t -periodic iff ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) ) let F be real-valued Function; ::_thesis: ( F is t -periodic iff ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) ) thus ( F is t -periodic implies ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) ) ::_thesis: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) implies F is t -periodic ) proof assume A1: F is t -periodic ; ::_thesis: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) proof let x be real number ; ::_thesis: ( x in dom F implies ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) assume x in dom F ; ::_thesis: ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) then (x - t) + t in dom F ; hence ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) by A1, Def1; ::_thesis: verum end; hence ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Def1; ::_thesis: verum end; assume A2: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) ; ::_thesis: F is t -periodic for x being real number holds ( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) proof let x be real number ; ::_thesis: ( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) ( x in dom F iff x + t in dom F ) proof ( x + t in dom F implies x in dom F ) proof assume x + t in dom F ; ::_thesis: x in dom F then (x + t) - t in dom F by A2; hence x in dom F ; ::_thesis: verum end; hence ( x in dom F iff x + t in dom F ) by A2; ::_thesis: verum end; hence ( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) by A2; ::_thesis: verum end; hence F is t -periodic by A2, Def1; ::_thesis: verum end; theorem Th2: :: FUNCT_9:2 for t being real number for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F + G is t -periodic proof let t be real number ; ::_thesis: for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F + G is t -periodic let F, G be real-valued Function; ::_thesis: ( F is t -periodic & G is t -periodic implies F + G is t -periodic ) assume that A1: F is t -periodic and A2: G is t -periodic ; ::_thesis: F + G is t -periodic A3: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Th1; for x being real number st x in dom (F + G) holds ( x + t in dom (F + G) & x - t in dom (F + G) & (F + G) . x = (F + G) . (x + t) ) proof let x be real number ; ::_thesis: ( x in dom (F + G) implies ( x + t in dom (F + G) & x - t in dom (F + G) & (F + G) . x = (F + G) . (x + t) ) ) assume A4: x in dom (F + G) ; ::_thesis: ( x + t in dom (F + G) & x - t in dom (F + G) & (F + G) . x = (F + G) . (x + t) ) then A5: x in (dom F) /\ (dom G) by VALUED_1:def_1; A6: ( (dom F) /\ (dom G) c= dom F & (dom F) /\ (dom G) c= dom G ) by XBOOLE_1:17; then A7: ( x + t in dom F & x - t in dom F ) by A1, Th1, A5; ( x + t in dom G & x - t in dom G ) by A2, Th1, A5, A6; then A8: ( x + t in (dom F) /\ (dom G) & x - t in (dom F) /\ (dom G) ) by A7, XBOOLE_0:def_4; then A9: ( x + t in dom (F + G) & x - t in dom (F + G) ) by VALUED_1:def_1; (F + G) . x = (F . x) + (G . x) by A4, VALUED_1:def_1 .= (F . (x + t)) + (G . x) by A1, Th1, A5, A6 .= (F . (x + t)) + (G . (x + t)) by A2, Th1, A5, A6 .= (F + G) . (x + t) by A9, VALUED_1:def_1 ; hence ( x + t in dom (F + G) & x - t in dom (F + G) & (F + G) . x = (F + G) . (x + t) ) by A8, VALUED_1:def_1; ::_thesis: verum end; hence F + G is t -periodic by A3, Th1; ::_thesis: verum end; Lm1: for t, a being real number st t <> 0 holds REAL --> a is t -periodic proof let t, a be real number ; ::_thesis: ( t <> 0 implies REAL --> a is t -periodic ) set F = REAL --> a; assume t <> 0 ; ::_thesis: REAL --> a is t -periodic hence t <> 0 ; :: according to FUNCT_9:def_1 ::_thesis: for x being real number holds ( ( x in dom (REAL --> a) implies x + t in dom (REAL --> a) ) & ( x + t in dom (REAL --> a) implies x in dom (REAL --> a) ) & ( x in dom (REAL --> a) implies (REAL --> a) . x = (REAL --> a) . (x + t) ) ) let x be real number ; ::_thesis: ( ( x in dom (REAL --> a) implies x + t in dom (REAL --> a) ) & ( x + t in dom (REAL --> a) implies x in dom (REAL --> a) ) & ( x in dom (REAL --> a) implies (REAL --> a) . x = (REAL --> a) . (x + t) ) ) A1: ( x in REAL & x + t in REAL ) by XREAL_0:def_1; hence ( x in dom (REAL --> a) iff x + t in dom (REAL --> a) ) by FUNCOP_1:13; ::_thesis: ( x in dom (REAL --> a) implies (REAL --> a) . x = (REAL --> a) . (x + t) ) assume x in dom (REAL --> a) ; ::_thesis: (REAL --> a) . x = (REAL --> a) . (x + t) thus (REAL --> a) . x = a by A1, FUNCOP_1:7 .= (REAL --> a) . (x + t) by A1, FUNCOP_1:7 ; ::_thesis: verum end; theorem Th3: :: FUNCT_9:3 for t being real number for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F - G is t -periodic proof let t be real number ; ::_thesis: for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F - G is t -periodic let F, G be real-valued Function; ::_thesis: ( F is t -periodic & G is t -periodic implies F - G is t -periodic ) assume that A1: F is t -periodic and A2: G is t -periodic ; ::_thesis: F - G is t -periodic A3: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Th1; for x being real number st x in dom (F - G) holds ( x + t in dom (F - G) & x - t in dom (F - G) & (F - G) . x = (F - G) . (x + t) ) proof let x be real number ; ::_thesis: ( x in dom (F - G) implies ( x + t in dom (F - G) & x - t in dom (F - G) & (F - G) . x = (F - G) . (x + t) ) ) assume A4: x in dom (F - G) ; ::_thesis: ( x + t in dom (F - G) & x - t in dom (F - G) & (F - G) . x = (F - G) . (x + t) ) then A5: x in (dom F) /\ (dom G) by VALUED_1:12; A6: ( (dom F) /\ (dom G) c= dom F & (dom F) /\ (dom G) c= dom G ) by XBOOLE_1:17; then A7: ( x + t in dom F & x - t in dom F ) by A1, A5, Th1; ( x + t in dom G & x - t in dom G ) by A2, Th1, A5, A6; then A8: ( x + t in (dom F) /\ (dom G) & x - t in (dom F) /\ (dom G) ) by A7, XBOOLE_0:def_4; then A9: ( x + t in dom (F - G) & x - t in dom (F - G) ) by VALUED_1:12; (F - G) . x = (F . x) - (G . x) by A4, VALUED_1:13 .= (F . (x + t)) - (G . x) by A1, Th1, A5, A6 .= (F . (x + t)) - (G . (x + t)) by A2, Th1, A5, A6 .= (F - G) . (x + t) by A9, VALUED_1:13 ; hence ( x + t in dom (F - G) & x - t in dom (F - G) & (F - G) . x = (F - G) . (x + t) ) by A8, VALUED_1:12; ::_thesis: verum end; hence F - G is t -periodic by A3, Th1; ::_thesis: verum end; theorem Th4: :: FUNCT_9:4 for t being real number for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F (#) G is t -periodic proof let t be real number ; ::_thesis: for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F (#) G is t -periodic let F, G be real-valued Function; ::_thesis: ( F is t -periodic & G is t -periodic implies F (#) G is t -periodic ) assume that A1: F is t -periodic and A2: G is t -periodic ; ::_thesis: F (#) G is t -periodic A3: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Th1; for x being real number st x in dom (F (#) G) holds ( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) ) proof let x be real number ; ::_thesis: ( x in dom (F (#) G) implies ( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) ) ) assume A4: x in dom (F (#) G) ; ::_thesis: ( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) ) then A5: x in (dom F) /\ (dom G) by VALUED_1:def_4; A6: ( (dom F) /\ (dom G) c= dom F & (dom F) /\ (dom G) c= dom G ) by XBOOLE_1:17; then A7: ( x + t in dom F & x - t in dom F ) by A1, Th1, A5; ( x + t in dom G & x - t in dom G ) by A2, Th1, A5, A6; then A8: ( x + t in (dom F) /\ (dom G) & x - t in (dom F) /\ (dom G) ) by A7, XBOOLE_0:def_4; then A9: ( x + t in dom (F (#) G) & x - t in dom (F (#) G) ) by VALUED_1:def_4; (F (#) G) . x = (F . x) * (G . x) by A4, VALUED_1:def_4 .= (F . (x + t)) * (G . x) by A1, Th1, A5, A6 .= (F . (x + t)) * (G . (x + t)) by A2, Th1, A5, A6 .= (F (#) G) . (x + t) by A9, VALUED_1:def_4 ; hence ( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) ) by A8, VALUED_1:def_4; ::_thesis: verum end; hence F (#) G is t -periodic by A3, Th1; ::_thesis: verum end; theorem Th5: :: FUNCT_9:5 for t being real number for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F /" G is t -periodic proof let t be real number ; ::_thesis: for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F /" G is t -periodic let F, G be real-valued Function; ::_thesis: ( F is t -periodic & G is t -periodic implies F /" G is t -periodic ) assume that A1: F is t -periodic and A2: G is t -periodic ; ::_thesis: F /" G is t -periodic A3: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Th1; for x being real number st x in dom (F /" G) holds ( x + t in dom (F /" G) & x - t in dom (F /" G) & (F /" G) . x = (F /" G) . (x + t) ) proof let x be real number ; ::_thesis: ( x in dom (F /" G) implies ( x + t in dom (F /" G) & x - t in dom (F /" G) & (F /" G) . x = (F /" G) . (x + t) ) ) assume x in dom (F /" G) ; ::_thesis: ( x + t in dom (F /" G) & x - t in dom (F /" G) & (F /" G) . x = (F /" G) . (x + t) ) then A4: x in (dom F) /\ (dom G) by VALUED_1:16; A5: ( (dom F) /\ (dom G) c= dom F & (dom F) /\ (dom G) c= dom G ) by XBOOLE_1:17; then A6: ( x + t in dom F & x - t in dom F ) by A1, Th1, A4; ( x + t in dom G & x - t in dom G ) by A2, Th1, A4, A5; then A7: ( x + t in (dom F) /\ (dom G) & x - t in (dom F) /\ (dom G) ) by A6, XBOOLE_0:def_4; (F /" G) . x = (F . x) / (G . x) by VALUED_1:17 .= (F . (x + t)) / (G . x) by A1, Th1, A4, A5 .= (F . (x + t)) / (G . (x + t)) by A2, Th1, A4, A5 .= (F /" G) . (x + t) by VALUED_1:17 ; hence ( x + t in dom (F /" G) & x - t in dom (F /" G) & (F /" G) . x = (F /" G) . (x + t) ) by A7, VALUED_1:16; ::_thesis: verum end; hence F /" G is t -periodic by A3, Th1; ::_thesis: verum end; theorem Th6: :: FUNCT_9:6 for t being real number for F being real-valued Function st F is t -periodic holds - F is t -periodic proof let t be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds - F is t -periodic let F be real-valued Function; ::_thesis: ( F is t -periodic implies - F is t -periodic ) assume A1: F is t -periodic ; ::_thesis: - F is t -periodic then A2: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1; for x being real number st x in dom (- F) holds ( x + t in dom (- F) & x - t in dom (- F) & (- F) . x = (- F) . (x + t) ) proof let x be real number ; ::_thesis: ( x in dom (- F) implies ( x + t in dom (- F) & x - t in dom (- F) & (- F) . x = (- F) . (x + t) ) ) assume x in dom (- F) ; ::_thesis: ( x + t in dom (- F) & x - t in dom (- F) & (- F) . x = (- F) . (x + t) ) then A3: x in dom F by VALUED_1:8; then A4: ( x + t in dom F & x - t in dom F ) by A1, Th1; (- F) . x = - (F . x) by VALUED_1:8 .= - (F . (x + t)) by A1, Th1, A3 .= (- F) . (x + t) by VALUED_1:8 ; hence ( x + t in dom (- F) & x - t in dom (- F) & (- F) . x = (- F) . (x + t) ) by A4, VALUED_1:8; ::_thesis: verum end; hence - F is t -periodic by A2, Th1; ::_thesis: verum end; theorem Th7: :: FUNCT_9:7 for t, r being real number for F being real-valued Function st F is t -periodic holds r (#) F is t -periodic proof let t, r be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds r (#) F is t -periodic let F be real-valued Function; ::_thesis: ( F is t -periodic implies r (#) F is t -periodic ) assume A1: F is t -periodic ; ::_thesis: r (#) F is t -periodic then A2: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1; for x being real number st x in dom (r (#) F) holds ( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) ) proof let x be real number ; ::_thesis: ( x in dom (r (#) F) implies ( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) ) ) assume A3: x in dom (r (#) F) ; ::_thesis: ( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) ) then A4: x in dom F by VALUED_1:def_5; then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1; then A6: ( x + t in dom (r (#) F) & x - t in dom (r (#) F) ) by VALUED_1:def_5; (r (#) F) . x = r * (F . x) by A3, VALUED_1:def_5 .= r * (F . (x + t)) by A1, Th1, A4 .= (r (#) F) . (x + t) by A6, VALUED_1:def_5 ; hence ( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) ) by A5, VALUED_1:def_5; ::_thesis: verum end; hence r (#) F is t -periodic by A2, Th1; ::_thesis: verum end; theorem Th8: :: FUNCT_9:8 for t, r being real number for F being real-valued Function st F is t -periodic holds r + F is t -periodic proof let t, r be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds r + F is t -periodic let F be real-valued Function; ::_thesis: ( F is t -periodic implies r + F is t -periodic ) assume A1: F is t -periodic ; ::_thesis: r + F is t -periodic then A2: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1; for x being real number st x in dom (r + F) holds ( x + t in dom (r + F) & x - t in dom (r + F) & (r + F) . x = (r + F) . (x + t) ) proof let x be real number ; ::_thesis: ( x in dom (r + F) implies ( x + t in dom (r + F) & x - t in dom (r + F) & (r + F) . x = (r + F) . (x + t) ) ) assume A3: x in dom (r + F) ; ::_thesis: ( x + t in dom (r + F) & x - t in dom (r + F) & (r + F) . x = (r + F) . (x + t) ) then A4: x in dom F by VALUED_1:def_2; then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1; then A6: ( x + t in dom (r + F) & x - t in dom (r + F) ) by VALUED_1:def_2; (r + F) . x = r + (F . x) by A3, VALUED_1:def_2 .= r + (F . (x + t)) by A1, Th1, A4 .= (r + F) . (x + t) by A6, VALUED_1:def_2 ; hence ( x + t in dom (r + F) & x - t in dom (r + F) & (r + F) . x = (r + F) . (x + t) ) by A5, VALUED_1:def_2; ::_thesis: verum end; hence r + F is t -periodic by A2, Th1; ::_thesis: verum end; theorem :: FUNCT_9:9 for t, r being real number for F being real-valued Function st F is t -periodic holds F - r is t -periodic by Th8; theorem Th10: :: FUNCT_9:10 for t being real number for F being real-valued Function st F is t -periodic holds |.F.| is t -periodic proof let t be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds |.F.| is t -periodic let F be real-valued Function; ::_thesis: ( F is t -periodic implies |.F.| is t -periodic ) assume A1: F is t -periodic ; ::_thesis: |.F.| is t -periodic then A2: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1; for x being real number st x in dom |.F.| holds ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) ) proof let x be real number ; ::_thesis: ( x in dom |.F.| implies ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) ) ) assume A3: x in dom |.F.| ; ::_thesis: ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) ) then A4: x in dom F by VALUED_1:def_11; then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1; then A6: ( x + t in dom |.F.| & x - t in dom |.F.| ) by VALUED_1:def_11; |.F.| . x = |.(F . x).| by A3, VALUED_1:def_11 .= |.(F . (x + t)).| by A1, Th1, A4 .= |.F.| . (x + t) by A6, VALUED_1:def_11 ; hence ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) ) by A5, VALUED_1:def_11; ::_thesis: verum end; hence |.F.| is t -periodic by A2, Th1; ::_thesis: verum end; theorem Th11: :: FUNCT_9:11 for t being real number for F being real-valued Function st F is t -periodic holds F " is t -periodic proof let t be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds F " is t -periodic let F be real-valued Function; ::_thesis: ( F is t -periodic implies F " is t -periodic ) assume A1: F is t -periodic ; ::_thesis: F " is t -periodic then A2: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1; for x being real number st x in dom (F ") holds ( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) ) proof let x be real number ; ::_thesis: ( x in dom (F ") implies ( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) ) ) assume A3: x in dom (F ") ; ::_thesis: ( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) ) then A4: x in dom F by VALUED_1:def_7; then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1; then A6: ( x + t in dom (F ") & x - t in dom (F ") ) by VALUED_1:def_7; (F ") . x = (F . x) " by A3, VALUED_1:def_7 .= (F . (x + t)) " by A1, Th1, A4 .= (F ") . (x + t) by A6, VALUED_1:def_7 ; hence ( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) ) by A5, VALUED_1:def_7; ::_thesis: verum end; hence F " is t -periodic by A2, Th1; ::_thesis: verum end; theorem :: FUNCT_9:12 for t being real number for F being real-valued Function st F is t -periodic holds F ^2 is t -periodic by Th4; theorem Th13: :: FUNCT_9:13 for t being real number for F being real-valued Function st F is t -periodic holds for x being real number st x in dom F holds F . x = F . (x - t) proof let t be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds for x being real number st x in dom F holds F . x = F . (x - t) let F be real-valued Function; ::_thesis: ( F is t -periodic implies for x being real number st x in dom F holds F . x = F . (x - t) ) assume A1: F is t -periodic ; ::_thesis: for x being real number st x in dom F holds F . x = F . (x - t) let x be real number ; ::_thesis: ( x in dom F implies F . x = F . (x - t) ) assume x in dom F ; ::_thesis: F . x = F . (x - t) then ( x + t in dom F & x - t in dom F ) by A1, Th1; then F . (x - t) = F . ((x - t) + t) by A1, Th1 .= F . x ; hence F . x = F . (x - t) ; ::_thesis: verum end; theorem Th14: :: FUNCT_9:14 for t being real number for F being real-valued Function st F is t -periodic holds F is - t -periodic proof let t be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds F is - t -periodic let F be real-valued Function; ::_thesis: ( F is t -periodic implies F is - t -periodic ) assume A1: F is t -periodic ; ::_thesis: F is - t -periodic then A2: - t <> 0 by Th1; for x being real number st x in dom F holds ( x + (- t) in dom F & x - (- t) in dom F & F . x = F . (x + (- t)) ) proof let x be real number ; ::_thesis: ( x in dom F implies ( x + (- t) in dom F & x - (- t) in dom F & F . x = F . (x + (- t)) ) ) assume A3: x in dom F ; ::_thesis: ( x + (- t) in dom F & x - (- t) in dom F & F . x = F . (x + (- t)) ) then ( x + t in dom F & x - t in dom F ) by A1, Th1; hence ( x + (- t) in dom F & x - (- t) in dom F & F . x = F . (x + (- t)) ) by A1, Th13, A3; ::_thesis: verum end; hence F is - t -periodic by A2, Th1; ::_thesis: verum end; theorem :: FUNCT_9:15 for t1, t2 being real number for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 holds F is t1 + t2 -periodic proof let t1, t2 be real number ; ::_thesis: for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 holds F is t1 + t2 -periodic let F be real-valued Function; ::_thesis: ( F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 implies F is t1 + t2 -periodic ) assume A1: ( F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 ) ; ::_thesis: F is t1 + t2 -periodic for x being real number st x in dom F holds ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) proof let x be real number ; ::_thesis: ( x in dom F implies ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) ) assume A2: x in dom F ; ::_thesis: ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) then ( x + t1 in dom F & x - t1 in dom F ) by A1, Th1; then ( (x + t1) + t2 in dom F & (x - t1) - t2 in dom F & F . (x + t1) = F . ((x + t1) + t2) ) by A1, Th1; hence ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) by A1, Th1, A2; ::_thesis: verum end; hence F is t1 + t2 -periodic by A1, Th1; ::_thesis: verum end; theorem :: FUNCT_9:16 for t1, t2 being real number for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 holds F is t1 - t2 -periodic proof let t1, t2 be real number ; ::_thesis: for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 holds F is t1 - t2 -periodic let F be real-valued Function; ::_thesis: ( F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 implies F is t1 - t2 -periodic ) assume A1: ( F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 ) ; ::_thesis: F is t1 - t2 -periodic for x being real number st x in dom F holds ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) proof let x be real number ; ::_thesis: ( x in dom F implies ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) ) assume A2: x in dom F ; ::_thesis: ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) then ( x + t1 in dom F & x - t1 in dom F ) by A1, Th1; then A3: ( (x + t1) - t2 in dom F & (x - t1) + t2 in dom F ) by A1, Th1; A4: x - t2 in dom F by A1, Th1, A2; then F . ((x - t2) + t1) = F . (x - t2) by A1, Th1 .= F . ((x - t2) + t2) by A1, Th1, A4 .= F . x ; hence ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) by A3; ::_thesis: verum end; hence F is t1 - t2 -periodic by A1, Th1; ::_thesis: verum end; theorem :: FUNCT_9:17 for t being real number for F being real-valued Function st t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . (x + t) = F . (x - t) ) ) holds ( F is 2 * t -periodic & F is periodic ) proof let t be real number ; ::_thesis: for F being real-valued Function st t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . (x + t) = F . (x - t) ) ) holds ( F is 2 * t -periodic & F is periodic ) let F be real-valued Function; ::_thesis: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . (x + t) = F . (x - t) ) ) implies ( F is 2 * t -periodic & F is periodic ) ) assume that A1: t <> 0 and A2: for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . (x + t) = F . (x - t) ) ; ::_thesis: ( F is 2 * t -periodic & F is periodic ) for x being real number st x in dom F holds ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) proof let x be real number ; ::_thesis: ( x in dom F implies ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) ) assume x in dom F ; ::_thesis: ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) then A3: ( x + t in dom F & x - t in dom F ) by A2; then A4: ( (x + t) + t in dom F & (x - t) - t in dom F ) by A2; F . (x + (2 * t)) = F . ((x + t) + t) .= F . ((x + t) - t) by A2, A3 .= F . x ; hence ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) by A4; ::_thesis: verum end; then F is 2 * t -periodic by A1, Th1; hence ( F is 2 * t -periodic & F is periodic ) by Def2; ::_thesis: verum end; theorem :: FUNCT_9:18 for t1, t2 being real number for F being real-valued Function st t1 + t2 <> 0 & ( for x being real number st x in dom F holds ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ) holds ( F is t1 + t2 -periodic & F is periodic ) proof let t1, t2 be real number ; ::_thesis: for F being real-valued Function st t1 + t2 <> 0 & ( for x being real number st x in dom F holds ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ) holds ( F is t1 + t2 -periodic & F is periodic ) let F be real-valued Function; ::_thesis: ( t1 + t2 <> 0 & ( for x being real number st x in dom F holds ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ) implies ( F is t1 + t2 -periodic & F is periodic ) ) assume that A1: t1 + t2 <> 0 and A2: for x being real number st x in dom F holds ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ; ::_thesis: ( F is t1 + t2 -periodic & F is periodic ) for x being real number st x in dom F holds ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) proof let x be real number ; ::_thesis: ( x in dom F implies ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) ) assume x in dom F ; ::_thesis: ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) then A3: ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F ) by A2; then A4: ( (x + t1) + t2 in dom F & (x - t1) - t2 in dom F ) by A2; F . (x + (t1 + t2)) = F . ((x + t2) + t1) .= F . ((x + t2) - t2) by A2, A3 .= F . x ; hence ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) by A4; ::_thesis: verum end; then F is t1 + t2 -periodic by Th1, A1; hence ( F is t1 + t2 -periodic & F is periodic ) by Def2; ::_thesis: verum end; theorem :: FUNCT_9:19 for t1, t2 being real number for F being real-valued Function st t1 - t2 <> 0 & ( for x being real number st x in dom F holds ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x + t2) ) ) holds ( F is t1 - t2 -periodic & F is periodic ) proof let t1, t2 be real number ; ::_thesis: for F being real-valued Function st t1 - t2 <> 0 & ( for x being real number st x in dom F holds ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x + t2) ) ) holds ( F is t1 - t2 -periodic & F is periodic ) let F be real-valued Function; ::_thesis: ( t1 - t2 <> 0 & ( for x being real number st x in dom F holds ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x + t2) ) ) implies ( F is t1 - t2 -periodic & F is periodic ) ) assume that A1: t1 - t2 <> 0 and A2: for x being real number st x in dom F holds ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x + t2) ) ; ::_thesis: ( F is t1 - t2 -periodic & F is periodic ) for x being real number st x in dom F holds ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) proof let x be real number ; ::_thesis: ( x in dom F implies ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) ) assume x in dom F ; ::_thesis: ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) then A3: ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F ) by A2; then A4: ( (x + t1) - t2 in dom F & (x - t1) + t2 in dom F ) by A2; F . (x + (t1 - t2)) = F . ((x - t2) + t1) .= F . ((x - t2) + t2) by A2, A3 .= F . x ; hence ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) by A4; ::_thesis: verum end; then F is t1 - t2 -periodic by Th1, A1; hence ( F is t1 - t2 -periodic & F is periodic ) by Def2; ::_thesis: verum end; theorem :: FUNCT_9:20 for t being real number for F being real-valued Function st t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . (x + t) = (F . x) " ) ) holds ( F is 2 * t -periodic & F is periodic ) proof let t be real number ; ::_thesis: for F being real-valued Function st t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . (x + t) = (F . x) " ) ) holds ( F is 2 * t -periodic & F is periodic ) let F be real-valued Function; ::_thesis: ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . (x + t) = (F . x) " ) ) implies ( F is 2 * t -periodic & F is periodic ) ) assume that A1: t <> 0 and A2: for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . (x + t) = (F . x) " ) ; ::_thesis: ( F is 2 * t -periodic & F is periodic ) for x being real number st x in dom F holds ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) proof let x be real number ; ::_thesis: ( x in dom F implies ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) ) assume A3: x in dom F ; ::_thesis: ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) then A4: ( x + t in dom F & x - t in dom F ) by A2; then A5: ( (x + t) + t in dom F & (x - t) - t in dom F ) by A2; F . (x + (2 * t)) = F . ((x + t) + t) .= (F . (x + t)) " by A2, A4 .= ((F . x) ") " by A2, A3 .= F . x ; hence ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) by A5; ::_thesis: verum end; then F is 2 * t -periodic by A1, Th1; hence ( F is 2 * t -periodic & F is periodic ) by Def2; ::_thesis: verum end; Lm2: sin is 2 * PI -periodic proof for x being real number st x in dom sin holds ( x + (2 * PI) in dom sin & x - (2 * PI) in dom sin & sin . x = sin . (x + (2 * PI)) ) by SIN_COS:24, SIN_COS:78; hence sin is 2 * PI -periodic by Th1; ::_thesis: verum end; registration cluster Relation-like Function-like real-valued periodic for set ; existence ex b1 being Function st ( b1 is periodic & b1 is real-valued ) proof take sin ; ::_thesis: ( sin is periodic & sin is real-valued ) thus ( sin is periodic & sin is real-valued ) by Lm2, Def2; ::_thesis: verum end; cluster Relation-like Function-like complex-valued ext-real-valued real-valued periodic for Element of K6(K7(REAL,REAL)); existence ex b1 being PartFunc of REAL,REAL st b1 is periodic proof take sin ; ::_thesis: sin is periodic thus sin is periodic by Lm2, Def2; ::_thesis: verum end; end; registration let t be non zero real number ; clusterREAL --> t -> t -periodic ; coherence REAL --> t is t -periodic by Lm1; cluster Relation-like Function-like real-valued t -periodic for set ; existence ex b1 being Function st ( b1 is t -periodic & b1 is real-valued ) proof take REAL --> t ; ::_thesis: ( REAL --> t is t -periodic & REAL --> t is real-valued ) thus ( REAL --> t is t -periodic & REAL --> t is real-valued ) ; ::_thesis: verum end; end; registration let t be non zero real number ; let F, G be real-valued t -periodic Function; clusterF + G -> t -periodic ; coherence F + G is t -periodic by Th2; clusterF - G -> t -periodic ; coherence F - G is t -periodic by Th3; clusterF (#) G -> t -periodic ; coherence F (#) G is t -periodic by Th4; clusterF /" G -> t -periodic ; coherence F /" G is t -periodic by Th5; end; registration let F be real-valued periodic Function; cluster - F -> periodic ; coherence - F is periodic proof consider t being real number such that A1: F is t -periodic by Def2; - F is t -periodic by A1, Th6; hence - F is periodic by Def2; ::_thesis: verum end; end; registration let F be real-valued periodic Function; let r be real number ; clusterr (#) F -> periodic ; coherence r (#) F is periodic proof consider t being real number such that A1: F is t -periodic by Def2; r (#) F is t -periodic by A1, Th7; hence r (#) F is periodic by Def2; ::_thesis: verum end; clusterr + F -> periodic ; coherence r + F is periodic proof consider t being real number such that A2: F is t -periodic by Def2; r + F is t -periodic by A2, Th8; hence r + F is periodic by Def2; ::_thesis: verum end; clusterF - r -> periodic ; coherence F - r is periodic ; end; registration let F be real-valued periodic Function; cluster|.F.| -> periodic ; coherence |.F.| is periodic proof consider t being real number such that A1: F is t -periodic by Def2; |.F.| is t -periodic by A1, Th10; hence |.F.| is periodic by Def2; ::_thesis: verum end; clusterF " -> periodic ; coherence F " is periodic proof consider t being real number such that A2: F is t -periodic by Def2; F " is t -periodic by A2, Th11; hence F " is periodic by Def2; ::_thesis: verum end; clusterF ^2 -> periodic ; coherence F ^2 is periodic proof consider t being real number such that A3: F is t -periodic by Def2; F ^2 is t -periodic by A3, Th4; hence F ^2 is periodic by Def2; ::_thesis: verum end; end; begin Lm3: cos is 2 * PI -periodic proof for x being real number st x in dom cos holds ( x + (2 * PI) in dom cos & x - (2 * PI) in dom cos & cos . x = cos . (x + (2 * PI)) ) by SIN_COS:24, SIN_COS:78; hence cos is 2 * PI -periodic by Th1; ::_thesis: verum end; registration cluster sin -> periodic ; coherence sin is periodic by Def2, Lm2; cluster cos -> periodic ; coherence cos is periodic by Def2, Lm3; end; Lm4: for k being Nat holds sin is (2 * PI) * (k + 1) -periodic proof let k be Nat; ::_thesis: sin is (2 * PI) * (k + 1) -periodic defpred S1[ Nat] means sin is (2 * PI) * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm2; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: sin is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1] sin is (2 * PI) * ((k + 1) + 1) -periodic proof for x being real number st x in dom sin holds sin . x = sin . (x + ((2 * PI) * ((k + 1) + 1))) proof let x be real number ; ::_thesis: ( x in dom sin implies sin . x = sin . (x + ((2 * PI) * ((k + 1) + 1))) ) assume A4: x in dom sin ; ::_thesis: sin . x = sin . (x + ((2 * PI) * ((k + 1) + 1))) sin . (x + ((2 * PI) * (k + 1))) = sin . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) by SIN_COS:78; hence sin . x = sin . (x + ((2 * PI) * ((k + 1) + 1))) by A3, Th1, A4; ::_thesis: verum end; then ( (2 * PI) * ((k + 1) + 1) <> 0 & ( for x being real number st x in dom sin holds ( x + ((2 * PI) * ((k + 1) + 1)) in dom sin & x - ((2 * PI) * ((k + 1) + 1)) in dom sin & sin . x = sin . (x + ((2 * PI) * ((k + 1) + 1))) ) ) ) by SIN_COS:24; hence sin is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence sin is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:21 for i being non zero Integer holds sin is (2 * PI) * i -periodic proof let i be non zero Integer; ::_thesis: sin is (2 * PI) * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: sin is (2 * PI) * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence sin is (2 * PI) * i -periodic by Lm4; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: sin is (2 * PI) * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; sin is (2 * PI) * (m + 1) -periodic by Lm4; then sin is - ((2 * PI) * (m + 1)) -periodic by Th14; hence sin is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm5: for k being Nat holds cos is (2 * PI) * (k + 1) -periodic proof let k be Nat; ::_thesis: cos is (2 * PI) * (k + 1) -periodic defpred S1[ Nat] means cos is (2 * PI) * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm3; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: cos is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1] cos is (2 * PI) * ((k + 1) + 1) -periodic proof for x being real number st x in dom cos holds cos . x = cos . (x + ((2 * PI) * ((k + 1) + 1))) proof let x be real number ; ::_thesis: ( x in dom cos implies cos . x = cos . (x + ((2 * PI) * ((k + 1) + 1))) ) assume A4: x in dom cos ; ::_thesis: cos . x = cos . (x + ((2 * PI) * ((k + 1) + 1))) cos . (x + ((2 * PI) * (k + 1))) = cos . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) by SIN_COS:78; hence cos . x = cos . (x + ((2 * PI) * ((k + 1) + 1))) by A3, Th1, A4; ::_thesis: verum end; then ( (2 * PI) * ((k + 1) + 1) <> 0 & ( for x being real number st x in dom cos holds ( x + ((2 * PI) * ((k + 1) + 1)) in dom cos & x - ((2 * PI) * ((k + 1) + 1)) in dom cos & cos . x = cos . (x + ((2 * PI) * ((k + 1) + 1))) ) ) ) by SIN_COS:24; hence cos is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence cos is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:22 for i being non zero Integer holds cos is (2 * PI) * i -periodic proof let i be non zero Integer; ::_thesis: cos is (2 * PI) * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: cos is (2 * PI) * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence cos is (2 * PI) * i -periodic by Lm5; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: cos is (2 * PI) * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; cos is (2 * PI) * (m + 1) -periodic by Lm5; then cos is - ((2 * PI) * (m + 1)) -periodic by Th14; hence cos is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm6: cosec is 2 * PI -periodic proof for x being real number st x in dom cosec holds ( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec & cosec . x = cosec . (x + (2 * PI)) ) proof let x be real number ; ::_thesis: ( x in dom cosec implies ( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec & cosec . x = cosec . (x + (2 * PI)) ) ) assume A1: x in dom cosec ; ::_thesis: ( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec & cosec . x = cosec . (x + (2 * PI)) ) then x in (dom sin) \ (sin " {0}) by RFUNCT_1:def_2; then ( x in dom sin & not x in sin " {0} ) by XBOOLE_0:def_5; then A2: not sin . x in {0} by FUNCT_1:def_7; then sin . x <> 0 by TARSKI:def_1; then sin . (x + (2 * PI)) <> 0 by SIN_COS:78; then not sin . (x + (2 * PI)) in {0} by TARSKI:def_1; then ( x + (2 * PI) in dom sin & not x + (2 * PI) in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24; then A3: x + (2 * PI) in (dom sin) \ (sin " {0}) by XBOOLE_0:def_5; sin . (x - (2 * PI)) = sin . ((x - (2 * PI)) + (2 * PI)) by Lm2, Th1, SIN_COS:24; then ( x - (2 * PI) in dom sin & not x - (2 * PI) in sin " {0} ) by A2, FUNCT_1:def_7, SIN_COS:24; then A4: x - (2 * PI) in (dom sin) \ (sin " {0}) by XBOOLE_0:def_5; then ( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec ) by A3, RFUNCT_1:def_2; then cosec . (x + (2 * PI)) = (sin . (x + (2 * PI))) " by RFUNCT_1:def_2 .= (sin . x) " by SIN_COS:78 .= cosec . x by A1, RFUNCT_1:def_2 ; hence ( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec & cosec . x = cosec . (x + (2 * PI)) ) by A3, A4, RFUNCT_1:def_2; ::_thesis: verum end; hence cosec is 2 * PI -periodic by Th1; ::_thesis: verum end; Lm7: sec is 2 * PI -periodic proof for x being real number st x in dom sec holds ( x + (2 * PI) in dom sec & x - (2 * PI) in dom sec & sec . x = sec . (x + (2 * PI)) ) proof let x be real number ; ::_thesis: ( x in dom sec implies ( x + (2 * PI) in dom sec & x - (2 * PI) in dom sec & sec . x = sec . (x + (2 * PI)) ) ) assume A1: x in dom sec ; ::_thesis: ( x + (2 * PI) in dom sec & x - (2 * PI) in dom sec & sec . x = sec . (x + (2 * PI)) ) then x in (dom cos) \ (cos " {0}) by RFUNCT_1:def_2; then ( x in dom cos & not x in cos " {0} ) by XBOOLE_0:def_5; then A2: not cos . x in {0} by FUNCT_1:def_7; then cos . x <> 0 by TARSKI:def_1; then cos . (x + (2 * PI)) <> 0 by SIN_COS:78; then not cos . (x + (2 * PI)) in {0} by TARSKI:def_1; then ( x + (2 * PI) in dom cos & not x + (2 * PI) in cos " {0} ) by FUNCT_1:def_7, SIN_COS:24; then A3: x + (2 * PI) in (dom cos) \ (cos " {0}) by XBOOLE_0:def_5; cos . (x - (2 * PI)) = cos . ((x - (2 * PI)) + (2 * PI)) by Lm3, Th1, SIN_COS:24; then ( x - (2 * PI) in dom cos & not x - (2 * PI) in cos " {0} ) by A2, FUNCT_1:def_7, SIN_COS:24; then A4: x - (2 * PI) in (dom cos) \ (cos " {0}) by XBOOLE_0:def_5; then ( x + (2 * PI) in dom sec & x - (2 * PI) in dom sec ) by A3, RFUNCT_1:def_2; then sec . (x + (2 * PI)) = (cos . (x + (2 * PI))) " by RFUNCT_1:def_2 .= (cos . x) " by SIN_COS:78 .= sec . x by A1, RFUNCT_1:def_2 ; hence ( x + (2 * PI) in dom sec & x - (2 * PI) in dom sec & sec . x = sec . (x + (2 * PI)) ) by A3, A4, RFUNCT_1:def_2; ::_thesis: verum end; hence sec is 2 * PI -periodic by Th1; ::_thesis: verum end; registration cluster cosec -> periodic ; coherence cosec is periodic by Def2, Lm6; cluster sec -> periodic ; coherence sec is periodic by Def2, Lm7; end; Lm8: for k being Nat holds sec is (2 * PI) * (k + 1) -periodic proof let k be Nat; ::_thesis: 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; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: sec is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1] sec is (2 * PI) * ((k + 1) + 1) -periodic proof for x being real number 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 number ; ::_thesis: ( 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 ; ::_thesis: ( 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; then A6: x + ((2 * PI) * ((k + 1) + 1)) in (dom cos) \ (cos " {0}) by XBOOLE_0:def_5; cos . (x - ((2 * PI) * ((k + 1) + 1))) = cos . ((x - ((2 * PI) * ((k + 1) + 1))) + (2 * PI)) by Lm3, Th1, SIN_COS:24; 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; 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; ::_thesis: verum end; hence sec is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence sec is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:23 for i being non zero Integer holds sec is (2 * PI) * i -periodic proof let i be non zero Integer; ::_thesis: sec is (2 * PI) * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: sec is (2 * PI) * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence sec is (2 * PI) * i -periodic by Lm8; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: sec is (2 * PI) * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; sec is (2 * PI) * (m + 1) -periodic by Lm8; then sec is - ((2 * PI) * (m + 1)) -periodic by Th14; hence sec is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm9: for k being Nat holds cosec is (2 * PI) * (k + 1) -periodic proof let k be Nat; ::_thesis: cosec is (2 * PI) * (k + 1) -periodic defpred S1[ Nat] means cosec is (2 * PI) * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm6; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: cosec is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1] cosec is (2 * PI) * ((k + 1) + 1) -periodic proof for x being real number st x in dom cosec holds ( x + ((2 * PI) * ((k + 1) + 1)) in dom cosec & x - ((2 * PI) * ((k + 1) + 1)) in dom cosec & cosec . x = cosec . (x + ((2 * PI) * ((k + 1) + 1))) ) proof let x be real number ; ::_thesis: ( x in dom cosec implies ( x + ((2 * PI) * ((k + 1) + 1)) in dom cosec & x - ((2 * PI) * ((k + 1) + 1)) in dom cosec & cosec . x = cosec . (x + ((2 * PI) * ((k + 1) + 1))) ) ) assume x in dom cosec ; ::_thesis: ( x + ((2 * PI) * ((k + 1) + 1)) in dom cosec & x - ((2 * PI) * ((k + 1) + 1)) in dom cosec & cosec . x = cosec . (x + ((2 * PI) * ((k + 1) + 1))) ) then A4: ( x + ((2 * PI) * (k + 1)) in dom cosec & x - ((2 * PI) * (k + 1)) in dom cosec & cosec . x = cosec . (x + ((2 * PI) * (k + 1))) ) by A3, Th1; then ( x + ((2 * PI) * (k + 1)) in (dom sin) \ (sin " {0}) & x - ((2 * PI) * (k + 1)) in (dom sin) \ (sin " {0}) ) by RFUNCT_1:def_2; then ( x + ((2 * PI) * (k + 1)) in dom sin & not x + ((2 * PI) * (k + 1)) in sin " {0} & x - ((2 * PI) * (k + 1)) in dom sin & not x - ((2 * PI) * (k + 1)) in sin " {0} ) by XBOOLE_0:def_5; then A5: ( not sin . (x + ((2 * PI) * (k + 1))) in {0} & not sin . (x - ((2 * PI) * (k + 1))) in {0} ) by FUNCT_1:def_7; then sin . (x + ((2 * PI) * (k + 1))) <> 0 by TARSKI:def_1; then sin . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) <> 0 by SIN_COS:78; then not sin . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) in {0} by TARSKI:def_1; then ( (x + ((2 * PI) * (k + 1))) + (2 * PI) in dom sin & not (x + ((2 * PI) * (k + 1))) + (2 * PI) in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24; then A6: x + ((2 * PI) * ((k + 1) + 1)) in (dom sin) \ (sin " {0}) by XBOOLE_0:def_5; sin . (x - ((2 * PI) * ((k + 1) + 1))) = sin . ((x - ((2 * PI) * ((k + 1) + 1))) + (2 * PI)) by Lm2, Th1, SIN_COS:24; then ( x - ((2 * PI) * ((k + 1) + 1)) in dom sin & not x - ((2 * PI) * ((k + 1) + 1)) in sin " {0} ) by A5, FUNCT_1:def_7, SIN_COS:24; then A7: x - ((2 * PI) * ((k + 1) + 1)) in (dom sin) \ (sin " {0}) by XBOOLE_0:def_5; then ( x + ((2 * PI) * ((k + 1) + 1)) in dom cosec & x - ((2 * PI) * ((k + 1) + 1)) in dom cosec ) by A6, RFUNCT_1:def_2; then cosec . (x + ((2 * PI) * ((k + 1) + 1))) = (sin . ((x + ((2 * PI) * (k + 1))) + (2 * PI))) " by RFUNCT_1:def_2 .= (sin . (x + ((2 * PI) * (k + 1)))) " by SIN_COS:78 .= cosec . x by A4, RFUNCT_1:def_2 ; hence ( x + ((2 * PI) * ((k + 1) + 1)) in dom cosec & x - ((2 * PI) * ((k + 1) + 1)) in dom cosec & cosec . x = cosec . (x + ((2 * PI) * ((k + 1) + 1))) ) by A6, A7, RFUNCT_1:def_2; ::_thesis: verum end; hence cosec is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence cosec is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:24 for i being non zero Integer holds cosec is (2 * PI) * i -periodic proof let i be non zero Integer; ::_thesis: cosec is (2 * PI) * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: cosec is (2 * PI) * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence cosec is (2 * PI) * i -periodic by Lm9; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: cosec is (2 * PI) * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; cosec is (2 * PI) * (m + 1) -periodic by Lm9; then cosec is - ((2 * PI) * (m + 1)) -periodic by Th14; hence cosec is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm10: tan is PI -periodic proof for x being real number st x in dom tan holds ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI) ) proof let x be real number ; ::_thesis: ( x in dom tan implies ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI) ) ) assume A1: x in dom tan ; ::_thesis: ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI) ) then x in (dom sin) /\ ((dom cos) \ (cos " {0})) by RFUNCT_1:def_1; then ( x in dom sin & x in (dom cos) \ (cos " {0}) ) by XBOOLE_0:def_4; then ( x in dom sin & x in dom cos & not x in cos " {0} ) by XBOOLE_0:def_5; then not cos . x in {0} by FUNCT_1:def_7; then A2: cos . x <> 0 by TARSKI:def_1; A3: cos . (x + PI) = - (cos . x) by SIN_COS:78; then not cos . (x + PI) in {0} by A2, TARSKI:def_1; then ( x + PI in dom sin & x + PI in dom cos & not x + PI in cos " {0} ) by FUNCT_1:def_7, SIN_COS:24; then ( x + PI in dom sin & x + PI in (dom cos) \ (cos " {0}) ) by XBOOLE_0:def_5; then A4: x + PI in (dom sin) /\ ((dom cos) \ (cos " {0})) by XBOOLE_0:def_4; cos . (x - PI) = cos . ((x - PI) + (2 * PI)) by SIN_COS:78 .= cos . (x + PI) ; then not cos . (x - PI) in {0} by A2, A3, TARSKI:def_1; then ( x - PI in dom sin & x - PI in dom cos & not x - PI in cos " {0} ) by FUNCT_1:def_7, SIN_COS:24; then ( x - PI in dom sin & x - PI in (dom cos) \ (cos " {0}) ) by XBOOLE_0:def_5; then A5: x - PI in (dom sin) /\ ((dom cos) \ (cos " {0})) by XBOOLE_0:def_4; then ( x + PI in dom tan & x - PI in dom tan ) by A4, RFUNCT_1:def_1; then tan . (x + PI) = (sin . (x + PI)) / (cos . (x + PI)) by RFUNCT_1:def_1 .= (- (sin . x)) / (cos . (x + PI)) by SIN_COS:78 .= (- (sin . x)) / (- (cos . x)) by SIN_COS:78 .= (sin . x) / (cos . x) by XCMPLX_1:191 .= tan . x by A1, RFUNCT_1:def_1 ; hence ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI) ) by A4, A5, RFUNCT_1:def_1; ::_thesis: verum end; hence tan is PI -periodic by Th1; ::_thesis: verum end; Lm11: cot is PI -periodic proof for x being real number st x in dom cot holds ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) ) proof let x be real number ; ::_thesis: ( x in dom cot implies ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) ) ) assume A1: x in dom cot ; ::_thesis: ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) ) then x in (dom cos) /\ ((dom sin) \ (sin " {0})) by RFUNCT_1:def_1; then ( x in dom cos & x in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_4; then ( x in dom cos & x in dom sin & not x in sin " {0} ) by XBOOLE_0:def_5; then not sin . x in {0} by FUNCT_1:def_7; then A2: sin . x <> 0 by TARSKI:def_1; A3: sin . (x + PI) = - (sin . x) by SIN_COS:78; then not sin . (x + PI) in {0} by A2, TARSKI:def_1; then ( x + PI in dom cos & x + PI in dom sin & not x + PI in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24; then ( x + PI in dom cos & x + PI in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_5; then A4: x + PI in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def_4; sin . (x - PI) = sin . ((x - PI) + (2 * PI)) by SIN_COS:78 .= sin . (x + PI) ; then not sin . (x - PI) in {0} by A2, A3, TARSKI:def_1; then ( x - PI in dom cos & x - PI in dom sin & not x - PI in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24; then ( x - PI in dom cos & x - PI in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_5; then A5: x - PI in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def_4; then ( x + PI in dom cot & x - PI in dom cot ) by A4, RFUNCT_1:def_1; then cot . (x + PI) = (cos . (x + PI)) / (sin . (x + PI)) by RFUNCT_1:def_1 .= (- (cos . x)) / (sin . (x + PI)) by SIN_COS:78 .= (- (cos . x)) / (- (sin . x)) by SIN_COS:78 .= (cos . x) / (sin . x) by XCMPLX_1:191 .= cot . x by A1, RFUNCT_1:def_1 ; hence ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) ) by A4, A5, RFUNCT_1:def_1; ::_thesis: verum end; hence cot is PI -periodic by Th1; ::_thesis: verum end; registration cluster tan -> periodic ; coherence tan is periodic by Def2, Lm10; cluster cot -> periodic ; coherence cot is periodic by Def2, Lm11; end; Lm12: for k being Nat holds tan is PI * (k + 1) -periodic proof let k be Nat; ::_thesis: tan is PI * (k + 1) -periodic defpred S1[ Nat] means tan is PI * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm10; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: tan is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1] tan is PI * ((k + 1) + 1) -periodic proof for x being real number st x in dom tan holds ( x + (PI * ((k + 1) + 1)) in dom tan & x - (PI * ((k + 1) + 1)) in dom tan & tan . x = tan . (x + (PI * ((k + 1) + 1))) ) proof let x be real number ; ::_thesis: ( x in dom tan implies ( x + (PI * ((k + 1) + 1)) in dom tan & x - (PI * ((k + 1) + 1)) in dom tan & tan . x = tan . (x + (PI * ((k + 1) + 1))) ) ) assume x in dom tan ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom tan & x - (PI * ((k + 1) + 1)) in dom tan & tan . x = tan . (x + (PI * ((k + 1) + 1))) ) then A4: ( x + (PI * (k + 1)) in dom tan & x - (PI * (k + 1)) in dom tan & tan . x = tan . (x + (PI * (k + 1))) ) by A3, Th1; then ( x + (PI * (k + 1)) in (dom sin) /\ ((dom cos) \ (cos " {0})) & x - (PI * (k + 1)) in (dom sin) /\ ((dom cos) \ (cos " {0})) ) by RFUNCT_1:def_1; then ( x + (PI * (k + 1)) in dom sin & x + (PI * (k + 1)) in (dom cos) \ (cos " {0}) & x - (PI * (k + 1)) in dom sin & x - (PI * (k + 1)) in (dom cos) \ (cos " {0}) ) by XBOOLE_0:def_4; then ( x + (PI * (k + 1)) in dom sin & x + (PI * (k + 1)) in dom cos & not x + (PI * (k + 1)) in cos " {0} & x - (PI * (k + 1)) in dom sin & x - (PI * (k + 1)) in dom cos & not x - (PI * (k + 1)) in cos " {0} ) by XBOOLE_0:def_5; then ( not cos . (x + (PI * (k + 1))) in {0} & not cos . (x - (PI * (k + 1))) in {0} ) by FUNCT_1:def_7; then A5: ( cos . (x + (PI * (k + 1))) <> 0 & cos . (x - (PI * (k + 1))) <> 0 ) by TARSKI:def_1; cos . ((x + (PI * (k + 1))) + PI) = - (cos . (x + (PI * (k + 1)))) by SIN_COS:78; then not cos . ((x + (PI * (k + 1))) + PI) in {0} by A5, TARSKI:def_1; then ( (x + (PI * (k + 1))) + PI in dom sin & (x + (PI * (k + 1))) + PI in dom cos & not (x + (PI * (k + 1))) + PI in cos " {0} ) by FUNCT_1:def_7, SIN_COS:24; then ( (x + (PI * (k + 1))) + PI in dom sin & (x + (PI * (k + 1))) + PI in (dom cos) \ (cos " {0}) ) by XBOOLE_0:def_5; then A6: (x + (PI * (k + 1))) + PI in (dom sin) /\ ((dom cos) \ (cos " {0})) by XBOOLE_0:def_4; cos . ((x - (PI * ((k + 1) + 1))) + PI) = - (cos . (x - (PI * ((k + 1) + 1)))) by SIN_COS:78; then cos . (x - (PI * ((k + 1) + 1))) = - (cos . (x - (PI * (k + 1)))) ; then not cos . (x - (PI * ((k + 1) + 1))) in {0} by A5, TARSKI:def_1; then ( x - (PI * ((k + 1) + 1)) in dom sin & x - (PI * ((k + 1) + 1)) in dom cos & not x - (PI * ((k + 1) + 1)) in cos " {0} ) by FUNCT_1:def_7, SIN_COS:24; then ( x - (PI * ((k + 1) + 1)) in dom sin & x - (PI * ((k + 1) + 1)) in (dom cos) \ (cos " {0}) ) by XBOOLE_0:def_5; then A7: x - (PI * ((k + 1) + 1)) in (dom sin) /\ ((dom cos) \ (cos " {0})) by XBOOLE_0:def_4; then ( x + (PI * ((k + 1) + 1)) in dom tan & x - (PI * ((k + 1) + 1)) in dom tan ) by A6, RFUNCT_1:def_1; then tan . (x + (PI * ((k + 1) + 1))) = (sin . ((x + (PI * (k + 1))) + PI)) / (cos . ((x + (PI * (k + 1))) + PI)) by RFUNCT_1:def_1 .= (- (sin . (x + (PI * (k + 1))))) / (cos . ((x + (PI * (k + 1))) + PI)) by SIN_COS:78 .= (- (sin . (x + (PI * (k + 1))))) / (- (cos . (x + (PI * (k + 1))))) by SIN_COS:78 .= (sin . (x + (PI * (k + 1)))) / (cos . (x + (PI * (k + 1)))) by XCMPLX_1:191 .= tan . x by A4, RFUNCT_1:def_1 ; hence ( x + (PI * ((k + 1) + 1)) in dom tan & x - (PI * ((k + 1) + 1)) in dom tan & tan . x = tan . (x + (PI * ((k + 1) + 1))) ) by A7, A6, RFUNCT_1:def_1; ::_thesis: verum end; hence tan is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence tan is PI * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:25 for i being non zero Integer holds tan is PI * i -periodic proof let i be non zero Integer; ::_thesis: tan is PI * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: tan is PI * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence tan is PI * i -periodic by Lm12; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: tan is PI * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; tan is PI * (m + 1) -periodic by Lm12; then tan is - (PI * (m + 1)) -periodic by Th14; hence tan is PI * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm13: for k being Nat holds cot is PI * (k + 1) -periodic proof let k be Nat; ::_thesis: cot is PI * (k + 1) -periodic defpred S1[ Nat] means cot is PI * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm11; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: cot is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1] cot is PI * ((k + 1) + 1) -periodic proof for x being real number st x in dom cot holds ( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot & cot . x = cot . (x + (PI * ((k + 1) + 1))) ) proof let x be real number ; ::_thesis: ( x in dom cot implies ( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot & cot . x = cot . (x + (PI * ((k + 1) + 1))) ) ) assume x in dom cot ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot & cot . x = cot . (x + (PI * ((k + 1) + 1))) ) then A4: ( x + (PI * (k + 1)) in dom cot & x - (PI * (k + 1)) in dom cot & cot . x = cot . (x + (PI * (k + 1))) ) by A3, Th1; then ( x + (PI * (k + 1)) in (dom cos) /\ ((dom sin) \ (sin " {0})) & x - (PI * (k + 1)) in (dom cos) /\ ((dom sin) \ (sin " {0})) ) by RFUNCT_1:def_1; then ( x + (PI * (k + 1)) in dom cos & x + (PI * (k + 1)) in (dom sin) \ (sin " {0}) & x - (PI * (k + 1)) in dom cos & x - (PI * (k + 1)) in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_4; then ( x + (PI * (k + 1)) in dom cos & x + (PI * (k + 1)) in dom sin & not x + (PI * (k + 1)) in sin " {0} & x - (PI * (k + 1)) in dom cos & x - (PI * (k + 1)) in dom sin & not x - (PI * (k + 1)) in sin " {0} ) by XBOOLE_0:def_5; then ( not sin . (x + (PI * (k + 1))) in {0} & not sin . (x - (PI * (k + 1))) in {0} ) by FUNCT_1:def_7; then A5: ( sin . (x + (PI * (k + 1))) <> 0 & sin . (x - (PI * (k + 1))) <> 0 ) by TARSKI:def_1; sin . ((x + (PI * (k + 1))) + PI) = - (sin . (x + (PI * (k + 1)))) by SIN_COS:78; then not sin . ((x + (PI * (k + 1))) + PI) in {0} by A5, TARSKI:def_1; then ( (x + (PI * (k + 1))) + PI in dom cos & (x + (PI * (k + 1))) + PI in dom sin & not (x + (PI * (k + 1))) + PI in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24; then ( (x + (PI * (k + 1))) + PI in dom cos & (x + (PI * (k + 1))) + PI in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_5; then A6: (x + (PI * (k + 1))) + PI in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def_4; sin . ((x - (PI * ((k + 1) + 1))) + PI) = - (sin . (x - (PI * ((k + 1) + 1)))) by SIN_COS:78; then sin . (x - (PI * ((k + 1) + 1))) = - (sin . (x - (PI * (k + 1)))) ; then not sin . (x - (PI * ((k + 1) + 1))) in {0} by A5, TARSKI:def_1; then ( x - (PI * ((k + 1) + 1)) in dom cos & x - (PI * ((k + 1) + 1)) in dom sin & not x - (PI * ((k + 1) + 1)) in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24; then ( x - (PI * ((k + 1) + 1)) in dom cos & x - (PI * ((k + 1) + 1)) in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_5; then A7: x - (PI * ((k + 1) + 1)) in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def_4; then ( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot ) by A6, RFUNCT_1:def_1; then cot . (x + (PI * ((k + 1) + 1))) = (cos . ((x + (PI * (k + 1))) + PI)) / (sin . ((x + (PI * (k + 1))) + PI)) by RFUNCT_1:def_1 .= (- (cos . (x + (PI * (k + 1))))) / (sin . ((x + (PI * (k + 1))) + PI)) by SIN_COS:78 .= (- (cos . (x + (PI * (k + 1))))) / (- (sin . (x + (PI * (k + 1))))) by SIN_COS:78 .= (cos . (x + (PI * (k + 1)))) / (sin . (x + (PI * (k + 1)))) by XCMPLX_1:191 .= cot . x by A4, RFUNCT_1:def_1 ; hence ( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot & cot . x = cot . (x + (PI * ((k + 1) + 1))) ) by A7, A6, RFUNCT_1:def_1; ::_thesis: verum end; hence cot is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence cot is PI * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:26 for i being non zero Integer holds cot is PI * i -periodic proof let i be non zero Integer; ::_thesis: cot is PI * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: cot is PI * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence cot is PI * i -periodic by Lm13; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: cot is PI * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; cot is PI * (m + 1) -periodic by Lm13; then cot is - (PI * (m + 1)) -periodic by Th14; hence cot is PI * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm14: |.sin.| is PI -periodic proof for x being real number st x in dom |.sin.| holds ( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) ) proof let x be real number ; ::_thesis: ( x in dom |.sin.| implies ( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) ) ) assume A1: x in dom |.sin.| ; ::_thesis: ( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) ) A2: ( x + PI in dom sin & x - PI in dom sin ) by SIN_COS:24; then ( x + PI in dom |.sin.| & x - PI in dom |.sin.| ) by VALUED_1:def_11; then |.sin.| . (x + PI) = |.(sin (x + PI)).| by VALUED_1:def_11 .= |.(- (sin . x)).| by SIN_COS:78 .= |.(sin . x).| by COMPLEX1:52 .= |.sin.| . x by A1, VALUED_1:def_11 ; hence ( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) ) by A2, VALUED_1:def_11; ::_thesis: verum end; hence |.sin.| is PI -periodic by Th1; ::_thesis: verum end; Lm15: |.cos.| is PI -periodic proof for x being real number st x in dom |.cos.| holds ( x + PI in dom |.cos.| & x - PI in dom |.cos.| & |.cos.| . x = |.cos.| . (x + PI) ) proof let x be real number ; ::_thesis: ( x in dom |.cos.| implies ( x + PI in dom |.cos.| & x - PI in dom |.cos.| & |.cos.| . x = |.cos.| . (x + PI) ) ) assume A1: x in dom |.cos.| ; ::_thesis: ( x + PI in dom |.cos.| & x - PI in dom |.cos.| & |.cos.| . x = |.cos.| . (x + PI) ) A2: ( x + PI in dom cos & x - PI in dom cos ) by SIN_COS:24; then ( x + PI in dom |.cos.| & x - PI in dom |.cos.| ) by VALUED_1:def_11; then |.cos.| . (x + PI) = |.(cos (x + PI)).| by VALUED_1:def_11 .= |.(- (cos . x)).| by SIN_COS:78 .= |.(cos . x).| by COMPLEX1:52 .= |.cos.| . x by A1, VALUED_1:def_11 ; hence ( x + PI in dom |.cos.| & x - PI in dom |.cos.| & |.cos.| . x = |.cos.| . (x + PI) ) by A2, VALUED_1:def_11; ::_thesis: verum end; hence |.cos.| is PI -periodic by Th1; ::_thesis: verum end; Lm16: for k being Nat holds |.sin.| is PI * (k + 1) -periodic proof let k be Nat; ::_thesis: |.sin.| is PI * (k + 1) -periodic defpred S1[ Nat] means |.sin.| is PI * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm14; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: |.sin.| is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1] |.sin.| is PI * ((k + 1) + 1) -periodic proof for x being real number st x in dom |.sin.| holds ( x + (PI * ((k + 1) + 1)) in dom |.sin.| & x - (PI * ((k + 1) + 1)) in dom |.sin.| & |.sin.| . x = |.sin.| . (x + (PI * ((k + 1) + 1))) ) proof let x be real number ; ::_thesis: ( x in dom |.sin.| implies ( x + (PI * ((k + 1) + 1)) in dom |.sin.| & x - (PI * ((k + 1) + 1)) in dom |.sin.| & |.sin.| . x = |.sin.| . (x + (PI * ((k + 1) + 1))) ) ) assume A4: x in dom |.sin.| ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom |.sin.| & x - (PI * ((k + 1) + 1)) in dom |.sin.| & |.sin.| . x = |.sin.| . (x + (PI * ((k + 1) + 1))) ) then A5: ( x + (PI * (k + 1)) in dom |.sin.| & x - (PI * (k + 1)) in dom |.sin.| ) by A3, Th1; A6: ( x + (PI * ((k + 1) + 1)) in dom sin & x - (PI * ((k + 1) + 1)) in dom sin ) by SIN_COS:24; then ( x + (PI * ((k + 1) + 1)) in dom |.sin.| & x - (PI * ((k + 1) + 1)) in dom |.sin.| ) by VALUED_1:def_11; then |.sin.| . (x + (PI * ((k + 1) + 1))) = |.(sin . ((x + (PI * (k + 1))) + PI)).| by VALUED_1:def_11 .= |.(- (sin . (x + (PI * (k + 1))))).| by SIN_COS:78 .= |.(sin . (x + (PI * (k + 1)))).| by COMPLEX1:52 .= |.sin.| . (x + (PI * (k + 1))) by A5, VALUED_1:def_11 ; hence ( x + (PI * ((k + 1) + 1)) in dom |.sin.| & x - (PI * ((k + 1) + 1)) in dom |.sin.| & |.sin.| . x = |.sin.| . (x + (PI * ((k + 1) + 1))) ) by A3, Th1, A4, A6, VALUED_1:def_11; ::_thesis: verum end; hence |.sin.| is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence |.sin.| is PI * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:27 for i being non zero Integer holds |.sin.| is PI * i -periodic proof let i be non zero Integer; ::_thesis: |.sin.| is PI * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: |.sin.| is PI * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence |.sin.| is PI * i -periodic by Lm16; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: |.sin.| is PI * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; |.sin.| is PI * (m + 1) -periodic by Lm16; then |.sin.| is - (PI * (m + 1)) -periodic by Th14; hence |.sin.| is PI * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm17: for k being Nat holds |.cos.| is PI * (k + 1) -periodic proof let k be Nat; ::_thesis: |.cos.| is PI * (k + 1) -periodic defpred S1[ Nat] means |.cos.| is PI * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm15; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: |.cos.| is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1] |.cos.| is PI * ((k + 1) + 1) -periodic proof for x being real number st x in dom |.cos.| holds ( x + (PI * ((k + 1) + 1)) in dom |.cos.| & x - (PI * ((k + 1) + 1)) in dom |.cos.| & |.cos.| . x = |.cos.| . (x + (PI * ((k + 1) + 1))) ) proof let x be real number ; ::_thesis: ( x in dom |.cos.| implies ( x + (PI * ((k + 1) + 1)) in dom |.cos.| & x - (PI * ((k + 1) + 1)) in dom |.cos.| & |.cos.| . x = |.cos.| . (x + (PI * ((k + 1) + 1))) ) ) assume A4: x in dom |.cos.| ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom |.cos.| & x - (PI * ((k + 1) + 1)) in dom |.cos.| & |.cos.| . x = |.cos.| . (x + (PI * ((k + 1) + 1))) ) then A5: ( x + (PI * (k + 1)) in dom |.cos.| & x - (PI * (k + 1)) in dom |.cos.| ) by A3, Th1; A6: ( x + (PI * ((k + 1) + 1)) in dom cos & x - (PI * ((k + 1) + 1)) in dom cos ) by SIN_COS:24; then ( x + (PI * ((k + 1) + 1)) in dom |.cos.| & x - (PI * ((k + 1) + 1)) in dom |.cos.| ) by VALUED_1:def_11; then |.cos.| . (x + (PI * ((k + 1) + 1))) = |.(cos . ((x + (PI * (k + 1))) + PI)).| by VALUED_1:def_11 .= |.(- (cos . (x + (PI * (k + 1))))).| by SIN_COS:78 .= |.(cos . (x + (PI * (k + 1)))).| by COMPLEX1:52 .= |.cos.| . (x + (PI * (k + 1))) by A5, VALUED_1:def_11 ; hence ( x + (PI * ((k + 1) + 1)) in dom |.cos.| & x - (PI * ((k + 1) + 1)) in dom |.cos.| & |.cos.| . x = |.cos.| . (x + (PI * ((k + 1) + 1))) ) by A3, Th1, A4, A6, VALUED_1:def_11; ::_thesis: verum end; hence |.cos.| is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence |.cos.| is PI * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:28 for i being non zero Integer holds |.cos.| is PI * i -periodic proof let i be non zero Integer; ::_thesis: |.cos.| is PI * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: |.cos.| is PI * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence |.cos.| is PI * i -periodic by Lm17; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: |.cos.| is PI * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; |.cos.| is PI * (m + 1) -periodic by Lm17; then |.cos.| is - (PI * (m + 1)) -periodic by Th14; hence |.cos.| is PI * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm18: |.sin.| + |.cos.| is PI / 2 -periodic proof for x being real number st x in dom (|.sin.| + |.cos.|) holds ( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) ) proof let x be real number ; ::_thesis: ( x in dom (|.sin.| + |.cos.|) implies ( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) ) ) assume A1: x in dom (|.sin.| + |.cos.|) ; ::_thesis: ( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) ) A2: ( dom (|.sin.| + |.cos.|) = REAL & dom |.sin.| = REAL & dom |.cos.| = REAL ) proof A3: dom (|.sin.| + |.cos.|) = (dom |.sin.|) /\ (dom |.cos.|) by VALUED_1:def_1; ( dom |.sin.| = REAL & dom |.cos.| = REAL ) by SIN_COS:24, VALUED_1:def_11; hence ( dom (|.sin.| + |.cos.|) = REAL & dom |.sin.| = REAL & dom |.cos.| = REAL ) by A3; ::_thesis: verum end; then (|.sin.| + |.cos.|) . (x + (PI / 2)) = (|.sin.| . (x + (PI / 2))) + (|.cos.| . (x + (PI / 2))) by VALUED_1:def_1 .= |.(sin . (x + (PI / 2))).| + (|.cos.| . (x + (PI / 2))) by A2, VALUED_1:def_11 .= |.(sin . (x + (PI / 2))).| + |.(cos . (x + (PI / 2))).| by A2, VALUED_1:def_11 .= |.(cos . x).| + |.(cos . (x + (PI / 2))).| by SIN_COS:78 .= |.(cos . x).| + |.(- (sin . x)).| by SIN_COS:78 .= |.(cos . x).| + |.(sin . x).| by COMPLEX1:52 .= (|.cos.| . x) + |.(sin . x).| by A1, A2, VALUED_1:def_11 .= (|.cos.| . x) + (|.sin.| . x) by A1, A2, VALUED_1:def_11 .= (|.sin.| + |.cos.|) . x by A1, VALUED_1:def_1 ; hence ( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) ) by A2; ::_thesis: verum end; hence |.sin.| + |.cos.| is PI / 2 -periodic by Th1; ::_thesis: verum end; Lm19: for k being Nat holds |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic proof let k be Nat; ::_thesis: |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic defpred S1[ Nat] means |.sin.| + |.cos.| is (PI / 2) * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm18; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic ; ::_thesis: S1[k + 1] A4: ( dom (|.sin.| + |.cos.|) = REAL & dom |.sin.| = REAL & dom |.cos.| = REAL ) proof A5: dom (|.sin.| + |.cos.|) = (dom |.sin.|) /\ (dom |.cos.|) by VALUED_1:def_1; ( dom |.sin.| = REAL & dom |.cos.| = REAL ) by SIN_COS:24, VALUED_1:def_11; hence ( dom (|.sin.| + |.cos.|) = REAL & dom |.sin.| = REAL & dom |.cos.| = REAL ) by A5; ::_thesis: verum end; |.sin.| + |.cos.| is (PI / 2) * ((k + 1) + 1) -periodic proof for x being real number st x in dom (|.sin.| + |.cos.|) holds ( x + ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & x - ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + ((PI / 2) * ((k + 1) + 1))) ) proof let x be real number ; ::_thesis: ( x in dom (|.sin.| + |.cos.|) implies ( x + ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & x - ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + ((PI / 2) * ((k + 1) + 1))) ) ) assume A6: x in dom (|.sin.| + |.cos.|) ; ::_thesis: ( x + ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & x - ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + ((PI / 2) * ((k + 1) + 1))) ) (|.sin.| + |.cos.|) . (x + ((PI / 2) * ((k + 1) + 1))) = (|.sin.| . (x + ((PI / 2) * ((k + 1) + 1)))) + (|.cos.| . (x + ((PI / 2) * ((k + 1) + 1)))) by A4, VALUED_1:def_1 .= |.(sin . (x + ((PI / 2) * ((k + 1) + 1)))).| + (|.cos.| . (x + ((PI / 2) * ((k + 1) + 1)))) by A4, VALUED_1:def_11 .= |.(sin . ((x + ((PI / 2) * (k + 1))) + (PI / 2))).| + |.(cos . ((x + ((PI / 2) * (k + 1))) + (PI / 2))).| by A4, VALUED_1:def_11 .= |.(cos . (x + ((PI / 2) * (k + 1)))).| + |.(cos . ((x + ((PI / 2) * (k + 1))) + (PI / 2))).| by SIN_COS:78 .= |.(cos . (x + ((PI / 2) * (k + 1)))).| + |.(- (sin . (x + ((PI / 2) * (k + 1))))).| by SIN_COS:78 .= |.(cos . (x + ((PI / 2) * (k + 1)))).| + |.(sin . (x + ((PI / 2) * (k + 1)))).| by COMPLEX1:52 .= (|.cos.| . (x + ((PI / 2) * (k + 1)))) + |.(sin . (x + ((PI / 2) * (k + 1)))).| by A4, VALUED_1:def_11 .= (|.cos.| . (x + ((PI / 2) * (k + 1)))) + (|.sin.| . (x + ((PI / 2) * (k + 1)))) by A4, VALUED_1:def_11 .= (|.sin.| + |.cos.|) . (x + ((PI / 2) * (k + 1))) by A4, VALUED_1:def_1 ; hence ( x + ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & x - ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + ((PI / 2) * ((k + 1) + 1))) ) by A3, Th1, A4, A6; ::_thesis: verum end; hence |.sin.| + |.cos.| is (PI / 2) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:29 for i being non zero Integer holds |.sin.| + |.cos.| is (PI / 2) * i -periodic proof let i be non zero Integer; ::_thesis: |.sin.| + |.cos.| is (PI / 2) * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: |.sin.| + |.cos.| is (PI / 2) * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence |.sin.| + |.cos.| is (PI / 2) * i -periodic by Lm19; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: |.sin.| + |.cos.| is (PI / 2) * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; |.sin.| + |.cos.| is (PI / 2) * (m + 1) -periodic by Lm19; then |.sin.| + |.cos.| is - ((PI / 2) * (m + 1)) -periodic by Th14; hence |.sin.| + |.cos.| is (PI / 2) * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm20: sin ^2 is PI -periodic proof for x being real number st x in dom (sin ^2) holds ( x + PI in dom (sin ^2) & x - PI in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + PI) ) proof let x be real number ; ::_thesis: ( x in dom (sin ^2) implies ( x + PI in dom (sin ^2) & x - PI in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + PI) ) ) assume x in dom (sin ^2) ; ::_thesis: ( x + PI in dom (sin ^2) & x - PI in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + PI) ) A1: ( x + PI in dom sin & x - PI in dom sin ) by SIN_COS:24; (sin ^2) . (x + PI) = (sin (x + PI)) ^2 by VALUED_1:11 .= (- (sin . x)) ^2 by SIN_COS:78 .= (sin . x) ^2 .= (sin ^2) . x by VALUED_1:11 ; hence ( x + PI in dom (sin ^2) & x - PI in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + PI) ) by A1, VALUED_1:11; ::_thesis: verum end; hence sin ^2 is PI -periodic by Th1; ::_thesis: verum end; Lm21: cos ^2 is PI -periodic proof for x being real number st x in dom (cos ^2) holds ( x + PI in dom (cos ^2) & x - PI in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + PI) ) proof let x be real number ; ::_thesis: ( x in dom (cos ^2) implies ( x + PI in dom (cos ^2) & x - PI in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + PI) ) ) assume x in dom (cos ^2) ; ::_thesis: ( x + PI in dom (cos ^2) & x - PI in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + PI) ) A1: ( x + PI in dom cos & x - PI in dom cos ) by SIN_COS:24; (cos ^2) . (x + PI) = (cos (x + PI)) ^2 by VALUED_1:11 .= (- (cos . x)) ^2 by SIN_COS:78 .= (cos . x) ^2 .= (cos ^2) . x by VALUED_1:11 ; hence ( x + PI in dom (cos ^2) & x - PI in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + PI) ) by A1, VALUED_1:11; ::_thesis: verum end; hence cos ^2 is PI -periodic by Th1; ::_thesis: verum end; Lm22: for k being Nat holds sin ^2 is PI * (k + 1) -periodic proof let k be Nat; ::_thesis: sin ^2 is PI * (k + 1) -periodic defpred S1[ Nat] means sin ^2 is PI * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm20; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: sin ^2 is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1] sin ^2 is PI * ((k + 1) + 1) -periodic proof for x being real number 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))) ) proof let x be real number ; ::_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; (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, Th1, A4, A5, VALUED_1:11; ::_thesis: verum end; hence sin ^2 is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence sin ^2 is PI * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:30 for i being non zero Integer holds sin ^2 is PI * i -periodic proof let i be non zero Integer; ::_thesis: sin ^2 is PI * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: sin ^2 is PI * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence sin ^2 is PI * i -periodic by Lm22; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: sin ^2 is PI * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; sin ^2 is PI * (m + 1) -periodic by Lm22; then sin ^2 is - (PI * (m + 1)) -periodic by Th14; hence sin ^2 is PI * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm23: for k being Nat holds cos ^2 is PI * (k + 1) -periodic proof let k be Nat; ::_thesis: cos ^2 is PI * (k + 1) -periodic defpred S1[ Nat] means cos ^2 is PI * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm21; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: cos ^2 is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1] cos ^2 is PI * ((k + 1) + 1) -periodic proof for x being real number st x in dom (cos ^2) holds ( x + (PI * ((k + 1) + 1)) in dom (cos ^2) & x - (PI * ((k + 1) + 1)) in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + (PI * ((k + 1) + 1))) ) proof let x be real number ; ::_thesis: ( x in dom (cos ^2) implies ( x + (PI * ((k + 1) + 1)) in dom (cos ^2) & x - (PI * ((k + 1) + 1)) in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + (PI * ((k + 1) + 1))) ) ) assume A4: x in dom (cos ^2) ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom (cos ^2) & x - (PI * ((k + 1) + 1)) in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + (PI * ((k + 1) + 1))) ) A5: ( x + (PI * ((k + 1) + 1)) in dom cos & x - (PI * ((k + 1) + 1)) in dom cos ) by SIN_COS:24; (cos ^2) . (x + (PI * ((k + 1) + 1))) = (cos . ((x + (PI * (k + 1))) + PI)) ^2 by VALUED_1:11 .= (- (cos . (x + (PI * (k + 1))))) ^2 by SIN_COS:78 .= (cos . (x + (PI * (k + 1)))) ^2 .= (cos ^2) . (x + (PI * (k + 1))) by VALUED_1:11 ; hence ( x + (PI * ((k + 1) + 1)) in dom (cos ^2) & x - (PI * ((k + 1) + 1)) in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + (PI * ((k + 1) + 1))) ) by A3, Th1, A4, A5, VALUED_1:11; ::_thesis: verum end; hence cos ^2 is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence cos ^2 is PI * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:31 for i being non zero Integer holds cos ^2 is PI * i -periodic proof let i be non zero Integer; ::_thesis: cos ^2 is PI * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: cos ^2 is PI * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence cos ^2 is PI * i -periodic by Lm23; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: cos ^2 is PI * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; cos ^2 is PI * (m + 1) -periodic by Lm23; then cos ^2 is - (PI * (m + 1)) -periodic by Th14; hence cos ^2 is PI * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm24: sin (#) cos is PI -periodic proof for x being real number st x in dom (sin (#) cos) holds ( x + PI in dom (sin (#) cos) & x - PI in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + PI) ) proof let x be real number ; ::_thesis: ( x in dom (sin (#) cos) implies ( x + PI in dom (sin (#) cos) & x - PI in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + PI) ) ) assume A1: x in dom (sin (#) cos) ; ::_thesis: ( x + PI in dom (sin (#) cos) & x - PI in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + PI) ) A2: ( x + PI in (dom sin) /\ (dom cos) & x - PI in (dom sin) /\ (dom cos) ) by SIN_COS:24; then ( x + PI in dom (sin (#) cos) & x - PI in dom (sin (#) cos) ) by VALUED_1:def_4; then (sin (#) cos) . (x + PI) = (sin . (x + PI)) * (cos . (x + PI)) by VALUED_1:def_4 .= (- (sin . x)) * (cos . (x + PI)) by SIN_COS:78 .= (- (sin . x)) * (- (cos . x)) by SIN_COS:78 .= (sin . x) * (cos . x) .= (sin (#) cos) . x by A1, VALUED_1:def_4 ; hence ( x + PI in dom (sin (#) cos) & x - PI in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + PI) ) by A2, VALUED_1:def_4; ::_thesis: verum end; hence sin (#) cos is PI -periodic by Th1; ::_thesis: verum end; Lm25: for k being Nat holds sin (#) cos is PI * (k + 1) -periodic proof let k be Nat; ::_thesis: sin (#) cos is PI * (k + 1) -periodic defpred S1[ Nat] means sin (#) cos is PI * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm24; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: sin (#) cos is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1] sin (#) cos is PI * ((k + 1) + 1) -periodic proof for x being real number st x in dom (sin (#) cos) holds ( x + (PI * ((k + 1) + 1)) in dom (sin (#) cos) & x - (PI * ((k + 1) + 1)) in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + (PI * ((k + 1) + 1))) ) proof let x be real number ; ::_thesis: ( x in dom (sin (#) cos) implies ( x + (PI * ((k + 1) + 1)) in dom (sin (#) cos) & x - (PI * ((k + 1) + 1)) in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + (PI * ((k + 1) + 1))) ) ) assume A4: x in dom (sin (#) cos) ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom (sin (#) cos) & x - (PI * ((k + 1) + 1)) in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + (PI * ((k + 1) + 1))) ) then A5: ( x + (PI * (k + 1)) in dom (sin (#) cos) & x - (PI * (k + 1)) in dom (sin (#) cos) ) by A3, Th1; A6: ( x + (PI * ((k + 1) + 1)) in (dom cos) /\ (dom sin) & x - (PI * ((k + 1) + 1)) in (dom cos) /\ (dom sin) ) by SIN_COS:24; then ( x + (PI * ((k + 1) + 1)) in dom (sin (#) cos) & x - (PI * ((k + 1) + 1)) in dom (sin (#) cos) ) by VALUED_1:def_4; then (sin (#) cos) . (x + (PI * ((k + 1) + 1))) = (sin . ((x + (PI * (k + 1))) + PI)) * (cos . ((x + (PI * (k + 1))) + PI)) by VALUED_1:def_4 .= (- (sin . (x + (PI * (k + 1))))) * (cos . ((x + (PI * (k + 1))) + PI)) by SIN_COS:78 .= (- (sin . (x + (PI * (k + 1))))) * (- (cos . (x + (PI * (k + 1))))) by SIN_COS:78 .= (sin . (x + (PI * (k + 1)))) * (cos . (x + (PI * (k + 1)))) .= (sin (#) cos) . (x + (PI * (k + 1))) by A5, VALUED_1:def_4 ; hence ( x + (PI * ((k + 1) + 1)) in dom (sin (#) cos) & x - (PI * ((k + 1) + 1)) in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + (PI * ((k + 1) + 1))) ) by A3, Th1, A4, A6, VALUED_1:def_4; ::_thesis: verum end; hence sin (#) cos is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence sin (#) cos is PI * (k + 1) -periodic ; ::_thesis: verum end; theorem :: FUNCT_9:32 for i being non zero Integer holds sin (#) cos is PI * i -periodic proof let i be non zero Integer; ::_thesis: sin (#) cos is PI * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: sin (#) cos is PI * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence sin (#) cos is PI * i -periodic by Lm25; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: sin (#) cos is PI * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; sin (#) cos is PI * (m + 1) -periodic by Lm25; then sin (#) cos is - (PI * (m + 1)) -periodic by Th14; hence sin (#) cos is PI * i -periodic by A2, A3; ::_thesis: verum end; end; end; Lm26: for b, a being real number holds b + (a (#) sin) is 2 * PI -periodic proof let b, a be real number ; ::_thesis: b + (a (#) sin) is 2 * PI -periodic for x being real number st x in dom (b + (a (#) sin)) holds ( x + (2 * PI) in dom (b + (a (#) sin)) & x - (2 * PI) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + (2 * PI)) ) proof let x be real number ; ::_thesis: ( x in dom (b + (a (#) sin)) implies ( x + (2 * PI) in dom (b + (a (#) sin)) & x - (2 * PI) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + (2 * PI)) ) ) assume x in dom (b + (a (#) sin)) ; ::_thesis: ( x + (2 * PI) in dom (b + (a (#) sin)) & x - (2 * PI) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + (2 * PI)) ) x in REAL by XREAL_0:def_1; then A1: x in dom (a (#) sin) by SIN_COS:24, VALUED_1:def_5; then A2: ( x in dom (b + (a (#) sin)) & x in dom (b + (a (#) sin)) ) by VALUED_1:def_2; ( x + (2 * PI) in dom sin & x - (2 * PI) in dom sin ) by SIN_COS:24; then A3: ( x + (2 * PI) in dom (a (#) sin) & x - (2 * PI) in dom (a (#) sin) ) by VALUED_1:def_5; then ( x + (2 * PI) in dom (b + (a (#) sin)) & x - (2 * PI) in dom (b + (a (#) sin)) ) by VALUED_1:def_2; then (b + (a (#) sin)) . (x + (2 * PI)) = b + ((a (#) sin) . (x + (2 * PI))) by VALUED_1:def_2 .= b + (a * (sin . (x + (2 * PI)))) by A3, VALUED_1:def_5 .= b + (a * (sin . x)) by SIN_COS:78 .= b + ((a (#) sin) . x) by A1, VALUED_1:def_5 .= (b + (a (#) sin)) . x by A2, VALUED_1:def_2 ; hence ( x + (2 * PI) in dom (b + (a (#) sin)) & x - (2 * PI) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + (2 * PI)) ) by A3, VALUED_1:def_2; ::_thesis: verum end; hence b + (a (#) sin) is 2 * PI -periodic by Th1; ::_thesis: verum end; Lm27: for b, a being real number holds b + (a (#) cos) is 2 * PI -periodic proof let b, a be real number ; ::_thesis: b + (a (#) cos) is 2 * PI -periodic for x being real number st x in dom (b + (a (#) cos)) holds ( x + (2 * PI) in dom (b + (a (#) cos)) & x - (2 * PI) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + (2 * PI)) ) proof let x be real number ; ::_thesis: ( x in dom (b + (a (#) cos)) implies ( x + (2 * PI) in dom (b + (a (#) cos)) & x - (2 * PI) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + (2 * PI)) ) ) assume x in dom (b + (a (#) cos)) ; ::_thesis: ( x + (2 * PI) in dom (b + (a (#) cos)) & x - (2 * PI) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + (2 * PI)) ) x in REAL by XREAL_0:def_1; then A1: x in dom (a (#) cos) by SIN_COS:24, VALUED_1:def_5; then A2: ( x in dom (b + (a (#) cos)) & x in dom (b + (a (#) cos)) ) by VALUED_1:def_2; ( x + (2 * PI) in dom cos & x - (2 * PI) in dom cos ) by SIN_COS:24; then A3: ( x + (2 * PI) in dom (a (#) cos) & x - (2 * PI) in dom (a (#) cos) ) by VALUED_1:def_5; then ( x + (2 * PI) in dom (b + (a (#) cos)) & x - (2 * PI) in dom (b + (a (#) cos)) ) by VALUED_1:def_2; then (b + (a (#) cos)) . (x + (2 * PI)) = b + ((a (#) cos) . (x + (2 * PI))) by VALUED_1:def_2 .= b + (a * (cos . (x + (2 * PI)))) by A3, VALUED_1:def_5 .= b + (a * (cos . x)) by SIN_COS:78 .= b + ((a (#) cos) . x) by A1, VALUED_1:def_5 .= (b + (a (#) cos)) . x by A2, VALUED_1:def_2 ; hence ( x + (2 * PI) in dom (b + (a (#) cos)) & x - (2 * PI) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + (2 * PI)) ) by A3, VALUED_1:def_2; ::_thesis: verum end; hence b + (a (#) cos) is 2 * PI -periodic by Th1; ::_thesis: verum end; Lm28: for b, a being real number for k being Nat holds b + (a (#) sin) is (2 * PI) * (k + 1) -periodic proof let b, a be real number ; ::_thesis: for k being Nat holds b + (a (#) sin) is (2 * PI) * (k + 1) -periodic let k be Nat; ::_thesis: b + (a (#) sin) is (2 * PI) * (k + 1) -periodic defpred S1[ Nat] means b + (a (#) sin) is (2 * PI) * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm26; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: b + (a (#) sin) is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1] b + (a (#) sin) is (2 * PI) * ((k + 1) + 1) -periodic proof for x being real number st x in dom (b + (a (#) sin)) holds ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + ((2 * PI) * ((k + 1) + 1))) ) proof let x be real number ; ::_thesis: ( x in dom (b + (a (#) sin)) implies ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + ((2 * PI) * ((k + 1) + 1))) ) ) assume x in dom (b + (a (#) sin)) ; ::_thesis: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + ((2 * PI) * ((k + 1) + 1))) ) x in REAL by XREAL_0:def_1; then x in dom (a (#) sin) by SIN_COS:24, VALUED_1:def_5; then A4: x in dom (b + (a (#) sin)) by VALUED_1:def_2; ( x + ((2 * PI) * ((k + 1) + 1)) in dom sin & x - ((2 * PI) * ((k + 1) + 1)) in dom sin & x + ((2 * PI) * (k + 1)) in dom sin & x - ((2 * PI) * (k + 1)) in dom sin ) by SIN_COS:24; then A5: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (a (#) sin) & x - ((2 * PI) * ((k + 1) + 1)) in dom (a (#) sin) & x + ((2 * PI) * (k + 1)) in dom (a (#) sin) & x - ((2 * PI) * (k + 1)) in dom (a (#) sin) ) by VALUED_1:def_5; then A6: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x + ((2 * PI) * (k + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * (k + 1)) in dom (b + (a (#) sin)) ) by VALUED_1:def_2; then (b + (a (#) sin)) . (x + ((2 * PI) * ((k + 1) + 1))) = b + ((a (#) sin) . (x + ((2 * PI) * ((k + 1) + 1)))) by VALUED_1:def_2 .= b + (a * (sin . ((x + ((2 * PI) * (k + 1))) + (2 * PI)))) by A5, VALUED_1:def_5 .= b + (a * (sin . (x + ((2 * PI) * (k + 1))))) by SIN_COS:78 .= b + ((a (#) sin) . (x + ((2 * PI) * (k + 1)))) by A5, VALUED_1:def_5 .= (b + (a (#) sin)) . (x + ((2 * PI) * (k + 1))) by A6, VALUED_1:def_2 ; hence ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + ((2 * PI) * ((k + 1) + 1))) ) by A3, Th1, A5, A4, VALUED_1:def_2; ::_thesis: verum end; hence b + (a (#) sin) is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence b + (a (#) sin) is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum end; theorem Th33: :: FUNCT_9:33 for b, a being real number for i being non zero Integer holds b + (a (#) sin) is (2 * PI) * i -periodic proof let b, a be real number ; ::_thesis: for i being non zero Integer holds b + (a (#) sin) is (2 * PI) * i -periodic let i be non zero Integer; ::_thesis: b + (a (#) sin) is (2 * PI) * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: b + (a (#) sin) is (2 * PI) * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence b + (a (#) sin) is (2 * PI) * i -periodic by Lm28; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: b + (a (#) sin) is (2 * PI) * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; b + (a (#) sin) is (2 * PI) * (m + 1) -periodic by Lm28; then b + (a (#) sin) is - ((2 * PI) * (m + 1)) -periodic by Th14; hence b + (a (#) sin) is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum end; end; end; theorem :: FUNCT_9:34 for a, b being real number for i being non zero Integer holds (a (#) sin) - b is (2 * PI) * i -periodic by Th33; Lm29: for b, a being real number for k being Nat holds b + (a (#) cos) is (2 * PI) * (k + 1) -periodic proof let b, a be real number ; ::_thesis: for k being Nat holds b + (a (#) cos) is (2 * PI) * (k + 1) -periodic let k be Nat; ::_thesis: b + (a (#) cos) is (2 * PI) * (k + 1) -periodic defpred S1[ Nat] means b + (a (#) cos) is (2 * PI) * (\$1 + 1) -periodic ; A1: S1[ 0 ] by Lm27; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: b + (a (#) cos) is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1] b + (a (#) cos) is (2 * PI) * ((k + 1) + 1) -periodic proof for x being real number st x in dom (b + (a (#) cos)) holds ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + ((2 * PI) * ((k + 1) + 1))) ) proof let x be real number ; ::_thesis: ( x in dom (b + (a (#) cos)) implies ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + ((2 * PI) * ((k + 1) + 1))) ) ) assume x in dom (b + (a (#) cos)) ; ::_thesis: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + ((2 * PI) * ((k + 1) + 1))) ) x in REAL by XREAL_0:def_1; then x in dom (a (#) cos) by SIN_COS:24, VALUED_1:def_5; then A4: x in dom (b + (a (#) cos)) by VALUED_1:def_2; ( x + ((2 * PI) * ((k + 1) + 1)) in dom cos & x - ((2 * PI) * ((k + 1) + 1)) in dom cos & x + ((2 * PI) * (k + 1)) in dom cos & x - ((2 * PI) * (k + 1)) in dom cos ) by SIN_COS:24; then A5: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (a (#) cos) & x - ((2 * PI) * ((k + 1) + 1)) in dom (a (#) cos) & x + ((2 * PI) * (k + 1)) in dom (a (#) cos) & x - ((2 * PI) * (k + 1)) in dom (a (#) cos) ) by VALUED_1:def_5; then A6: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x + ((2 * PI) * (k + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * (k + 1)) in dom (b + (a (#) cos)) ) by VALUED_1:def_2; then (b + (a (#) cos)) . (x + ((2 * PI) * ((k + 1) + 1))) = b + ((a (#) cos) . (x + ((2 * PI) * ((k + 1) + 1)))) by VALUED_1:def_2 .= b + (a * (cos . ((x + ((2 * PI) * (k + 1))) + (2 * PI)))) by A5, VALUED_1:def_5 .= b + (a * (cos . (x + ((2 * PI) * (k + 1))))) by SIN_COS:78 .= b + ((a (#) cos) . (x + ((2 * PI) * (k + 1)))) by A5, VALUED_1:def_5 .= (b + (a (#) cos)) . (x + ((2 * PI) * (k + 1))) by A6, VALUED_1:def_2 ; hence ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + ((2 * PI) * ((k + 1) + 1))) ) by A3, Th1, A5, A4, VALUED_1:def_2; ::_thesis: verum end; hence b + (a (#) cos) is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence b + (a (#) cos) is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum end; theorem Th35: :: FUNCT_9:35 for b, a being real number for i being non zero Integer holds b + (a (#) cos) is (2 * PI) * i -periodic proof let b, a be real number ; ::_thesis: for i being non zero Integer holds b + (a (#) cos) is (2 * PI) * i -periodic let i be non zero Integer; ::_thesis: b + (a (#) cos) is (2 * PI) * i -periodic i in INT by INT_1:def_2; then consider k being Element of NAT such that A1: ( i = k or i = - k ) by INT_1:def_1; percases ( i = k or i = - k ) by A1; suppose i = k ; ::_thesis: b + (a (#) cos) is (2 * PI) * i -periodic then ex m being Nat st i = m + 1 by NAT_1:6; hence b + (a (#) cos) is (2 * PI) * i -periodic by Lm29; ::_thesis: verum end; supposeA2: i = - k ; ::_thesis: b + (a (#) cos) is (2 * PI) * i -periodic then consider m being Nat such that A3: - i = m + 1 by NAT_1:6; b + (a (#) cos) is (2 * PI) * (m + 1) -periodic by Lm29; then b + (a (#) cos) is - ((2 * PI) * (m + 1)) -periodic by Th14; hence b + (a (#) cos) is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum end; end; end; theorem :: FUNCT_9:36 for a, b being real number for i being non zero Integer holds (a (#) cos) - b is (2 * PI) * i -periodic by Th35; theorem :: FUNCT_9:37 for t, a being real number st t <> 0 holds REAL --> a is t -periodic by Lm1; registration let a be real number ; clusterREAL --> a -> periodic ; coherence REAL --> a is periodic proof take 1 ; :: according to FUNCT_9:def_2 ::_thesis: REAL --> a is 1 -periodic thus REAL --> a is 1 -periodic by Lm1; ::_thesis: verum end; end; registration let t be non zero real number ; cluster Relation-like Function-like V27( REAL , REAL ) complex-valued ext-real-valued real-valued t -periodic for Element of K6(K7(REAL,REAL)); existence ex b1 being Function of REAL,REAL st b1 is t -periodic proof take REAL --> the Real ; ::_thesis: REAL --> the Real is t -periodic thus REAL --> the Real is t -periodic by Lm1; ::_thesis: verum end; end;