fourierdlem93 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem93 46204

Description: Integral by substitution (the domain is shifted by 𝑋) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem93.1	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem93.2	⊢ 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋))
fourierdlem93.3	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem93.4	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem93.5	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem93.6	⊢ (𝜑 → 𝐹:(-π[,]π)⟶ℂ)
fourierdlem93.7	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
fourierdlem93.8	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
fourierdlem93.9	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))

**Assertion**
Ref	Expression
fourierdlem93	⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)

Distinct variable groups: 𝑖,𝐹,𝑠,𝑡 𝑖,𝐻,𝑠,𝑡 𝑡,𝐿 𝑖,𝑀,𝑚,𝑝 𝑀,𝑠,𝑡 𝑄,𝑖,𝑝 𝑄,𝑠,𝑡 𝑡,𝑅 𝑖,𝑋,𝑠,𝑡 𝜑,𝑖,𝑠,𝑡 Allowed substitution hints: 𝜑(𝑚,𝑝) 𝑃(𝑡,𝑖,𝑚,𝑠,𝑝) 𝑄(𝑚) 𝑅(𝑖,𝑚,𝑠,𝑝) 𝐹(𝑚,𝑝) 𝐻(𝑚,𝑝) 𝐿(𝑖,𝑚,𝑠,𝑝) 𝑋(𝑚,𝑝)

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

