fourierdlem102 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem102 41870

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

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

**Assertion**
Ref	Expression
fourierdlem102	⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ≠ ∅))

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

**Proof of Theorem fourierdlem102**
Step	Hyp	Ref	Expression
1		fourierdlem102.f	. 2 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
2		fourierdlem102.t	. 2 ⊢ 𝑇 = (2 · π)
3		fourierdlem102.per	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
4		fourierdlem102.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℝ)
5		fourierdlem102.p	. 2 ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
6		fourierdlem102.m	. . 3 ⊢ 𝑀 = ((♯‘𝐻) − 1)
7		2z 11820	. . . . . 6 ⊢ 2 ∈ ℤ
8	7	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
9		fourierdlem102.h	. . . . . . . 8 ⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
10		tpfi 8581	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ Fin
11	10	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ∈ Fin)
12		pire 24737	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ
13	12	renegcli 10740	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
14	13	rexri 10491	. . . . . . . . . . . . 13 ⊢ -π ∈ ℝ^*
15	12	rexri 10491	. . . . . . . . . . . . 13 ⊢ π ∈ ℝ^*
16		negpilt0 40921	. . . . . . . . . . . . . . 15 ⊢ -π < 0
17		pipos 24739	. . . . . . . . . . . . . . 15 ⊢ 0 < π
18		0re 10433	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
19	13, 18, 12	lttri 10558	. . . . . . . . . . . . . . 15 ⊢ ((-π < 0 ∧ 0 < π) → -π < π)
20	16, 17, 19	mp2an 679	. . . . . . . . . . . . . 14 ⊢ -π < π
21	13, 12, 20	ltleii 10555	. . . . . . . . . . . . 13 ⊢ -π ≤ π
22		prunioo 12676	. . . . . . . . . . . . 13 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → ((-π(,)π) ∪ {-π, π}) = (-π[,]π))
23	14, 15, 21, 22	mp3an 1440	. . . . . . . . . . . 12 ⊢ ((-π(,)π) ∪ {-π, π}) = (-π[,]π)
24	23	difeq1i 3981	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = ((-π[,]π) ∖ dom 𝐺)
25		difundir 4139	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
26	24, 25	eqtr3i 2798	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
27		fourierdlem102.dmdv	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin)
28		prfi 8580	. . . . . . . . . . . 12 ⊢ {-π, π} ∈ Fin
29		diffi 8537	. . . . . . . . . . . 12 ⊢ ({-π, π} ∈ Fin → ({-π, π} ∖ dom 𝐺) ∈ Fin)
30	28, 29	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → ({-π, π} ∖ dom 𝐺) ∈ Fin)
31		unfi 8572	. . . . . . . . . . 11 ⊢ ((((-π(,)π) ∖ dom 𝐺) ∈ Fin ∧ ({-π, π} ∖ dom 𝐺) ∈ Fin) → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
32	27, 30, 31	syl2anc 576	. . . . . . . . . 10 ⊢ (𝜑 → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
33	26, 32	syl5eqel 2864	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ∈ Fin)
34		unfi 8572	. . . . . . . . 9 ⊢ (({-π, π, (𝐸‘𝑋)} ∈ Fin ∧ ((-π[,]π) ∖ dom 𝐺) ∈ Fin) → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
35	11, 33, 34	syl2anc 576	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
36	9, 35	syl5eqel 2864	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ Fin)
37		hashcl 13525	. . . . . . 7 ⊢ (𝐻 ∈ Fin → (♯‘𝐻) ∈ ℕ₀)
38	36, 37	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ₀)
39	38	nn0zd 11891	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
40	13, 20	ltneii 10545	. . . . . . 7 ⊢ -π ≠ π
41		hashprg 13560	. . . . . . . 8 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π ≠ π ↔ (♯‘{-π, π}) = 2))
42	13, 12, 41	mp2an 679	. . . . . . 7 ⊢ (-π ≠ π ↔ (♯‘{-π, π}) = 2)
43	40, 42	mpbi 222	. . . . . 6 ⊢ (♯‘{-π, π}) = 2
44	10	elexi 3428	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ V
45		ovex 7002	. . . . . . . . . . 11 ⊢ (-π[,]π) ∈ V
46		difexg 5081	. . . . . . . . . . 11 ⊢ ((-π[,]π) ∈ V → ((-π[,]π) ∖ dom 𝐺) ∈ V)
47	45, 46	ax-mp 5	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) ∈ V
48	44, 47	unex 7280	. . . . . . . . 9 ⊢ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ V
49	9, 48	eqeltri 2856	. . . . . . . 8 ⊢ 𝐻 ∈ V
50		negex 10676	. . . . . . . . . . 11 ⊢ -π ∈ V
51	50	tpid1 4572	. . . . . . . . . 10 ⊢ -π ∈ {-π, π, (𝐸‘𝑋)}
52	12	elexi 3428	. . . . . . . . . . 11 ⊢ π ∈ V
53	52	tpid2 4574	. . . . . . . . . 10 ⊢ π ∈ {-π, π, (𝐸‘𝑋)}
54		prssi 4622	. . . . . . . . . 10 ⊢ ((-π ∈ {-π, π, (𝐸‘𝑋)} ∧ π ∈ {-π, π, (𝐸‘𝑋)}) → {-π, π} ⊆ {-π, π, (𝐸‘𝑋)})
55	51, 53, 54	mp2an 679	. . . . . . . . 9 ⊢ {-π, π} ⊆ {-π, π, (𝐸‘𝑋)}
56		ssun1 4033	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
57	56, 9	sseqtr4i 3890	. . . . . . . . 9 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ 𝐻
58	55, 57	sstri 3863	. . . . . . . 8 ⊢ {-π, π} ⊆ 𝐻
59		hashss 13574	. . . . . . . 8 ⊢ ((𝐻 ∈ V ∧ {-π, π} ⊆ 𝐻) → (♯‘{-π, π}) ≤ (♯‘𝐻))
60	49, 58, 59	mp2an 679	. . . . . . 7 ⊢ (♯‘{-π, π}) ≤ (♯‘𝐻)
61	60	a1i 11	. . . . . 6 ⊢ (𝜑 → (♯‘{-π, π}) ≤ (♯‘𝐻))
62	43, 61	syl5eqbrr 4959	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
63		eluz2 12057	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
64	8, 39, 62, 63	syl3anbrc 1323	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
65		uz2m1nn 12130	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
66	64, 65	syl 17	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
67	6, 66	syl5eqel 2864	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
68	13	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → -π ∈ ℝ)
69	12	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → π ∈ ℝ)
70		negpitopissre 24815	. . . . . . . . . . . 12 ⊢ (-π(,]π) ⊆ ℝ
71	20	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
72		picn 24738	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℂ
73	72	2timesi 11578	. . . . . . . . . . . . . . 15 ⊢ (2 · π) = (π + π)
74	72, 72	subnegi 10758	. . . . . . . . . . . . . . 15 ⊢ (π − -π) = (π + π)
75	73, 2, 74	3eqtr4i 2806	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (π − -π)
76		fourierdlem102.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
77	68, 69, 71, 75, 76	fourierdlem4 41773	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:ℝ⟶(-π(,]π))
78	77, 4	ffvelrnd 6671	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π(,]π))
79	70, 78	sseldi 3852	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
80	68, 69, 79	3jca 1108	. . . . . . . . . 10 ⊢ (𝜑 → (-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ))
81		fvex 6506	. . . . . . . . . . 11 ⊢ (𝐸‘𝑋) ∈ V
82	50, 52, 81	tpss 4636	. . . . . . . . . 10 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ) ↔ {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
83	80, 82	sylib 210	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
84		iccssre 12627	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
85	13, 12, 84	mp2an 679	. . . . . . . . . 10 ⊢ (-π[,]π) ⊆ ℝ
86		ssdifss 3998	. . . . . . . . . 10 ⊢ ((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
87	85, 86	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
88	83, 87	unssd 4046	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ ℝ)
89	9, 88	syl5eqss 3901	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
90		fourierdlem102.q	. . . . . . 7 ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻))
91	36, 89, 90, 6	fourierdlem36 41805	. . . . . 6 ⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻))
92		isof1o 6893	. . . . . 6 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–1-1-onto→𝐻)
93		f1of 6438	. . . . . 6 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)⟶𝐻)
94	91, 92, 93	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻)
95	94, 89	fssd 6352	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
96		reex 10418	. . . . 5 ⊢ ℝ ∈ V
97		ovex 7002	. . . . 5 ⊢ (0...𝑀) ∈ V
98	96, 97	elmap 8227	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ)
99	95, 98	sylibr 226	. . 3 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)))
100		fveq2 6493	. . . . . . . . . . 11 ⊢ (0 = 𝑖 → (𝑄‘0) = (𝑄‘𝑖))
101	100	adantl 474	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) = (𝑄‘𝑖))
102	95	ffvelrnda 6670	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
103	102	leidd 10999	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
104	103	adantr 473	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
105	101, 104	eqbrtrd 4945	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
106		elfzelz 12717	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
107	106	zred 11893	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
108	107	ad2antlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ∈ ℝ)
109		elfzle1 12719	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
110	109	ad2antlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 ≤ 𝑖)
111		neqne 2969	. . . . . . . . . . . . 13 ⊢ (¬ 0 = 𝑖 → 0 ≠ 𝑖)
112	111	necomd 3016	. . . . . . . . . . . 12 ⊢ (¬ 0 = 𝑖 → 𝑖 ≠ 0)
113	112	adantl 474	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ≠ 0)
114	108, 110, 113	ne0gt0d 10569	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 < 𝑖)
115		nnssnn0 11703	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℕ₀
116		nn0uz 12087	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ = (ℤ_≥‘0)
117	115, 116	sseqtri 3889	. . . . . . . . . . . . . . . 16 ⊢ ℕ ⊆ (ℤ_≥‘0)
118	117, 67	sseldi 3852	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
119		eluzfz1 12723	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
120	118, 119	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑀))
121	94, 120	ffvelrnd 6671	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘0) ∈ 𝐻)
122	89, 121	sseldd 3855	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
123	122	ad2antrr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ∈ ℝ)
124	102	adantr 473	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘𝑖) ∈ ℝ)
125		simpr 477	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 0 < 𝑖)
126	91	ad2antrr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
127	120	anim1i 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀)))
128	127	adantr 473	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀)))
129		isorel 6896	. . . . . . . . . . . . 13 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖)))
130	126, 128, 129	syl2anc 576	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖)))
131	125, 130	mpbid 224	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) < (𝑄‘𝑖))
132	123, 124, 131	ltled 10580	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
133	114, 132	syldan 582	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
134	105, 133	pm2.61dan 800	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
135	134	adantr 473	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ (𝑄‘𝑖))
136		simpr 477	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘𝑖) = -π)
137	135, 136	breqtrd 4949	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ -π)
138	68	rexrd 10482	. . . . . . . 8 ⊢ (𝜑 → -π ∈ ℝ^*)
139	69	rexrd 10482	. . . . . . . 8 ⊢ (𝜑 → π ∈ ℝ^*)
140		lbicc2 12661	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → -π ∈ (-π[,]π))
141	14, 15, 21, 140	mp3an 1440	. . . . . . . . . . . . 13 ⊢ -π ∈ (-π[,]π)
142	141	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -π ∈ (-π[,]π))
143		ubicc2 12662	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → π ∈ (-π[,]π))
144	14, 15, 21, 143	mp3an 1440	. . . . . . . . . . . . 13 ⊢ π ∈ (-π[,]π)
145	144	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → π ∈ (-π[,]π))
146		iocssicc 12634	. . . . . . . . . . . . 13 ⊢ (-π(,]π) ⊆ (-π[,]π)
147	146, 78	sseldi 3852	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π[,]π))
148		tpssi 4637	. . . . . . . . . . . 12 ⊢ ((-π ∈ (-π[,]π) ∧ π ∈ (-π[,]π) ∧ (𝐸‘𝑋) ∈ (-π[,]π)) → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
149	142, 145, 147, 148	syl3anc 1351	. . . . . . . . . . 11 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
150		difssd 3995	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ (-π[,]π))
151	149, 150	unssd 4046	. . . . . . . . . 10 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ (-π[,]π))
152	9, 151	syl5eqss 3901	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ (-π[,]π))
153	152, 121	sseldd 3855	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ (-π[,]π))
154		iccgelb 12602	. . . . . . . 8 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘0) ∈ (-π[,]π)) → -π ≤ (𝑄‘0))
155	138, 139, 153, 154	syl3anc 1351	. . . . . . 7 ⊢ (𝜑 → -π ≤ (𝑄‘0))
156	155	ad2antrr 713	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ≤ (𝑄‘0))
157	122	ad2antrr 713	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ∈ ℝ)
158	13	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ∈ ℝ)
159	157, 158	letri3d 10574	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → ((𝑄‘0) = -π ↔ ((𝑄‘0) ≤ -π ∧ -π ≤ (𝑄‘0))))
160	137, 156, 159	mpbir2and 700	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) = -π)
161	57, 51	sselii 3851	. . . . . . 7 ⊢ -π ∈ 𝐻
162		f1ofo 6445	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)–onto→𝐻)
163	92, 162	syl 17	. . . . . . . 8 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–onto→𝐻)
164		forn 6416	. . . . . . . 8 ⊢ (𝑄:(0...𝑀)–onto→𝐻 → ran 𝑄 = 𝐻)
165	91, 163, 164	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran 𝑄 = 𝐻)
166	161, 165	syl5eleqr 2867	. . . . . 6 ⊢ (𝜑 → -π ∈ ran 𝑄)
167		ffn 6338	. . . . . . 7 ⊢ (𝑄:(0...𝑀)⟶𝐻 → 𝑄 Fn (0...𝑀))
168		fvelrnb 6550	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → (-π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π))
169	94, 167, 168	3syl 18	. . . . . 6 ⊢ (𝜑 → (-π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π))
170	166, 169	mpbid 224	. . . . 5 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π)
171	160, 170	r19.29a 3228	. . . 4 ⊢ (𝜑 → (𝑄‘0) = -π)
172	57, 53	sselii 3851	. . . . . . 7 ⊢ π ∈ 𝐻
173	172, 165	syl5eleqr 2867	. . . . . 6 ⊢ (𝜑 → π ∈ ran 𝑄)
174		fvelrnb 6550	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π))
175	94, 167, 174	3syl 18	. . . . . 6 ⊢ (𝜑 → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π))
176	173, 175	mpbid 224	. . . . 5 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π)
177	94, 152	fssd 6352	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
178		eluzfz2 12724	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
179	118, 178	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
180	177, 179	ffvelrnd 6671	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ (-π[,]π))
181		iccleub 12601	. . . . . . . . 9 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘𝑀) ∈ (-π[,]π)) → (𝑄‘𝑀) ≤ π)
182	138, 139, 180, 181	syl3anc 1351	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘𝑀) ≤ π)
183	182	3ad2ant1 1113	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ≤ π)
184		id 22	. . . . . . . . . 10 ⊢ ((𝑄‘𝑖) = π → (𝑄‘𝑖) = π)
185	184	eqcomd 2778	. . . . . . . . 9 ⊢ ((𝑄‘𝑖) = π → π = (𝑄‘𝑖))
186	185	3ad2ant3 1115	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π = (𝑄‘𝑖))
187	103	adantr 473	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
188		fveq2 6493	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
189	188	adantl 474	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) = (𝑄‘𝑀))
190	187, 189	breqtrd 4949	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
191	107	ad2antlr 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ∈ ℝ)
192		elfzel2 12715	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
193	192	zred 11893	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
194	193	ad2antlr 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ∈ ℝ)
195		elfzle2 12720	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
196	195	ad2antlr 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ≤ 𝑀)
197		neqne 2969	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑖 = 𝑀 → 𝑖 ≠ 𝑀)
198	197	necomd 3016	. . . . . . . . . . . . 13 ⊢ (¬ 𝑖 = 𝑀 → 𝑀 ≠ 𝑖)
199	198	adantl 474	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ≠ 𝑖)
200	191, 194, 196, 199	leneltd 10586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 < 𝑀)
201	102	adantr 473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ∈ ℝ)
202	85, 180	sseldi 3852	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
203	202	ad2antrr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑀) ∈ ℝ)
204		simpr 477	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑖 < 𝑀)
205	91	ad2antrr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
206		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
207	179	adantr 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (0...𝑀))
208	206, 207	jca 504	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)))
209	208	adantr 473	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)))
210		isorel 6896	. . . . . . . . . . . . . 14 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀))) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀)))
211	205, 209, 210	syl2anc 576	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀)))
212	204, 211	mpbid 224	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) < (𝑄‘𝑀))
213	201, 203, 212	ltled 10580	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
214	200, 213	syldan 582	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
215	190, 214	pm2.61dan 800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
216	215	3adant3 1112	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
217	186, 216	eqbrtrd 4945	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ≤ (𝑄‘𝑀))
218	202	3ad2ant1 1113	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ∈ ℝ)
219	12	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ∈ ℝ)
220	218, 219	letri3d 10574	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → ((𝑄‘𝑀) = π ↔ ((𝑄‘𝑀) ≤ π ∧ π ≤ (𝑄‘𝑀))))
221	183, 217, 220	mpbir2and 700	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) = π)
222	221	rexlimdv3a 3225	. . . . 5 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π → (𝑄‘𝑀) = π))
223	176, 222	mpd 15	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = π)
224		elfzoelz 12847	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
225	224	zred 11893	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
226	225	ltp1d 11363	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
227	226	adantl 474	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 < (𝑖 + 1))
228		elfzofz 12862	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
229		fzofzp1 12942	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
230	228, 229	jca 504	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀)))
231		isorel 6896	. . . . . . 7 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀))) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
232	91, 230, 231	syl2an 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
233	227, 232	mpbid 224	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
234	233	ralrimiva 3126	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
235	171, 223, 234	jca31 507	. . 3 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
236	5	fourierdlem2 41771	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
237	67, 236	syl 17	. . 3 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
238	99, 235, 237	mpbir2and 700	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
239		fourierdlem102.g	. . . . 5 ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π))
240	239	reseq1i 5684	. . . 4 ⊢ (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
241	14	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ^*)
242	15	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈ ℝ^*)
243	177	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
244		simpr 477	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
245	241, 242, 243, 244	fourierdlem27 41796	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π(,)π))
246	245	resabs1d 5723	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
247	240, 246	syl5req 2821	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
248		fourierdlem102.gcn	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
249	248, 5, 67, 238, 9, 165	fourierdlem38 41807	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
250	247, 249	eqeltrd 2860	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
251	247	oveq1d 6985	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
252	248	adantr 473	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺 ∈ (dom 𝐺–cn→ℂ))
253		fourierdlem102.rlim	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
254	253	adantlr 702	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
255		fourierdlem102.llim	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
256	255	adantlr 702	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
257	91	adantr 473	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
258	257, 92, 93	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶𝐻)
259	79	adantr 473	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐸‘𝑋) ∈ ℝ)
260	257, 163, 164	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran 𝑄 = 𝐻)
261	252, 254, 256, 257, 258, 244, 233, 245, 259, 9, 260	fourierdlem46 41814	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅ ∧ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅))
262	261	simpld 487	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
263	251, 262	eqnetrd 3028	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
264	247	oveq1d 6985	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
265	261	simprd 488	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
266	264, 265	eqnetrd 3028	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
267	1, 2, 3, 4, 5, 67, 238, 250, 263, 266	fourierdlem94 41862	1 ⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ≠ ∅))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2048 ≠ wne 2961 ∀wral 3082 ∃wrex 3083 {crab 3086 Vcvv 3409 ∖ cdif 3822 ∪ cun 3823 ⊆ wss 3825 ∅c0 4173 {cpr 4437 {ctp 4439 class class class wbr 4923 ↦ cmpt 5002 dom cdm 5400 ran crn 5401 ↾ cres 5402 ℩cio 6144 Fn wfn 6177 ⟶wf 6178 –onto→wfo 6180 –1-1-onto→wf1o 6181 ‘cfv 6182 Isom wiso 6183 (class class class)co 6970 ↑_𝑚 cmap 8198 Fincfn 8298 ℂcc 10325 ℝcr 10326 0cc0 10327 1c1 10328 + caddc 10330 · cmul 10332 +∞cpnf 10463 -∞cmnf 10464 ℝ^*cxr 10465 < clt 10466 ≤ cle 10467 − cmin 10662 -cneg 10663 / cdiv 11090 ℕcn 11431 2c2 11488 ℕ₀cn0 11700 ℤcz 11786 ℤ_≥cuz 12051 (,)cioo 12547 (,]cioc 12548 [,)cico 12549 [,]cicc 12550 ...cfz 12701 ..^cfzo 12842 ⌊cfl 12968 ♯chash 13498 πcpi 15270 –cn→ccncf 23177 lim_ℂ climc 24153 D cdv 24154

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-inf2 8890 ax-cnex 10383 ax-resscn 10384 ax-1cn 10385 ax-icn 10386 ax-addcl 10387 ax-addrcl 10388 ax-mulcl 10389 ax-mulrcl 10390 ax-mulcom 10391 ax-addass 10392 ax-mulass 10393 ax-distr 10394 ax-i2m1 10395 ax-1ne0 10396 ax-1rid 10397 ax-rnegex 10398 ax-rrecex 10399 ax-cnre 10400 ax-pre-lttri 10401 ax-pre-lttrn 10402 ax-pre-ltadd 10403 ax-pre-mulgt0 10404 ax-pre-sup 10405 ax-addf 10406 ax-mulf 10407

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-pss 3841 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-iin 4789 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5305 df-eprel 5310 df-po 5319 df-so 5320 df-fr 5359 df-se 5360 df-we 5361 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-isom 6191 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-of 7221 df-om 7391 df-1st 7494 df-2nd 7495 df-supp 7627 df-wrecs 7743 df-recs 7805 df-rdg 7843 df-1o 7897 df-2o 7898 df-oadd 7901 df-er 8081 df-map 8200 df-pm 8201 df-ixp 8252 df-en 8299 df-dom 8300 df-sdom 8301 df-fin 8302 df-fsupp 8621 df-fi 8662 df-sup 8693 df-inf 8694 df-oi 8761 df-dju 9116 df-card 9154 df-cda 9380 df-pnf 10468 df-mnf 10469 df-xr 10470 df-ltxr 10471 df-le 10472 df-sub 10664 df-neg 10665 df-div 11091 df-nn 11432 df-2 11496 df-3 11497 df-4 11498 df-5 11499 df-6 11500 df-7 11501 df-8 11502 df-9 11503 df-n0 11701 df-xnn0 11773 df-z 11787 df-dec 11905 df-uz 12052 df-q 12156 df-rp 12198 df-xneg 12317 df-xadd 12318 df-xmul 12319 df-ioo 12551 df-ioc 12552 df-ico 12553 df-icc 12554 df-fz 12702 df-fzo 12843 df-fl 12970 df-seq 13178 df-exp 13238 df-fac 13442 df-bc 13471 df-hash 13499 df-shft 14277 df-cj 14309 df-re 14310 df-im 14311 df-sqrt 14445 df-abs 14446 df-limsup 14679 df-clim 14696 df-rlim 14697 df-sum 14894 df-ef 15271 df-sin 15273 df-cos 15274 df-pi 15276 df-struct 16331 df-ndx 16332 df-slot 16333 df-base 16335 df-sets 16336 df-ress 16337 df-plusg 16424 df-mulr 16425 df-starv 16426 df-sca 16427 df-vsca 16428 df-ip 16429 df-tset 16430 df-ple 16431 df-ds 16433 df-unif 16434 df-hom 16435 df-cco 16436 df-rest 16542 df-topn 16543 df-0g 16561 df-gsum 16562 df-topgen 16563 df-pt 16564 df-prds 16567 df-xrs 16621 df-qtop 16626 df-imas 16627 df-xps 16629 df-mre 16705 df-mrc 16706 df-acs 16708 df-mgm 17700 df-sgrp 17742 df-mnd 17753 df-submnd 17794 df-mulg 18002 df-cntz 18208 df-cmn 18658 df-psmet 20229 df-xmet 20230 df-met 20231 df-bl 20232 df-mopn 20233 df-fbas 20234 df-fg 20235 df-cnfld 20238 df-top 21196 df-topon 21213 df-topsp 21235 df-bases 21248 df-cld 21321 df-ntr 21322 df-cls 21323 df-nei 21400 df-lp 21438 df-perf 21439 df-cn 21529 df-cnp 21530 df-haus 21617 df-cmp 21689 df-tx 21864 df-hmeo 22057 df-fil 22148 df-fm 22240 df-flim 22241 df-flf 22242 df-xms 22623 df-ms 22624 df-tms 22625 df-cncf 23179 df-limc 24157 df-dv 24158

This theorem is referenced by: fourierdlem106 41874

W3C validator