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	$$⊢\phi \to F:ℝ⟶ℂ$$
	fperiodmul.t	$$⊢\phi \to T\in ℝ$$
	fperiodmul.n	$$⊢\phi \to N\in \mathbb{Z}$$
	fperiodmul.x	$$⊢\phi \to X\in ℝ$$
	fperiodmul.per	$$⊢\left(\phi \wedge x\in ℝ\right)\to F\left(x+T\right)=F\left(x\right)$$
Assertion	fperiodmul	$$⊢\phi \to F\left(X+NT\right)=F\left(X\right)$$

Proof

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