Metamath Proof Explorer

Theorem fperiodmullem

Description: A function with period T is also periodic with period nonnegative multiple of T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fperiodmullem.f 
|- ( ph -> F : RR --> CC )
fperiodmullem.t 
|- ( ph -> T e. RR )
fperiodmullem.n 
|- ( ph -> N e. NN0 )
fperiodmullem.x 
|- ( ph -> X e. RR )
fperiodmullem.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
Assertion fperiodmullem 
|- ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) )

Proof

Step Hyp Ref Expression
1 fperiodmullem.f 
 |-  ( ph -> F : RR --> CC )
2 fperiodmullem.t 
 |-  ( ph -> T e. RR )
3 fperiodmullem.n 
 |-  ( ph -> N e. NN0 )
4 fperiodmullem.x 
 |-  ( ph -> X e. RR )
5 fperiodmullem.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
6 oveq1 
 |-  ( n = 0 -> ( n x. T ) = ( 0 x. T ) )
7 6 oveq2d 
 |-  ( n = 0 -> ( X + ( n x. T ) ) = ( X + ( 0 x. T ) ) )
8 7 fveqeq2d 
 |-  ( n = 0 -> ( ( F ` ( X + ( n x. T ) ) ) = ( F ` X ) <-> ( F ` ( X + ( 0 x. T ) ) ) = ( F ` X ) ) )
9 8 imbi2d 
 |-  ( n = 0 -> ( ( ph -> ( F ` ( X + ( n x. T ) ) ) = ( F ` X ) ) <-> ( ph -> ( F ` ( X + ( 0 x. T ) ) ) = ( F ` X ) ) ) )
10 oveq1 
 |-  ( n = m -> ( n x. T ) = ( m x. T ) )
11 10 oveq2d 
 |-  ( n = m -> ( X + ( n x. T ) ) = ( X + ( m x. T ) ) )
12 11 fveqeq2d 
 |-  ( n = m -> ( ( F ` ( X + ( n x. T ) ) ) = ( F ` X ) <-> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) )
13 12 imbi2d 
 |-  ( n = m -> ( ( ph -> ( F ` ( X + ( n x. T ) ) ) = ( F ` X ) ) <-> ( ph -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) ) )
14 oveq1 
 |-  ( n = ( m + 1 ) -> ( n x. T ) = ( ( m + 1 ) x. T ) )
15 14 oveq2d 
 |-  ( n = ( m + 1 ) -> ( X + ( n x. T ) ) = ( X + ( ( m + 1 ) x. T ) ) )
16 15 fveqeq2d 
 |-  ( n = ( m + 1 ) -> ( ( F ` ( X + ( n x. T ) ) ) = ( F ` X ) <-> ( F ` ( X + ( ( m + 1 ) x. T ) ) ) = ( F ` X ) ) )
17 16 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ph -> ( F ` ( X + ( n x. T ) ) ) = ( F ` X ) ) <-> ( ph -> ( F ` ( X + ( ( m + 1 ) x. T ) ) ) = ( F ` X ) ) ) )
18 oveq1 
 |-  ( n = N -> ( n x. T ) = ( N x. T ) )
19 18 oveq2d 
 |-  ( n = N -> ( X + ( n x. T ) ) = ( X + ( N x. T ) ) )
20 19 fveqeq2d 
 |-  ( n = N -> ( ( F ` ( X + ( n x. T ) ) ) = ( F ` X ) <-> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) ) )
21 20 imbi2d 
 |-  ( n = N -> ( ( ph -> ( F ` ( X + ( n x. T ) ) ) = ( F ` X ) ) <-> ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) ) ) )
22 2 recnd 
 |-  ( ph -> T e. CC )
23 22 mul02d 
 |-  ( ph -> ( 0 x. T ) = 0 )
24 23 oveq2d 
 |-  ( ph -> ( X + ( 0 x. T ) ) = ( X + 0 ) )
25 4 recnd 
 |-  ( ph -> X e. CC )
26 25 addid1d 
 |-  ( ph -> ( X + 0 ) = X )
27 24 26 eqtrd 
 |-  ( ph -> ( X + ( 0 x. T ) ) = X )
28 27 fveq2d 
 |-  ( ph -> ( F ` ( X + ( 0 x. T ) ) ) = ( F ` X ) )
29 simp3 
 |-  ( ( m e. NN0 /\ ( ph -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) /\ ph ) -> ph )
30 simp1 
 |-  ( ( m e. NN0 /\ ( ph -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) /\ ph ) -> m e. NN0 )
31 simpr 
 |-  ( ( ( ph -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) /\ ph ) -> ph )
32 simpl 
 |-  ( ( ( ph -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) /\ ph ) -> ( ph -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) )
33 31 32 mpd 
 |-  ( ( ( ph -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) /\ ph ) -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) )
34 33 3adant1 
 |-  ( ( m e. NN0 /\ ( ph -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) /\ ph ) -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) )
35 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
36 35 adantl 
 |-  ( ( ph /\ m e. NN0 ) -> m e. CC )
37 1cnd 
 |-  ( ( ph /\ m e. NN0 ) -> 1 e. CC )
38 22 adantr 
 |-  ( ( ph /\ m e. NN0 ) -> T e. CC )
