This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fperiodmul

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

Ref Expression
Hypotheses fperiodmul.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
fperiodmul.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
fperiodmul.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
fperiodmul.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fperiodmul.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
Assertion fperiodmul ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 fperiodmul.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
2 fperiodmul.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
3 fperiodmul.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 fperiodmul.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
5 fperiodmul.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
6 1 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → 𝐹 : ℝ ⟶ ℂ )
7 2 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → 𝑇 ∈ ℝ )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
9 4 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → 𝑋 ∈ ℝ )
10 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
11 6 7 8 9 10 fperiodmullem ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑋 ) )
12 4 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
13 3 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
14 2 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
15 13 14 mulcld ⊢ ( 𝜑 → ( 𝑁 · 𝑇 ) ∈ ℂ )
16 12 15 subnegd ⊢ ( 𝜑 → ( 𝑋 − - ( 𝑁 · 𝑇 ) ) = ( 𝑋 + ( 𝑁 · 𝑇 ) ) )
17 13 14 mulneg1d ⊢ ( 𝜑 → ( - 𝑁 · 𝑇 ) = - ( 𝑁 · 𝑇 ) )
18 17 eqcomd ⊢ ( 𝜑 → - ( 𝑁 · 𝑇 ) = ( - 𝑁 · 𝑇 ) )
19 18 oveq2d ⊢ ( 𝜑 → ( 𝑋 − - ( 𝑁 · 𝑇 ) ) = ( 𝑋 − ( - 𝑁 · 𝑇 ) ) )
20 16 19 eqtr3d ⊢ ( 𝜑 → ( 𝑋 + ( 𝑁 · 𝑇 ) ) = ( 𝑋 − ( - 𝑁 · 𝑇 ) ) )
21 20 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹 ‘ ( 𝑋 − ( - 𝑁 · 𝑇 ) ) ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹 ‘ ( 𝑋 − ( - 𝑁 · 𝑇 ) ) ) )
23 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → 𝐹 : ℝ ⟶ ℂ )
24 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → 𝑇 ∈ ℝ )
25 znnn0nn ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 ∈ ℕ0 ) → - 𝑁 ∈ ℕ )
26 3 25 sylan ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → - 𝑁 ∈ ℕ )
27 26 nnnn0d ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → - 𝑁 ∈ ℕ0 )
28 4 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → 𝑋 ∈ ℝ )
29 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
30 29 zred ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
31 30 renegcld ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → - 𝑁 ∈ ℝ )
32 31 24 remulcld ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → ( - 𝑁 · 𝑇 ) ∈ ℝ )
33 28 32 resubcld ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → ( 𝑋 − ( - 𝑁 · 𝑇 ) ) ∈ ℝ )
34 5 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
35 23 24 27 33 34 fperiodmullem ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑋 − ( - 𝑁 · 𝑇 ) ) + ( - 𝑁 · 𝑇 ) ) ) = ( 𝐹 ‘ ( 𝑋 − ( - 𝑁 · 𝑇 ) ) ) )
36 28 recnd ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → 𝑋 ∈ ℂ )
37 30 recnd ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
38 37 negcld ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → - 𝑁 ∈ ℂ )
39 24 recnd ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → 𝑇 ∈ ℂ )
40 38 39 mulcld ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → ( - 𝑁 · 𝑇 ) ∈ ℂ )
41 36 40 npcand ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → ( ( 𝑋 − ( - 𝑁 · 𝑇 ) ) + ( - 𝑁 · 𝑇 ) ) = 𝑋 )
42 41 fveq2d ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑋 − ( - 𝑁 · 𝑇 ) ) + ( - 𝑁 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑋 ) )
43 22 35 42 3eqtr2d ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑋 ) )
44 11 43 pm2.61dan ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑋 ) )