fourierdlem75 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem75 47160

Description: Given a piecewise smooth function 𝐹, the derived function 𝐻 has a limit at the lower bound of each interval of the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem75.xre	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem75.p	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem75.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem75.x	⊢ (𝜑 → 𝑋 ∈ ran 𝑉)
fourierdlem75.y	⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
fourierdlem75.w	⊢ (𝜑 → 𝑊 ∈ ℝ)
fourierdlem75.h	⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
fourierdlem75.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem75.v	⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
fourierdlem75.r	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
fourierdlem75.q	⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
fourierdlem75.o	⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem75.g	⊢ 𝐺 = (ℝ D 𝐹)
fourierdlem75.gcn	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ)
fourierdlem75.e	⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
fourierdlem75.a	⊢ 𝐴 = if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)))

**Assertion**
Ref	Expression
fourierdlem75	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))

Distinct variable groups: 𝐸,𝑠 𝐹,𝑠 𝐻,𝑠 𝑖,𝑀,𝑚,𝑝 𝑀,𝑠,𝑖 𝑄,𝑖,𝑝 𝑄,𝑠 𝑅,𝑠 𝑖,𝑉,𝑝 𝑉,𝑠 𝑊,𝑠 𝑖,𝑋,𝑚,𝑝 𝑋,𝑠 𝑌,𝑠 𝜑,𝑖,𝑠 Allowed substitution hints: 𝜑(𝑚, 𝑝) 𝐴(𝑖, 𝑚, 𝑠, 𝑝) 𝑃(𝑖, 𝑚, 𝑠, 𝑝) 𝑄(𝑚) 𝑅(𝑖, 𝑚, 𝑝) 𝐸(𝑖, 𝑚, 𝑝) 𝐹(𝑖, 𝑚, 𝑝) 𝐺(𝑖, 𝑚, 𝑠, 𝑝) 𝐻(𝑖, 𝑚, 𝑝) 𝑂(𝑖, 𝑚, 𝑠, 𝑝) 𝑉(𝑚) 𝑊(𝑖, 𝑚, 𝑝) 𝑌(𝑖, 𝑚, 𝑝)

