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

Proof

Step	Hyp	Ref	Expression
1		fperiodmullem.f	$⊢ φ \to F : ℝ ⟶ ℂ$
2		fperiodmullem.t	$⊢ φ \to T \in ℝ$
3		fperiodmullem.n	$⊢ φ \to N \in ℕ_{0}$
4		fperiodmullem.x	$⊢ φ \to X \in ℝ$
5		fperiodmullem.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
6		oveq1	$⊢ n = 0 \to n T = 0 \cdot T$
7	6	oveq2d	$⊢ n = 0 \to X + n T = X + 0 \cdot T$
8	7	fveqeq2d	$⊢ n = 0 \to (F (X + n T) = F (X) \leftrightarrow F (X + 0 \cdot T) = F (X))$
9	8	imbi2d	$⊢ n = 0 \to ((φ \to F (X + n T) = F (X)) \leftrightarrow (φ \to F (X + 0 \cdot T) = F (X)))$
10		oveq1	$⊢ n = m \to n T = m T$
11	10	oveq2d	$⊢ n = m \to X + n T = X + m T$
12	11	fveqeq2d	$⊢ n = m \to (F (X + n T) = F (X) \leftrightarrow F (X + m T) = F (X))$
13	12	imbi2d	$⊢ n = m \to ((φ \to F (X + n T) = F (X)) \leftrightarrow (φ \to F (X + m T) = F (X)))$
14		oveq1	$⊢ n = m + 1 \to n T = (m + 1) T$
15	14	oveq2d	$⊢ n = m + 1 \to X + n T = X + (m + 1) T$
16	15	fveqeq2d	$⊢ n = m + 1 \to (F (X + n T) = F (X) \leftrightarrow F (X + (m + 1) T) = F (X))$
17	16	imbi2d	$⊢ n = m + 1 \to ((φ \to F (X + n T) = F (X)) \leftrightarrow (φ \to F (X + (m + 1) T) = F (X)))$
18		oveq1	$⊢ n = N \to n T = N T$
19	18	oveq2d	$⊢ n = N \to X + n T = X + N T$
20	19	fveqeq2d	$⊢ n = N \to (F (X + n T) = F (X) \leftrightarrow F (X + N T) = F (X))$
21	20	imbi2d	$⊢ n = N \to ((φ \to F (X + n T) = F (X)) \leftrightarrow (φ \to F (X + N T) = F (X)))$
22	2	recnd	$⊢ φ \to T \in ℂ$
23	22	mul02d	$⊢ φ \to 0 \cdot T = 0$
24	23	oveq2d	$⊢ φ \to X + 0 \cdot T = X + 0$
25	4	recnd	$⊢ φ \to X \in ℂ$
26	25	addid1d	$⊢ φ \to X + 0 = X$
27	24 26	eqtrd	$⊢ φ \to X + 0 \cdot T = X$
28	27	fveq2d	$⊢ φ \to F (X + 0 \cdot T) = F (X)$
29		simp3	$⊢ (m \in ℕ_{0} \land (φ \to F (X + m T) = F (X)) \land φ) \to φ$
30		simp1	$⊢ (m \in ℕ_{0} \land (φ \to F (X + m T) = F (X)) \land φ) \to m \in ℕ_{0}$
31		simpr	$⊢ ((φ \to F (X + m T) = F (X)) \land φ) \to φ$
32		simpl	$⊢ ((φ \to F (X + m T) = F (X)) \land φ) \to (φ \to F (X + m T) = F (X))$
33	31 32	mpd	$⊢ ((φ \to F (X + m T) = F (X)) \land φ) \to F (X + m T) = F (X)$
34	33	3adant1	$⊢ (m \in ℕ_{0} \land (φ \to F (X + m T) = F (X)) \land φ) \to F (X + m T) = F (X)$
35		nn0cn	$⊢ m \in ℕ_{0} \to m \in ℂ$
36	35	adantl	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℂ$
37		1cnd	$⊢ (φ \land m \in ℕ_{0}) \to 1 \in ℂ$
38	22	adantr	$⊢ (φ \land m \in ℕ_{0}) \to T \in ℂ$
39	36 37 38	adddird	$⊢ (φ \land m \in ℕ_{0}) \to (m + 1) T = m T + 1 T$
40	39	oveq2d	$⊢ (φ \land m \in ℕ_{0}) \to X + (m + 1) T = X + m T + 1 T$
41	25	adantr	$⊢ (φ \land m \in ℕ_{0}) \to X \in ℂ$
42	36 38	mulcld	$⊢ (φ \land m \in ℕ_{0}) \to m T \in ℂ$
43	37 38	mulcld	$⊢ (φ \land m \in ℕ_{0}) \to 1 T \in ℂ$
44	41 42 43	addassd	$⊢ (φ \land m \in ℕ_{0}) \to X + m T + 1 T = X + m T + 1 T$
45	38	mulid2d	$⊢ (φ \land m \in ℕ_{0}) \to 1 T = T$
46	45	oveq2d	$⊢ (φ \land m \in ℕ_{0}) \to X + m T + 1 T = X + m T + T$
47	40 44 46	3eqtr2d	$⊢ (φ \land m \in ℕ_{0}) \to X + (m + 1) T = X + m T + T$
48	47	fveq2d	$⊢ (φ \land m \in ℕ_{0}) \to F (X + (m + 1) T) = F (X + m T + T)$
49	48	3adant3	$⊢ (φ \land m \in ℕ_{0} \land F (X + m T) = F (X)) \to F (X + (m + 1) T) = F (X + m T + T)$
50	4	adantr	$⊢ (φ \land m \in ℕ_{0}) \to X \in ℝ$
51		nn0re	$⊢ m \in ℕ_{0} \to m \in ℝ$
52	51	adantl	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℝ$
53	2	adantr	$⊢ (φ \land m \in ℕ_{0}) \to T \in ℝ$
54	52 53	remulcld	$⊢ (φ \land m \in ℕ_{0}) \to m T \in ℝ$
55	50 54	readdcld	$⊢ (φ \land m \in ℕ_{0}) \to X + m T \in ℝ$
56	55	ex	$⊢ φ \to (m \in ℕ_{0} \to X + m T \in ℝ)$
57	56	imdistani	$⊢ (φ \land m \in ℕ_{0}) \to (φ \land X + m T \in ℝ)$
58		eleq1	$⊢ x = X + m T \to (x \in ℝ \leftrightarrow X + m T \in ℝ)$
59	58	anbi2d	$⊢ x = X + m T \to ((φ \land x \in ℝ) \leftrightarrow (φ \land X + m T \in ℝ))$
60		fvoveq1	$⊢ x = X + m T \to F (x + T) = F (X + m T + T)$
61		fveq2	$⊢ x = X + m T \to F (x) = F (X + m T)$
62	60 61	eqeq12d	$⊢ x = X + m T \to (F (x + T) = F (x) \leftrightarrow F (X + m T + T) = F (X + m T))$
63	59 62	imbi12d	$⊢ x = X + m T \to (((φ \land x \in ℝ) \to F (x + T) = F (x)) \leftrightarrow ((φ \land X + m T \in ℝ) \to F (X + m T + T) = F (X + m T)))$
64	63 5	vtoclg	$⊢ X + m T \in ℝ \to ((φ \land X + m T \in ℝ) \to F (X + m T + T) = F (X + m T))$
65	55 57 64	sylc	$⊢ (φ \land m \in ℕ_{0}) \to F (X + m T + T) = F (X + m T)$
66	65	3adant3	$⊢ (φ \land m \in ℕ_{0} \land F (X + m T) = F (X)) \to F (X + m T + T) = F (X + m T)$
67		simp3	$⊢ (φ \land m \in ℕ_{0} \land F (X + m T) = F (X)) \to F (X + m T) = F (X)$
68	49 66 67	3eqtrd	$⊢ (φ \land m \in ℕ_{0} \land F (X + m T) = F (X)) \to F (X + (m + 1) T) = F (X)$
69	29 30 34 68	syl3anc	$⊢ (m \in ℕ_{0} \land (φ \to F (X + m T) = F (X)) \land φ) \to F (X + (m + 1) T) = F (X)$
70	69	3exp	$⊢ m \in ℕ_{0} \to ((φ \to F (X + m T) = F (X)) \to (φ \to F (X + (m + 1) T) = F (X)))$
71	9 13 17 21 28 70	nn0ind	$⊢ N \in ℕ_{0} \to (φ \to F (X + N T) = F (X))$
72	3 71	mpcom	$⊢ φ \to F (X + N T) = F (X)$

Metamath Proof Explorer

Theorem fperiodmullem

Proof