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	$⊢ φ \to F : ℝ ⟶ ℂ$
	fperiodmul.t	$⊢ φ \to T \in ℝ$
	fperiodmul.n	$⊢ φ \to N \in ℤ$
	fperiodmul.x	$⊢ φ \to X \in ℝ$
	fperiodmul.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
Assertion	fperiodmul	$⊢ φ \to F (X + N T) = F (X)$

Proof

Step	Hyp	Ref	Expression
1		fperiodmul.f	$⊢ φ \to F : ℝ ⟶ ℂ$
2		fperiodmul.t	$⊢ φ \to T \in ℝ$
3		fperiodmul.n	$⊢ φ \to N \in ℤ$
4		fperiodmul.x	$⊢ φ \to X \in ℝ$
5		fperiodmul.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
6	1	adantr	$⊢ (φ \land N \in ℕ_{0}) \to F : ℝ ⟶ ℂ$
7	2	adantr	$⊢ (φ \land N \in ℕ_{0}) \to T \in ℝ$
8		simpr	$⊢ (φ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
9	4	adantr	$⊢ (φ \land N \in ℕ_{0}) \to X \in ℝ$
10	5	adantlr	$⊢ ((φ \land N \in ℕ_{0}) \land x \in ℝ) \to F (x + T) = F (x)$
11	6 7 8 9 10	fperiodmullem	$⊢ (φ \land N \in ℕ_{0}) \to F (X + N T) = F (X)$
12	4	recnd	$⊢ φ \to X \in ℂ$
13	3	zcnd	$⊢ φ \to N \in ℂ$
14	2	recnd	$⊢ φ \to T \in ℂ$
15	13 14	mulcld	$⊢ φ \to N T \in ℂ$
16	12 15	subnegd	$⊢ φ \to X - (- N T) = X + N T$
17	13 14	mulneg1d	$⊢ φ \to -N T = - N T$
18	17	eqcomd	$⊢ φ \to - N T = -N T$
19	18	oveq2d	$⊢ φ \to X - (- N T) = X - -N T$
20	16 19	eqtr3d	$⊢ φ \to X + N T = X - -N T$
21	20	fveq2d	$⊢ φ \to F (X + N T) = F (X - -N T)$
22	21	adantr	$⊢ (φ \land \neg N \in ℕ_{0}) \to F (X + N T) = F (X - -N T)$
23	1	adantr	$⊢ (φ \land \neg N \in ℕ_{0}) \to F : ℝ ⟶ ℂ$
24	2	adantr	$⊢ (φ \land \neg N \in ℕ_{0}) \to T \in ℝ$
25		znnn0nn	$⊢ (N \in ℤ \land \neg N \in ℕ_{0}) \to - N \in ℕ$
26	3 25	sylan	$⊢ (φ \land \neg N \in ℕ_{0}) \to - N \in ℕ$
27	26	nnnn0d	$⊢ (φ \land \neg N \in ℕ_{0}) \to - N \in ℕ_{0}$
28	4	adantr	$⊢ (φ \land \neg N \in ℕ_{0}) \to X \in ℝ$
29	3	adantr	$⊢ (φ \land \neg N \in ℕ_{0}) \to N \in ℤ$
30	29	zred	$⊢ (φ \land \neg N \in ℕ_{0}) \to N \in ℝ$
31	30	renegcld	$⊢ (φ \land \neg N \in ℕ_{0}) \to - N \in ℝ$
32	31 24	remulcld	$⊢ (φ \land \neg N \in ℕ_{0}) \to -N T \in ℝ$
33	28 32	resubcld	$⊢ (φ \land \neg N \in ℕ_{0}) \to X - -N T \in ℝ$
34	5	adantlr	$⊢ ((φ \land \neg N \in ℕ_{0}) \land x \in ℝ) \to F (x + T) = F (x)$
35	23 24 27 33 34	fperiodmullem	$⊢ (φ \land \neg N \in ℕ_{0}) \to F (X - -N T + -N T) = F (X - -N T)$
36	28	recnd	$⊢ (φ \land \neg N \in ℕ_{0}) \to X \in ℂ$
37	30	recnd	$⊢ (φ \land \neg N \in ℕ_{0}) \to N \in ℂ$
38	37	negcld	$⊢ (φ \land \neg N \in ℕ_{0}) \to - N \in ℂ$
39	24	recnd	$⊢ (φ \land \neg N \in ℕ_{0}) \to T \in ℂ$
40	38 39	mulcld	$⊢ (φ \land \neg N \in ℕ_{0}) \to -N T \in ℂ$
41	36 40	npcand	$⊢ (φ \land \neg N \in ℕ_{0}) \to X - -N T + -N T = X$
42	41	fveq2d	$⊢ (φ \land \neg N \in ℕ_{0}) \to F (X - -N T + -N T) = F (X)$
43	22 35 42	3eqtr2d	$⊢ (φ \land \neg N \in ℕ_{0}) \to F (X + N T) = F (X)$
44	11 43	pm2.61dan	$⊢ φ \to F (X + N T) = F (X)$

Metamath Proof Explorer

Theorem fperiodmul

Proof