fourierdlem114 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fourierdlem114		Structured version Visualization version GIF version

Theorem fourierdlem114 46670

Description: Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem114.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem114.t	⊢ 𝑇 = (2 · π)
fourierdlem114.per	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
fourierdlem114.g	⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π))
fourierdlem114.dmdv	⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin)
fourierdlem114.gcn	⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
fourierdlem114.rlim	⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
fourierdlem114.llim	⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
fourierdlem114.x	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem114.l	⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
fourierdlem114.r	⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
fourierdlem114.a	⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem114.b	⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem114.s	⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
fourierdlem114.p	⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem114.e	⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
fourierdlem114.h	⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
fourierdlem114.m	⊢ 𝑀 = ((♯‘𝐻) − 1)
fourierdlem114.q	⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻))

**Assertion**
Ref	Expression
fourierdlem114	⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))

Distinct variable groups: 𝐴,𝑛 𝐵,𝑛 𝑥,𝐸 𝑖,𝐹,𝑛,𝑥 𝑖,𝐺,𝑥 𝑔,𝐻 𝑖,𝐿,𝑛 𝑔,𝑀 𝑖,𝑀,𝑛,𝑝 𝑥,𝑀 𝑄,𝑔 𝑄,𝑖,𝑛,𝑝 𝑥,𝑄 𝑅,𝑖,𝑛 𝑇,𝑖,𝑛,𝑝 𝑥,𝑇 𝑖,𝑋,𝑛,𝑝 𝑥,𝑋 𝜑,𝑔 𝜑,𝑖,𝑛,𝑥 Allowed substitution hints: 𝜑(𝑝) 𝐴(𝑥,𝑔,𝑖,𝑝) 𝐵(𝑥,𝑔,𝑖,𝑝) 𝑃(𝑥,𝑔,𝑖,𝑛,𝑝) 𝑅(𝑥,𝑔,𝑝) 𝑆(𝑥,𝑔,𝑖,𝑛,𝑝) 𝑇(𝑔) 𝐸(𝑔,𝑖,𝑛,𝑝) 𝐹(𝑔,𝑝) 𝐺(𝑔,𝑛,𝑝) 𝐻(𝑥,𝑖,𝑛,𝑝) 𝐿(𝑥,𝑔,𝑝) 𝑋(𝑔)

