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 46623

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 13621	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
2		pire 26439	. . . . . . . . . . . 12 ⊢ π ∈ ℝ
3	2	renegcli 11446	. . . . . . . . . . 11 ⊢ -π ∈ ℝ
4	3	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → -π ∈ ℝ)
5		fourierdlem74.xre	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
6	4, 5	readdcld 11165	. . . . . . . . 9 ⊢ (𝜑 → (-π + 𝑋) ∈ ℝ)
7	2	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → π ∈ ℝ)
8	7, 5	readdcld 11165	. . . . . . . . 9 ⊢ (𝜑 → (π + 𝑋) ∈ ℝ)
9	6, 8	iccssred 13378	. . . . . . . 8 ⊢ (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
10	9	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
11		fourierdlem74.p	. . . . . . . . 9 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
12		fourierdlem74.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
13		fourierdlem74.v	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
14	11, 12, 13	fourierdlem15 46565	. . . . . . . 8 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
15	14	ffvelcdmda 7025	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
16	10, 15	sseldd 3916	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ℝ)
17	1, 16	sylan2 599	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
18	17	adantr 481	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘𝑖) ∈ ℝ)
19	5	ad2antrr 732	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℝ)
20	11	fourierdlem2 46552	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
21	12, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
22	13, 21	mpbid 233	. . . . . . . 8 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
23	22	simprrd 779	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
24	23	r19.21bi 3231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
25	24	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
26		eqcom 2746	. . . . . 6 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 ↔ 𝑋 = (𝑉‘(𝑖 + 1)))
27	26	bilani 505	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 = (𝑉‘(𝑖 + 1)))
28	25, 27	breqtrrd 5100	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘𝑖) < 𝑋)
29		fourierdlem74.f	. . . . . 6 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
30		ioossre 13351	. . . . . . 7 ⊢ ((𝑉‘𝑖)(,)𝑋) ⊆ ℝ
31	30	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑉‘𝑖)(,)𝑋) ⊆ ℝ)
32	29, 31	fssresd 6694	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ)
33	32	ad2antrr 732	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ)
34		limcresi 25870	. . . . . . . 8 ⊢ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋)
35		fourierdlem74.w	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
36	34, 35	sselid 3913	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
37	36	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
38		mnfxr 11193	. . . . . . . . . 10 ⊢ -∞ ∈ ℝ^*
39	38	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ^*)
40	17	rexrd 11186	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ^*)
41	17	mnfltd 13066	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ < (𝑉‘𝑖))
42	39, 40, 41	xrltled 13092	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑉‘𝑖))
43		iooss1 13324	. . . . . . . . 9 ⊢ ((-∞ ∈ ℝ^* ∧ -∞ ≤ (𝑉‘𝑖)) → ((𝑉‘𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
44	39, 42, 43	syl2anc 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
45	44	resabs1d 5960	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) = (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)))
46	45	oveq1d 7371	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
47	37, 46	eleqtrd 2841	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
48	47	adantr 481	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑊 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
49		eqid 2739	. . . 4 ⊢ (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋)))
50		ax-resscn 11086	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
51	50	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℂ)
52	29, 51	fssd 6672	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
53		ssid 3937	. . . . . . . . . 10 ⊢ ℝ ⊆ ℝ
54	53	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ ⊆ ℝ)
55		eqid 2739	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
56		tgioo4 24788	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
57	55, 56	dvres 25896	. . . . . . . . 9 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑉‘𝑖)(,)𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))))
58	51, 52, 54, 31, 57	syl22anc 844	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))))
59		fourierdlem74.g	. . . . . . . . . . 11 ⊢ 𝐺 = (ℝ D 𝐹)
60	59	eqcomi 2748	. . . . . . . . . 10 ⊢ (ℝ D 𝐹) = 𝐺
61		ioontr 45956	. . . . . . . . . 10 ⊢ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋)) = ((𝑉‘𝑖)(,)𝑋)
62	60, 61	reseq12i 5929	. . . . . . . . 9 ⊢ ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋))
63	62	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉‘𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
64	58, 63	eqtrd 2774	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
65	64	dmeqd 5847	. . . . . 6 ⊢ (𝜑 → dom (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
66	65	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
67		fourierdlem74.gcn	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
68	67	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
69		oveq2 7364	. . . . . . . . . 10 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) = ((𝑉‘𝑖)(,)𝑋))
70	69	reseq2d 5931	. . . . . . . . 9 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
71	70, 69	feq12d 6643	. . . . . . . 8 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ))
72	71	adantl 482	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ))
73	68, 72	mpbid 233	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ)
74		fdm 6664	. . . . . 6 ⊢ ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)):((𝑉‘𝑖)(,)𝑋)⟶ℝ → dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) = ((𝑉‘𝑖)(,)𝑋))
75	73, 74	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) = ((𝑉‘𝑖)(,)𝑋))
76	66, 75	eqtrd 2774	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) = ((𝑉‘𝑖)(,)𝑋))
77		limcresi 25870	. . . . . . . 8 ⊢ ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋)
78	44	resabs1d 5960	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) = (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)))
79	78	oveq1d 7371	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
80	77, 79	sseqtrid 3957	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
81		fourierdlem74.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
82	81	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
83	80, 82	sseldd 3916	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋))
84	58, 63	eqtr2d 2775	. . . . . . . 8 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) = (ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))))
85	84	oveq1d 7371	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
86	85	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑉‘𝑖)(,)𝑋)) lim_ℂ 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
87	83, 86	eleqtrd 2841	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
88	87	adantr 481	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))) lim_ℂ 𝑋))
89		eqid 2739	. . . 4 ⊢ (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
90		oveq2 7364	. . . . . . 7 ⊢ (𝑥 = 𝑠 → (𝑋 + 𝑥) = (𝑋 + 𝑠))
91	90	fveq2d 6831	. . . . . 6 ⊢ (𝑥 = 𝑠 → ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑥)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
92	91	oveq1d 7371	. . . . 5 ⊢ (𝑥 = 𝑠 → (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊) = (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
93	92	cbvmptv 5176	. . . 4 ⊢ (𝑥 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊)) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
94		id 22	. . . . 5 ⊢ (𝑥 = 𝑠 → 𝑥 = 𝑠)
95	94	cbvmptv 5176	. . . 4 ⊢ (𝑥 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ 𝑥) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ 𝑠)
96	18, 19, 28, 33, 48, 49, 76, 88, 89, 93, 95	fourierdlem60 46609	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim_ℂ 0))
97		fourierdlem74.a	. . . . 5 ⊢ 𝐴 = if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
98		iftrue 4460	. . . . 5 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = 𝐸)
99	97, 98	eqtrid 2786	. . . 4 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → 𝐴 = 𝐸)
100	99	adantl 482	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = 𝐸)
101		fourierdlem74.h	. . . . . . 7 ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
102	101	reseq1i 5927	. . . . . 6 ⊢ (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
103	102	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
104		ioossicc 13377	. . . . . . . 8 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
105	3	rexri 11194	. . . . . . . . . 10 ⊢ -π ∈ ℝ^*
106	105	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ^*)
107	2	rexri 11194	. . . . . . . . . 10 ⊢ π ∈ ℝ^*
108	107	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈ ℝ^*)
109	3	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ∈ ℝ)
110	2	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈ ℝ)
111	5	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
112	16, 111	resubcld 11569	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
113	4	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -π ∈ ℂ)
114	5	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ ℂ)
115	113, 114	pncand 11497	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
116	115	eqcomd 2745	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π = ((-π + 𝑋) − 𝑋))
117	116	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π = ((-π + 𝑋) − 𝑋))
118	6	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ∈ ℝ)
119	8	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (π + 𝑋) ∈ ℝ)
120		elicc2 13355	. . . . . . . . . . . . . . . . 17 ⊢ (((-π + 𝑋) ∈ ℝ ∧ (π + 𝑋) ∈ ℝ) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))))
121	118, 119, 120	syl2anc 590	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋))))
122	15, 121	mpbid 233	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (π + 𝑋)))
123	122	simp2d 1149	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ≤ (𝑉‘𝑖))
124	118, 16, 111, 123	lesub1dd 11757	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((-π + 𝑋) − 𝑋) ≤ ((𝑉‘𝑖) − 𝑋))
125	117, 124	eqbrtrd 5094	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → -π ≤ ((𝑉‘𝑖) − 𝑋))
126	122	simp3d 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ≤ (π + 𝑋))
127	16, 119, 111, 126	lesub1dd 11757	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ ((π + 𝑋) − 𝑋))
128	110	recnd 11164	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → π ∈ ℂ)
129	114	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℂ)
130	128, 129	pncand 11497	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((π + 𝑋) − 𝑋) = π)
131	127, 130	breqtrd 5098	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ≤ π)
132	109, 110, 112, 125, 131	eliccd 45949	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π))
133		fourierdlem74.q	. . . . . . . . . . 11 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
134	132, 133	fmptd 7055	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
135	134	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
136		simpr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
137	106, 108, 135, 136	fourierdlem8 46558	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
138	104, 137	sstrid 3926	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
139	138	resmptd 5992	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
140	139	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
141	1	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
142	1, 112	sylan2 599	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
143	133	fvmpt2 6947	. . . . . . . . 9 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
144	141, 142, 143	syl2anc 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
145	144	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
146		fveq2 6827	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
147	146	oveq1d 7371	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
148	147	cbvmptv 5176	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
149	133, 148	eqtri 2762	. . . . . . . . . . 11 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
150	149	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
151		fveq2 6827	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
152	151	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
153	152	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
154		fzofzp1 13710	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
155	154	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
156	22	simpld 495	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ∈ (ℝ ↑_m (0...𝑀)))
157		elmapi 8786	. . . . . . . . . . . . . 14 ⊢ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
158	156, 157	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶ℝ)
159	158	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
160	159, 155	ffvelcdmd 7026	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
161	5	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
162	160, 161	resubcld 11569	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
163	150, 153, 155, 162	fvmptd 6943	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
164	163	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
165		oveq1 7363	. . . . . . . . 9 ⊢ ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋 − 𝑋))
166	165	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋 − 𝑋))
167	114	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
168	167	subidd 11484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋 − 𝑋) = 0)
169	1, 168	sylanl2 687	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋 − 𝑋) = 0)
170	164, 166, 169	3eqtrd 2778	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = 0)
171	145, 170	oveq12d 7374	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑉‘𝑖) − 𝑋)(,)0))
172		simplr 774	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
173		fourierdlem74.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
174	12	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑀 ∈ ℕ)
175	4, 7, 5, 11, 173, 12, 13, 133	fourierdlem14 46564	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀))
176	175	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑄 ∈ (𝑂‘𝑀))
177		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 = 0)
178		fourierdlem74.x	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ ran 𝑉)
179		ffn 6655	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)) → 𝑉 Fn (0...𝑀))
180		fvelrnb 6887	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑉 Fn (0...𝑀) → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋))
181	14, 179, 180	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋))
182	178, 181	mpbid 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋)
183		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
184	133	fvmpt2 6947	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ (-π[,]π)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
185	183, 132, 184	syl2anc 590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
186	185	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
187		oveq1 7363	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉‘𝑖) = 𝑋 → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋))
188	187	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → ((𝑉‘𝑖) − 𝑋) = (𝑋 − 𝑋))
189	114	subidd 11484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑋 − 𝑋) = 0)
190	189	ad2antrr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑋 − 𝑋) = 0)
191	186, 188, 190	3eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑉‘𝑖) = 𝑋) → (𝑄‘𝑖) = 0)
192	191	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) = 𝑋 → (𝑄‘𝑖) = 0))
193	192	reximdva 3152	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑉‘𝑖) = 𝑋 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
194	182, 193	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0)
195	112, 133	fmptd 7055	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
196		ffn 6655	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
197		fvelrnb 6887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 Fn (0...𝑀) → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
198	195, 196, 197	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = 0))
199	194, 198	mpbird 258	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ran 𝑄)
200	199	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 = 0) → 0 ∈ ran 𝑄)
201	177, 200	eqeltrd 2839	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 = 0) → 𝑠 ∈ ran 𝑄)
202	173, 174, 176, 201	fourierdlem12 46562	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
203	202	an32s 658	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
204	203	adantlr 721	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
205	172, 204	pm2.65da 822	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
206	205	adantlr 721	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
207	206	iffalsed 4465	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
208		elioore 13319	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
209	208	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
210		0red 11138	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
211		elioo3g 13318	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ℝ^*) ∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1)))))
212	211	biimpi 217	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ℝ^*) ∧ ((𝑄‘𝑖) < 𝑠 ∧ 𝑠 < (𝑄‘(𝑖 + 1)))))
213	212	simprrd 779	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 < (𝑄‘(𝑖 + 1)))
214	213	adantl 482	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
215	170	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) = 0)
216	214, 215	breqtrd 5098	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
217	209, 210, 216	ltnsymd 11286	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
218	217	iffalsed 4465	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
219	218	oveq2d 7372	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
220	219	oveq1d 7371	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
221	40	ad2antrr 732	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
222	5	rexrd 11186	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
223	222	ad3antrrr 736	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ^*)
224	161	ad2antrr 732	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
225	224, 209	readdcld 11165	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
226	114	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
227		iccssre 13373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
228	3, 2, 227	mp2an 698	. . . . . . . . . . . . . . . . . 18 ⊢ (-π[,]π) ⊆ ℝ
229	228, 50	sstri 3924	. . . . . . . . . . . . . . . . 17 ⊢ (-π[,]π) ⊆ ℂ
230	185, 132	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π))
231	1, 230	sylan2 599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ (-π[,]π))
232	229, 231	sselid 3913	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
233	226, 232	addcomd 11339	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘𝑖)) = ((𝑄‘𝑖) + 𝑋))
234	144	oveq1d 7371	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑋) = (((𝑉‘𝑖) − 𝑋) + 𝑋))
235	17	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℂ)
236	235, 226	npcand 11500	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑉‘𝑖) − 𝑋) + 𝑋) = (𝑉‘𝑖))
237	233, 234, 236	3eqtrrd 2779	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
238	237	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
239	144, 142	eqeltrd 2839	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
240	239	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
241	208	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
242	5	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
243	212	simprld 777	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) < 𝑠)
244	243	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
245	240, 241, 242, 244	ltadd2dd 11296	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
246	238, 245	eqbrtrd 5094	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
247	246	adantlr 721	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
248		ltaddneg 11353	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
249	209, 224, 248	syl2anc 590	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
250	216, 249	mpbid 233	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < 𝑋)
251	221, 223, 225, 247, 250	eliood 45943	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)𝑋))
252		fvres 6846	. . . . . . . . . . 11 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)𝑋) → ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
253	252	eqcomd 2745	. . . . . . . . . 10 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)𝑋) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
254	251, 253	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
255	254	oveq1d 7371	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝑊) = (((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
256	255	oveq1d 7371	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠) = ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
257	207, 220, 256	3eqtrd 2778	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
258	171, 257	mpteq12dva 5158	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
259	103, 140, 258	3eqtrd 2778	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
260	259, 170	oveq12d 7374	. . 3 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ (((𝑉‘𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉‘𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim_ℂ 0))
261	96, 100, 260	3eltr4d 2854	. 2 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
262		eqid 2739	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
263		eqid 2739	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠)
264		eqid 2739	. . . . 5 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
265	29	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℝ)
266	5	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
267	208	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
268	266, 267	readdcld 11165	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
269	265, 268	ffvelcdmd 7026	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
270	269	recnd 11164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
271	270	adantlr 721	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
272	271	3adantl3 1175	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
273		fourierdlem74.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ ℝ)
274	273	recnd 11164	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ ℂ)
275		limccl 25860	. . . . . . . . . 10 ⊢ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ⊆ ℂ
276	275, 35	sselid 3913	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ℂ)
277	274, 276	ifcld 4501	. . . . . . . 8 ⊢ (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
278	277	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
279	278	3ad2antl1 1192	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
280	272, 279	subcld 11496	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
281	208	recnd 11164	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℂ)
282	281	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
283		velsn 4571	. . . . . . . 8 ⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0)
284	205, 283	sylnibr 330	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
285	284	3adantl3 1175	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
286	282, 285	eldifd 3894	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
287		eqid 2739	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
288		eqid 2739	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊)
289		eqid 2739	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
290	276	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑊 ∈ ℂ)
291	29	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℝ)
292		ioossre 13351	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
293	292	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
294	40	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
295	160	rexrd 11186	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
296	295	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
297	268	adantlr 721	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
298	195	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
299	298, 155	ffvelcdmd 7026	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
300	299	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
301	213	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
302	241, 300, 242, 301	ltadd2dd 11296	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
303	163	oveq2d 7372	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
304	160	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
305	226, 304	pncan3d 11499	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
306	303, 305	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
307	306	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
308	302, 307	breqtrd 5098	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
309	294, 296, 297, 246, 308	eliood 45943	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
310		ioossre 13351	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
311	310	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
312	241, 301	ltned 11273	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
313		fourierdlem74.r	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
314	306	eqcomd 2745	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
315	314	oveq2d 7372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
316	313, 315	eleqtrd 2841	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
317	299	recnd 11164	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
318	291, 161, 293, 287, 309, 311, 312, 316, 317	fourierdlem53 46602	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
319		ioosscn 13352	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
320	319	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
321	276	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ℂ)
322	288, 320, 321, 317	constlimc 46069	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) lim_ℂ (𝑄‘(𝑖 + 1))))
323	287, 288, 289, 271, 290, 318, 322	sublimc 46095	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
324	323	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − 𝑊) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
325		iftrue 4460	. . . . . . . . . 10 ⊢ ((𝑉‘(𝑖 + 1)) < 𝑋 → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑊)
326	325	oveq2d 7372	. . . . . . . . 9 ⊢ ((𝑉‘(𝑖 + 1)) < 𝑋 → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊))
327	326	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅 − 𝑊))
328	208	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
329		0red 11138	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
330	299	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
331	213	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
332	163	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
333	160	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
334	5	ad2antrr 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
335		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) < 𝑋)
336	333, 334, 335	ltled 11285	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ≤ 𝑋)
337	333, 334	suble0d 11732	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0 ↔ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
338	336, 337	mpbird 258	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0)
339	332, 338	eqbrtrd 5094	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) ≤ 0)
340	339	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ≤ 0)
341	328, 330, 329, 331, 340	ltletrd 11297	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
342	328, 329, 341	ltnsymd 11286	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
343	342	iffalsed 4465	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
344	343	oveq2d 7372	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
345	344	mpteq2dva 5165	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)))
346	345	oveq1d 7371	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
347	324, 327, 346	3eltr4d 2854	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
348	347	3adantl3 1175	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
349		simpl1 1198	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝜑)
350		simpl2 1199	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑖 ∈ (0..^𝑀))
351	5	ad2antrr 732	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
352	351	3adantl3 1175	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
353	160	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
354	353	3adantl3 1175	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
355		neqne 2942	. . . . . . . . . . 11 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
356	355	necomd 2989	. . . . . . . . . 10 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
357	356	adantr 481	. . . . . . . . 9 ⊢ ((¬ (𝑉‘(𝑖 + 1)) = 𝑋 ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
358	357	3ad2antl3 1194	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
359		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
360	352, 354, 358, 359	lttri5d 45747	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
361		eqid 2739	. . . . . . . 8 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊))
362	271	adantlr 721	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
363	277	ad3antrrr 736	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
364	318	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
365		eqid 2739	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌)
366	274	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ℂ)
367	365, 320, 366, 317	constlimc 46069	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘(𝑖 + 1))))
368	367	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑌 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘(𝑖 + 1))))
369	5	ad2antrr 732	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ∈ ℝ)
370	160	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
371		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 < (𝑉‘(𝑖 + 1)))
372	369, 370, 371	ltnsymd 11286	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
373	372	iffalsed 4465	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑌)
374		0red 11138	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
375	239	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
376	208	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
377	189	eqcomd 2745	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 = (𝑋 − 𝑋))
378	377	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 = (𝑋 − 𝑋))
379	17	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉‘𝑖) ∈ ℝ)
380	40	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) ∈ ℝ^*)
381	295	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
382	161	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 ∈ ℝ)
383		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → ¬ 𝑋 ≤ (𝑉‘𝑖))
384	17	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) ∈ ℝ)
385	5	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 ∈ ℝ)
386	384, 385	ltnled 11284	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → ((𝑉‘𝑖) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑉‘𝑖)))
387	383, 386	mpbird 258	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) < 𝑋)
388	387	adantlr 721	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → (𝑉‘𝑖) < 𝑋)
389		simplr 774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 < (𝑉‘(𝑖 + 1)))
390	380, 381, 382, 388, 389	eliood 45943	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
391	11, 12, 13, 178	fourierdlem12 46562	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
392	391	ad2antrr 732	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉‘𝑖)) → ¬ 𝑋 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
393	390, 392	condan 823	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ≤ (𝑉‘𝑖))
394	369, 379, 369, 393	lesub1dd 11757	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑋 − 𝑋) ≤ ((𝑉‘𝑖) − 𝑋))
395	378, 394	eqbrtrd 5094	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ ((𝑉‘𝑖) − 𝑋))
396	144	eqcomd 2745	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖))
397	396	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑉‘𝑖) − 𝑋) = (𝑄‘𝑖))
398	395, 397	breqtrd 5098	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ (𝑄‘𝑖))
399	398	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ≤ (𝑄‘𝑖))
400	243	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
401	374, 375, 376, 399, 400	lelttrd 11295	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
402	401	iftrued 4462	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
403	402	mpteq2dva 5165	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌))
404	403	oveq1d 7371	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim_ℂ (𝑄‘(𝑖 + 1))))
405	368, 373, 404	3eltr4d 2854	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim_ℂ (𝑄‘(𝑖 + 1))))
406	287, 361, 262, 362, 363, 364, 405	sublimc 46095	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
407	349, 350, 360, 406	syl21anc 843	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
408	348, 407	pm2.61dan 818	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim_ℂ (𝑄‘(𝑖 + 1))))
409	320, 263, 317	idlimc 46071	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim_ℂ (𝑄‘(𝑖 + 1))))
410	409	3adant3 1138	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim_ℂ (𝑄‘(𝑖 + 1))))
411	163	3adant3 1138	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
412	304	3adant3 1138	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
413	226	3adant3 1138	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
414	355	3ad2ant3 1141	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
415	412, 413, 414	subne0d 11505	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≠ 0)
416	411, 415	eqnetrd 3001	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ≠ 0)
417	205	3adantl3 1175	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
418	417	neqned 2941	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
419	262, 263, 264, 280, 286, 408, 410, 416, 418	divlimc 46099	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))) ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim_ℂ (𝑄‘(𝑖 + 1))))
420		iffalse 4463	. . . . . 6 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
421	97, 420	eqtrid 2786	. . . . 5 ⊢ (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → 𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
422	421	3ad2ant3 1141	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
423		ioossre 13351	. . . . . . . . . . . . 13 ⊢ (-∞(,)𝑋) ⊆ ℝ
424	423	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (-∞(,)𝑋) ⊆ ℝ)
425	29, 424	fssresd 6694	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝑋)):(-∞(,)𝑋)⟶ℝ)
426	423, 51	sstrid 3926	. . . . . . . . . . 11 ⊢ (𝜑 → (-∞(,)𝑋) ⊆ ℂ)
427	38	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ∈ ℝ^*)
428	5	mnfltd 13066	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ < 𝑋)
429	55, 427, 5, 428	lptioo2cn 46088	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(-∞(,)𝑋)))
430	425, 426, 429, 35	limcrecl 46074	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ ℝ)
431	29, 5, 273, 430, 101	fourierdlem9 46559	. . . . . . . . 9 ⊢ (𝜑 → 𝐻:(-π[,]π)⟶ℝ)
432	431	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻:(-π[,]π)⟶ℝ)
433	432, 138	feqresmpt 6896	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)))
434	138	sselda 3915	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (-π[,]π))
435		0cnd 11128	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℂ)
436	277	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
437	271, 436	subcld 11496	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
438	281	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
439	205	neqned 2941	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
440	437, 438, 439	divcld 11922	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℂ)
441	435, 440	ifcld 4501	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ)
442	101	fvmpt2 6947	. . . . . . . . . 10 ⊢ ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
443	434, 441, 442	syl2anc 590	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
444	205	iffalsed 4465	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
445	443, 444	eqtrd 2774	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
446	445	mpteq2dva 5165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
447	433, 446	eqtrd 2774	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
448	447	3adant3 1138	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
449	448	oveq1d 7371	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim_ℂ (𝑄‘(𝑖 + 1))))
450	419, 422, 449	3eltr4d 2854	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
451	450	3expa 1124	. 2 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
452	261, 451	pm2.61dan 818	1 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 {crab 3391 ⊆ wss 3883 ifcif 4454 {csn 4555 class class class wbr 5072 ↦ cmpt 5153 dom cdm 5618 ran crn 5619 ↾ cres 5620 Fn wfn 6480 ⟶wf 6481 ‘cfv 6485 (class class class)co 7356 ↑_m cmap 8763 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 -∞cmnf 11168 ℝ^*cxr 11169 < clt 11170 ≤ cle 11171 − cmin 11368 -cneg 11369 / cdiv 11798 ℕcn 12165 (,)cioo 13289 [,]cicc 13292 ...cfz 13452 ..^cfzo 13599 πcpi 16022 TopOpenctopn 17375 topGenctg 17391 ℂ_fldccnfld 21347 intcnt 23000 lim_ℂ climc 25847 D cdv 25848

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107 ax-addf 11108

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-iin 4924 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-isom 6494 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8633 df-map 8765 df-pm 8766 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9265 df-fi 9314 df-sup 9345 df-inf 9346 df-oi 9415 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-z 12516 df-dec 12636 df-uz 12780 df-q 12890 df-rp 12934 df-xneg 13054 df-xadd 13055 df-xmul 13056 df-ioo 13293 df-ioc 13294 df-ico 13295 df-icc 13296 df-fz 13453 df-fzo 13600 df-fl 13742 df-seq 13955 df-exp 14015 df-fac 14227 df-bc 14256 df-hash 14284 df-shft 15020 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-limsup 15424 df-clim 15441 df-rlim 15442 df-sum 15640 df-ef 16023 df-sin 16025 df-cos 16026 df-pi 16028 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-starv 17226 df-sca 17227 df-vsca 17228 df-ip 17229 df-tset 17230 df-ple 17231 df-ds 17233 df-unif 17234 df-hom 17235 df-cco 17236 df-rest 17376 df-topn 17377 df-0g 17395 df-gsum 17396 df-topgen 17397 df-pt 17398 df-prds 17401 df-xrs 17457 df-qtop 17462 df-imas 17463 df-xps 17465 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-submnd 18743 df-mulg 19035 df-cntz 19283 df-cmn 19748 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 22877 df-topon 22894 df-topsp 22916 df-bases 22929 df-cld 23002 df-ntr 23003 df-cls 23004 df-nei 23081 df-lp 23119 df-perf 23120 df-cn 23210 df-cnp 23211 df-haus 23298 df-cmp 23370 df-tx 23545 df-hmeo 23738 df-fil 23829 df-fm 23921 df-flim 23922 df-flf 23923 df-xms 24303 df-ms 24304 df-tms 24305 df-cncf 24863 df-limc 25851 df-dv 25852

This theorem is referenced by: fourierdlem88 46637 fourierdlem103 46652 fourierdlem104 46653

W3C validator