Proof of Theorem fourierdlem75 Dummy variables 𝑥 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem75.xre	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℝ)
2	1	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 ∈ ℝ)
3		fourierdlem75.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
4		fourierdlem75.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ)
5		fourierdlem75.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
6	5	fourierdlem2 47088	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
7	4, 6	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
8	3, 7	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
9	8	simpld 500	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ∈ (ℝ ↑_m (0...𝑀)))
10		elmapi 8862	. . . . . . . 8 ⊢ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
11	9, 10	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶ℝ)
12	11	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
13		fzofzp1 13892	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
14	13	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
15	12, 14	ffvelcdmd 7083	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
16	15	adantr 486	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
17		eqcom 2768	. . . . . 6 ⊢ ((𝑉‘𝑖) = 𝑋 ↔ 𝑋 = (𝑉‘𝑖))
18	17	bilani 510	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 = (𝑉‘𝑖))
19	8	simprrd 786	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
20	19	r19.21bi 3255	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
21	20	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
22	18, 21	eqbrtrd 5127	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
23		fourierdlem75.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
24	23	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℝ)
25		ioossre 13531	. . . . . . 7 ⊢ (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
26	25	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
27	24, 26	fssresd 6747	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
28	27	adantr 486	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
29		limcresi 26198	. . . . . . . 8 ⊢ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ⊆ (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋)
30		fourierdlem75.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
31	29, 30	sselid 3929	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
32	31	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
33		pnfxr 11356	. . . . . . . . . 10 ⊢ +∞ ∈ ℝ^*
34	33	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → +∞ ∈ ℝ^*)
35	15	rexrd 11352	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
36	15	ltpnfd 13243	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) < +∞)
37	35, 34, 36	xrltled 13272	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ≤ +∞)
38		iooss2 13505	. . . . . . . . 9 ⊢ ((+∞ ∈ ℝ^* ∧ (𝑉‘(𝑖 + 1)) ≤ +∞) → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ (𝑋(,)+∞))
39	34, 37, 38	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ (𝑋(,)+∞))
40	39	resabs1d 5999	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
41	40	oveq1d 7433	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋) = ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
42	32, 41	eleqtrd 2863	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
43	42	adantr 486	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
44		eqid 2761	. . . 4 ⊢ (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
45		ax-resscn 11250	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
46	45	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
47	23, 46	fssd 6725	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
48		ssid 3953	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℝ
49	48	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℝ)
50	25	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
51		eqid 2761	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
52		tgioo4 25117	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
53	51, 52	dvres 26224	. . . . . . . . . 10 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑋(,)(𝑉‘(𝑖 + 1))))))
54	46, 47, 49, 50, 53	syl22anc 852	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑋(,)(𝑉‘(𝑖 + 1))))))
55		fourierdlem75.g	. . . . . . . . . . 11 ⊢ 𝐺 = (ℝ D 𝐹)
56	55	eqcomi 2770	. . . . . . . . . 10 ⊢ (ℝ D 𝐹) = 𝐺
57		ioontr 46492	. . . . . . . . . 10 ⊢ ((int‘(topGen‘ran (,)))‘(𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝑋(,)(𝑉‘(𝑖 + 1)))
58	56, 57	reseq12i 5968	. . . . . . . . 9 ⊢ ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))
59	54, 58	eqtrdi 2812	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
60	59	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑉‘𝑖) = 𝑋) → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
61	60	dmeqd 5887	. . . . . 6 ⊢ ((𝜑 ∧ (𝑉‘𝑖) = 𝑋) → dom (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
62	61	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → dom (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
63		fourierdlem75.gcn	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ)
64	63	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ)
65		oveq1 7425	. . . . . . . . . . 11 ⊢ ((𝑉‘𝑖) = 𝑋 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) = (𝑋(,)(𝑉‘(𝑖 + 1))))
66	65	reseq2d 5970	. . . . . . . . . 10 ⊢ ((𝑉‘𝑖) = 𝑋 → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
67	66	feq1d 6689	. . . . . . . . 9 ⊢ ((𝑉‘𝑖) = 𝑋 → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ ↔ (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ))
68	67	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ ↔ (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ))
69	64, 68	mpbid 235	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ)
70	65	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) = (𝑋(,)(𝑉‘(𝑖 + 1))))
71	70	feq2d 6691	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ ↔ (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℂ))
72	69, 71	mpbid 235	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℂ)
73		fdm 6717	. . . . . 6 ⊢ ((𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℂ → dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝑋(,)(𝑉‘(𝑖 + 1))))
74	72, 73	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝑋(,)(𝑉‘(𝑖 + 1))))
75	62, 74	eqtrd 2796	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → dom (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝑋(,)(𝑉‘(𝑖 + 1))))
76		limcresi 26198	. . . . . . . 8 ⊢ ((𝐺 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ⊆ (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋)
77		fourierdlem75.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
78	76, 77	sselid 3929	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
79	78	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
80	39	resabs1d 5999	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
81	59	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
82	80, 81	eqtr4d 2799	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))))
83	82	oveq1d 7433	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋) = ((ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) lim_ℂ 𝑋))
84	79, 83	eleqtrd 2863	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) lim_ℂ 𝑋))
85	84	adantr 486	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐸 ∈ ((ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) lim_ℂ 𝑋))
86		eqid 2761	. . . 4 ⊢ (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠))
87		oveq2 7426	. . . . . . 7 ⊢ (𝑥 = 𝑠 → (𝑋 + 𝑥) = (𝑋 + 𝑠))
88	87	fveq2d 6887	. . . . . 6 ⊢ (𝑥 = 𝑠 → ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑥)) = ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
89	88	oveq1d 7433	. . . . 5 ⊢ (𝑥 = 𝑠 → (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑥)) − 𝑌) = (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌))
90	89	cbvmptv 5209	. . . 4 ⊢ (𝑥 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑥)) − 𝑌)) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌))
91		id 23	. . . . 5 ⊢ (𝑥 = 𝑠 → 𝑥 = 𝑠)
92	91	cbvmptv 5209	. . . 4 ⊢ (𝑥 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ 𝑥) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ 𝑠)
93	2, 16, 22, 28, 43, 44, 75, 85, 86, 90, 92	fourierdlem61 47146	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐸 ∈ ((𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) lim_ℂ 0))
94		fourierdlem75.a	. . . . 5 ⊢ 𝐴 = if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)))
95		iftrue 4488	. . . . 5 ⊢ ((𝑉‘𝑖) = 𝑋 → if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) = 𝐸)
96	94, 95	eqtrid 2808	. . . 4 ⊢ ((𝑉‘𝑖) = 𝑋 → 𝐴 = 𝐸)
97	96	adantl 487	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐴 = 𝐸)
98		fourierdlem75.h	. . . . . . 7 ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
99	98	reseq1i 5966	. . . . . 6 ⊢ (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
100	99	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
101		ioossicc 13557	. . . . . . . 8 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
102		pire 26776	. . . . . . . . . . . 12 ⊢ π ∈ ℝ
103	102	renegcli 11612	. . . . . . . . . . 11 ⊢ -π ∈ ℝ
104	103	rexri 11360	. . . . . . . . . 10 ⊢ -π ∈ ℝ^*
105	104	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ^*)
106	102	rexri 11360	. . . . . . . . . 10 ⊢ π ∈ ℝ^*
107	106	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈ ℝ^*)
108	103	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ∈ ℝ)
109	102	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈ ℝ)
110	103	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -π ∈ ℝ)
111	110, 1	readdcld 11331	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-π + 𝑋) ∈ ℝ)
112	102	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → π ∈ ℝ)
113	112, 1	readdcld 11331	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (π + 𝑋) ∈ ℝ)
114	111, 113	iccssred 13558	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
115	114	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
116	5, 4, 3	fourierdlem15 47101	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
117	116	ffvelcdmda 7082	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
118	115, 117	sseldd 3932	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ℝ)
119	1	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
120	118, 119	resubcld 11737	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
121	110	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -π ∈ ℂ)
122	1	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ ℂ)
123	121, 122	pncand 11663	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
124	123	eqcomd 2767	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π = ((-π + 𝑋) − 𝑋))
125	124	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π = ((-π + 𝑋) − 𝑋))
126	111	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ∈ ℝ)
127	113	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (π + 𝑋) ∈ ℝ)
128		elicc2 13535	. . . . . . . . . . . . . . . . 17 ⊢ (((-π + 𝑋) ∈ ℝ ∧ (π + 𝑋) ∈ ℝ) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))))
129	126, 127, 128	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))))
130	117, 129	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋)))
131	130	simp2d 1161	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ≤ (𝑉‘𝑖))
132	126, 118, 119, 131	lesub1dd 11925	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋) − 𝑋) ≤ ((𝑉‘𝑖) − 𝑋))
133	125, 132	eqbrtrd 5127	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ≤ ((𝑉‘𝑖) − 𝑋))
134	130	simp3d 1162	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ≤ (π + 𝑋))
135	118, 127, 119, 134	lesub1dd 11925	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ ((π + 𝑋) − 𝑋))
136	109	recnd 11330	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈ ℂ)
137	122	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℂ)
138	136, 137	pncand 11663	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((π + 𝑋) − 𝑋) = π)
139	135, 138	breqtrd 5131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ π)
140	108, 109, 120, 133, 139	eliccd 46485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π))
141		fourierdlem75.q	. . . . . . . . . . 11 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
142	140, 141	fmptd 7112	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
143	142	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
144		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
145	105, 107, 143, 144	fourierdlem8 47094	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
146	101, 145	sstrid 3942	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
147	146	resmptd 6032	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
148	147	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
149		elfzofz 13803	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
150		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
151	141	fvmpt2 7003	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
152	150, 140, 151	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
153	152	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
154		oveq1 7425	. . . . . . . . . 10 ⊢ ((𝑉‘𝑖) = 𝑋 → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋))
155	154	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋))
156	122	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 ∈ ℂ)
157	156	subidd 11650	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑋 − 𝑋) = 0)
158	153, 155, 157	3eqtrd 2800	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = 0)
159	149, 158	sylanl2 694	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = 0)
160		fveq2 6883	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
161	160	oveq1d 7433	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
162	161	cbvmptv 5209	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
163	141, 162	eqtri 2784	. . . . . . . . . 10 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
164	163	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
165		fveq2 6883	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
166	165	oveq1d 7433	. . . . . . . . . 10 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
167	166	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
168	1	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
169	15, 168	resubcld 11737	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
170	164, 167, 14, 169	fvmptd 6999	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
171	170	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
172	159, 171	oveq12d 7436	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)))
173		simplr 781	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
174		fourierdlem75.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
175	4	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑀 ∈ ℕ)
176	110, 112, 1, 5, 174, 4, 3, 141	fourierdlem14 47100	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀))
177	176	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑄 ∈ (𝑂‘𝑀))
178		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 = 0)
179		fourierdlem75.x	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ ran 𝑉)
180		ffn 6707	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)) → 𝑉 Fn (0...𝑀))
181		fvelrnb 6943	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 Fn (0...𝑀) → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋))
182	116, 180, 181	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋))
183	179, 182	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋)
184	158	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) = 𝑋 → (𝑄‘𝑖) = 0))
185	184	reximdva 3176	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
186	183, 185	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0)
187	120, 141	fmptd 7112	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
188		ffn 6707	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
189		fvelrnb 6943	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 Fn (0...𝑀) → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
190	187, 188, 189	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
191	186, 190	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ran 𝑄)
192	191	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 = 0) → 0 ∈ ran 𝑄)
193	178, 192	eqeltrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 ∈ ran 𝑄)
194	174, 175, 177, 193	fourierdlem12 47098	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
195	194	an32s 665	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
196	195	adantlr 728	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
197	173, 196	pm2.65da 829	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
198	197	adantlr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
199	198	iffalsed 4493	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
200	159	eqcomd 2767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 0 = (𝑄‘𝑖))
201	200	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 = (𝑄‘𝑖))
202		elioo3g 13498	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ℝ^*) ∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1)))))
203	202	biimpi 219	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ℝ^*) ∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1)))))
204	203	simprld 784	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) < 𝑠)
205	204	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
206	201, 205	eqbrtrd 5127	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
207	206	iftrued 4490	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
208	207	oveq2d 7434	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑌))
209	208	oveq1d 7433	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − 𝑌) / 𝑠))
210	1	rexrd 11352	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
211	210	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ^*)
212	35	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
213	168	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
214		elioore 13499	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
215	214	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
216	213, 215	readdcld 11331	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
217	215, 206	elrpd 13154	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ⁺)
218	213, 217	ltaddrpd 13190	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 < (𝑋 + 𝑠))
219	214	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
220	187	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
221	220, 14	ffvelcdmd 7083	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
222	221	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
223	1	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
224	203	simprrd 786	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 < (𝑄‘(𝑖 + 1)))
225	224	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
226	219, 222, 223, 225	ltadd2dd 11462	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
227	170	oveq2d 7434	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
228	122	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
229	15	recnd 11330	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
230	228, 229	pncan3d 11665	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
231	227, 230	eqtrd 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
232	231	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
233	226, 232	breqtrd 5131	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
234	233	adantlr 728	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
235	211, 212, 216, 218, 234	eliood 46479	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ (𝑋(,)(𝑉‘(𝑖 + 1))))
236		fvres 6902	. . . . . . . . . . 11 ⊢ ((𝑋 + 𝑠) ∈ (𝑋(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
237	235, 236	syl 18	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
238	237	eqcomd 2767	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
239	238	oveq1d 7433	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝑌) = (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌))
240	239	oveq1d 7433	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝑌) / 𝑠) = ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠))
241	199, 209, 240	3eqtrd 2800	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠))
242	172, 241	mpteq12dva 5191	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)))
243	100, 148, 242	3eqtrd 2800	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)))
244	243, 159	oveq12d 7436	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) lim_ℂ 0))
245	93, 97, 244	3eltr4d 2876	. 2 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
246		eqid 2761	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
247		eqid 2761	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠)
248		eqid 2761	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
249	23	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℝ)
250	1	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
251	214	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
252	250, 251	readdcld 11331	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
253	249, 252	ffvelcdmd 7083	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
254	253	recnd 11330	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
255	254	adantlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
256	255	3adantl3 1187	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
257		limccl 26188	. . . . . . . . . 10 ⊢ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ⊆ ℂ
258	257, 30	sselid 3929	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℂ)
259		fourierdlem75.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ ℝ)
260	259	recnd 11330	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ℂ)
261	258, 260	ifcld 4529	. . . . . . . 8 ⊢ (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
262	261	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
263	262	3ad2antl1 1204	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
264	256, 263	subcld 11662	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
265	214	recnd 11330	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℂ)
266	265	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
267		velsn 4600	. . . . . . . 8 ⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0)
268	197, 267	sylnibr 332	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
269	268	3adantl3 1187	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
270	266, 269	eldifd 3910	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
271		eqid 2761	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
272		eqid 2761	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊)
273		eqid 2761	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
274	260	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑊 ∈ ℂ)
275		ioossre 13531	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
276	275	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
277	149, 118	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
278	277	rexrd 11352	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ^*)
279	278	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
280	35	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
281	252	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
282		iccssre 13553	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
283	103, 102, 282	mp2an 705	. . . . . . . . . . . . . . . . . 18 ⊢ (-π[,]π) ⊆ ℝ
284	283, 45	sstri 3940	. . . . . . . . . . . . . . . . 17 ⊢ (-π[,]π) ⊆ ℂ
285	152, 140	eqeltrd 2861	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π))
286	149, 285	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π))
287	284, 286	sselid 3929	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
288	228, 287	addcomd 11505	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘𝑖)) = ((𝑄‘𝑖) + 𝑋))
289	149	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
290	149, 120	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
291	141	fvmpt2 7003	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
292	289, 290, 291	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
293	292	oveq1d 7433	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑋) = (((𝑉‘𝑖) − 𝑋) + 𝑋))
294	277	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℂ)
295	294, 228	npcand 11666	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑉‘𝑖) − 𝑋) + 𝑋) = (𝑉‘𝑖))
296	288, 293, 295	3eqtrrd 2801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
297	296	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
298	292, 290	eqeltrd 2861	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
299	298	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
300	204	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
301	299, 219, 223, 300	ltadd2dd 11462	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
302	297, 301	eqbrtrd 5127	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
303	279, 280, 281, 302, 233	eliood 46479	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
304		ioossre 13531	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
305	304	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
306	299, 300	gtned 11438	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘𝑖))
307		fourierdlem75.r	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
308	296	oveq2d 7434	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
309	307, 308	eleqtrd 2863	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
310	24, 168, 276, 271, 303, 305, 306, 309, 287	fourierdlem53 47138	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘𝑖)))
311		ioosscn 13532	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
312	311	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
313	260	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ℂ)
314	272, 312, 313, 287	constlimc 46605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) lim_ℂ (𝑄‘𝑖)))
315	271, 272, 273, 255, 274, 310, 314	sublimc 46631	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘𝑖)))
316	315	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘𝑖)))
317		iftrue 4488	. . . . . . . . . 10 ⊢ ((𝑉‘𝑖) < 𝑋 → if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌) = 𝑊)
318	317	oveq2d 7434	. . . . . . . . 9 ⊢ ((𝑉‘𝑖) < 𝑋 → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊))
319	318	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊))
320	214	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
321		0red 11304	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
322	221	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
323	224	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
324	170	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
325	278	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘𝑖) ∈ ℝ^*)
326	35	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
327	168	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 ∈ ℝ)
328		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘𝑖) < 𝑋)
329		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋)
330	1	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 ∈ ℝ)
331	15	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
332	330, 331	ltnled 11450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑋 < (𝑉‘(𝑖 + 1)) ↔ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
333	329, 332	mpbird 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
334	333	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
335	325, 326, 327, 328, 334	eliood 46479	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
336	5, 4, 3, 179	fourierdlem12 47098	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
337	336	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
338	335, 337	condan 830	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑉‘(𝑖 + 1)) ≤ 𝑋)
339	15	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
340	1	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → 𝑋 ∈ ℝ)
341	339, 340	suble0d 11900	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0 ↔ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
342	338, 341	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0)
343	324, 342	eqbrtrd 5127	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑄‘(𝑖 + 1)) ≤ 0)
344	343	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ≤ 0)
345	320, 322, 321, 323, 344	ltletrd 11463	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
346	320, 321, 345	ltnsymd 11452	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
347	346	iffalsed 4493	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
348	347	oveq2d 7434	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
349	348	mpteq2dva 5198	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)))
350	349	oveq1d 7433	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘𝑖)))
351	316, 319, 350	3eltr4d 2876	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)))
352	351	3adantl3 1187	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)))
353		eqid 2761	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌)
354		eqid 2761	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌))
355	258	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑌 ∈ ℂ)
356	258	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ℂ)
357	353, 312, 356, 287	constlimc 46605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘𝑖)))
358	271, 353, 354, 255, 355, 310, 357	sublimc 46631	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑅 − 𝑌) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) lim_ℂ (𝑄‘𝑖)))
359	358	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − 𝑌) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) lim_ℂ (𝑄‘𝑖)))
360		iffalse 4491	. . . . . . . . . 10 ⊢ (¬ (𝑉‘𝑖) < 𝑋 → if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌) = 𝑌)
361	360	oveq2d 7434	. . . . . . . . 9 ⊢ (¬ (𝑉‘𝑖) < 𝑋 → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑌))
362	361	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑌))
363		0red 11304	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
364	298	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
365	214	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
366	1	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 𝑋 ∈ ℝ)
367	277	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑉‘𝑖) ∈ ℝ)
368		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → ¬ (𝑉‘𝑖) < 𝑋)
369	366, 367, 368	nltled 11453	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 𝑋 ≤ (𝑉‘𝑖))
370	367, 366	subge0d 11899	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (0 ≤ ((𝑉‘𝑖) − 𝑋) ↔ 𝑋 ≤ (𝑉‘𝑖)))
371	369, 370	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 0 ≤ ((𝑉‘𝑖) − 𝑋))
372	292	eqcomd 2767	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖))
373	372	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖))
374	371, 373	breqtrd 5131	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 0 ≤ (𝑄‘𝑖))
375	374	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ≤ (𝑄‘𝑖))
376	204	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
377	363, 364, 365, 375, 376	lelttrd 11461	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
378	377	iftrued 4490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
379	378	oveq2d 7434	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑌))
380	379	mpteq2dva 5198	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)))
381	380	oveq1d 7433	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) lim_ℂ (𝑄‘𝑖)))
382	359, 362, 381	3eltr4d 2876	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)))
383	382	3adantl3 1187	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)))
384	352, 383	pm2.61dan 825	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)))
385	312, 247, 287	idlimc 46607	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim_ℂ (𝑄‘𝑖)))
386	385	3adant3 1150	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim_ℂ (𝑄‘𝑖)))
387	292	3adant3 1150	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
388	294	3adant3 1150	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑉‘𝑖) ∈ ℂ)
389	228	3adant3 1150	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝑋 ∈ ℂ)
390		neqne 2964	. . . . . . . 8 ⊢ (¬ (𝑉‘𝑖) = 𝑋 → (𝑉‘𝑖) ≠ 𝑋)
391	390	3ad2ant3 1153	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑉‘𝑖) ≠ 𝑋)
392	388, 389, 391	subne0d 11672	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖) − 𝑋) ≠ 0)
393	387, 392	eqnetrd 3023	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) ≠ 0)
394	197	3adantl3 1187	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
395	394	neqned 2963	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
396	246, 247, 248, 264, 270, 384, 386, 393, 395	divlimc 46635	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim_ℂ (𝑄‘𝑖)))
397		iffalse 4491	. . . . . 6 ⊢ (¬ (𝑉‘𝑖) = 𝑋 → if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) = ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)))
398	94, 397	eqtrid 2808	. . . . 5 ⊢ (¬ (𝑉‘𝑖) = 𝑋 → 𝐴 = ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)))
399	398	3ad2ant3 1153	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝐴 = ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)))
400		ioossre 13531	. . . . . . . . . . . . 13 ⊢ (𝑋(,)+∞) ⊆ ℝ
401	400	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋(,)+∞) ⊆ ℝ)
402	23, 401	fssresd 6747	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)+∞)):(𝑋(,)+∞)⟶ℝ)
403	400, 46	sstrid 3942	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋(,)+∞) ⊆ ℂ)
404	33	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → +∞ ∈ ℝ^*)
405	1	ltpnfd 13243	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 < +∞)
406	51, 404, 1, 405	lptioo1cn 46625	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)+∞)))
407	402, 403, 406, 30	limcrecl 46610	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ ℝ)
408	23, 1, 407, 259, 98	fourierdlem9 47095	. . . . . . . . 9 ⊢ (𝜑 → 𝐻:(-π[,]π)⟶ℝ)
409	408	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻:(-π[,]π)⟶ℝ)
410	409, 146	feqresmpt 6952	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)))
411	146	sselda 3931	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (-π[,]π))
412		0cnd 11292	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℂ)
413	261	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
414	255, 413	subcld 11662	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
415	265	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
416	197	neqned 2963	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
417	414, 415, 416	divcld 12086	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℂ)
418	412, 417	ifcld 4529	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ)
419	98	fvmpt2 7003	. . . . . . . . . 10 ⊢ ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
420	411, 418, 419	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
421	197	iffalsed 4493	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
422	420, 421	eqtrd 2796	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
423	422	mpteq2dva 5198	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
424	410, 423	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
425	424	3adant3 1150	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
426	425	oveq1d 7433	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim_ℂ (𝑄‘𝑖)))
427	396, 399, 426	3eltr4d 2876	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
428	427	3expa 1136	. 2 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
429	245, 428	pm2.61dan 825	1 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 {crab 3413 ⊆ wss 3899 ifcif 4482 {csn 4584 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5651 ran crn 5652 ↾ cres 5653 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7418 ↑_m cmap 8840 ℂcc 11191 ℝcr 11192 0cc0 11193 1c1 11194 + caddc 11196 +∞cpnf 11333 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 − cmin 11534 -cneg 11535 / cdiv 11966 ℕcn 12328 (,)cioo 13469 [,]cicc 13472 ...cfz 13632 ..^cfzo 13781 πcpi 16225 TopOpenctopn 17585 topGenctg 17601 ℂ_fldccnfld 21671 intcnt 23328 lim_ℂ climc 26175 D cdv 26176

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271 ax-addf 11272

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-om 7876 df-1st 7999 df-2nd 8000 df-supp 8171 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-pm 8843 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9347 df-fi 9396 df-sup 9427 df-inf 9428 df-oi 9497 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-5 12401 df-6 12402 df-7 12403 df-8 12404 df-9 12405 df-n0 12600 df-z 12687 df-dec 12808 df-uz 12959 df-q 13069 df-rp 13114 df-xneg 13234 df-xadd 13235 df-xmul 13236 df-ioo 13473 df-ioc 13474 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-fl 13925 df-seq 14138 df-exp 14198 df-fac 14411 df-bc 14440 df-hash 14468 df-shft 15213 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-limsup 15631 df-clim 15648 df-rlim 15649 df-sum 15847 df-ef 16226 df-sin 16228 df-cos 16229 df-pi 16231 df-struct 17318 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-ress 17402 df-plusg 17434 df-mulr 17435 df-starv 17436 df-sca 17437 df-vsca 17438 df-ip 17439 df-tset 17440 df-ple 17441 df-ds 17443 df-unif 17444 df-hom 17445 df-cco 17446 df-rest 17586 df-topn 17587 df-0g 17605 df-gsum 17606 df-topgen 17607 df-pt 17608 df-prds 17611 df-xrs 17667 df-qtop 17672 df-imas 17673 df-xps 17675 df-mre 17749 df-mrc 17750 df-acs 17752 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-submnd 18972 df-mulg 19271 df-cntz 19524 df-cmn 19989 df-psmet 21663 df-xmet 21664 df-met 21665 df-bl 21666 df-mopn 21667 df-fbas 21668 df-fg 21669 df-cnfld 21672 df-top 23205 df-topon 23222 df-topsp 23244 df-bases 23257 df-cld 23330 df-ntr 23331 df-cls 23332 df-nei 23409 df-lp 23447 df-perf 23448 df-cn 23538 df-cnp 23539 df-haus 23626 df-cmp 23698 df-tx 23874 df-hmeo 24067 df-fil 24158 df-fm 24250 df-flim 24251 df-flf 24252 df-xms 24632 df-ms 24633 df-tms 24634 df-cncf 25192 df-limc 26179 df-dv 26180

This theorem is used by: fourierdlem85 47170 fourierdlem88 47173 fourierdlem103 47188 fourierdlem104 47189

W3C validator