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 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑋 ) )