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 45627

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 13675	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
2		pire 26406	. . . . . . . . . . . 12 ⊢ π ∈ ℝ
3	2	renegcli 11546	. . . . . . . . . . 11 ⊢ -π ∈ ℝ
4	3	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → -π ∈ ℝ)
5		fourierdlem74.xre	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
6	4, 5	readdcld 11268	. . . . . . . . 9 ⊢ (𝜑 → (-π + 𝑋) ∈ ℝ)
7	2	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → π ∈ ℝ)
8	7, 5	readdcld 11268	. . . . . . . . 9 ⊢ (𝜑 → (π + 𝑋) ∈ ℝ)
9	6, 8	iccssred 13438	. . . . . . . 8 ⊢ (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
10	9	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
11		fourierdlem74.p	. . . . . . . . 9 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
12		fourierdlem74.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
13		fourierdlem74.v	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
14	11, 12, 13	fourierdlem15 45569	. . . . . . . 8 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
15	14	ffvelcdmda 7087	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
16	10, 15	sseldd 3974	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ℝ)
17	1, 16	sylan2 591	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
18	17	adantr 479	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘𝑖) ∈ ℝ)
19	5	ad2antrr 724	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℝ)
20	11	fourierdlem2 45556	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
21	12, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
22	13, 21	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
23	22	simprrd 772	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
24	23	r19.21bi 3239	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
25	24	adantr 479	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
26		eqcom 2732	. . . . . . 7 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 ↔ 𝑋 = (𝑉‘(𝑖 + 1)))
27	26	biimpi 215	. . . . . 6 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → 𝑋 = (𝑉‘(𝑖 + 1)))
28	27	adantl 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 = (𝑉‘(𝑖 + 1)))
29	25, 28	breqtrrd 5172	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘𝑖) < 𝑋)
30		fourierdlem74.f	. . . . . 6 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
31		ioossre 13412	. . . . . . 7 ⊢ ((𝑉‘𝑖)(,)𝑋) ⊆ ℝ
32	31	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑉‘𝑖)(,)𝑋) ⊆ ℝ)
33	30, 32	fssresd 6758	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ)
34	33	ad2antrr 724	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ)
35		limcresi 25827	. . . . . . . 8 ⊢ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋)
36		fourierdlem74.w	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
37	35, 36	sselid 3971	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
38	37	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
39		mnfxr 11296	. . . . . . . . . 10 ⊢ -∞ ∈ ℝ^*
40	39	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ^*)
41	17	rexrd 11289	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ^*)
42	17	mnfltd 13131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ < (𝑉‘𝑖))
43	40, 41, 42	xrltled 13156	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑉‘𝑖))
44		iooss1 13386	. . . . . . . . 9 ⊢ ((-∞ ∈ ℝ^* ∧ -∞ ≤ (𝑉‘𝑖)) → ((𝑉‘𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
45	40, 43, 44	syl2anc 582	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
46	45	resabs1d 6008	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) = (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)))
47	46	oveq1d 7428	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
48	38, 47	eleqtrd 2827	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
49	48	adantr 479	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑊 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
50		eqid 2725	. . . 4 ⊢ (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)))
51		ax-resscn 11190	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
52	51	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℂ)
53	30, 52	fssd 6734	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
54		ssid 3996	. . . . . . . . . 10 ⊢ ℝ ⊆ ℝ
55	54	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℝ)
56		eqid 2725	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
57	56	tgioo2 24732	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
58	56, 57	dvres 25853	. . . . . . . . 9 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑉‘𝑖)(,)𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))))
59	52, 53, 55, 32, 58	syl22anc 837	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))))
60		fourierdlem74.g	. . . . . . . . . . 11 ⊢ 𝐺 = (ℝ D 𝐹)
61	60	eqcomi 2734	. . . . . . . . . 10 ⊢ (ℝ D 𝐹) = 𝐺
62		ioontr 44955	. . . . . . . . . 10 ⊢ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋)) = ((𝑉‘𝑖)(,)𝑋)
63	61, 62	reseq12i 5978	. . . . . . . . 9 ⊢ ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋))
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
65	59, 64	eqtrd 2765	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
66	65	dmeqd 5903	. . . . . 6 ⊢ (𝜑 → dom (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
67	66	ad2antrr 724	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
68		fourierdlem74.gcn	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
69	68	adantr 479	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
70		oveq2 7421	. . . . . . . . . 10 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) = ((𝑉‘𝑖)(,)𝑋))
71	70	reseq2d 5980	. . . . . . . . 9 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
72	71, 70	feq12d 6705	. . . . . . . 8 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ))
73	72	adantl 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ))
74	69, 73	mpbid 231	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ)
75		fdm 6726	. . . . . 6 ⊢ ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ → dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) = ((𝑉‘𝑖)(,)𝑋))
76	74, 75	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) = ((𝑉‘𝑖)(,)𝑋))
77	67, 76	eqtrd 2765	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = ((𝑉‘𝑖)(,)𝑋))
78		limcresi 25827	. . . . . . . 8 ⊢ ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋)
79	45	resabs1d 6008	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
80	79	oveq1d 7428	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
81	78, 80	sseqtrid 4026	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
82		fourierdlem74.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
83	82	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
84	81, 83	sseldd 3974	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
85	59, 64	eqtr2d 2766	. . . . . . . 8 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) = (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))))
86	85	oveq1d 7428	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
87	86	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
88	84, 87	eleqtrd 2827	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
89	88	adantr 479	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
90		eqid 2725	. . . 4 ⊢ (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
91		oveq2 7421	. . . . . . 7 ⊢ (𝑥 = 𝑠 → (𝑋 + 𝑥) = (𝑋 + 𝑠))
92	91	fveq2d 6894	. . . . . 6 ⊢ (𝑥 = 𝑠 → ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑥)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
93	92	oveq1d 7428	. . . . 5 ⊢ (𝑥 = 𝑠 → (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊) = (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
94	93	cbvmptv 5257	. . . 4 ⊢ (𝑥 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊)) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
95		id 22	. . . . 5 ⊢ (𝑥 = 𝑠 → 𝑥 = 𝑠)
96	95	cbvmptv 5257	. . . 4 ⊢ (𝑥 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ 𝑥) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ 𝑠)
97	18, 19, 29, 34, 49, 50, 77, 89, 90, 94, 96	fourierdlem60 45613	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim_ℂ 0))
98		fourierdlem74.a	. . . . 5 ⊢ 𝐴 = if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
99		iftrue 4531	. . . . 5 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = 𝐸)
100	98, 99	eqtrid 2777	. . . 4 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → 𝐴 = 𝐸)
101	100	adantl 480	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = 𝐸)
102		fourierdlem74.h	. . . . . . 7 ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
103	102	reseq1i 5976	. . . . . 6 ⊢ (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
104	103	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
105		ioossicc 13437	. . . . . . . 8 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
106	3	rexri 11297	. . . . . . . . . 10 ⊢ -π ∈ ℝ^*
107	106	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ^*)
108	2	rexri 11297	. . . . . . . . . 10 ⊢ π ∈ ℝ^*
109	108	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈ ℝ^*)
110	3	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ∈ ℝ)
111	2	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈ ℝ)
112	5	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
113	16, 112	resubcld 11667	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
114	4	recnd 11267	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -π ∈ ℂ)
115	5	recnd 11267	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ ℂ)
116	114, 115	pncand 11597	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
117	116	eqcomd 2731	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π = ((-π + 𝑋) − 𝑋))
118	117	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π = ((-π + 𝑋) − 𝑋))
119	6	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ∈ ℝ)
120	8	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (π + 𝑋) ∈ ℝ)
121		elicc2 13416	. . . . . . . . . . . . . . . . 17 ⊢ (((-π + 𝑋) ∈ ℝ ∧ (π + 𝑋) ∈ ℝ) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))))
122	119, 120, 121	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))))
123	15, 122	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋)))
124	123	simp2d 1140	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ≤ (𝑉‘𝑖))
125	119, 16, 112, 124	lesub1dd 11855	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋) − 𝑋) ≤ ((𝑉‘𝑖) − 𝑋))
126	118, 125	eqbrtrd 5166	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ≤ ((𝑉‘𝑖) − 𝑋))
127	123	simp3d 1141	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ≤ (π + 𝑋))
128	16, 120, 112, 127	lesub1dd 11855	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ ((π + 𝑋) − 𝑋))
129	111	recnd 11267	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈ ℂ)
130	115	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℂ)
131	129, 130	pncand 11597	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((π + 𝑋) − 𝑋) = π)
132	128, 131	breqtrd 5170	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ π)
133	110, 111, 113, 126, 132	eliccd 44948	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π))
134		fourierdlem74.q	. . . . . . . . . . 11 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
135	133, 134	fmptd 7117	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
136	135	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
137		simpr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
138	107, 109, 136, 137	fourierdlem8 45562	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
139	105, 138	sstrid 3985	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
140	139	resmptd 6040	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
141	140	adantr 479	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
142	1	adantl 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
143	1, 113	sylan2 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
144	134	fvmpt2 7009	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
145	142, 143, 144	syl2anc 582	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
146	145	adantr 479	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
147		fveq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
148	147	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
149	148	cbvmptv 5257	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
150	134, 149	eqtri 2753	. . . . . . . . . . 11 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
151	150	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
152		fveq2 6890	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
153	152	oveq1d 7428	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
154	153	adantl 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
155		fzofzp1 13756	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
156	155	adantl 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
157	22	simpld 493	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ∈ (ℝ ↑_m (0...𝑀)))
158		elmapi 8861	. . . . . . . . . . . . . 14 ⊢ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
159	157, 158	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶ℝ)
160	159	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
161	160, 156	ffvelcdmd 7088	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
162	5	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
163	161, 162	resubcld 11667	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
164	151, 154, 156, 163	fvmptd 7005	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
165	164	adantr 479	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
166		oveq1 7420	. . . . . . . . 9 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋 − 𝑋))
167	166	adantl 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋 − 𝑋))
168	115	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
169	168	subidd 11584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋 − 𝑋) = 0)
170	1, 169	sylanl2 679	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋 − 𝑋) = 0)
171	165, 167, 170	3eqtrd 2769	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = 0)
172	146, 171	oveq12d 7431	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑉‘𝑖) − 𝑋)(,)0))
173		simplr 767	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
174		fourierdlem74.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
175	12	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑀 ∈ ℕ)
176	4, 7, 5, 11, 174, 12, 13, 134	fourierdlem14 45568	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀))
177	176	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑄 ∈ (𝑂‘𝑀))
178		simpr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 = 0)
179		fourierdlem74.x	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ ran 𝑉)
180		ffn 6717	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)) → 𝑉 Fn (0...𝑀))
181		fvelrnb 6952	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 Fn (0...𝑀) → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋))
182	14, 180, 181	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋))
183	179, 182	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋)
184		simpr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
185	134	fvmpt2 7009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
186	184, 133, 185	syl2anc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
187	186	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
188		oveq1 7420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉‘𝑖) = 𝑋 → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋))
189	188	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋))
190	115	subidd 11584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑋 − 𝑋) = 0)
191	190	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑋 − 𝑋) = 0)
192	187, 189, 191	3eqtrd 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = 0)
193	192	ex 411	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) = 𝑋 → (𝑄‘𝑖) = 0))
194	193	reximdva 3158	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
195	183, 194	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0)
196	113, 134	fmptd 7117	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
197		ffn 6717	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
198		fvelrnb 6952	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 Fn (0...𝑀) → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
199	196, 197, 198	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
200	195, 199	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ran 𝑄)
201	200	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 = 0) → 0 ∈ ran 𝑄)
202	178, 201	eqeltrd 2825	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 ∈ ran 𝑄)
203	174, 175, 177, 202	fourierdlem12 45566	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
204	203	an32s 650	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
205	204	adantlr 713	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
206	173, 205	pm2.65da 815	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
207	206	adantlr 713	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
208	207	iffalsed 4536	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
209		elioore 13381	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
210	209	adantl 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
211		0red 11242	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
212		elioo3g 13380	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ℝ^*) ∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1)))))
213	212	biimpi 215	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ℝ^*) ∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1)))))
214	213	simprrd 772	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 < (𝑄‘(𝑖 + 1)))
215	214	adantl 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
216	171	adantr 479	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) = 0)
217	215, 216	breqtrd 5170	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
218	210, 211, 217	ltnsymd 11388	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
219	218	iffalsed 4536	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
220	219	oveq2d 7429	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
221	220	oveq1d 7428	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
222	41	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
223	5	rexrd 11289	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
224	223	ad3antrrr 728	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ^*)
225	162	ad2antrr 724	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
226	225, 210	readdcld 11268	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
227	115	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
228		iccssre 13433	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
229	3, 2, 228	mp2an 690	. . . . . . . . . . . . . . . . . 18 ⊢ (-π[,]π) ⊆ ℝ
230	229, 51	sstri 3983	. . . . . . . . . . . . . . . . 17 ⊢ (-π[,]π) ⊆ ℂ
231	186, 133	eqeltrd 2825	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π))
232	1, 231	sylan2 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π))
233	230, 232	sselid 3971	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
234	227, 233	addcomd 11441	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘𝑖)) = ((𝑄‘𝑖) + 𝑋))
235	145	oveq1d 7428	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑋) = (((𝑉‘𝑖) − 𝑋) + 𝑋))
236	17	recnd 11267	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℂ)
237	236, 227	npcand 11600	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑉‘𝑖) − 𝑋) + 𝑋) = (𝑉‘𝑖))
238	234, 235, 237	3eqtrrd 2770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
239	238	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
240	145, 143	eqeltrd 2825	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
241	240	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
242	209	adantl 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
243	5	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
244	213	simprld 770	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) < 𝑠)
245	244	adantl 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
246	241, 242, 243, 245	ltadd2dd 11398	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
247	239, 246	eqbrtrd 5166	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
248	247	adantlr 713	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
249		ltaddneg 11454	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
250	210, 225, 249	syl2anc 582	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
251	217, 250	mpbid 231	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < 𝑋)
252	222, 224, 226, 248, 251	eliood 44942	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)𝑋))
253		fvres 6909	. . . . . . . . . . 11 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)𝑋) → ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
254	253	eqcomd 2731	. . . . . . . . . 10 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)𝑋) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
255	252, 254	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
256	255	oveq1d 7428	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝑊) = (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
257	256	oveq1d 7428	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠) = ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
258	208, 221, 257	3eqtrd 2769	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
259	172, 258	mpteq12dva 5233	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
260	104, 141, 259	3eqtrd 2769	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
261	260, 171	oveq12d 7431	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim_ℂ 0))
262	97, 101, 261	3eltr4d 2840	. 2 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
263		eqid 2725	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
264		eqid 2725	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠)
265		eqid 2725	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
266	30	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℝ)
267	5	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
268	209	adantl 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
269	267, 268	readdcld 11268	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
270	266, 269	ffvelcdmd 7088	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
271	270	recnd 11267	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
272	271	adantlr 713	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
273	272	3adantl3 1165	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
274		fourierdlem74.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ ℝ)
275	274	recnd 11267	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℂ)
276		limccl 25817	. . . . . . . . . 10 ⊢ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ ℂ
277	276, 36	sselid 3971	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ℂ)
278	275, 277	ifcld 4571	. . . . . . . 8 ⊢ (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
279	278	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
280	279	3ad2antl1 1182	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
281	273, 280	subcld 11596	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
282	209	recnd 11267	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℂ)
283	282	adantl 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
284		velsn 4641	. . . . . . . 8 ⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0)
285	206, 284	sylnibr 328	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
286	285	3adantl3 1165	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
287	283, 286	eldifd 3952	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
288		eqid 2725	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
289		eqid 2725	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊)
290		eqid 2725	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
291	277	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑊 ∈ ℂ)
292	30	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℝ)
293		ioossre 13412	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
294	293	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
295	41	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
296	161	rexrd 11289	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
297	296	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
298	269	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
299	196	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
300	299, 156	ffvelcdmd 7088	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
301	300	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
302	214	adantl 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
303	242, 301, 243, 302	ltadd2dd 11398	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
304	164	oveq2d 7429	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
305	161	recnd 11267	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
306	227, 305	pncan3d 11599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
307	304, 306	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
308	307	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
309	303, 308	breqtrd 5170	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
310	295, 297, 298, 247, 309	eliood 44942	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
311		ioossre 13412	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
312	311	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
313	242, 302	ltned 11375	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
314		fourierdlem74.r	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
315	307	eqcomd 2731	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
316	315	oveq2d 7429	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
317	314, 316	eleqtrd 2827	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
318	300	recnd 11267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
319	292, 162, 294, 288, 310, 312, 313, 317, 318	fourierdlem53 45606	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
320		ioosscn 13413	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
321	320	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
322	277	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ℂ)
323	289, 321, 322, 318	constlimc 45071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) lim_ℂ (𝑄‘(𝑖 + 1))))
324	288, 289, 290, 272, 291, 319, 323	sublimc 45099	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
325	324	adantr 479	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
326		iftrue 4531	. . . . . . . . . 10 ⊢ ((𝑉‘(𝑖 + 1)) < 𝑋 → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑊)
327	326	oveq2d 7429	. . . . . . . . 9 ⊢ ((𝑉‘(𝑖 + 1)) < 𝑋 → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊))
328	327	adantl 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊))
329	209	adantl 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
330		0red 11242	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
331	300	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
332	214	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
333	164	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
334	161	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
335	5	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
336		simpr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) < 𝑋)
337	334, 335, 336	ltled 11387	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ≤ 𝑋)
338	334, 335	suble0d 11830	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0 ↔ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
339	337, 338	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0)
340	333, 339	eqbrtrd 5166	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) ≤ 0)
341	340	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ≤ 0)
342	329, 331, 330, 332, 341	ltletrd 11399	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
343	329, 330, 342	ltnsymd 11388	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
344	343	iffalsed 4536	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
345	344	oveq2d 7429	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
346	345	mpteq2dva 5244	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)))
347	346	oveq1d 7428	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
348	325, 328, 347	3eltr4d 2840	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
349	348	3adantl3 1165	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
350		simpl1 1188	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝜑)
351		simpl2 1189	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑖 ∈ (0..^𝑀))
352	5	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
353	352	3adantl3 1165	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
354	161	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
355	354	3adantl3 1165	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
356		neqne 2938	. . . . . . . . . . 11 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
357	356	necomd 2986	. . . . . . . . . 10 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
358	357	adantr 479	. . . . . . . . 9 ⊢ ((¬ (𝑉‘(𝑖 + 1)) = 𝑋 ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
359	358	3ad2antl3 1184	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
360		simpr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
361	353, 355, 359, 360	lttri5d 44740	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
362		eqid 2725	. . . . . . . 8 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊))
363	272	adantlr 713	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
364	278	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
365	319	adantr 479	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
366		eqid 2725	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌)
367	275	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ℂ)
368	366, 321, 367, 318	constlimc 45071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘(𝑖 + 1))))
369	368	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑌 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘(𝑖 + 1))))
370	5	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ∈ ℝ)
371	161	adantr 479	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
372		simpr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 < (𝑉‘(𝑖 + 1)))
373	370, 371, 372	ltnsymd 11388	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
374	373	iffalsed 4536	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑌)
375		0red 11242	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
376	240	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
377	209	adantl 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
378	190	eqcomd 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 = (𝑋 − 𝑋))
379	378	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 = (𝑋 − 𝑋))
380	17	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉‘𝑖) ∈ ℝ)
381	41	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) ∈ ℝ^*)
382	296	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
383	162	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 ∈ ℝ)
384		simpr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → ¬ 𝑋 ≤ (𝑉‘𝑖))
385	17	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) ∈ ℝ)
386	5	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 ∈ ℝ)
387	385, 386	ltnled 11386	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → ((𝑉‘𝑖) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑉‘𝑖)))
388	384, 387	mpbird 256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) < 𝑋)
389	388	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) < 𝑋)
390		simplr 767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 < (𝑉‘(𝑖 + 1)))
391	381, 382, 383, 389, 390	eliood 44942	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
392	11, 12, 13, 179	fourierdlem12 45566	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
393	392	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
394	391, 393	condan 816	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ≤ (𝑉‘𝑖))
395	370, 380, 370, 394	lesub1dd 11855	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑋 − 𝑋) ≤ ((𝑉‘𝑖) − 𝑋))
396	379, 395	eqbrtrd 5166	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ ((𝑉‘𝑖) − 𝑋))
397	145	eqcomd 2731	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖))
398	397	adantr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖))
399	396, 398	breqtrd 5170	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ (𝑄‘𝑖))
400	399	adantr 479	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ≤ (𝑄‘𝑖))
401	244	adantl 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
402	375, 376, 377, 400, 401	lelttrd 11397	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
403	402	iftrued 4533	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
404	403	mpteq2dva 5244	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌))
405	404	oveq1d 7428	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘(𝑖 + 1))))
406	369, 374, 405	3eltr4d 2840	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
407	288, 362, 263, 363, 364, 365, 406	sublimc 45099	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
408	350, 351, 361, 407	syl21anc 836	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
409	349, 408	pm2.61dan 811	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
410	321, 264, 318	idlimc 45073	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim_ℂ (𝑄‘(𝑖 + 1))))
411	410	3adant3 1129	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim_ℂ (𝑄‘(𝑖 + 1))))
412	164	3adant3 1129	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
413	305	3adant3 1129	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
414	227	3adant3 1129	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
415	356	3ad2ant3 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
416	413, 414, 415	subne0d 11605	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≠ 0)
417	412, 416	eqnetrd 2998	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ≠ 0)
418	206	3adantl3 1165	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
419	418	neqned 2937	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
420	263, 264, 265, 281, 287, 409, 411, 417, 419	divlimc 45103	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim_ℂ (𝑄‘(𝑖 + 1))))
421		iffalse 4534	. . . . . 6 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
422	98, 421	eqtrid 2777	. . . . 5 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → 𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
423	422	3ad2ant3 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
424		ioossre 13412	. . . . . . . . . . . . 13 ⊢ (-∞(,)𝑋) ⊆ ℝ
425	424	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (-∞(,)𝑋) ⊆ ℝ)
426	30, 425	fssresd 6758	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝑋)):(-∞(,)𝑋)⟶ℝ)
427	424, 52	sstrid 3985	. . . . . . . . . . 11 ⊢ (𝜑 → (-∞(,)𝑋) ⊆ ℂ)
428	39	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ∈ ℝ^*)
429	5	mnfltd 13131	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ < 𝑋)
430	56, 428, 5, 429	lptioo2cn 45092	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(-∞(,)𝑋)))
431	426, 427, 430, 36	limcrecl 45076	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ ℝ)
432	30, 5, 274, 431, 102	fourierdlem9 45563	. . . . . . . . 9 ⊢ (𝜑 → 𝐻:(-π[,]π)⟶ℝ)
433	432	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻:(-π[,]π)⟶ℝ)
434	433, 139	feqresmpt 6961	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)))
435	139	sselda 3973	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (-π[,]π))
436		0cnd 11232	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℂ)
437	278	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
438	272, 437	subcld 11596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
439	282	adantl 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
440	206	neqned 2937	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
441	438, 439, 440	divcld 12015	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℂ)
442	436, 441	ifcld 4571	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ)
443	102	fvmpt2 7009	. . . . . . . . . 10 ⊢ ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
444	435, 442, 443	syl2anc 582	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
445	206	iffalsed 4536	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
446	444, 445	eqtrd 2765	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
447	446	mpteq2dva 5244	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
448	434, 447	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
449	448	3adant3 1129	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
450	449	oveq1d 7428	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim_ℂ (𝑄‘(𝑖 + 1))))
451	420, 423, 450	3eltr4d 2840	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
452	451	3expa 1115	. 2 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
453	262, 452	pm2.61dan 811	1 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ≠ wne 2930 ∀wral 3051 ∃wrex 3060 {crab 3419 ⊆ wss 3941 ifcif 4525 {csn 4625 class class class wbr 5144 ↦ cmpt 5227 dom cdm 5673 ran crn 5674 ↾ cres 5675 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 (class class class)co 7413 ↑_m cmap 8838 ℂcc 11131 ℝcr 11132 0cc0 11133 1c1 11134 + caddc 11136 -∞cmnf 11271 ℝ^*cxr 11272 < clt 11273 ≤ cle 11274 − cmin 11469 -cneg 11470 / cdiv 11896 ℕcn 12237 (,)cioo 13351 [,]cicc 13354 ...cfz 13511 ..^cfzo 13654 πcpi 16037 TopOpenctopn 17397 topGenctg 17413 ℂ_fldccnfld 21278 intcnt 22934 lim_ℂ climc 25804 D cdv 25805

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5281 ax-sep 5295 ax-nul 5302 ax-pow 5360 ax-pr 5424 ax-un 7735 ax-inf2 9659 ax-cnex 11189 ax-resscn 11190 ax-1cn 11191 ax-icn 11192 ax-addcl 11193 ax-addrcl 11194 ax-mulcl 11195 ax-mulrcl 11196 ax-mulcom 11197 ax-addass 11198 ax-mulass 11199 ax-distr 11200 ax-i2m1 11201 ax-1ne0 11202 ax-1rid 11203 ax-rnegex 11204 ax-rrecex 11205 ax-cnre 11206 ax-pre-lttri 11207 ax-pre-lttrn 11208 ax-pre-ltadd 11209 ax-pre-mulgt0 11210 ax-pre-sup 11211 ax-addf 11212

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-pss 3961 df-nul 4320 df-if 4526 df-pw 4601 df-sn 4626 df-pr 4628 df-tp 4630 df-op 4632 df-uni 4905 df-int 4946 df-iun 4994 df-iin 4995 df-br 5145 df-opab 5207 df-mpt 5228 df-tr 5262 df-id 5571 df-eprel 5577 df-po 5585 df-so 5586 df-fr 5628 df-se 5629 df-we 5630 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7369 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7679 df-om 7866 df-1st 7987 df-2nd 7988 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-er 8718 df-map 8840 df-pm 8841 df-ixp 8910 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fsupp 9381 df-fi 9429 df-sup 9460 df-inf 9461 df-oi 9528 df-card 9957 df-pnf 11275 df-mnf 11276 df-xr 11277 df-ltxr 11278 df-le 11279 df-sub 11471 df-neg 11472 df-div 11897 df-nn 12238 df-2 12300 df-3 12301 df-4 12302 df-5 12303 df-6 12304 df-7 12305 df-8 12306 df-9 12307 df-n0 12498 df-z 12584 df-dec 12703 df-uz 12848 df-q 12958 df-rp 13002 df-xneg 13119 df-xadd 13120 df-xmul 13121 df-ioo 13355 df-ioc 13356 df-ico 13357 df-icc 13358 df-fz 13512 df-fzo 13655 df-fl 13784 df-seq 13994 df-exp 14054 df-fac 14260 df-bc 14289 df-hash 14317 df-shft 15041 df-cj 15073 df-re 15074 df-im 15075 df-sqrt 15209 df-abs 15210 df-limsup 15442 df-clim 15459 df-rlim 15460 df-sum 15660 df-ef 16038 df-sin 16040 df-cos 16041 df-pi 16043 df-struct 17110 df-sets 17127 df-slot 17145 df-ndx 17157 df-base 17175 df-ress 17204 df-plusg 17240 df-mulr 17241 df-starv 17242 df-sca 17243 df-vsca 17244 df-ip 17245 df-tset 17246 df-ple 17247 df-ds 17249 df-unif 17250 df-hom 17251 df-cco 17252 df-rest 17398 df-topn 17399 df-0g 17417 df-gsum 17418 df-topgen 17419 df-pt 17420 df-prds 17423 df-xrs 17478 df-qtop 17483 df-imas 17484 df-xps 17486 df-mre 17560 df-mrc 17561 df-acs 17563 df-mgm 18594 df-sgrp 18673 df-mnd 18689 df-submnd 18735 df-mulg 19023 df-cntz 19267 df-cmn 19736 df-psmet 21270 df-xmet 21271 df-met 21272 df-bl 21273 df-mopn 21274 df-fbas 21275 df-fg 21276 df-cnfld 21279 df-top 22809 df-topon 22826 df-topsp 22848 df-bases 22862 df-cld 22936 df-ntr 22937 df-cls 22938 df-nei 23015 df-lp 23053 df-perf 23054 df-cn 23144 df-cnp 23145 df-haus 23232 df-cmp 23304 df-tx 23479 df-hmeo 23672 df-fil 23763 df-fm 23855 df-flim 23856 df-flf 23857 df-xms 24239 df-ms 24240 df-tms 24241 df-cncf 24811 df-limc 25808 df-dv 25809

This theorem is referenced by: fourierdlem88 45641 fourierdlem103 45656 fourierdlem104 45657

W3C validator