**Proof of Theorem fourierdlem114**
Step	Hyp	Ref	Expression
1		fourierdlem114.f	. 2 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
2		fourierdlem114.t	. 2 ⊢ 𝑇 = (2 · π)
3		fourierdlem114.per	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
4		fourierdlem114.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℝ)
5		fourierdlem114.l	. 2 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
6		fourierdlem114.r	. 2 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
7		fourierdlem114.p	. 2 ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
8		fourierdlem114.m	. . 3 ⊢ 𝑀 = ((♯‘𝐻) − 1)
9		2z 12557	. . . . . 6 ⊢ 2 ∈ ℤ
10	9	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
11		fourierdlem114.h	. . . . . . . 8 ⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
12		tpfi 9233	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ Fin
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ∈ Fin)
14		pire 26446	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ
15	14	renegcli 11453	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
16	15	rexri 11201	. . . . . . . . . . . . 13 ⊢ -π ∈ ℝ^*
17	14	rexri 11201	. . . . . . . . . . . . 13 ⊢ π ∈ ℝ^*
18		negpilt0 45736	. . . . . . . . . . . . . . 15 ⊢ -π < 0
19		pipos 26448	. . . . . . . . . . . . . . 15 ⊢ 0 < π
20		0re 11144	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
21	15, 20, 14	lttri 11270	. . . . . . . . . . . . . . 15 ⊢ ((-π < 0 ∧ 0 < π) → -π < π)
22	18, 19, 21	mp2an 698	. . . . . . . . . . . . . 14 ⊢ -π < π
23	15, 14, 22	ltleii 11267	. . . . . . . . . . . . 13 ⊢ -π ≤ π
24		prunioo 13432	. . . . . . . . . . . . 13 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → ((-π(,)π) ∪ {-π, π}) = (-π[,]π))
25	16, 17, 23, 24	mp3an 1469	. . . . . . . . . . . 12 ⊢ ((-π(,)π) ∪ {-π, π}) = (-π[,]π)
26	25	difeq1i 4060	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = ((-π[,]π) ∖ dom 𝐺)
27		difundir 4226	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
28	26, 27	eqtr3i 2765	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
29		fourierdlem114.dmdv	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin)
30		prfi 9231	. . . . . . . . . . . 12 ⊢ {-π, π} ∈ Fin
31		diffi 9106	. . . . . . . . . . . 12 ⊢ ({-π, π} ∈ Fin → ({-π, π} ∖ dom 𝐺) ∈ Fin)
32	30, 31	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → ({-π, π} ∖ dom 𝐺) ∈ Fin)
33		unfi 9102	. . . . . . . . . . 11 ⊢ ((((-π(,)π) ∖ dom 𝐺) ∈ Fin ∧ ({-π, π} ∖ dom 𝐺) ∈ Fin) → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
34	29, 32, 33	syl2anc 590	. . . . . . . . . 10 ⊢ (𝜑 → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
35	28, 34	eqeltrid 2844	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ∈ Fin)
36		unfi 9102	. . . . . . . . 9 ⊢ (({-π, π, (𝐸‘𝑋)} ∈ Fin ∧ ((-π[,]π) ∖ dom 𝐺) ∈ Fin) → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
37	13, 35, 36	syl2anc 590	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
38	11, 37	eqeltrid 2844	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ Fin)
39		hashcl 14316	. . . . . . 7 ⊢ (𝐻 ∈ Fin → (♯‘𝐻) ∈ ℕ₀)
40	38, 39	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ₀)
41	40	nn0zd 12547	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
42	15, 22	ltneii 11257	. . . . . . 7 ⊢ -π ≠ π
43		hashprg 14355	. . . . . . . 8 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π ≠ π ↔ (♯‘{-π, π}) = 2))
44	15, 14, 43	mp2an 698	. . . . . . 7 ⊢ (-π ≠ π ↔ (♯‘{-π, π}) = 2)
45	42, 44	mpbi 231	. . . . . 6 ⊢ (♯‘{-π, π}) = 2
46	12	elexi 3455	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ V
47		ovex 7396	. . . . . . . . . . 11 ⊢ (-π[,]π) ∈ V
48		difexg 5264	. . . . . . . . . . 11 ⊢ ((-π[,]π) ∈ V → ((-π[,]π) ∖ dom 𝐺) ∈ V)
49	47, 48	ax-mp 5	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) ∈ V
50	46, 49	unex 7694	. . . . . . . . 9 ⊢ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ V
51	11, 50	eqeltri 2836	. . . . . . . 8 ⊢ 𝐻 ∈ V
52		negex 11389	. . . . . . . . . . 11 ⊢ -π ∈ V
53	52	tpid1 4707	. . . . . . . . . 10 ⊢ -π ∈ {-π, π, (𝐸‘𝑋)}
54	14	elexi 3455	. . . . . . . . . . 11 ⊢ π ∈ V
55	54	tpid2 4709	. . . . . . . . . 10 ⊢ π ∈ {-π, π, (𝐸‘𝑋)}
56		prssi 4759	. . . . . . . . . 10 ⊢ ((-π ∈ {-π, π, (𝐸‘𝑋)} ∧ π ∈ {-π, π, (𝐸‘𝑋)}) → {-π, π} ⊆ {-π, π, (𝐸‘𝑋)})
57	53, 55, 56	mp2an 698	. . . . . . . . 9 ⊢ {-π, π} ⊆ {-π, π, (𝐸‘𝑋)}
58		ssun1 4114	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
59	58, 11	sseqtrri 3971	. . . . . . . . 9 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ 𝐻
60	57, 59	sstri 3931	. . . . . . . 8 ⊢ {-π, π} ⊆ 𝐻
61		hashss 14369	. . . . . . . 8 ⊢ ((𝐻 ∈ V ∧ {-π, π} ⊆ 𝐻) → (♯‘{-π, π}) ≤ (♯‘𝐻))
62	51, 60, 61	mp2an 698	. . . . . . 7 ⊢ (♯‘{-π, π}) ≤ (♯‘𝐻)
63	62	a1i 11	. . . . . 6 ⊢ (𝜑 → (♯‘{-π, π}) ≤ (♯‘𝐻))
64	45, 63	eqbrtrrid 5115	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
65		eluz2 12792	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
66	10, 41, 64, 65	syl3anbrc 1350	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
67		uz2m1nn 12871	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
68	66, 67	syl 17	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
69	8, 68	eqeltrid 2844	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
70	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → -π ∈ ℝ)
71	14	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → π ∈ ℝ)
72		negpitopissre 26529	. . . . . . . . . . . 12 ⊢ (-π(,]π) ⊆ ℝ
73	22	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
74		picn 26447	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℂ
75	74	2timesi 12312	. . . . . . . . . . . . . . 15 ⊢ (2 · π) = (π + π)
76	74, 74	subnegi 11471	. . . . . . . . . . . . . . 15 ⊢ (π − -π) = (π + π)
77	75, 2, 76	3eqtr4i 2773	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (π − -π)
78		fourierdlem114.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
79	70, 71, 73, 77, 78	fourierdlem4 46561	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:ℝ⟶(-π(,]π))
80	79, 4	ffvelcdmd 7033	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π(,]π))
81	72, 80	sselid 3920	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
82	70, 71, 81	3jca 1134	. . . . . . . . . 10 ⊢ (𝜑 → (-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ))
83		fvex 6847	. . . . . . . . . . 11 ⊢ (𝐸‘𝑋) ∈ V
84	52, 54, 83	tpss 4775	. . . . . . . . . 10 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ) ↔ {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
85	82, 84	sylib 219	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
86		iccssre 13380	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
87	15, 14, 86	mp2an 698	. . . . . . . . . 10 ⊢ (-π[,]π) ⊆ ℝ
88		ssdifss 4077	. . . . . . . . . 10 ⊢ ((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
89	87, 88	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
90	85, 89	unssd 4128	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ ℝ)
91	11, 90	eqsstrid 3960	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
92		fourierdlem114.q	. . . . . . 7 ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻))
93	38, 91, 92, 8	fourierdlem36 46593	. . . . . 6 ⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻))
94		isof1o 7274	. . . . . 6 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–1-1-onto→𝐻)
95		f1of 6774	. . . . . 6 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)⟶𝐻)
96	93, 94, 95	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻)
97	96, 91	fssd 6679	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
98		reex 11127	. . . . 5 ⊢ ℝ ∈ V
99		ovex 7396	. . . . 5 ⊢ (0...𝑀) ∈ V
100	98, 99	elmap 8816	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ)
101	97, 100	sylibr 235	. . 3 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
102		fveq2 6834	. . . . . . . . . . 11 ⊢ (0 = 𝑖 → (𝑄‘0) = (𝑄‘𝑖))
103	102	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) = (𝑄‘𝑖))
104	97	ffvelcdmda 7032	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
105	104	leidd 11714	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
106	105	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
107	103, 106	eqbrtrd 5101	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
108		elfzelz 13476	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
109	108	zred 12631	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
110	109	ad2antlr 733	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ∈ ℝ)
111		elfzle1 13479	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
112	111	ad2antlr 733	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 ≤ 𝑖)
113		neqne 2943	. . . . . . . . . . . . 13 ⊢ (¬ 0 = 𝑖 → 0 ≠ 𝑖)
114	113	necomd 2990	. . . . . . . . . . . 12 ⊢ (¬ 0 = 𝑖 → 𝑖 ≠ 0)
115	114	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ≠ 0)
116	110, 112, 115	ne0gt0d 11281	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 < 𝑖)
117		nnssnn0 12438	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℕ₀
118		nn0uz 12824	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ = (ℤ_≥‘0)
119	117, 118	sseqtri 3970	. . . . . . . . . . . . . . . 16 ⊢ ℕ ⊆ (ℤ_≥‘0)
120	119, 69	sselid 3920	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
121		eluzfz1 13483	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
122	120, 121	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑀))
123	96, 122	ffvelcdmd 7033	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘0) ∈ 𝐻)
124	91, 123	sseldd 3923	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
125	124	ad2antrr 732	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ∈ ℝ)
126	104	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘𝑖) ∈ ℝ)
127		simpr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 0 < 𝑖)
128	93	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
129	122	anim1i 621	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀)))
130	129	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀)))
131		isorel 7277	. . . . . . . . . . . . 13 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖)))
132	128, 130, 131	syl2anc 590	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖)))
133	127, 132	mpbid 233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) < (𝑄‘𝑖))
134	125, 126, 133	ltled 11292	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
135	116, 134	syldan 597	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
136	107, 135	pm2.61dan 818	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
137	136	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ (𝑄‘𝑖))
138		simpr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘𝑖) = -π)
139	137, 138	breqtrd 5105	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ -π)
140	70	rexrd 11193	. . . . . . . 8 ⊢ (𝜑 → -π ∈ ℝ^*)
141	71	rexrd 11193	. . . . . . . 8 ⊢ (𝜑 → π ∈ ℝ^*)
142		lbicc2 13415	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → -π ∈ (-π[,]π))
143	16, 17, 23, 142	mp3an 1469	. . . . . . . . . . . . 13 ⊢ -π ∈ (-π[,]π)
144	143	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -π ∈ (-π[,]π))
145		ubicc2 13416	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → π ∈ (-π[,]π))
146	16, 17, 23, 145	mp3an 1469	. . . . . . . . . . . . 13 ⊢ π ∈ (-π[,]π)
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → π ∈ (-π[,]π))
148		iocssicc 13388	. . . . . . . . . . . . 13 ⊢ (-π(,]π) ⊆ (-π[,]π)
149	148, 80	sselid 3920	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π[,]π))
150		tpssi 4776	. . . . . . . . . . . 12 ⊢ ((-π ∈ (-π[,]π) ∧ π ∈ (-π[,]π) ∧ (𝐸‘𝑋) ∈ (-π[,]π)) → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
151	144, 147, 149, 150	syl3anc 1379	. . . . . . . . . . 11 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
152		difssd 4074	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ (-π[,]π))
153	151, 152	unssd 4128	. . . . . . . . . 10 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ (-π[,]π))
154	11, 153	eqsstrid 3960	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ (-π[,]π))
155	154, 123	sseldd 3923	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ (-π[,]π))
156		iccgelb 13353	. . . . . . . 8 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘0) ∈ (-π[,]π)) → -π ≤ (𝑄‘0))
157	140, 141, 155, 156	syl3anc 1379	. . . . . . 7 ⊢ (𝜑 → -π ≤ (𝑄‘0))
158	157	ad2antrr 732	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ≤ (𝑄‘0))
159	124	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ∈ ℝ)
160	15	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ∈ ℝ)
161	159, 160	letri3d 11286	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → ((𝑄‘0) = -π ↔ ((𝑄‘0) ≤ -π ∧ -π ≤ (𝑄‘0))))
162	139, 158, 161	mpbir2and 719	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) = -π)
163	59, 53	sselii 3919	. . . . . . 7 ⊢ -π ∈ 𝐻
164		f1ofo 6781	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)–onto→𝐻)
165	94, 164	syl 17	. . . . . . . 8 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–onto→𝐻)
166		forn 6749	. . . . . . . 8 ⊢ (𝑄:(0...𝑀)–onto→𝐻 → ran 𝑄 = 𝐻)
167	93, 165, 166	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran 𝑄 = 𝐻)
168	163, 167	eleqtrrid 2847	. . . . . 6 ⊢ (𝜑 → -π ∈ ran 𝑄)
169		ffn 6662	. . . . . . 7 ⊢ (𝑄:(0...𝑀)⟶𝐻 → 𝑄 Fn (0...𝑀))
170		fvelrnb 6894	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → (-π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π))
171	96, 169, 170	3syl 18	. . . . . 6 ⊢ (𝜑 → (-π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π))
172	168, 171	mpbid 233	. . . . 5 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π)
173	162, 172	r19.29a 3148	. . . 4 ⊢ (𝜑 → (𝑄‘0) = -π)
174	59, 55	sselii 3919	. . . . . . 7 ⊢ π ∈ 𝐻
175	174, 167	eleqtrrid 2847	. . . . . 6 ⊢ (𝜑 → π ∈ ran 𝑄)
176		fvelrnb 6894	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π))
177	96, 169, 176	3syl 18	. . . . . 6 ⊢ (𝜑 → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π))
178	175, 177	mpbid 233	. . . . 5 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π)
179	96, 154	fssd 6679	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
180		eluzfz2 13484	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
181	120, 180	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
182	179, 181	ffvelcdmd 7033	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ (-π[,]π))
183		iccleub 13352	. . . . . . . . 9 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘𝑀) ∈ (-π[,]π)) → (𝑄‘𝑀) ≤ π)
184	140, 141, 182, 183	syl3anc 1379	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘𝑀) ≤ π)
185	184	3ad2ant1 1139	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ≤ π)
186		id 22	. . . . . . . . . 10 ⊢ ((𝑄‘𝑖) = π → (𝑄‘𝑖) = π)
187	186	eqcomd 2746	. . . . . . . . 9 ⊢ ((𝑄‘𝑖) = π → π = (𝑄‘𝑖))
188	187	3ad2ant3 1141	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π = (𝑄‘𝑖))
189	105	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
190		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
191	190	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) = (𝑄‘𝑀))
192	189, 191	breqtrd 5105	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
193	109	ad2antlr 733	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ∈ ℝ)
194		elfzel2 13474	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
195	194	zred 12631	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
196	195	ad2antlr 733	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ∈ ℝ)
197		elfzle2 13480	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
198	197	ad2antlr 733	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ≤ 𝑀)
199		neqne 2943	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑖 = 𝑀 → 𝑖 ≠ 𝑀)
200	199	necomd 2990	. . . . . . . . . . . . 13 ⊢ (¬ 𝑖 = 𝑀 → 𝑀 ≠ 𝑖)
201	200	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ≠ 𝑖)
202	193, 196, 198, 201	leneltd 11298	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 < 𝑀)
203	104	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ∈ ℝ)
204	87, 182	sselid 3920	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
205	204	ad2antrr 732	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑀) ∈ ℝ)
206		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑖 < 𝑀)
207	93	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
208		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
209	181	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (0...𝑀))
210	208, 209	jca 516	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)))
211	210	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)))
212		isorel 7277	. . . . . . . . . . . . . 14 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀))) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀)))
213	207, 211, 212	syl2anc 590	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀)))
214	206, 213	mpbid 233	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) < (𝑄‘𝑀))
215	203, 205, 214	ltled 11292	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
216	202, 215	syldan 597	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
217	192, 216	pm2.61dan 818	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
218	217	3adant3 1138	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
219	188, 218	eqbrtrd 5101	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ≤ (𝑄‘𝑀))
220	204	3ad2ant1 1139	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ∈ ℝ)
221	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ∈ ℝ)
222	220, 221	letri3d 11286	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → ((𝑄‘𝑀) = π ↔ ((𝑄‘𝑀) ≤ π ∧ π ≤ (𝑄‘𝑀))))
223	185, 219, 222	mpbir2and 719	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) = π)
224	223	rexlimdv3a 3145	. . . . 5 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π → (𝑄‘𝑀) = π))
225	178, 224	mpd 15	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = π)
226		elfzoelz 13611	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
227	226	zred 12631	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
228	227	ltp1d 12084	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
229	228	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 < (𝑖 + 1))
230		elfzofz 13628	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
231		fzofzp1 13717	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
232	230, 231	jca 516	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀)))
233		isorel 7277	. . . . . . 7 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀))) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
234	93, 232, 233	syl2an 602	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
235	229, 234	mpbid 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
236	235	ralrimiva 3132	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
237	173, 225, 236	jca31 519	. . 3 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
238	7	fourierdlem2 46559	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
239	69, 238	syl 17	. . 3 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
240	101, 237, 239	mpbir2and 719	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
241		fourierdlem114.g	. . . . 5 ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π))
242	241	reseq1i 5934	. . . 4 ⊢ (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
243	16	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ^*)
244	17	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈ ℝ^*)
245	179	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
246		simpr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
247	243, 244, 245, 246	fourierdlem27 46584	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π(,)π))
248	247	resabs1d 5967	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
249	242, 248	eqtr2id 2788	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
250		fourierdlem114.gcn	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
251	250, 7, 69, 240, 11, 167	fourierdlem38 46595	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
252	249, 251	eqeltrd 2840	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
253	249	oveq1d 7378	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
254	250	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺 ∈ (dom 𝐺–cn→ℂ))
255		fourierdlem114.rlim	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
256	255	adantlr 721	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
257		fourierdlem114.llim	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
258	257	adantlr 721	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
259	93	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
260	259, 94, 95	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶𝐻)
261	81	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐸‘𝑋) ∈ ℝ)
262	259, 165, 166	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran 𝑄 = 𝐻)
263	254, 256, 258, 259, 260, 246, 235, 247, 261, 11, 262	fourierdlem46 46602	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅ ∧ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅))
264	263	simpld 495	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
265	253, 264	eqnetrd 3002	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
266	249	oveq1d 7378	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
267	263	simprd 496	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
268	266, 267	eqnetrd 3002	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
269		fourierdlem114.a	. 2 ⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
270		fourierdlem114.b	. 2 ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
271		fourierdlem114.s	. 2 ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
272	83	tpid3 4712	. . . . 5 ⊢ (𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)}
273		elun1 4118	. . . . 5 ⊢ ((𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)} → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))
274	272, 273	mp1i 13	. . . 4 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))
275	274, 11	eleqtrrdi 2851	. . 3 ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐻)
276	275, 167	eleqtrrd 2843	. 2 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄)
277	1, 2, 3, 4, 5, 6, 7, 69, 240, 252, 265, 268, 269, 270, 271, 78, 276	fourierdlem113 46669	1 ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2935 ∀wral 3054 ∃wrex 3064 {crab 3392 Vcvv 3432 ∖ cdif 3887 ∪ cun 3888 ⊆ wss 3890 ∅c0 4268 {cpr 4564 {ctp 4566 class class class wbr 5079 ↦ cmpt 5160 dom cdm 5625 ran crn 5626 ↾ cres 5627 ℩cio 6446 Fn wfn 6487 ⟶wf 6488 –onto→wfo 6490 –1-1-onto→wf1o 6491 ‘cfv 6492 Isom wiso 6493 (class class class)co 7363 ↑_m cmap 8770 Fincfn 8890 ℂcc 11034 ℝcr 11035 0cc0 11036 1c1 11037 + caddc 11039 · cmul 11041 +∞cpnf 11174 -∞cmnf 11175 ℝ^*cxr 11176 < clt 11177 ≤ cle 11178 − cmin 11375 -cneg 11376 / cdiv 11805 ℕcn 12172 2c2 12234 ℕ₀cn0 12435 ℤcz 12522 ℤ_≥cuz 12786 (,)cioo 13296 (,]cioc 13297 [,)cico 13298 [,]cicc 13299 ...cfz 13459 ..^cfzo 13606 ⌊cfl 13747 seqcseq 13961 ♯chash 14290 ⇝ cli 15444 Σcsu 15646 sincsin 16026 cosccos 16027 πcpi 16029 –cn→ccncf 24868 ∫citg 25610 lim_ℂ climc 25854 D cdv 25855

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-inf2 9560 ax-cc 10355 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113 ax-pre-sup 11114 ax-addf 11115

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-symdif 4188 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4846 df-int 4885 df-iun 4930 df-iin 4931 df-disj 5047 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-of 7627 df-ofr 7628 df-om 7814 df-1st 7938 df-2nd 7939 df-supp 8108 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-2o 8403 df-oadd 8406 df-omul 8407 df-er 8640 df-map 8772 df-pm 8773 df-ixp 8843 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-fsupp 9272 df-fi 9321 df-sup 9352 df-inf 9353 df-oi 9422 df-dju 9823 df-card 9861 df-acn 9864 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-div 11806 df-nn 12173 df-2 12242 df-3 12243 df-4 12244 df-5 12245 df-6 12246 df-7 12247 df-8 12248 df-9 12249 df-n0 12436 df-xnn0 12509 df-z 12523 df-dec 12643 df-uz 12787 df-q 12897 df-rp 12941 df-xneg 13061 df-xadd 13062 df-xmul 13063 df-ioo 13300 df-ioc 13301 df-ico 13302 df-icc 13303 df-fz 13460 df-fzo 13607 df-fl 13749 df-mod 13827 df-seq 13962 df-exp 14022 df-fac 14234 df-bc 14263 df-hash 14291 df-shft 15027 df-cj 15059 df-re 15060 df-im 15061 df-sqrt 15195 df-abs 15196 df-limsup 15431 df-clim 15448 df-rlim 15449 df-sum 15647 df-ef 16030 df-sin 16032 df-cos 16033 df-pi 16035 df-struct 17115 df-sets 17132 df-slot 17150 df-ndx 17162 df-base 17178 df-ress 17199 df-plusg 17231 df-mulr 17232 df-starv 17233 df-sca 17234 df-vsca 17235 df-ip 17236 df-tset 17237 df-ple 17238 df-ds 17240 df-unif 17241 df-hom 17242 df-cco 17243 df-rest 17383 df-topn 17384 df-0g 17402 df-gsum 17403 df-topgen 17404 df-pt 17405 df-prds 17408 df-xrs 17464 df-qtop 17469 df-imas 17470 df-xps 17472 df-mre 17546 df-mrc 17547 df-acs 17549 df-mgm 18606 df-sgrp 18685 df-mnd 18701 df-submnd 18750 df-mulg 19042 df-cntz 19290 df-cmn 19755 df-psmet 21346 df-xmet 21347 df-met 21348 df-bl 21349 df-mopn 21350 df-fbas 21351 df-fg 21352 df-cnfld 21355 df-top 22884 df-topon 22901 df-topsp 22923 df-bases 22936 df-cld 23009 df-ntr 23010 df-cls 23011 df-nei 23088 df-lp 23126 df-perf 23127 df-cn 23217 df-cnp 23218 df-t1 23304 df-haus 23305 df-cmp 23377 df-tx 23552 df-hmeo 23745 df-fil 23836 df-fm 23928 df-flim 23929 df-flf 23930 df-xms 24310 df-ms 24311 df-tms 24312 df-cncf 24870 df-ovol 25456 df-vol 25457 df-mbf 25611 df-itg1 25612 df-itg2 25613 df-ibl 25614 df-itg 25615 df-0p 25662 df-ditg 25839 df-limc 25858 df-dv 25859

This theorem is referenced by: fourierdlem115 46671

W3C validator