Step	Hyp	Ref	Expression
1		fourierdlem93.4	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
2		fourierdlem93.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3		fourierdlem93.1	. . . . . . . . . 10 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
4	3	fourierdlem2 46114	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simprd 495	. . . . . 6 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
8	7	simplld 767	. . . . 5 ⊢ (𝜑 → (𝑄‘0) = -π)
9	8	eqcomd 2736	. . . 4 ⊢ (𝜑 → -π = (𝑄‘0))
10	7	simplrd 769	. . . . 5 ⊢ (𝜑 → (𝑄‘𝑀) = π)
11	10	eqcomd 2736	. . . 4 ⊢ (𝜑 → π = (𝑄‘𝑀))
12	9, 11	oveq12d 7408	. . 3 ⊢ (𝜑 → (-π[,]π) = ((𝑄‘0)[,](𝑄‘𝑀)))
13	12	itgeq1d 45962	. 2 ⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑡) d𝑡)
14		0zd 12548	. . 3 ⊢ (𝜑 → 0 ∈ ℤ)
15		nnuz 12843	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
16	2, 15	eleqtrdi 2839	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
17		1e0p1 12698	. . . . . 6 ⊢ 1 = (0 + 1)
18	17	a1i 11	. . . . 5 ⊢ (𝜑 → 1 = (0 + 1))
19	18	fveq2d 6865	. . . 4 ⊢ (𝜑 → (ℤ_≥‘1) = (ℤ_≥‘(0 + 1)))
20	16, 19	eleqtrd 2831	. . 3 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(0 + 1)))
21	3, 2, 1	fourierdlem15 46127	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
22		pire 26373	. . . . . . 7 ⊢ π ∈ ℝ
23	22	renegcli 11490	. . . . . 6 ⊢ -π ∈ ℝ
24		iccssre 13397	. . . . . 6 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
25	23, 22, 24	mp2an 692	. . . . 5 ⊢ (-π[,]π) ⊆ ℝ
26	25	a1i 11	. . . 4 ⊢ (𝜑 → (-π[,]π) ⊆ ℝ)
27	21, 26	fssd 6708	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
28	7	simprd 495	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
29	28	r19.21bi 3230	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
30		fourierdlem93.6	. . . . 5 ⊢ (𝜑 → 𝐹:(-π[,]π)⟶ℂ)
31	30	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝐹:(-π[,]π)⟶ℂ)
32		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
33	12	eqcomd 2736	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0)[,](𝑄‘𝑀)) = (-π[,]π))
34	33	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → ((𝑄‘0)[,](𝑄‘𝑀)) = (-π[,]π))
35	32, 34	eleqtrd 2831	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑡 ∈ (-π[,]π))
36	31, 35	ffvelcdmd 7060	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝐹‘𝑡) ∈ ℂ)
37	27	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
38		elfzofz 13643	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
39	38	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
40	37, 39	ffvelcdmd 7060	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
41		fzofzp1 13732	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
42	41	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
43	37, 42	ffvelcdmd 7060	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
44	30	feqmptd 6932	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)))
45	44	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)))
46	45	reseq1d 5952	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
47		ioossicc 13401	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
48	47	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
49	23	rexri 11239	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ^*
50	49	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → -π ∈ ℝ^*)
51	22	rexri 11239	. . . . . . . . . . . . . 14 ⊢ π ∈ ℝ^*
52	51	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → π ∈ ℝ^*)
53	21	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π))
54		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
55		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
56	50, 52, 53, 54, 55	fourierdlem1 46113	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ (-π[,]π))
57	56	ralrimiva 3126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π))
58		dfss3 3938	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ∀𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π))
59	57, 58	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
60	48, 59	sstrd 3960	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
61	60	resmptd 6014	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)))
62	46, 61	eqtrd 2765	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)))
63	62	eqcomd 2736	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
64		fourierdlem93.7	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
65	63, 64	eqeltrd 2829	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
66		fourierdlem93.9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
67	62	oveq1d 7405	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘(𝑖 + 1))))
68	66, 67	eleqtrd 2831	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘(𝑖 + 1))))
69		fourierdlem93.8	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
70	62	oveq1d 7405	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘𝑖)))
71	69, 70	eleqtrd 2831	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘𝑖)))
72	40, 43, 65, 68, 71	iblcncfioo 45983	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ 𝐿¹)
73	30	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ)
74	73, 56	ffvelcdmd 7060	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑡) ∈ ℂ)
75	40, 43, 72, 74	ibliooicc 45976	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ 𝐿¹)
76	14, 20, 27, 29, 36, 75	itgspltprt 45984	. 2 ⊢ (𝜑 → ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡)
77		fvres 6880	. . . . . . . 8 ⊢ (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) = (𝐹‘𝑡))
78	77	eqcomd 2736	. . . . . . 7 ⊢ (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → (𝐹‘𝑡) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡))
79	78	adantl 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑡) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡))
80	79	itgeq2dv 25690	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡)
81		eqid 2730	. . . . . 6 ⊢ (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))) = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
82	30	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:(-π[,]π)⟶ℂ)
83	82, 59	fssresd 6730	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))⟶ℂ)
84	48	resabs1d 5982	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
85	84, 64	eqeltrd 2829	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
86	84	oveq1d 7405	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
87	40, 43, 29, 83	limcicciooub 45642	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
88	86, 87	eqtr3d 2767	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
89	66, 88	eleqtrd 2831	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
90	84	eqcomd 2736	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
91	90	oveq1d 7405	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
92	40, 43, 29, 83	limciccioolb 45626	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
93	91, 92	eqtrd 2765	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
94	69, 93	eleqtrd 2831	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
95		fourierdlem93.5	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℝ)
96	95	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
97	81, 40, 43, 29, 83, 85, 89, 94, 96	fourierdlem82 46193	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡)
98	40	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘𝑖) ∈ ℝ)
99	43	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
100	95	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑋 ∈ ℝ)
101	98, 100	resubcld 11613	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
102	99, 100	resubcld 11613	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
103		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
104		eliccre 45510	. . . . . . . . . 10 ⊢ ((((𝑄‘𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ)
105	101, 102, 103, 104	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ)
106	100, 105	readdcld 11210	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ℝ)
107		elicc2 13379	. . . . . . . . . . . 12 ⊢ ((((𝑄‘𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))))
108	101, 102, 107	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))))
109	103, 108	mpbid 232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))
110	109	simp2d 1143	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘𝑖) − 𝑋) ≤ 𝑡)
111	98, 100, 105	lesubadd2d 11784	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ↔ (𝑄‘𝑖) ≤ (𝑋 + 𝑡)))
112	110, 111	mpbid 232	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘𝑖) ≤ (𝑋 + 𝑡))
113	109	simp3d 1144	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))
114	100, 105, 99	leaddsub2d 11787	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)) ↔ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))
115	113, 114	mpbird 257	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)))
116	98, 99, 106, 112, 115	eliccd 45509	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
117		fvres 6880	. . . . . . 7 ⊢ ((𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
118	116, 117	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
119	118	itgeq2dv 25690	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
120	80, 97, 119	3eqtrd 2769	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
121	120	sumeq2dv 15675	. . 3 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
122		oveq2 7398	. . . . . . 7 ⊢ (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
123	122	fveq2d 6865	. . . . . 6 ⊢ (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
124	123	cbvitgv 25685	. . . . 5 ⊢ ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡
125	124	a1i 11	. . . 4 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
126		fourierdlem93.2	. . . . . . . . 9 ⊢ 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋))
127	126	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)))
128		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
129	128	oveq1d 7405	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
130	129	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
131	2	nnzd 12563	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
132		0le0 12294	. . . . . . . . . 10 ⊢ 0 ≤ 0
133	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 0)
134		0red 11184	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
135	2	nnred 12208	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℝ)
136	2	nngt0d 12242	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
137	134, 135, 136	ltled 11329	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑀)
138	14, 131, 14, 133, 137	elfzd 13483	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
139	8, 23	eqeltrdi 2837	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
140	139, 95	resubcld 11613	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0) − 𝑋) ∈ ℝ)
141	127, 130, 138, 140	fvmptd 6978	. . . . . . 7 ⊢ (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋))
142	8	oveq1d 7405	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0) − 𝑋) = (-π − 𝑋))
143	141, 142	eqtr2d 2766	. . . . . 6 ⊢ (𝜑 → (-π − 𝑋) = (𝐻‘0))
144		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
145	144	oveq1d 7405	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑀) − 𝑋))
146	145	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 𝑀) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑀) − 𝑋))
147	135	leidd 11751	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
148	14, 131, 131, 137, 147	elfzd 13483	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
149	10, 22	eqeltrdi 2837	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
150	149, 95	resubcld 11613	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝑀) − 𝑋) ∈ ℝ)
151	127, 146, 148, 150	fvmptd 6978	. . . . . . 7 ⊢ (𝜑 → (𝐻‘𝑀) = ((𝑄‘𝑀) − 𝑋))
152	10	oveq1d 7405	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝑀) − 𝑋) = (π − 𝑋))
153	151, 152	eqtr2d 2766	. . . . . 6 ⊢ (𝜑 → (π − 𝑋) = (𝐻‘𝑀))
154	143, 153	oveq12d 7408	. . . . 5 ⊢ (𝜑 → ((-π − 𝑋)[,](π − 𝑋)) = ((𝐻‘0)[,](𝐻‘𝑀)))
155	154	itgeq1d 45962	. . . 4 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡)
156	27	ffvelcdmda 7059	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
157	95	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
158	156, 157	resubcld 11613	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
159	158, 126	fmptd 7089	. . . . . 6 ⊢ (𝜑 → 𝐻:(0...𝑀)⟶ℝ)
160	40, 43, 96, 29	ltsub1dd 11797	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − 𝑋) < ((𝑄‘(𝑖 + 1)) − 𝑋))
161	39, 158	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
162	126	fvmpt2 6982	. . . . . . . 8 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑄‘𝑖) − 𝑋) ∈ ℝ) → (𝐻‘𝑖) = ((𝑄‘𝑖) − 𝑋))
163	39, 161, 162	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) = ((𝑄‘𝑖) − 𝑋))
164		fveq2 6861	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
165	164	oveq1d 7405	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑗) − 𝑋))
166	165	cbvmptv 5214	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋))
167	126, 166	eqtri 2753	. . . . . . . . 9 ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋))
168	167	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋)))
169		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑗 = (𝑖 + 1) → (𝑄‘𝑗) = (𝑄‘(𝑖 + 1)))
170	169	oveq1d 7405	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 + 1) → ((𝑄‘𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋))
171	170	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄‘𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋))
172	43, 96	resubcld 11613	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
173	168, 171, 42, 172	fvmptd 6978	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) − 𝑋))
174	160, 163, 173	3brtr4d 5142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) < (𝐻‘(𝑖 + 1)))
175		frn 6698	. . . . . . . . 9 ⊢ (𝐹:(-π[,]π)⟶ℂ → ran 𝐹 ⊆ ℂ)
176	30, 175	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 ⊆ ℂ)
177	176	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → ran 𝐹 ⊆ ℂ)
178		ffun 6694	. . . . . . . . . 10 ⊢ (𝐹:(-π[,]π)⟶ℂ → Fun 𝐹)
179	30, 178	syl 17	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐹)
180	179	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → Fun 𝐹)
181	23	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π ∈ ℝ)
182	22	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → π ∈ ℝ)
183	95	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑋 ∈ ℝ)
184	141, 140	eqeltrd 2829	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘0) ∈ ℝ)
185	184	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘0) ∈ ℝ)
186	151, 150	eqeltrd 2829	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘𝑀) ∈ ℝ)
187	186	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘𝑀) ∈ ℝ)
188		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)))
189		eliccre 45510	. . . . . . . . . . . 12 ⊢ (((𝐻‘0) ∈ ℝ ∧ (𝐻‘𝑀) ∈ ℝ ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ℝ)
190	185, 187, 188, 189	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ℝ)
191	183, 190	readdcld 11210	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ ℝ)
192	128	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑄‘𝑖) = (𝑄‘0))
193	192	oveq1d 7405	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
194	127, 193, 138, 140	fvmptd 6978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋))
195	194	oveq2d 7406	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (𝐻‘0)) = (𝑋 + ((𝑄‘0) − 𝑋)))
196	95	recnd 11209	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ ℂ)
197	139	recnd 11209	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄‘0) ∈ ℂ)
198	196, 197	pncan3d 11543	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + ((𝑄‘0) − 𝑋)) = (𝑄‘0))
199	195, 198, 8	3eqtrrd 2770	. . . . . . . . . . . 12 ⊢ (𝜑 → -π = (𝑋 + (𝐻‘0)))
200	199	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π = (𝑋 + (𝐻‘0)))
201		elicc2 13379	. . . . . . . . . . . . . . 15 ⊢ (((𝐻‘0) ∈ ℝ ∧ (𝐻‘𝑀) ∈ ℝ) → (𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀))))
202	185, 187, 201	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀))))
203	188, 202	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀)))
204	203	simp2d 1143	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘0) ≤ 𝑡)
205	185, 190, 183, 204	leadd2dd 11800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + (𝐻‘0)) ≤ (𝑋 + 𝑡))
206	200, 205	eqbrtrd 5132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π ≤ (𝑋 + 𝑡))
207	203	simp3d 1144	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ≤ (𝐻‘𝑀))
208	190, 187, 183, 207	leadd2dd 11800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ≤ (𝑋 + (𝐻‘𝑀)))
209	151	oveq2d 7406	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (𝐻‘𝑀)) = (𝑋 + ((𝑄‘𝑀) − 𝑋)))
210	149	recnd 11209	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℂ)
211	196, 210	pncan3d 11543	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + ((𝑄‘𝑀) − 𝑋)) = (𝑄‘𝑀))
212	209, 211, 10	3eqtrrd 2770	. . . . . . . . . . . 12 ⊢ (𝜑 → π = (𝑋 + (𝐻‘𝑀)))
213	212	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → π = (𝑋 + (𝐻‘𝑀)))
214	208, 213	breqtrrd 5138	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ≤ π)
215	181, 182, 191, 206, 214	eliccd 45509	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ (-π[,]π))
216		fdm 6700	. . . . . . . . . . . 12 ⊢ (𝐹:(-π[,]π)⟶ℂ → dom 𝐹 = (-π[,]π))
217	30, 216	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = (-π[,]π))
218	217	eqcomd 2736	. . . . . . . . . 10 ⊢ (𝜑 → (-π[,]π) = dom 𝐹)
219	218	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (-π[,]π) = dom 𝐹)
220	215, 219	eleqtrd 2831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ dom 𝐹)
221		fvelrn 7051	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ (𝑋 + 𝑡) ∈ dom 𝐹) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
222	180, 220, 221	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
223	177, 222	sseldd 3950	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
224	163, 161	eqeltrd 2829	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℝ)
225	173, 172	eqeltrd 2829	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
226	82, 60	fssresd 6730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
227	40	rexrd 11231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
228	227	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
229	43	rexrd 11231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
230	229	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
231	95	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232		elioore 13343	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑡 ∈ ℝ)
233	232	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
234	231, 233	readdcld 11210	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ℝ)
235	163	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + ((𝑄‘𝑖) − 𝑋)))
236	196	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
237	40	recnd 11209	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
238	236, 237	pncan3d 11543	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘𝑖) − 𝑋)) = (𝑄‘𝑖))
239		eqidd 2731	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (𝑄‘𝑖))
240	235, 238, 239	3eqtrrd 2770	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
241	240	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
242	224	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) ∈ ℝ)
243		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
244	242	rexrd 11231	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) ∈ ℝ^*)
245	225	rexrd 11231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ^*)
246	245	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ^*)
247		elioo2 13354	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^*) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1)))))
248	244, 246, 247	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1)))))
249	243, 248	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1))))
250	249	simp2d 1143	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) < 𝑡)
251	242, 233, 231, 250	ltadd2dd 11340	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘𝑖)) < (𝑋 + 𝑡))
252	241, 251	eqbrtrd 5132	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑋 + 𝑡))
253	225	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
254	249	simp3d 1144	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 < (𝐻‘(𝑖 + 1)))
255	233, 253, 231, 254	ltadd2dd 11340	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑋 + (𝐻‘(𝑖 + 1))))
256	173	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)))
257	43	recnd 11209	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
258	236, 257	pncan3d 11543	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)) = (𝑄‘(𝑖 + 1)))
259	256, 258	eqtrd 2765	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1)))
260	259	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1)))
261	255, 260	breqtrd 5136	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1)))
262	228, 230, 234, 252, 261	eliood 45503	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
263		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
264	262, 263	fmptd 7089	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
265		fcompt 7108	. . . . . . . . . . 11 ⊢ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))))
266	226, 264, 265	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))))
267		oveq2 7398	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑟 → (𝑋 + 𝑡) = (𝑋 + 𝑟))
268	267	cbvmptv 5214	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))
269	268	fveq1i 6862	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)
270	269	fveq2i 6864	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))
271	270	mpteq2i 5206	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)))
272	271	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))))
273		fveq2 6861	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠) = ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))
274	273	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))
275	274	cbvmptv 5214	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))
276	275	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))))
277		eqidd 2731	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)) = (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)))
278		oveq2 7398	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑡 → (𝑋 + 𝑟) = (𝑋 + 𝑡))
279	278	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) ∧ 𝑟 = 𝑡) → (𝑋 + 𝑟) = (𝑋 + 𝑡))
280	277, 279, 243, 234	fvmptd 6978	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡) = (𝑋 + 𝑡))
281	280	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)))
282		fvres 6880	. . . . . . . . . . . . . 14 ⊢ ((𝑋 + 𝑡) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
283	262, 282	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
284	281, 283	eqtrd 2765	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = (𝐹‘(𝑋 + 𝑡)))
285	284	mpteq2dva 5203	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
286	272, 276, 285	3eqtrd 2769	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
287	266, 286	eqtr2d 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))))
288		eqid 2730	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡))
289		ssid 3972	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
290	289	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → ℂ ⊆ ℂ)
291		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → 𝑋 ∈ ℂ)
292	290, 291, 290	constcncfg 45877	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑋) ∈ (ℂ–cn→ℂ))
293		cncfmptid 24813	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ))
294	289, 289, 293	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)
295	294	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ))
296	292, 295	addcncf 25351	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ))
297	236, 296	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ))
298		ioosscn 13376	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ
299	298	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ)
300		ioosscn 13376	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
301	300	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
302	288, 297, 299, 301, 262	cncfmptssg 45876	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
303	302, 64	cncfco 24807	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
304	287, 303	eqeltrd 2829	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
305	227	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) ∈ ℝ^*)
306	229	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
307		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
308		vex 3454	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑟 ∈ V
309	263	elrnmpt 5925	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡)))
310	308, 309	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))
311	307, 310	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))
312		nfv 1914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0..^𝑀))
313		nfmpt1 5209	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
314	313	nfrn 5919	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
315	314	nfcri 2884	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
316	312, 315	nfan 1899	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
317		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑟 ∈ ℝ
318		simp3 1138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡))
319	95	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑋 ∈ ℝ)
320	232	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑡 ∈ ℝ)
321	319, 320	readdcld 11210	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) ∈ ℝ)
322	318, 321	eqeltrd 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 ∈ ℝ)
323	322	3exp 1119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)))
324	323	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)))
325	316, 317, 324	rexlimd 3245	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ))
326	311, 325	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ℝ)
327		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝑄‘𝑖) < 𝑟
328	252	3adant3 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄‘𝑖) < (𝑋 + 𝑡))
329		simp3 1138	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡))
330	328, 329	breqtrrd 5138	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄‘𝑖) < 𝑟)
331	330	3exp 1119	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟)))
332	331	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟)))
333	316, 327, 332	rexlimd 3245	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟))
334	311, 333	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) < 𝑟)
335		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑟 < (𝑄‘(𝑖 + 1))
336	261	3adant3 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1)))
337	329, 336	eqbrtrd 5132	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 < (𝑄‘(𝑖 + 1)))
338	337	3exp 1119	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))))
339	338	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))))
340	316, 335, 339	rexlimd 3245	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1))))
341	311, 340	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 < (𝑄‘(𝑖 + 1)))
342	305, 306, 326, 334, 341	eliood 45503	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
343	217	ineq2d 4186	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
344	343	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
345		dmres 5986	. . . . . . . . . . . . . . . . 17 ⊢ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹)
346	345	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹))
347		dfss 3936	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
348	60, 347	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
349	344, 346, 348	3eqtr4d 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
350	349	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
351	342, 350	eleqtrrd 2832	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
352	326, 341	ltned 11317	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘(𝑖 + 1)))
353	352	neneqd 2931	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘(𝑖 + 1)))
354		velsn 4608	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {(𝑄‘(𝑖 + 1))} ↔ 𝑟 = (𝑄‘(𝑖 + 1)))
355	353, 354	sylnibr 329	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘(𝑖 + 1))})
356	351, 355	eldifd 3928	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
357	356	ralrimiva 3126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
358		dfss3 3938	. . . . . . . . . . 11 ⊢ (ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
359	357, 358	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
360		eqid 2730	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠))
361	196	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑋 ∈ ℂ)
362		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑠 ∈ ℂ)
363	361, 362	addcomd 11383	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → (𝑋 + 𝑠) = (𝑠 + 𝑋))
364	363	mpteq2dva 5203	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)))
365		eqid 2730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋))
366	365	addccncf 24817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 ∈ ℂ → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ))
367	196, 366	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ))
368	364, 367	eqeltrd 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ))
369	368	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ))
370	224	rexrd 11231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℝ^*)
371		iocssre 13395	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ)
372	370, 225, 371	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ)
373		ax-resscn 11132	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℂ
374	372, 373	sstrdi 3962	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ)
375	289	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℂ ⊆ ℂ)
376	196	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ)
377	374	sselda 3949	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
378	376, 377	addcld 11200	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ)
379	360, 369, 374, 375, 378	cncfmptssg 45876	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ))
380		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
381		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
382	380	cnfldtop 24678	. . . . . . . . . . . . . . . . . . . 20 ⊢ (TopOpen‘ℂ_fld) ∈ Top
383		unicntop 24680	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
384	383	restid 17403	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
385	382, 384	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
386	385	eqcomi 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
387	380, 381, 386	cncfcn 24810	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
388	374, 375, 387	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
389	379, 388	eleqtrd 2831	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
390	380	cnfldtopon 24677	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
391	390	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
392		resttopon 23055	. . . . . . . . . . . . . . . . 17 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
393	391, 374, 392	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
394		cncnp 23174	. . . . . . . . . . . . . . . 16 ⊢ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∧ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)) ↔ ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))))
395	393, 391, 394	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)) ↔ ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))))
396	389, 395	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡)))
397	396	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))
398		ubioc1 13367	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
399	370, 245, 174, 398	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
400		fveq2 6861	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (𝐻‘(𝑖 + 1)) → ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
401	400	eleq2d 2815	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝐻‘(𝑖 + 1)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1)))))
402	401	rspccva 3590	. . . . . . . . . . . . 13 ⊢ ((∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ∧ (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
403	397, 399, 402	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
404		ioounsn 13445	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
405	370, 245, 174, 404	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
406	259	eqcomd 2736	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1))))
407	406	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1))))
408		iftrue 4497	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1)))
409	408	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1)))
410		oveq2 7398	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝐻‘(𝑖 + 1)) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1))))
411	410	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1))))
412	407, 409, 411	3eqtr4d 2775	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
413		iffalse 4500	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
414	413	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
415		eqidd 2731	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
416		oveq2 7398	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑠 → (𝑋 + 𝑡) = (𝑋 + 𝑠))
417	416	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠))
418		velsn 4608	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ 𝑠 = (𝐻‘(𝑖 + 1)))
419	418	notbii 320	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ ¬ 𝑠 = (𝐻‘(𝑖 + 1)))
420		elun 4119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}))
421	420	biimpi 216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}))
422	421	orcomd 871	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ∨ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
423	422	ord 864	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
424	419, 423	biimtrrid 243	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 = (𝐻‘(𝑖 + 1)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
425	424	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
426	425	adantll 714	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
427	95	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑋 ∈ ℝ)
428		elioore 13343	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
429	428	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
430		elsni 4609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 = (𝐻‘(𝑖 + 1)))
431	430	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 = (𝐻‘(𝑖 + 1)))
432	225	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
433	431, 432	eqeltrd 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 ∈ ℝ)
434	429, 433	jaodan 959	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ)
435	420, 434	sylan2b 594	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ)
436	427, 435	readdcld 11210	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → (𝑋 + 𝑠) ∈ ℝ)
437	436	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) ∈ ℝ)
438	415, 417, 426, 437	fvmptd 6978	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠))
439	414, 438	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
440	412, 439	pm2.61dan 812	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
441	405, 440	mpteq12dva 5196	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)))
442	405	oveq2d 7406	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
443	442	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld)))
444	443	fveq1d 6863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
445	403, 441, 444	3eltr4d 2844	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
446		eqid 2730	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}))
447		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))
448	264, 301	fssd 6708	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶ℂ)
449	225	recnd 11209	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℂ)
450	446, 380, 447, 448, 299, 449	ellimc 25781	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘(𝑖 + 1))) ↔ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1)))))
451	445, 450	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘(𝑖 + 1))))
452	359, 451, 66	limccog 45625	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
453	266, 286	eqtrd 2765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
454	453	oveq1d 7405	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
455	452, 454	eleqtrd 2831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
456	40	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) ∈ ℝ)
457	456, 334	gtned 11316	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘𝑖))
458	457	neneqd 2931	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘𝑖))
459		velsn 4608	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {(𝑄‘𝑖)} ↔ 𝑟 = (𝑄‘𝑖))
460	458, 459	sylnibr 329	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘𝑖)})
461	351, 460	eldifd 3928	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
462	461	ralrimiva 3126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
463		dfss3 3938	. . . . . . . . . . 11 ⊢ (ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
464	462, 463	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
465		icossre 13396	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻‘𝑖) ∈ ℝ ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^*) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ)
466	224, 245, 465	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ)
467	466, 373	sstrdi 3962	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ)
468	196	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ)
469	467	sselda 3949	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
470	468, 469	addcld 11200	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ)
471	360, 369, 467, 375, 470	cncfmptssg 45876	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
472		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
473	380, 472, 386	cncfcn 24810	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
474	467, 375, 473	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
475	471, 474	eleqtrd 2831	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
476		resttopon 23055	. . . . . . . . . . . . . . . . 17 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
477	391, 467, 476	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
478		cncnp 23174	. . . . . . . . . . . . . . . 16 ⊢ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∧ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)) ↔ ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))))
479	477, 391, 478	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)) ↔ ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))))
480	475, 479	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡)))
481	480	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))
482		lbico1 13368	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
483	370, 245, 174, 482	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
484		fveq2 6861	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (𝐻‘𝑖) → ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
485	484	eleq2d 2815	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝐻‘𝑖) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ↔ (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖))))
486	485	rspccva 3590	. . . . . . . . . . . . 13 ⊢ ((∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ∧ (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
487	481, 483, 486	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
488		uncom 4124	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) = ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
489		snunioo 13446	. . . . . . . . . . . . . . 15 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
490	370, 245, 174, 489	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
491	488, 490	eqtrid 2777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
492		iftrue 4497	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝐻‘𝑖) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘𝑖))
493	492	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘𝑖))
494	240	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
495		oveq2 7398	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (𝐻‘𝑖) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘𝑖)))
496	495	eqcomd 2736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝐻‘𝑖) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + 𝑠))
497	496	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + 𝑠))
498	493, 494, 497	3eqtrd 2769	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
499	498	adantlr 715	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
500		iffalse 4500	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑠 = (𝐻‘𝑖) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
501	500	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
502		eqidd 2731	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
503	416	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠))
504		velsn 4608	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ {(𝐻‘𝑖)} ↔ 𝑠 = (𝐻‘𝑖))
505	504	notbii 320	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑠 ∈ {(𝐻‘𝑖)} ↔ ¬ 𝑠 = (𝐻‘𝑖))
506		elun 4119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)}))
507	506	biimpi 216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)}))
508	507	orcomd 871	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (𝑠 ∈ {(𝐻‘𝑖)} ∨ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
509	508	ord 864	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (¬ 𝑠 ∈ {(𝐻‘𝑖)} → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
510	505, 509	biimtrrid 243	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (¬ 𝑠 = (𝐻‘𝑖) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
511	510	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
512	511	adantll 714	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
513	95	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → 𝑋 ∈ ℝ)
514		elsni 4609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ {(𝐻‘𝑖)} → 𝑠 = (𝐻‘𝑖))
515	514	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → 𝑠 = (𝐻‘𝑖))
516	224	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → (𝐻‘𝑖) ∈ ℝ)
517	515, 516	eqeltrd 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → 𝑠 ∈ ℝ)
518	429, 517	jaodan 959	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)})) → 𝑠 ∈ ℝ)
519	506, 518	sylan2b 594	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → 𝑠 ∈ ℝ)
520	513, 519	readdcld 11210	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → (𝑋 + 𝑠) ∈ ℝ)
521	520	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → (𝑋 + 𝑠) ∈ ℝ)
522	502, 503, 512, 521	fvmptd 6978	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠))
523	501, 522	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
524	499, 523	pm2.61dan 812	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
525	491, 524	mpteq12dva 5196	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)))
526	491	oveq2d 7406	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
527	526	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld)))
528	527	fveq1d 6863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
529	487, 525, 528	3eltr4d 2844	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
530		eqid 2730	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) = ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}))
531		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))
532	224	recnd 11209	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℂ)
533	530, 380, 531, 448, 299, 532	ellimc 25781	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘𝑖)) ↔ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖))))
534	529, 533	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘𝑖)))
535	464, 534, 69	limccog 45625	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
536	453	oveq1d 7405	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
537	535, 536	eleqtrd 2831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
538	224, 225, 304, 455, 537	iblcncfioo 45983	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ 𝐿¹)
539	30	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ)
540	49	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → -π ∈ ℝ^*)
541	51	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → π ∈ ℝ^*)
542	21	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π))
543		simplr 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
544		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))))
545	163, 173	oveq12d 7408	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
546	545	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
547	544, 546	eleqtrd 2831	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
548	547, 116	syldan 591	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
549	540, 541, 542, 543, 548	fourierdlem1 46113	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ (-π[,]π))
550	539, 549	ffvelcdmd 7060	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
551	224, 225, 538, 550	ibliooicc 45976	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ 𝐿¹)
552	14, 20, 159, 174, 223, 551	itgspltprt 45984	. . . . 5 ⊢ (𝜑 → ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡)
553	545	itgeq1d 45962	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
554	553	sumeq2dv 15675	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
555	552, 554	eqtrd 2765	. . . 4 ⊢ (𝜑 → ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
556	125, 155, 555	3eqtrd 2769	. . 3 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
557	121, 556	eqtr4d 2768	. 2 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)
558	13, 76, 557	3eqtrd 2769	1 ⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3045 ∃wrex 3054 {crab 3408 Vcvv 3450 ∖ cdif 3914 ∪ cun 3915 ∩ cin 3916 ⊆ wss 3917 ifcif 4491 {csn 4592 class class class wbr 5110 ↦ cmpt 5191 dom cdm 5641 ran crn 5642 ↾ cres 5643 ∘ ccom 5645 Fun wfun 6508 ⟶wf 6510 ‘cfv 6514 (class class class)co 7390 ↑_m cmap 8802 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 + caddc 11078 ℝ^*cxr 11214 < clt 11215 ≤ cle 11216 − cmin 11412 -cneg 11413 ℕcn 12193 ℤ_≥cuz 12800 (,)cioo 13313 (,]cioc 13314 [,)cico 13315 [,]cicc 13316 ...cfz 13475 ..^cfzo 13622 Σcsu 15659 πcpi 16039 ↾_t crest 17390 TopOpenctopn 17391 ℂ_fldccnfld 21271 Topctop 22787 TopOnctopon 22804 Cn ccn 23118 CnP ccnp 23119 –cn→ccncf 24776 ∫citg 25526 lim_ℂ climc 25770

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601 ax-cc 10395 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153 ax-addf 11154

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-symdif 4219 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-iin 4961 df-disj 5078 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7656 df-ofr 7657 df-om 7846 df-1st 7971 df-2nd 7972 df-supp 8143 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-omul 8442 df-er 8674 df-map 8804 df-pm 8805 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9320 df-fi 9369 df-sup 9400 df-inf 9401 df-oi 9470 df-dju 9861 df-card 9899 df-acn 9902 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-4 12258 df-5 12259 df-6 12260 df-7 12261 df-8 12262 df-9 12263 df-n0 12450 df-z 12537 df-dec 12657 df-uz 12801 df-q 12915 df-rp 12959 df-xneg 13079 df-xadd 13080 df-xmul 13081 df-ioo 13317 df-ioc 13318 df-ico 13319 df-icc 13320 df-fz 13476 df-fzo 13623 df-fl 13761 df-mod 13839 df-seq 13974 df-exp 14034 df-fac 14246 df-bc 14275 df-hash 14303 df-shft 15040 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-limsup 15444 df-clim 15461 df-rlim 15462 df-sum 15660 df-ef 16040 df-sin 16042 df-cos 16043 df-pi 16045 df-struct 17124 df-sets 17141 df-slot 17159 df-ndx 17171 df-base 17187 df-ress 17208 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 17392 df-topn 17393 df-0g 17411 df-gsum 17412 df-topgen 17413 df-pt 17414 df-prds 17417 df-xrs 17472 df-qtop 17477 df-imas 17478 df-xps 17480 df-mre 17554 df-mrc 17555 df-acs 17557 df-mgm 18574 df-sgrp 18653 df-mnd 18669 df-submnd 18718 df-mulg 19007 df-cntz 19256 df-cmn 19719 df-psmet 21263 df-xmet 21264 df-met 21265 df-bl 21266 df-mopn 21267 df-fbas 21268 df-fg 21269 df-cnfld 21272 df-top 22788 df-topon 22805 df-topsp 22827 df-bases 22840 df-cld 22913 df-ntr 22914 df-cls 22915 df-nei 22992 df-lp 23030 df-perf 23031 df-cn 23121 df-cnp 23122 df-haus 23209 df-cmp 23281 df-tx 23456 df-hmeo 23649 df-fil 23740 df-fm 23832 df-flim 23833 df-flf 23834 df-xms 24215 df-ms 24216 df-tms 24217 df-cncf 24778 df-ovol 25372 df-vol 25373 df-mbf 25527 df-itg1 25528 df-itg2 25529 df-ibl 25530 df-itg 25531 df-0p 25578 df-ditg 25755 df-limc 25774 df-dv 25775

This theorem is referenced by: fourierdlem101 46212

W3C validator