39 36 37 38 adddird 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( m + 1 ) x. T ) = ( ( m x. T ) + ( 1 x. T ) ) )
40 39 oveq2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( X + ( ( m + 1 ) x. T ) ) = ( X + ( ( m x. T ) + ( 1 x. T ) ) ) )
41 25 adantr 
 |-  ( ( ph /\ m e. NN0 ) -> X e. CC )
42 36 38 mulcld 
 |-  ( ( ph /\ m e. NN0 ) -> ( m x. T ) e. CC )
43 37 38 mulcld 
 |-  ( ( ph /\ m e. NN0 ) -> ( 1 x. T ) e. CC )
44 41 42 43 addassd 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( X + ( m x. T ) ) + ( 1 x. T ) ) = ( X + ( ( m x. T ) + ( 1 x. T ) ) ) )
45 38 mulid2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( 1 x. T ) = T )
46 45 oveq2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( X + ( m x. T ) ) + ( 1 x. T ) ) = ( ( X + ( m x. T ) ) + T ) )
47 40 44 46 3eqtr2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( X + ( ( m + 1 ) x. T ) ) = ( ( X + ( m x. T ) ) + T ) )
48 47 fveq2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( F ` ( X + ( ( m + 1 ) x. T ) ) ) = ( F ` ( ( X + ( m x. T ) ) + T ) ) )
49 48 3adant3 
 |-  ( ( ph /\ m e. NN0 /\ ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) -> ( F ` ( X + ( ( m + 1 ) x. T ) ) ) = ( F ` ( ( X + ( m x. T ) ) + T ) ) )
50 4 adantr 
 |-  ( ( ph /\ m e. NN0 ) -> X e. RR )
51 nn0re 
 |-  ( m e. NN0 -> m e. RR )
52 51 adantl 
 |-  ( ( ph /\ m e. NN0 ) -> m e. RR )
53 2 adantr 
 |-  ( ( ph /\ m e. NN0 ) -> T e. RR )
54 52 53 remulcld 
 |-  ( ( ph /\ m e. NN0 ) -> ( m x. T ) e. RR )
55 50 54 readdcld 
 |-  ( ( ph /\ m e. NN0 ) -> ( X + ( m x. T ) ) e. RR )
56 55 ex 
 |-  ( ph -> ( m e. NN0 -> ( X + ( m x. T ) ) e. RR ) )
57 56 imdistani 
 |-  ( ( ph /\ m e. NN0 ) -> ( ph /\ ( X + ( m x. T ) ) e. RR ) )
58 eleq1 
 |-  ( x = ( X + ( m x. T ) ) -> ( x e. RR <-> ( X + ( m x. T ) ) e. RR ) )
59 58 anbi2d 
 |-  ( x = ( X + ( m x. T ) ) -> ( ( ph /\ x e. RR ) <-> ( ph /\ ( X + ( m x. T ) ) e. RR ) ) )
60 fvoveq1 
 |-  ( x = ( X + ( m x. T ) ) -> ( F ` ( x + T ) ) = ( F ` ( ( X + ( m x. T ) ) + T ) ) )
61 fveq2 
 |-  ( x = ( X + ( m x. T ) ) -> ( F ` x ) = ( F ` ( X + ( m x. T ) ) ) )
62 60 61 eqeq12d 
 |-  ( x = ( X + ( m x. T ) ) -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( ( X + ( m x. T ) ) + T ) ) = ( F ` ( X + ( m x. T ) ) ) ) )
63 59 62 imbi12d 
 |-  ( x = ( X + ( m x. T ) ) -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ ( X + ( m x. T ) ) e. RR ) -> ( F ` ( ( X + ( m x. T ) ) + T ) ) = ( F ` ( X + ( m x. T ) ) ) ) ) )
64 63 5 vtoclg 
 |-  ( ( X + ( m x. T ) ) e. RR -> ( ( ph /\ ( X + ( m x. T ) ) e. RR ) -> ( F ` ( ( X + ( m x. T ) ) + T ) ) = ( F ` ( X + ( m x. T ) ) ) ) )
65 55 57 64 sylc 
 |-  ( ( ph /\ m e. NN0 ) -> ( F ` ( ( X + ( m x. T ) ) + T ) ) = ( F ` ( X + ( m x. T ) ) ) )
66 65 3adant3 
 |-  ( ( ph /\ m e. NN0 /\ ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) -> ( F ` ( ( X + ( m x. T ) ) + T ) ) = ( F ` ( X + ( m x. T ) ) ) )
67 simp3 
 |-  ( ( ph /\ m e. NN0 /\ ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) )
68 49 66 67 3eqtrd 
 |-  ( ( ph /\ m e. NN0 /\ ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) -> ( F ` ( X + ( ( m + 1 ) x. T ) ) ) = ( F ` X ) )
69 29 30 34 68 syl3anc 
 |-  ( ( m e. NN0 /\ ( ph -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) /\ ph ) -> ( F ` ( X + ( ( m + 1 ) x. T ) ) ) = ( F ` X ) )
70 69 3exp 
 |-  ( m e. NN0 -> ( ( ph -> ( F ` ( X + ( m x. T ) ) ) = ( F ` X ) ) -> ( ph -> ( F ` ( X + ( ( m + 1 ) x. T ) ) ) = ( F ` X ) ) ) )
71 9 13 17 21 28 70 nn0ind 
 |-  ( N e. NN0 -> ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) ) )
72 3 71 mpcom 
 |-  ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) )