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 46219

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 726	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 ∈ ℝ)
3		fourierdlem75.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
4		fourierdlem75.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ)
5		fourierdlem75.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
6	5	fourierdlem2 46147	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
7	4, 6	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
8	3, 7	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
9	8	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ∈ (ℝ ↑_m (0...𝑀)))
10		elmapi 8768	. . . . . . . 8 ⊢ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
11	9, 10	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶ℝ)
12	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
13		fzofzp1 13659	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
14	13	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
15	12, 14	ffvelcdmd 7013	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
16	15	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
17		eqcom 2738	. . . . . . 7 ⊢ ((𝑉‘𝑖) = 𝑋 ↔ 𝑋 = (𝑉‘𝑖))
18	17	biimpi 216	. . . . . 6 ⊢ ((𝑉‘𝑖) = 𝑋 → 𝑋 = (𝑉‘𝑖))
19	18	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 = (𝑉‘𝑖))
20	8	simprrd 773	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
21	20	r19.21bi 3224	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
22	21	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
23	19, 22	eqbrtrd 5108	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
24		fourierdlem75.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
25	24	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℝ)
26		ioossre 13302	. . . . . . 7 ⊢ (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
27	26	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
28	25, 27	fssresd 6685	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
29	28	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
30		limcresi 25808	. . . . . . . 8 ⊢ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ⊆ (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋)
31		fourierdlem75.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
32	30, 31	sselid 3927	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
33	32	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
34		pnfxr 11161	. . . . . . . . . 10 ⊢ +∞ ∈ ℝ^*
35	34	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → +∞ ∈ ℝ^*)
36	15	rexrd 11157	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
37	15	ltpnfd 13015	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) < +∞)
38	36, 35, 37	xrltled 13044	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ≤ +∞)
39		iooss2 13276	. . . . . . . . 9 ⊢ ((+∞ ∈ ℝ^* ∧ (𝑉‘(𝑖 + 1)) ≤ +∞) → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ (𝑋(,)+∞))
40	35, 38, 39	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ (𝑋(,)+∞))
41	40	resabs1d 5952	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
42	41	oveq1d 7356	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋) = ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
43	33, 42	eleqtrd 2833	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
44	43	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
45		eqid 2731	. . . 4 ⊢ (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
46		ax-resscn 11058	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
47	46	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
48	24, 47	fssd 6663	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
49		ssid 3952	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℝ
50	49	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℝ)
51	26	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
52		eqid 2731	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
53		tgioo4 24715	. . . . . . . . . . 11 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
54	52, 53	dvres 25834	. . . . . . . . . 10 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ (𝑋(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑋(,)(𝑉‘(𝑖 + 1))))))
55	47, 48, 50, 51, 54	syl22anc 838	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑋(,)(𝑉‘(𝑖 + 1))))))
56		fourierdlem75.g	. . . . . . . . . . 11 ⊢ 𝐺 = (ℝ D 𝐹)
57	56	eqcomi 2740	. . . . . . . . . 10 ⊢ (ℝ D 𝐹) = 𝐺
58		ioontr 45551	. . . . . . . . . 10 ⊢ ((int‘(topGen‘ran (,)))‘(𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝑋(,)(𝑉‘(𝑖 + 1)))
59	57, 58	reseq12i 5921	. . . . . . . . 9 ⊢ ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))
60	55, 59	eqtrdi 2782	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
61	60	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑉‘𝑖) = 𝑋) → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
62	61	dmeqd 5840	. . . . . 6 ⊢ ((𝜑 ∧ (𝑉‘𝑖) = 𝑋) → dom (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
63	62	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → dom (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
64		fourierdlem75.gcn	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ)
65	64	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ)
66		oveq1 7348	. . . . . . . . . . 11 ⊢ ((𝑉‘𝑖) = 𝑋 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) = (𝑋(,)(𝑉‘(𝑖 + 1))))
67	66	reseq2d 5923	. . . . . . . . . 10 ⊢ ((𝑉‘𝑖) = 𝑋 → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
68	67	feq1d 6628	. . . . . . . . 9 ⊢ ((𝑉‘𝑖) = 𝑋 → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ ↔ (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ))
69	68	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ ↔ (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ))
70	65, 69	mpbid 232	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ)
71	66	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) = (𝑋(,)(𝑉‘(𝑖 + 1))))
72	71	feq2d 6630	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ ↔ (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℂ))
73	70, 72	mpbid 232	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℂ)
74		fdm 6655	. . . . . 6 ⊢ ((𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))):(𝑋(,)(𝑉‘(𝑖 + 1)))⟶ℂ → dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝑋(,)(𝑉‘(𝑖 + 1))))
75	73, 74	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → dom (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝑋(,)(𝑉‘(𝑖 + 1))))
76	63, 75	eqtrd 2766	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → dom (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝑋(,)(𝑉‘(𝑖 + 1))))
77		limcresi 25808	. . . . . . . 8 ⊢ ((𝐺 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ⊆ (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋)
78		fourierdlem75.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
79	77, 78	sselid 3927	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
80	79	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋))
81	40	resabs1d 5952	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
82	60	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) = (𝐺 ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))))
83	81, 82	eqtr4d 2769	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) = (ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))))
84	83	oveq1d 7356	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ (𝑋(,)+∞)) ↾ (𝑋(,)(𝑉‘(𝑖 + 1)))) lim_ℂ 𝑋) = ((ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) lim_ℂ 𝑋))
85	80, 84	eleqtrd 2833	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) lim_ℂ 𝑋))
86	85	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐸 ∈ ((ℝ D (𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))) lim_ℂ 𝑋))
87		eqid 2731	. . . 4 ⊢ (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠))
88		oveq2 7349	. . . . . . 7 ⊢ (𝑥 = 𝑠 → (𝑋 + 𝑥) = (𝑋 + 𝑠))
89	88	fveq2d 6821	. . . . . 6 ⊢ (𝑥 = 𝑠 → ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑥)) = ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
90	89	oveq1d 7356	. . . . 5 ⊢ (𝑥 = 𝑠 → (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑥)) − 𝑌) = (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌))
91	90	cbvmptv 5190	. . . 4 ⊢ (𝑥 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑥)) − 𝑌)) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌))
92		id 22	. . . . 5 ⊢ (𝑥 = 𝑠 → 𝑥 = 𝑠)
93	92	cbvmptv 5190	. . . 4 ⊢ (𝑥 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ 𝑥) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ 𝑠)
94	2, 16, 23, 29, 44, 45, 76, 86, 87, 91, 93	fourierdlem61 46205	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐸 ∈ ((𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) lim_ℂ 0))
95		fourierdlem75.a	. . . . 5 ⊢ 𝐴 = if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)))
96		iftrue 4476	. . . . 5 ⊢ ((𝑉‘𝑖) = 𝑋 → if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) = 𝐸)
97	95, 96	eqtrid 2778	. . . 4 ⊢ ((𝑉‘𝑖) = 𝑋 → 𝐴 = 𝐸)
98	97	adantl 481	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐴 = 𝐸)
99		fourierdlem75.h	. . . . . . 7 ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
100	99	reseq1i 5919	. . . . . 6 ⊢ (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
101	100	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
102		ioossicc 13328	. . . . . . . 8 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
103		pire 26388	. . . . . . . . . . . 12 ⊢ π ∈ ℝ
104	103	renegcli 11417	. . . . . . . . . . 11 ⊢ -π ∈ ℝ
105	104	rexri 11165	. . . . . . . . . 10 ⊢ -π ∈ ℝ^*
106	105	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ^*)
107	103	rexri 11165	. . . . . . . . . 10 ⊢ π ∈ ℝ^*
108	107	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈ ℝ^*)
109	104	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ∈ ℝ)
110	103	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈ ℝ)
111	104	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -π ∈ ℝ)
112	111, 1	readdcld 11136	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-π + 𝑋) ∈ ℝ)
113	103	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → π ∈ ℝ)
114	113, 1	readdcld 11136	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (π + 𝑋) ∈ ℝ)
115	112, 114	iccssred 13329	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
116	115	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
117	5, 4, 3	fourierdlem15 46160	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
118	117	ffvelcdmda 7012	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
119	116, 118	sseldd 3930	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ℝ)
120	1	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
121	119, 120	resubcld 11540	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
122	111	recnd 11135	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -π ∈ ℂ)
123	1	recnd 11135	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ ℂ)
124	122, 123	pncand 11468	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
125	124	eqcomd 2737	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π = ((-π + 𝑋) − 𝑋))
126	125	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π = ((-π + 𝑋) − 𝑋))
127	112	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ∈ ℝ)
128	114	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (π + 𝑋) ∈ ℝ)
129		elicc2 13306	. . . . . . . . . . . . . . . . 17 ⊢ (((-π + 𝑋) ∈ ℝ ∧ (π + 𝑋) ∈ ℝ) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))))
130	127, 128, 129	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))))
131	118, 130	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋)))
132	131	simp2d 1143	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ≤ (𝑉‘𝑖))
133	127, 119, 120, 132	lesub1dd 11728	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋) − 𝑋) ≤ ((𝑉‘𝑖) − 𝑋))
134	126, 133	eqbrtrd 5108	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ≤ ((𝑉‘𝑖) − 𝑋))
135	131	simp3d 1144	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ≤ (π + 𝑋))
136	119, 128, 120, 135	lesub1dd 11728	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ ((π + 𝑋) − 𝑋))
137	110	recnd 11135	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈ ℂ)
138	123	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℂ)
139	137, 138	pncand 11468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((π + 𝑋) − 𝑋) = π)
140	136, 139	breqtrd 5112	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ π)
141	109, 110, 121, 134, 140	eliccd 45544	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π))
142		fourierdlem75.q	. . . . . . . . . . 11 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
143	141, 142	fmptd 7042	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
144	143	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
145		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
146	106, 108, 144, 145	fourierdlem8 46153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
147	102, 146	sstrid 3941	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
148	147	resmptd 5984	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
149	148	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
150		elfzofz 13570	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
151		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
152	142	fvmpt2 6935	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
153	151, 141, 152	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
154	153	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
155		oveq1 7348	. . . . . . . . . 10 ⊢ ((𝑉‘𝑖) = 𝑋 → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋))
156	155	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋))
157	123	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝑋 ∈ ℂ)
158	157	subidd 11455	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑋 − 𝑋) = 0)
159	154, 156, 158	3eqtrd 2770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = 0)
160	150, 159	sylanl2 681	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = 0)
161		fveq2 6817	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
162	161	oveq1d 7356	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
163	162	cbvmptv 5190	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
164	142, 163	eqtri 2754	. . . . . . . . . 10 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
165	164	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
166		fveq2 6817	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
167	166	oveq1d 7356	. . . . . . . . . 10 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
168	167	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
169	1	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
170	15, 169	resubcld 11540	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
171	165, 168, 14, 170	fvmptd 6931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
172	171	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
173	160, 172	oveq12d 7359	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)))
174		simplr 768	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
175		fourierdlem75.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
176	4	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑀 ∈ ℕ)
177	111, 113, 1, 5, 175, 4, 3, 142	fourierdlem14 46159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀))
178	177	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑄 ∈ (𝑂‘𝑀))
179		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 = 0)
180		fourierdlem75.x	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ ran 𝑉)
181		ffn 6646	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)) → 𝑉 Fn (0...𝑀))
182		fvelrnb 6877	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 Fn (0...𝑀) → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋))
183	117, 181, 182	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋))
184	180, 183	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋)
185	159	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) = 𝑋 → (𝑄‘𝑖) = 0))
186	185	reximdva 3145	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
187	184, 186	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0)
188	121, 142	fmptd 7042	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
189		ffn 6646	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
190		fvelrnb 6877	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 Fn (0...𝑀) → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
191	188, 189, 190	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
192	187, 191	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ran 𝑄)
193	192	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 = 0) → 0 ∈ ran 𝑄)
194	179, 193	eqeltrd 2831	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 ∈ ran 𝑄)
195	175, 176, 178, 194	fourierdlem12 46157	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
196	195	an32s 652	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
197	196	adantlr 715	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
198	174, 197	pm2.65da 816	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
199	198	adantlr 715	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
200	199	iffalsed 4481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
201	160	eqcomd 2737	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 0 = (𝑄‘𝑖))
202	201	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 = (𝑄‘𝑖))
203		elioo3g 13269	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ℝ^*) ∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1)))))
204	203	biimpi 216	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ℝ^*) ∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1)))))
205	204	simprld 771	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) < 𝑠)
206	205	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
207	202, 206	eqbrtrd 5108	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
208	207	iftrued 4478	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
209	208	oveq2d 7357	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑌))
210	209	oveq1d 7356	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − 𝑌) / 𝑠))
211	1	rexrd 11157	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
212	211	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ^*)
213	36	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
214	169	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
215		elioore 13270	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
216	215	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
217	214, 216	readdcld 11136	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
218	216, 207	elrpd 12926	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ⁺)
219	214, 218	ltaddrpd 12962	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 < (𝑋 + 𝑠))
220	215	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
221	188	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
222	221, 14	ffvelcdmd 7013	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
223	222	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
224	1	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
225	204	simprrd 773	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 < (𝑄‘(𝑖 + 1)))
226	225	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
227	220, 223, 224, 226	ltadd2dd 11267	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
228	171	oveq2d 7357	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
229	123	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
230	15	recnd 11135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
231	229, 230	pncan3d 11470	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
232	228, 231	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
233	232	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
234	227, 233	breqtrd 5112	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
235	234	adantlr 715	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
236	212, 213, 217, 219, 235	eliood 45538	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ (𝑋(,)(𝑉‘(𝑖 + 1))))
237		fvres 6836	. . . . . . . . . . 11 ⊢ ((𝑋 + 𝑠) ∈ (𝑋(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
238	236, 237	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
239	238	eqcomd 2737	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
240	239	oveq1d 7356	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝑌) = (((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌))
241	240	oveq1d 7356	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝑌) / 𝑠) = ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠))
242	200, 210, 241	3eqtrd 2770	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠))
243	173, 242	mpteq12dva 5172	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)))
244	101, 149, 243	3eqtrd 2770	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)))
245	244, 160	oveq12d 7359	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝑠 ∈ (0(,)((𝑉‘(𝑖 + 1)) − 𝑋)) ↦ ((((𝐹 ↾ (𝑋(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) − 𝑌) / 𝑠)) lim_ℂ 0))
246	94, 98, 245	3eltr4d 2846	. 2 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
247		eqid 2731	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
248		eqid 2731	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠)
249		eqid 2731	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
250	24	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℝ)
251	1	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
252	215	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
253	251, 252	readdcld 11136	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
254	250, 253	ffvelcdmd 7013	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
255	254	recnd 11135	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
256	255	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
257	256	3adantl3 1169	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
258		limccl 25798	. . . . . . . . . 10 ⊢ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ⊆ ℂ
259	258, 31	sselid 3927	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℂ)
260		fourierdlem75.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ ℝ)
261	260	recnd 11135	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ℂ)
262	259, 261	ifcld 4517	. . . . . . . 8 ⊢ (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
263	262	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
264	263	3ad2antl1 1186	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
265	257, 264	subcld 11467	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
266	215	recnd 11135	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℂ)
267	266	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
268		velsn 4587	. . . . . . . 8 ⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0)
269	198, 268	sylnibr 329	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
270	269	3adantl3 1169	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
271	267, 270	eldifd 3908	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
272		eqid 2731	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
273		eqid 2731	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊)
274		eqid 2731	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
275	261	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑊 ∈ ℂ)
276		ioossre 13302	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
277	276	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
278	150, 119	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
279	278	rexrd 11157	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ^*)
280	279	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
281	36	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
282	253	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
283		iccssre 13324	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
284	104, 103, 283	mp2an 692	. . . . . . . . . . . . . . . . . 18 ⊢ (-π[,]π) ⊆ ℝ
285	284, 46	sstri 3939	. . . . . . . . . . . . . . . . 17 ⊢ (-π[,]π) ⊆ ℂ
286	153, 141	eqeltrd 2831	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π))
287	150, 286	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π))
288	285, 287	sselid 3927	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
289	229, 288	addcomd 11310	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘𝑖)) = ((𝑄‘𝑖) + 𝑋))
290	150	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
291	150, 121	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
292	142	fvmpt2 6935	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
293	290, 291, 292	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
294	293	oveq1d 7356	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑋) = (((𝑉‘𝑖) − 𝑋) + 𝑋))
295	278	recnd 11135	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℂ)
296	295, 229	npcand 11471	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑉‘𝑖) − 𝑋) + 𝑋) = (𝑉‘𝑖))
297	289, 294, 296	3eqtrrd 2771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
298	297	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
299	293, 291	eqeltrd 2831	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
300	299	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
301	205	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
302	300, 220, 224, 301	ltadd2dd 11267	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
303	298, 302	eqbrtrd 5108	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
304	280, 281, 282, 303, 234	eliood 45538	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
305		ioossre 13302	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
306	305	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
307	300, 301	gtned 11243	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘𝑖))
308		fourierdlem75.r	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
309	297	oveq2d 7357	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
310	308, 309	eleqtrd 2833	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
311	25, 169, 277, 272, 304, 306, 307, 310, 288	fourierdlem53 46197	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘𝑖)))
312		ioosscn 13303	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
313	312	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
314	261	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ℂ)
315	273, 313, 314, 288	constlimc 45664	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) lim_ℂ (𝑄‘𝑖)))
316	272, 273, 274, 256, 275, 311, 315	sublimc 45690	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘𝑖)))
317	316	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘𝑖)))
318		iftrue 4476	. . . . . . . . . 10 ⊢ ((𝑉‘𝑖) < 𝑋 → if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌) = 𝑊)
319	318	oveq2d 7357	. . . . . . . . 9 ⊢ ((𝑉‘𝑖) < 𝑋 → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊))
320	319	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊))
321	215	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
322		0red 11110	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
323	222	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
324	225	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
325	171	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
326	279	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘𝑖) ∈ ℝ^*)
327	36	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
328	169	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 ∈ ℝ)
329		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘𝑖) < 𝑋)
330		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋)
331	1	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 ∈ ℝ)
332	15	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
333	331, 332	ltnled 11255	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → (𝑋 < (𝑉‘(𝑖 + 1)) ↔ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
334	330, 333	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
335	334	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
336	326, 327, 328, 329, 335	eliood 45538	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
337	5, 4, 3, 180	fourierdlem12 46157	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
338	337	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) ≤ 𝑋) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
339	336, 338	condan 817	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑉‘(𝑖 + 1)) ≤ 𝑋)
340	15	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
341	1	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → 𝑋 ∈ ℝ)
342	340, 341	suble0d 11703	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0 ↔ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
343	339, 342	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0)
344	325, 343	eqbrtrd 5108	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑄‘(𝑖 + 1)) ≤ 0)
345	344	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ≤ 0)
346	321, 323, 322, 324, 345	ltletrd 11268	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
347	321, 322, 346	ltnsymd 11257	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
348	347	iffalsed 4481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
349	348	oveq2d 7357	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
350	349	mpteq2dva 5179	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)))
351	350	oveq1d 7356	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘𝑖)))
352	317, 320, 351	3eltr4d 2846	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)))
353	352	3adantl3 1169	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)))
354		eqid 2731	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌)
355		eqid 2731	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌))
356	259	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑌 ∈ ℂ)
357	259	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ℂ)
358	354, 313, 357, 288	constlimc 45664	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘𝑖)))
359	272, 354, 355, 256, 356, 311, 358	sublimc 45690	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑅 − 𝑌) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) lim_ℂ (𝑄‘𝑖)))
360	359	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − 𝑌) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) lim_ℂ (𝑄‘𝑖)))
361		iffalse 4479	. . . . . . . . . 10 ⊢ (¬ (𝑉‘𝑖) < 𝑋 → if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌) = 𝑌)
362	361	oveq2d 7357	. . . . . . . . 9 ⊢ (¬ (𝑉‘𝑖) < 𝑋 → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑌))
363	362	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑌))
364		0red 11110	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
365	299	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
366	215	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
367	1	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 𝑋 ∈ ℝ)
368	278	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑉‘𝑖) ∈ ℝ)
369		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → ¬ (𝑉‘𝑖) < 𝑋)
370	367, 368, 369	nltled 11258	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 𝑋 ≤ (𝑉‘𝑖))
371	368, 367	subge0d 11702	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (0 ≤ ((𝑉‘𝑖) − 𝑋) ↔ 𝑋 ≤ (𝑉‘𝑖)))
372	370, 371	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 0 ≤ ((𝑉‘𝑖) − 𝑋))
373	293	eqcomd 2737	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖))
374	373	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖))
375	372, 374	breqtrd 5112	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → 0 ≤ (𝑄‘𝑖))
376	375	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ≤ (𝑄‘𝑖))
377	205	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
378	364, 365, 366, 376, 377	lelttrd 11266	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
379	378	iftrued 4478	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
380	379	oveq2d 7357	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑌))
381	380	mpteq2dva 5179	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)))
382	381	oveq1d 7356	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑌)) lim_ℂ (𝑄‘𝑖)))
383	360, 363, 382	3eltr4d 2846	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)))
384	383	3adantl3 1169	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ ¬ (𝑉‘𝑖) < 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)))
385	353, 384	pm2.61dan 812	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘𝑖)))
386	313, 248, 288	idlimc 45666	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim_ℂ (𝑄‘𝑖)))
387	386	3adant3 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim_ℂ (𝑄‘𝑖)))
388	293	3adant3 1132	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
389	295	3adant3 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑉‘𝑖) ∈ ℂ)
390	229	3adant3 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝑋 ∈ ℂ)
391		neqne 2936	. . . . . . . 8 ⊢ (¬ (𝑉‘𝑖) = 𝑋 → (𝑉‘𝑖) ≠ 𝑋)
392	391	3ad2ant3 1135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑉‘𝑖) ≠ 𝑋)
393	389, 390, 392	subne0d 11476	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖) − 𝑋) ≠ 0)
394	388, 393	eqnetrd 2995	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) ≠ 0)
395	198	3adantl3 1169	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
396	395	neqned 2935	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
397	247, 248, 249, 265, 271, 385, 387, 394, 396	divlimc 45694	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim_ℂ (𝑄‘𝑖)))
398		iffalse 4479	. . . . . 6 ⊢ (¬ (𝑉‘𝑖) = 𝑋 → if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) = ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)))
399	95, 398	eqtrid 2778	. . . . 5 ⊢ (¬ (𝑉‘𝑖) = 𝑋 → 𝐴 = ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)))
400	399	3ad2ant3 1135	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝐴 = ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)))
401		ioossre 13302	. . . . . . . . . . . . 13 ⊢ (𝑋(,)+∞) ⊆ ℝ
402	401	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋(,)+∞) ⊆ ℝ)
403	24, 402	fssresd 6685	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)+∞)):(𝑋(,)+∞)⟶ℝ)
404	401, 47	sstrid 3941	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋(,)+∞) ⊆ ℂ)
405	34	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → +∞ ∈ ℝ^*)
406	1	ltpnfd 13015	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 < +∞)
407	52, 405, 1, 406	lptioo1cn 45684	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)+∞)))
408	403, 404, 407, 31	limcrecl 45669	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ ℝ)
409	24, 1, 408, 260, 99	fourierdlem9 46154	. . . . . . . . 9 ⊢ (𝜑 → 𝐻:(-π[,]π)⟶ℝ)
410	409	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻:(-π[,]π)⟶ℝ)
411	410, 147	feqresmpt 6886	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)))
412	147	sselda 3929	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (-π[,]π))
413		0cnd 11100	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℂ)
414	262	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
415	256, 414	subcld 11467	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
416	266	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
417	198	neqned 2935	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
418	415, 416, 417	divcld 11892	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℂ)
419	413, 418	ifcld 4517	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ)
420	99	fvmpt2 6935	. . . . . . . . . 10 ⊢ ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
421	412, 419, 420	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
422	198	iffalsed 4481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
423	421, 422	eqtrd 2766	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
424	423	mpteq2dva 5179	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
425	411, 424	eqtrd 2766	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
426	425	3adant3 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
427	426	oveq1d 7356	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim_ℂ (𝑄‘𝑖)))
428	397, 400, 427	3eltr4d 2846	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
429	428	3expa 1118	. 2 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘𝑖) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
430	246, 429	pm2.61dan 812	1 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 {crab 3395 ⊆ wss 3897 ifcif 4470 {csn 4571 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5611 ran crn 5612 ↾ cres 5613 Fn wfn 6471 ⟶wf 6472 ‘cfv 6476 (class class class)co 7341 ↑_m cmap 8745 ℂcc 10999 ℝcr 11000 0cc0 11001 1c1 11002 + caddc 11004 +∞cpnf 11138 ℝ^*cxr 11140 < clt 11141 ≤ cle 11142 − cmin 11339 -cneg 11340 / cdiv 11769 ℕcn 12120 (,)cioo 13240 [,]cicc 13243 ...cfz 13402 ..^cfzo 13549 πcpi 15968 TopOpenctopn 17320 topGenctg 17336 ℂ_fldccnfld 21286 intcnt 22927 lim_ℂ climc 25785 D cdv 25786

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-inf2 9526 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078 ax-pre-sup 11079 ax-addf 11080

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-tp 4576 df-op 4578 df-uni 4855 df-int 4893 df-iun 4938 df-iin 4939 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-se 5565 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-isom 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7605 df-om 7792 df-1st 7916 df-2nd 7917 df-supp 8086 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-2o 8381 df-er 8617 df-map 8747 df-pm 8748 df-ixp 8817 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-fsupp 9241 df-fi 9290 df-sup 9321 df-inf 9322 df-oi 9391 df-card 9827 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-div 11770 df-nn 12121 df-2 12183 df-3 12184 df-4 12185 df-5 12186 df-6 12187 df-7 12188 df-8 12189 df-9 12190 df-n0 12377 df-z 12464 df-dec 12584 df-uz 12728 df-q 12842 df-rp 12886 df-xneg 13006 df-xadd 13007 df-xmul 13008 df-ioo 13244 df-ioc 13245 df-ico 13246 df-icc 13247 df-fz 13403 df-fzo 13550 df-fl 13691 df-seq 13904 df-exp 13964 df-fac 14176 df-bc 14205 df-hash 14233 df-shft 14969 df-cj 15001 df-re 15002 df-im 15003 df-sqrt 15137 df-abs 15138 df-limsup 15373 df-clim 15390 df-rlim 15391 df-sum 15589 df-ef 15969 df-sin 15971 df-cos 15972 df-pi 15974 df-struct 17053 df-sets 17070 df-slot 17088 df-ndx 17100 df-base 17116 df-ress 17137 df-plusg 17169 df-mulr 17170 df-starv 17171 df-sca 17172 df-vsca 17173 df-ip 17174 df-tset 17175 df-ple 17176 df-ds 17178 df-unif 17179 df-hom 17180 df-cco 17181 df-rest 17321 df-topn 17322 df-0g 17340 df-gsum 17341 df-topgen 17342 df-pt 17343 df-prds 17346 df-xrs 17401 df-qtop 17406 df-imas 17407 df-xps 17409 df-mre 17483 df-mrc 17484 df-acs 17486 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-submnd 18687 df-mulg 18976 df-cntz 19224 df-cmn 19689 df-psmet 21278 df-xmet 21279 df-met 21280 df-bl 21281 df-mopn 21282 df-fbas 21283 df-fg 21284 df-cnfld 21287 df-top 22804 df-topon 22821 df-topsp 22843 df-bases 22856 df-cld 22929 df-ntr 22930 df-cls 22931 df-nei 23008 df-lp 23046 df-perf 23047 df-cn 23137 df-cnp 23138 df-haus 23225 df-cmp 23297 df-tx 23472 df-hmeo 23665 df-fil 23756 df-fm 23848 df-flim 23849 df-flf 23850 df-xms 24230 df-ms 24231 df-tms 24232 df-cncf 24793 df-limc 25789 df-dv 25790

This theorem is referenced by: fourierdlem85 46229 fourierdlem88 46232 fourierdlem103 46247 fourierdlem104 46248

W3C validator