fourierdlem74 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem74 46629

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

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

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

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

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

Step	Hyp	Ref	Expression
1		elfzofz 13624	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
2		pire 26437	. . . . . . . . . . . 12 ⊢ π ∈ ℝ
3	2	renegcli 11449	. . . . . . . . . . 11 ⊢ -π ∈ ℝ
4	3	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → -π ∈ ℝ)
5		fourierdlem74.xre	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
6	4, 5	readdcld 11168	. . . . . . . . 9 ⊢ (𝜑 → (-π + 𝑋) ∈ ℝ)
7	2	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → π ∈ ℝ)
8	7, 5	readdcld 11168	. . . . . . . . 9 ⊢ (𝜑 → (π + 𝑋) ∈ ℝ)
9	6, 8	iccssred 13381	. . . . . . . 8 ⊢ (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
10	9	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
11		fourierdlem74.p	. . . . . . . . 9 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
12		fourierdlem74.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
13		fourierdlem74.v	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
14	11, 12, 13	fourierdlem15 46571	. . . . . . . 8 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
15	14	ffvelcdmda 7031	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
16	10, 15	sseldd 3923	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ℝ)
17	1, 16	sylan2 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
18	17	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘𝑖) ∈ ℝ)
19	5	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℝ)
20	11	fourierdlem2 46558	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
21	12, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
22	13, 21	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
23	22	simprrd 774	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
24	23	r19.21bi 3230	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
25	24	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
26		eqcom 2744	. . . . . . 7 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 ↔ 𝑋 = (𝑉‘(𝑖 + 1)))
27	26	biimpi 216	. . . . . 6 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → 𝑋 = (𝑉‘(𝑖 + 1)))
28	27	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 = (𝑉‘(𝑖 + 1)))
29	25, 28	breqtrrd 5114	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘𝑖) < 𝑋)
30		fourierdlem74.f	. . . . . 6 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
31		ioossre 13354	. . . . . . 7 ⊢ ((𝑉‘𝑖)(,)𝑋) ⊆ ℝ
32	31	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑉‘𝑖)(,)𝑋) ⊆ ℝ)
33	30, 32	fssresd 6702	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ)
34	33	ad2antrr 727	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ)
35		limcresi 25865	. . . . . . . 8 ⊢ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋)
36		fourierdlem74.w	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
37	35, 36	sselid 3920	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
38	37	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
39		mnfxr 11196	. . . . . . . . . 10 ⊢ -∞ ∈ ℝ^*
40	39	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ^*)
41	17	rexrd 11189	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ^*)
42	17	mnfltd 13069	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ < (𝑉‘𝑖))
43	40, 41, 42	xrltled 13095	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑉‘𝑖))
44		iooss1 13327	. . . . . . . . 9 ⊢ ((-∞ ∈ ℝ^* ∧ -∞ ≤ (𝑉‘𝑖)) → ((𝑉‘𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
45	40, 43, 44	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
46	45	resabs1d 5968	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) = (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)))
47	46	oveq1d 7376	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
48	38, 47	eleqtrd 2839	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
49	48	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑊 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
50		eqid 2737	. . . 4 ⊢ (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)))
51		ax-resscn 11089	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
52	51	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℂ)
53	30, 52	fssd 6680	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
54		ssid 3945	. . . . . . . . . 10 ⊢ ℝ ⊆ ℝ
55	54	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℝ)
56		eqid 2737	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
57		tgioo4 24783	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
58	56, 57	dvres 25891	. . . . . . . . 9 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑉‘𝑖)(,)𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))))
59	52, 53, 55, 32, 58	syl22anc 839	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))))
60		fourierdlem74.g	. . . . . . . . . . 11 ⊢ 𝐺 = (ℝ D 𝐹)
61	60	eqcomi 2746	. . . . . . . . . 10 ⊢ (ℝ D 𝐹) = 𝐺
62		ioontr 45962	. . . . . . . . . 10 ⊢ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋)) = ((𝑉‘𝑖)(,)𝑋)
63	61, 62	reseq12i 5937	. . . . . . . . 9 ⊢ ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋))
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
65	59, 64	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
66	65	dmeqd 5855	. . . . . 6 ⊢ (𝜑 → dom (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
67	66	ad2antrr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
68		fourierdlem74.gcn	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
69	68	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
70		oveq2 7369	. . . . . . . . . 10 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) = ((𝑉‘𝑖)(,)𝑋))
71	70	reseq2d 5939	. . . . . . . . 9 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
72	71, 70	feq12d 6651	. . . . . . . 8 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ))
73	72	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ))
74	69, 73	mpbid 232	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ)
75		fdm 6672	. . . . . 6 ⊢ ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ → dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) = ((𝑉‘𝑖)(,)𝑋))
76	74, 75	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) = ((𝑉‘𝑖)(,)𝑋))
77	67, 76	eqtrd 2772	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = ((𝑉‘𝑖)(,)𝑋))
78		limcresi 25865	. . . . . . . 8 ⊢ ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋)
79	45	resabs1d 5968	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
80	79	oveq1d 7376	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
81	78, 80	sseqtrid 3965	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
82		fourierdlem74.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
83	82	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
84	81, 83	sseldd 3923	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
85	59, 64	eqtr2d 2773	. . . . . . . 8 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) = (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))))
86	85	oveq1d 7376	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
87	86	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
88	84, 87	eleqtrd 2839	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
89	88	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
90		eqid 2737	. . . 4 ⊢ (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
91		oveq2 7369	. . . . . . 7 ⊢ (𝑥 = 𝑠 → (𝑋 + 𝑥) = (𝑋 + 𝑠))
92	91	fveq2d 6839	. . . . . 6 ⊢ (𝑥 = 𝑠 → ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑥)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
93	92	oveq1d 7376	. . . . 5 ⊢ (𝑥 = 𝑠 → (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊) = (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
94	93	cbvmptv 5190	. . . 4 ⊢ (𝑥 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊)) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
95		id 22	. . . . 5 ⊢ (𝑥 = 𝑠 → 𝑥 = 𝑠)
96	95	cbvmptv 5190	. . . 4 ⊢ (𝑥 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ 𝑥) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ 𝑠)
97	18, 19, 29, 34, 49, 50, 77, 89, 90, 94, 96	fourierdlem60 46615	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim_ℂ 0))
98		fourierdlem74.a	. . . . 5 ⊢ 𝐴 = if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
99		iftrue 4473	. . . . 5 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = 𝐸)
100	98, 99	eqtrid 2784	. . . 4 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → 𝐴 = 𝐸)
101	100	adantl 481	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = 𝐸)
102		fourierdlem74.h	. . . . . . 7 ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
103	102	reseq1i 5935	. . . . . 6 ⊢ (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
104	103	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
105		ioossicc 13380	. . . . . . . 8 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
106	3	rexri 11197	. . . . . . . . . 10 ⊢ -π ∈ ℝ^*
107	106	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ^*)
108	2	rexri 11197	. . . . . . . . . 10 ⊢ π ∈ ℝ^*
109	108	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈ ℝ^*)
110	3	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ∈ ℝ)
111	2	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈ ℝ)
112	5	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
113	16, 112	resubcld 11572	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
114	4	recnd 11167	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -π ∈ ℂ)
115	5	recnd 11167	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ ℂ)
116	114, 115	pncand 11500	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
117	116	eqcomd 2743	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π = ((-π + 𝑋) − 𝑋))
118	117	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π = ((-π + 𝑋) − 𝑋))
119	6	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ∈ ℝ)
120	8	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (π + 𝑋) ∈ ℝ)
121		elicc2 13358	. . . . . . . . . . . . . . . . 17 ⊢ (((-π + 𝑋) ∈ ℝ ∧ (π + 𝑋) ∈ ℝ) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))))
122	119, 120, 121	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))))
123	15, 122	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋)))
124	123	simp2d 1144	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ≤ (𝑉‘𝑖))
125	119, 16, 112, 124	lesub1dd 11760	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋) − 𝑋) ≤ ((𝑉‘𝑖) − 𝑋))
126	118, 125	eqbrtrd 5108	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ≤ ((𝑉‘𝑖) − 𝑋))
127	123	simp3d 1145	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ≤ (π + 𝑋))
128	16, 120, 112, 127	lesub1dd 11760	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ ((π + 𝑋) − 𝑋))
129	111	recnd 11167	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈ ℂ)
130	115	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℂ)
131	129, 130	pncand 11500	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((π + 𝑋) − 𝑋) = π)
132	128, 131	breqtrd 5112	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ π)
133	110, 111, 113, 126, 132	eliccd 45955	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π))
134		fourierdlem74.q	. . . . . . . . . . 11 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
135	133, 134	fmptd 7061	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
136	135	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
137		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
138	107, 109, 136, 137	fourierdlem8 46564	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
139	105, 138	sstrid 3934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
140	139	resmptd 6000	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
141	140	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
142	1	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
143	1, 113	sylan2 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
144	134	fvmpt2 6954	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
145	142, 143, 144	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
146	145	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
147		fveq2 6835	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
148	147	oveq1d 7376	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
149	148	cbvmptv 5190	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
150	134, 149	eqtri 2760	. . . . . . . . . . 11 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
151	150	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
152		fveq2 6835	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
153	152	oveq1d 7376	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
154	153	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
155		fzofzp1 13713	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
156	155	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
157	22	simpld 494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ∈ (ℝ ↑_m (0...𝑀)))
158		elmapi 8790	. . . . . . . . . . . . . 14 ⊢ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
159	157, 158	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶ℝ)
160	159	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
161	160, 156	ffvelcdmd 7032	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
162	5	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
163	161, 162	resubcld 11572	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
164	151, 154, 156, 163	fvmptd 6950	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
165	164	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
166		oveq1 7368	. . . . . . . . 9 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋 − 𝑋))
167	166	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋 − 𝑋))
168	115	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
169	168	subidd 11487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋 − 𝑋) = 0)
170	1, 169	sylanl2 682	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋 − 𝑋) = 0)
171	165, 167, 170	3eqtrd 2776	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = 0)
172	146, 171	oveq12d 7379	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑉‘𝑖) − 𝑋)(,)0))
173		simplr 769	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
174		fourierdlem74.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
175	12	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑀 ∈ ℕ)
176	4, 7, 5, 11, 174, 12, 13, 134	fourierdlem14 46570	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀))
177	176	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑄 ∈ (𝑂‘𝑀))
178		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 = 0)
179		fourierdlem74.x	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ ran 𝑉)
180		ffn 6663	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)) → 𝑉 Fn (0...𝑀))
181		fvelrnb 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 Fn (0...𝑀) → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋))
182	14, 180, 181	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋))
183	179, 182	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋)
184		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
185	134	fvmpt2 6954	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
186	184, 133, 185	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
187	186	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
188		oveq1 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉‘𝑖) = 𝑋 → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋))
189	188	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋))
190	115	subidd 11487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑋 − 𝑋) = 0)
191	190	ad2antrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑋 − 𝑋) = 0)
192	187, 189, 191	3eqtrd 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = 0)
193	192	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) = 𝑋 → (𝑄‘𝑖) = 0))
194	193	reximdva 3151	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
195	183, 194	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0)
196	113, 134	fmptd 7061	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
197		ffn 6663	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
198		fvelrnb 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 Fn (0...𝑀) → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
199	196, 197, 198	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
200	195, 199	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ran 𝑄)
201	200	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 = 0) → 0 ∈ ran 𝑄)
202	178, 201	eqeltrd 2837	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 ∈ ran 𝑄)
203	174, 175, 177, 202	fourierdlem12 46568	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
204	203	an32s 653	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
205	204	adantlr 716	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
206	173, 205	pm2.65da 817	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
207	206	adantlr 716	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
208	207	iffalsed 4478	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
209		elioore 13322	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
210	209	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
211		0red 11141	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
212		elioo3g 13321	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ℝ^*) ∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1)))))
213	212	biimpi 216	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ℝ^*) ∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1)))))
214	213	simprrd 774	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 < (𝑄‘(𝑖 + 1)))
215	214	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
216	171	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) = 0)
217	215, 216	breqtrd 5112	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
218	210, 211, 217	ltnsymd 11289	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
219	218	iffalsed 4478	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
220	219	oveq2d 7377	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
221	220	oveq1d 7376	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
222	41	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
223	5	rexrd 11189	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
224	223	ad3antrrr 731	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ^*)
225	162	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
226	225, 210	readdcld 11168	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
227	115	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
228		iccssre 13376	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
229	3, 2, 228	mp2an 693	. . . . . . . . . . . . . . . . . 18 ⊢ (-π[,]π) ⊆ ℝ
230	229, 51	sstri 3932	. . . . . . . . . . . . . . . . 17 ⊢ (-π[,]π) ⊆ ℂ
231	186, 133	eqeltrd 2837	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π))
232	1, 231	sylan2 594	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π))
233	230, 232	sselid 3920	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
234	227, 233	addcomd 11342	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘𝑖)) = ((𝑄‘𝑖) + 𝑋))
235	145	oveq1d 7376	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑋) = (((𝑉‘𝑖) − 𝑋) + 𝑋))
236	17	recnd 11167	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℂ)
237	236, 227	npcand 11503	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑉‘𝑖) − 𝑋) + 𝑋) = (𝑉‘𝑖))
238	234, 235, 237	3eqtrrd 2777	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
239	238	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
240	145, 143	eqeltrd 2837	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
241	240	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
242	209	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
243	5	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
244	213	simprld 772	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) < 𝑠)
245	244	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
246	241, 242, 243, 245	ltadd2dd 11299	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
247	239, 246	eqbrtrd 5108	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
248	247	adantlr 716	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
249		ltaddneg 11356	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
250	210, 225, 249	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
251	217, 250	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < 𝑋)
252	222, 224, 226, 248, 251	eliood 45949	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)𝑋))
253		fvres 6854	. . . . . . . . . . 11 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)𝑋) → ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
254	253	eqcomd 2743	. . . . . . . . . 10 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)𝑋) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
255	252, 254	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
256	255	oveq1d 7376	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝑊) = (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
257	256	oveq1d 7376	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠) = ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
258	208, 221, 257	3eqtrd 2776	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
259	172, 258	mpteq12dva 5172	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
260	104, 141, 259	3eqtrd 2776	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
261	260, 171	oveq12d 7379	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim_ℂ 0))
262	97, 101, 261	3eltr4d 2852	. 2 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
263		eqid 2737	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
264		eqid 2737	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠)
265		eqid 2737	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
266	30	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℝ)
267	5	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
268	209	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
269	267, 268	readdcld 11168	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
270	266, 269	ffvelcdmd 7032	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
271	270	recnd 11167	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
272	271	adantlr 716	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
273	272	3adantl3 1170	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
274		fourierdlem74.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ ℝ)
275	274	recnd 11167	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℂ)
276		limccl 25855	. . . . . . . . . 10 ⊢ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ ℂ
277	276, 36	sselid 3920	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ℂ)
278	275, 277	ifcld 4514	. . . . . . . 8 ⊢ (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
279	278	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
280	279	3ad2antl1 1187	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
281	273, 280	subcld 11499	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
282	209	recnd 11167	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℂ)
283	282	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
284		velsn 4584	. . . . . . . 8 ⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0)
285	206, 284	sylnibr 329	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
286	285	3adantl3 1170	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
287	283, 286	eldifd 3901	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
288		eqid 2737	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
289		eqid 2737	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊)
290		eqid 2737	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
291	277	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑊 ∈ ℂ)
292	30	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℝ)
293		ioossre 13354	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
294	293	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
295	41	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
296	161	rexrd 11189	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
297	296	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
298	269	adantlr 716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
299	196	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
300	299, 156	ffvelcdmd 7032	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
301	300	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
302	214	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
303	242, 301, 243, 302	ltadd2dd 11299	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
304	164	oveq2d 7377	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
305	161	recnd 11167	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
306	227, 305	pncan3d 11502	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
307	304, 306	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
308	307	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
309	303, 308	breqtrd 5112	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
310	295, 297, 298, 247, 309	eliood 45949	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
311		ioossre 13354	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
312	311	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
313	242, 302	ltned 11276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
314		fourierdlem74.r	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
315	307	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
316	315	oveq2d 7377	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
317	314, 316	eleqtrd 2839	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
318	300	recnd 11167	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
319	292, 162, 294, 288, 310, 312, 313, 317, 318	fourierdlem53 46608	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
320		ioosscn 13355	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
321	320	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
322	277	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ℂ)
323	289, 321, 322, 318	constlimc 46075	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) lim_ℂ (𝑄‘(𝑖 + 1))))
324	288, 289, 290, 272, 291, 319, 323	sublimc 46101	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
325	324	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
326		iftrue 4473	. . . . . . . . . 10 ⊢ ((𝑉‘(𝑖 + 1)) < 𝑋 → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑊)
327	326	oveq2d 7377	. . . . . . . . 9 ⊢ ((𝑉‘(𝑖 + 1)) < 𝑋 → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊))
328	327	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊))
329	209	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
330		0red 11141	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
331	300	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
332	214	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
333	164	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
334	161	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
335	5	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
336		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) < 𝑋)
337	334, 335, 336	ltled 11288	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ≤ 𝑋)
338	334, 335	suble0d 11735	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0 ↔ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
339	337, 338	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0)
340	333, 339	eqbrtrd 5108	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) ≤ 0)
341	340	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ≤ 0)
342	329, 331, 330, 332, 341	ltletrd 11300	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
343	329, 330, 342	ltnsymd 11289	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
344	343	iffalsed 4478	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
345	344	oveq2d 7377	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
346	345	mpteq2dva 5179	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)))
347	346	oveq1d 7376	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
348	325, 328, 347	3eltr4d 2852	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
349	348	3adantl3 1170	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
350		simpl1 1193	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝜑)
351		simpl2 1194	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑖 ∈ (0..^𝑀))
352	5	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
353	352	3adantl3 1170	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
354	161	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
355	354	3adantl3 1170	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
356		neqne 2941	. . . . . . . . . . 11 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
357	356	necomd 2988	. . . . . . . . . 10 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
358	357	adantr 480	. . . . . . . . 9 ⊢ ((¬ (𝑉‘(𝑖 + 1)) = 𝑋 ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
359	358	3ad2antl3 1189	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
360		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
361	353, 355, 359, 360	lttri5d 45753	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
362		eqid 2737	. . . . . . . 8 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊))
363	272	adantlr 716	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
364	278	ad3antrrr 731	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
365	319	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
366		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌)
367	275	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ℂ)
368	366, 321, 367, 318	constlimc 46075	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘(𝑖 + 1))))
369	368	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑌 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘(𝑖 + 1))))
370	5	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ∈ ℝ)
371	161	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
372		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 < (𝑉‘(𝑖 + 1)))
373	370, 371, 372	ltnsymd 11289	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
374	373	iffalsed 4478	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑌)
375		0red 11141	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
376	240	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
377	209	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
378	190	eqcomd 2743	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 = (𝑋 − 𝑋))
379	378	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 = (𝑋 − 𝑋))
380	17	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉‘𝑖) ∈ ℝ)
381	41	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) ∈ ℝ^*)
382	296	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
383	162	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 ∈ ℝ)
384		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → ¬ 𝑋 ≤ (𝑉‘𝑖))
385	17	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) ∈ ℝ)
386	5	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 ∈ ℝ)
387	385, 386	ltnled 11287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → ((𝑉‘𝑖) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑉‘𝑖)))
388	384, 387	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) < 𝑋)
389	388	adantlr 716	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) < 𝑋)
390		simplr 769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 < (𝑉‘(𝑖 + 1)))
391	381, 382, 383, 389, 390	eliood 45949	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
392	11, 12, 13, 179	fourierdlem12 46568	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
393	392	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
394	391, 393	condan 818	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ≤ (𝑉‘𝑖))
395	370, 380, 370, 394	lesub1dd 11760	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑋 − 𝑋) ≤ ((𝑉‘𝑖) − 𝑋))
396	379, 395	eqbrtrd 5108	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ ((𝑉‘𝑖) − 𝑋))
397	145	eqcomd 2743	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖))
398	397	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖))
399	396, 398	breqtrd 5112	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ (𝑄‘𝑖))
400	399	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ≤ (𝑄‘𝑖))
401	244	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
402	375, 376, 377, 400, 401	lelttrd 11298	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
403	402	iftrued 4475	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
404	403	mpteq2dva 5179	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌))
405	404	oveq1d 7376	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘(𝑖 + 1))))
406	369, 374, 405	3eltr4d 2852	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
407	288, 362, 263, 363, 364, 365, 406	sublimc 46101	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
408	350, 351, 361, 407	syl21anc 838	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
409	349, 408	pm2.61dan 813	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
410	321, 264, 318	idlimc 46077	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim_ℂ (𝑄‘(𝑖 + 1))))
411	410	3adant3 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim_ℂ (𝑄‘(𝑖 + 1))))
412	164	3adant3 1133	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
413	305	3adant3 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
414	227	3adant3 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
415	356	3ad2ant3 1136	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
416	413, 414, 415	subne0d 11508	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≠ 0)
417	412, 416	eqnetrd 3000	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ≠ 0)
418	206	3adantl3 1170	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
419	418	neqned 2940	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
420	263, 264, 265, 281, 287, 409, 411, 417, 419	divlimc 46105	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim_ℂ (𝑄‘(𝑖 + 1))))
421		iffalse 4476	. . . . . 6 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
422	98, 421	eqtrid 2784	. . . . 5 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → 𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
423	422	3ad2ant3 1136	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
424		ioossre 13354	. . . . . . . . . . . . 13 ⊢ (-∞(,)𝑋) ⊆ ℝ
425	424	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (-∞(,)𝑋) ⊆ ℝ)
426	30, 425	fssresd 6702	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝑋)):(-∞(,)𝑋)⟶ℝ)
427	424, 52	sstrid 3934	. . . . . . . . . . 11 ⊢ (𝜑 → (-∞(,)𝑋) ⊆ ℂ)
428	39	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ∈ ℝ^*)
429	5	mnfltd 13069	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ < 𝑋)
430	56, 428, 5, 429	lptioo2cn 46094	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(-∞(,)𝑋)))
431	426, 427, 430, 36	limcrecl 46080	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ ℝ)
432	30, 5, 274, 431, 102	fourierdlem9 46565	. . . . . . . . 9 ⊢ (𝜑 → 𝐻:(-π[,]π)⟶ℝ)
433	432	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻:(-π[,]π)⟶ℝ)
434	433, 139	feqresmpt 6904	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)))
435	139	sselda 3922	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (-π[,]π))
436		0cnd 11131	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℂ)
437	278	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
438	272, 437	subcld 11499	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
439	282	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
440	206	neqned 2940	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
441	438, 439, 440	divcld 11925	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℂ)
442	436, 441	ifcld 4514	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ)
443	102	fvmpt2 6954	. . . . . . . . . 10 ⊢ ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
444	435, 442, 443	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
445	206	iffalsed 4478	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
446	444, 445	eqtrd 2772	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
447	446	mpteq2dva 5179	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
448	434, 447	eqtrd 2772	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
449	448	3adant3 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
450	449	oveq1d 7376	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim_ℂ (𝑄‘(𝑖 + 1))))
451	420, 423, 450	3eltr4d 2852	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
452	451	3expa 1119	. 2 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
453	262, 452	pm2.61dan 813	1 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3390 ⊆ wss 3890 ifcif 4467 {csn 4568 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5625 ran crn 5626 ↾ cres 5627 Fn wfn 6488 ⟶wf 6489 ‘cfv 6493 (class class class)co 7361 ↑_m cmap 8767 ℂcc 11030 ℝcr 11031 0cc0 11032 1c1 11033 + caddc 11035 -∞cmnf 11171 ℝ^*cxr 11172 < clt 11173 ≤ cle 11174 − cmin 11371 -cneg 11372 / cdiv 11801 ℕcn 12168 (,)cioo 13292 [,]cicc 13295 ...cfz 13455 ..^cfzo 13602 πcpi 16025 TopOpenctopn 17378 topGenctg 17394 ℂ_fldccnfld 21347 intcnt 22995 lim_ℂ climc 25842 D cdv 25843

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-inf2 9556 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110 ax-addf 11111

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-of 7625 df-om 7812 df-1st 7936 df-2nd 7937 df-supp 8105 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-er 8637 df-map 8769 df-pm 8770 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-fi 9318 df-sup 9349 df-inf 9350 df-oi 9419 df-card 9857 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-7 12243 df-8 12244 df-9 12245 df-n0 12432 df-z 12519 df-dec 12639 df-uz 12783 df-q 12893 df-rp 12937 df-xneg 13057 df-xadd 13058 df-xmul 13059 df-ioo 13296 df-ioc 13297 df-ico 13298 df-icc 13299 df-fz 13456 df-fzo 13603 df-fl 13745 df-seq 13958 df-exp 14018 df-fac 14230 df-bc 14259 df-hash 14287 df-shft 15023 df-cj 15055 df-re 15056 df-im 15057 df-sqrt 15191 df-abs 15192 df-limsup 15427 df-clim 15444 df-rlim 15445 df-sum 15643 df-ef 16026 df-sin 16028 df-cos 16029 df-pi 16031 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-mulr 17228 df-starv 17229 df-sca 17230 df-vsca 17231 df-ip 17232 df-tset 17233 df-ple 17234 df-ds 17236 df-unif 17237 df-hom 17238 df-cco 17239 df-rest 17379 df-topn 17380 df-0g 17398 df-gsum 17399 df-topgen 17400 df-pt 17401 df-prds 17404 df-xrs 17460 df-qtop 17465 df-imas 17466 df-xps 17468 df-mre 17542 df-mrc 17543 df-acs 17545 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-submnd 18746 df-mulg 19038 df-cntz 19286 df-cmn 19751 df-psmet 21339 df-xmet 21340 df-met 21341 df-bl 21342 df-mopn 21343 df-fbas 21344 df-fg 21345 df-cnfld 21348 df-top 22872 df-topon 22889 df-topsp 22911 df-bases 22924 df-cld 22997 df-ntr 22998 df-cls 22999 df-nei 23076 df-lp 23114 df-perf 23115 df-cn 23205 df-cnp 23206 df-haus 23293 df-cmp 23365 df-tx 23540 df-hmeo 23733 df-fil 23824 df-fm 23916 df-flim 23917 df-flf 23918 df-xms 24298 df-ms 24299 df-tms 24300 df-cncf 24858 df-limc 25846 df-dv 25847

This theorem is referenced by: fourierdlem88 46643 fourierdlem103 46658 fourierdlem104 46659

W3C validator