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 ( 𝜑𝐹 : ℝ ⟶ ℂ )
fperiodmullem.t ( 𝜑𝑇 ∈ ℝ )
fperiodmullem.n ( 𝜑𝑁 ∈ ℕ0 )
fperiodmullem.x ( 𝜑𝑋 ∈ ℝ )
fperiodmullem.per ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
Assertion fperiodmullem ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹𝑋 ) )

Proof

Step Hyp Ref Expression
1 fperiodmullem.f ( 𝜑𝐹 : ℝ ⟶ ℂ )
2 fperiodmullem.t ( 𝜑𝑇 ∈ ℝ )
3 fperiodmullem.n ( 𝜑𝑁 ∈ ℕ0 )
4 fperiodmullem.x ( 𝜑𝑋 ∈ ℝ )
5 fperiodmullem.per ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
6 oveq1 ( 𝑛 = 0 → ( 𝑛 · 𝑇 ) = ( 0 · 𝑇 ) )
7 6 oveq2d ( 𝑛 = 0 → ( 𝑋 + ( 𝑛 · 𝑇 ) ) = ( 𝑋 + ( 0 · 𝑇 ) ) )
8 7 fveqeq2d ( 𝑛 = 0 → ( ( 𝐹 ‘ ( 𝑋 + ( 𝑛 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ↔ ( 𝐹 ‘ ( 𝑋 + ( 0 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) )
9 8 imbi2d ( 𝑛 = 0 → ( ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑛 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 0 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ) )
10 oveq1 ( 𝑛 = 𝑚 → ( 𝑛 · 𝑇 ) = ( 𝑚 · 𝑇 ) )
11 10 oveq2d ( 𝑛 = 𝑚 → ( 𝑋 + ( 𝑛 · 𝑇 ) ) = ( 𝑋 + ( 𝑚 · 𝑇 ) ) )
12 11 fveqeq2d ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ ( 𝑋 + ( 𝑛 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ↔ ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) )
13 12 imbi2d ( 𝑛 = 𝑚 → ( ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑛 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ) )
14 oveq1 ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 · 𝑇 ) = ( ( 𝑚 + 1 ) · 𝑇 ) )
15 14 oveq2d ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑋 + ( 𝑛 · 𝑇 ) ) = ( 𝑋 + ( ( 𝑚 + 1 ) · 𝑇 ) ) )
16 15 fveqeq2d ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝐹 ‘ ( 𝑋 + ( 𝑛 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ↔ ( 𝐹 ‘ ( 𝑋 + ( ( 𝑚 + 1 ) · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) )
17 16 imbi2d ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑛 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( ( 𝑚 + 1 ) · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ) )
18 oveq1 ( 𝑛 = 𝑁 → ( 𝑛 · 𝑇 ) = ( 𝑁 · 𝑇 ) )
19 18 oveq2d ( 𝑛 = 𝑁 → ( 𝑋 + ( 𝑛 · 𝑇 ) ) = ( 𝑋 + ( 𝑁 · 𝑇 ) ) )
20 19 fveqeq2d ( 𝑛 = 𝑁 → ( ( 𝐹 ‘ ( 𝑋 + ( 𝑛 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ↔ ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) )
21 20 imbi2d ( 𝑛 = 𝑁 → ( ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑛 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ) )
22 2 recnd ( 𝜑𝑇 ∈ ℂ )
23 22 mul02d ( 𝜑 → ( 0 · 𝑇 ) = 0 )
24 23 oveq2d ( 𝜑 → ( 𝑋 + ( 0 · 𝑇 ) ) = ( 𝑋 + 0 ) )
25 4 recnd ( 𝜑𝑋 ∈ ℂ )
26 25 addid1d ( 𝜑 → ( 𝑋 + 0 ) = 𝑋 )
27 24 26 eqtrd ( 𝜑 → ( 𝑋 + ( 0 · 𝑇 ) ) = 𝑋 )
28 27 fveq2d ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 0 · 𝑇 ) ) ) = ( 𝐹𝑋 ) )
29 simp3 ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ∧ 𝜑 ) → 𝜑 )
30 simp1 ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ∧ 𝜑 ) → 𝑚 ∈ ℕ0 )
31 simpr ( ( ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ∧ 𝜑 ) → 𝜑 )
32 simpl ( ( ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ∧ 𝜑 ) → ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) )
33 31 32 mpd ( ( ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) )
34 33 3adant1 ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) )
35 nn0cn ( 𝑚 ∈ ℕ0𝑚 ∈ ℂ )
36 35 adantl ( ( 𝜑𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℂ )
37 1cnd ( ( 𝜑𝑚 ∈ ℕ0 ) → 1 ∈ ℂ )
38 22 adantr ( ( 𝜑𝑚 ∈ ℕ0 ) → 𝑇 ∈ ℂ )
39 36 37 38 adddird ( ( 𝜑𝑚 ∈ ℕ0 ) → ( ( 𝑚 + 1 ) · 𝑇 ) = ( ( 𝑚 · 𝑇 ) + ( 1 · 𝑇 ) ) )
40 39 oveq2d ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 𝑋 + ( ( 𝑚 + 1 ) · 𝑇 ) ) = ( 𝑋 + ( ( 𝑚 · 𝑇 ) + ( 1 · 𝑇 ) ) ) )
41 25 adantr ( ( 𝜑𝑚 ∈ ℕ0 ) → 𝑋 ∈ ℂ )
42 36 38 mulcld ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 𝑚 · 𝑇 ) ∈ ℂ )
43 37 38 mulcld ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 1 · 𝑇 ) ∈ ℂ )
44 41 42 43 addassd ( ( 𝜑𝑚 ∈ ℕ0 ) → ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + ( 1 · 𝑇 ) ) = ( 𝑋 + ( ( 𝑚 · 𝑇 ) + ( 1 · 𝑇 ) ) ) )
45 38 mulid2d ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 1 · 𝑇 ) = 𝑇 )
46 45 oveq2d ( ( 𝜑𝑚 ∈ ℕ0 ) → ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + ( 1 · 𝑇 ) ) = ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + 𝑇 ) )
47 40 44 46 3eqtr2d ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 𝑋 + ( ( 𝑚 + 1 ) · 𝑇 ) ) = ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + 𝑇 ) )
48 47 fveq2d ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑋 + ( ( 𝑚 + 1 ) · 𝑇 ) ) ) = ( 𝐹 ‘ ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + 𝑇 ) ) )
49 48 3adant3 ( ( 𝜑𝑚 ∈ ℕ0 ∧ ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) → ( 𝐹 ‘ ( 𝑋 + ( ( 𝑚 + 1 ) · 𝑇 ) ) ) = ( 𝐹 ‘ ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + 𝑇 ) ) )
50 4 adantr ( ( 𝜑𝑚 ∈ ℕ0 ) → 𝑋 ∈ ℝ )
51 nn0re ( 𝑚 ∈ ℕ0𝑚 ∈ ℝ )
52 51 adantl ( ( 𝜑𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℝ )
53 2 adantr ( ( 𝜑𝑚 ∈ ℕ0 ) → 𝑇 ∈ ℝ )
54 52 53 remulcld ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 𝑚 · 𝑇 ) ∈ ℝ )
55 50 54 readdcld ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 𝑋 + ( 𝑚 · 𝑇 ) ) ∈ ℝ )
56 55 ex ( 𝜑 → ( 𝑚 ∈ ℕ0 → ( 𝑋 + ( 𝑚 · 𝑇 ) ) ∈ ℝ ) )
57 56 imdistani ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 𝜑 ∧ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ∈ ℝ ) )
58 eleq1 ( 𝑥 = ( 𝑋 + ( 𝑚 · 𝑇 ) ) → ( 𝑥 ∈ ℝ ↔ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ∈ ℝ ) )
59 58 anbi2d ( 𝑥 = ( 𝑋 + ( 𝑚 · 𝑇 ) ) → ( ( 𝜑𝑥 ∈ ℝ ) ↔ ( 𝜑 ∧ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ∈ ℝ ) ) )
60 fvoveq1 ( 𝑥 = ( 𝑋 + ( 𝑚 · 𝑇 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + 𝑇 ) ) )
61 fveq2 ( 𝑥 = ( 𝑋 + ( 𝑚 · 𝑇 ) ) → ( 𝐹𝑥 ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) )
62 60 61 eqeq12d ( 𝑥 = ( 𝑋 + ( 𝑚 · 𝑇 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) ↔ ( 𝐹 ‘ ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) ) )
63 59 62 imbi12d ( 𝑥 = ( 𝑋 + ( 𝑚 · 𝑇 ) ) → ( ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) ) ↔ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ∈ ℝ ) → ( 𝐹 ‘ ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) ) ) )
64 63 5 vtoclg ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) ∈ ℝ → ( ( 𝜑 ∧ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ∈ ℝ ) → ( 𝐹 ‘ ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) ) )
65 55 57 64 sylc ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) )
66 65 3adant3 ( ( 𝜑𝑚 ∈ ℕ0 ∧ ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑋 + ( 𝑚 · 𝑇 ) ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) )
67 simp3 ( ( 𝜑𝑚 ∈ ℕ0 ∧ ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) )
68 49 66 67 3eqtrd ( ( 𝜑𝑚 ∈ ℕ0 ∧ ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) → ( 𝐹 ‘ ( 𝑋 + ( ( 𝑚 + 1 ) · 𝑇 ) ) ) = ( 𝐹𝑋 ) )
69 29 30 34 68 syl3anc ( ( 𝑚 ∈ ℕ0 ∧ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ ( 𝑋 + ( ( 𝑚 + 1 ) · 𝑇 ) ) ) = ( 𝐹𝑋 ) )
70 69 3exp ( 𝑚 ∈ ℕ0 → ( ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑚 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) → ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( ( 𝑚 + 1 ) · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) ) )
71 9 13 17 21 28 70 nn0ind ( 𝑁 ∈ ℕ0 → ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹𝑋 ) ) )
72 3 71 mpcom ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹𝑋 ) )