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