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 47027

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 46937	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simprd 501	. . . . . 6 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
8	7	simplld 780	. . . . 5 ⊢ (𝜑 → (𝑄‘0) = -π)
9	8	eqcomd 2766	. . . 4 ⊢ (𝜑 → -π = (𝑄‘0))
10	7	simplrd 782	. . . . 5 ⊢ (𝜑 → (𝑄‘𝑀) = π)
11	10	eqcomd 2766	. . . 4 ⊢ (𝜑 → π = (𝑄‘𝑀))
12	9, 11	oveq12d 7431	. . 3 ⊢ (𝜑 → (-π[,]π) = ((𝑄‘0)[,](𝑄‘𝑀)))
13	12	itgeq1d 46785	. 2 ⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑡) d𝑡)
14		0zd 12627	. . 3 ⊢ (𝜑 → 0 ∈ ℤ)
15		nnuz 12926	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
16	2, 15	eleqtrdi 2870	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
17		1e0p1 12783	. . . . . 6 ⊢ 1 = (0 + 1)
18	17	a1i 11	. . . . 5 ⊢ (𝜑 → 1 = (0 + 1))
19	18	fveq2d 6882	. . . 4 ⊢ (𝜑 → (ℤ_≥‘1) = (ℤ_≥‘(0 + 1)))
20	16, 19	eleqtrd 2862	. . 3 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(0 + 1)))
21	3, 2, 1	fourierdlem15 46950	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
22		pire 26692	. . . . . . 7 ⊢ π ∈ ℝ
23	22	renegcli 11543	. . . . . 6 ⊢ -π ∈ ℝ
24		iccssre 13482	. . . . . 6 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
25	23, 22, 24	mp2an 705	. . . . 5 ⊢ (-π[,]π) ⊆ ℝ
26	25	a1i 11	. . . 4 ⊢ (𝜑 → (-π[,]π) ⊆ ℝ)
27	21, 26	fssd 6720	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
28	7	simprd 501	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
29	28	r19.21bi 3254	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
30		fourierdlem93.6	. . . . 5 ⊢ (𝜑 → 𝐹:(-π[,]π)⟶ℂ)
31	30	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝐹:(-π[,]π)⟶ℂ)
32		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
33	12	eqcomd 2766	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0)[,](𝑄‘𝑀)) = (-π[,]π))
34	33	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → ((𝑄‘0)[,](𝑄‘𝑀)) = (-π[,]π))
35	32, 34	eleqtrd 2862	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑡 ∈ (-π[,]π))
36	31, 35	ffvelcdmd 7078	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝐹‘𝑡) ∈ ℂ)
37	27	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
38		elfzofz 13731	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
39	38	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
40	37, 39	ffvelcdmd 7078	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
41		fzofzp1 13820	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
42	41	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
43	37, 42	ffvelcdmd 7078	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
44	30	feqmptd 6946	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)))
45	44	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)))
46	45	reseq1d 5971	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
47		ioossicc 13486	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
48	47	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
49	23	rexri 11291	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ^*
50	49	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → -π ∈ ℝ^*)
51	22	rexri 11291	. . . . . . . . . . . . . 14 ⊢ π ∈ ℝ^*
52	51	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → π ∈ ℝ^*)
53	21	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π))
54		simplr 781	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
55		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
56	50, 52, 53, 54, 55	fourierdlem1 46936	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ (-π[,]π))
57	56	ralrimiva 3154	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π))
58		dfss3 3920	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ∀𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π))
59	57, 58	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
60	48, 59	sstrd 3941	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
61	60	resmptd 6036	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)))
62	46, 61	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)))
63	62	eqcomd 2766	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
64		fourierdlem93.7	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
65	63, 64	eqeltrd 2860	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
66		fourierdlem93.9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
67	62	oveq1d 7428	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘(𝑖 + 1))))
68	66, 67	eleqtrd 2862	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘(𝑖 + 1))))
69		fourierdlem93.8	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
70	62	oveq1d 7428	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘𝑖)))
71	69, 70	eleqtrd 2862	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘𝑖)))
72	40, 43, 65, 68, 71	iblcncfioo 46806	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ 𝐿¹)
73	30	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ)
74	73, 56	ffvelcdmd 7078	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑡) ∈ ℂ)
75	40, 43, 72, 74	ibliooicc 46799	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ 𝐿¹)
76	14, 20, 27, 29, 36, 75	itgspltprt 46807	. 2 ⊢ (𝜑 → ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡)
77		fvres 6897	. . . . . . . 8 ⊢ (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) = (𝐹‘𝑡))
78	77	eqcomd 2766	. . . . . . 7 ⊢ (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → (𝐹‘𝑡) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡))
79	78	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑡) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡))
80	79	itgeq2dv 26009	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡)
81		eqid 2760	. . . . . 6 ⊢ (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))) = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
82	30	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:(-π[,]π)⟶ℂ)
83	82, 59	fssresd 6742	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))⟶ℂ)
84	48	resabs1d 6001	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
85	84, 64	eqeltrd 2860	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
86	84	oveq1d 7428	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
87	40, 43, 29, 83	limcicciooub 46465	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
88	86, 87	eqtr3d 2797	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
89	66, 88	eleqtrd 2862	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
90	84	eqcomd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
91	90	oveq1d 7428	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
92	40, 43, 29, 83	limciccioolb 46451	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
93	91, 92	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
94	69, 93	eleqtrd 2862	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
95		fourierdlem93.5	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℝ)
96	95	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
97	81, 40, 43, 29, 83, 85, 89, 94, 96	fourierdlem82 47016	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡)
98	40	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘𝑖) ∈ ℝ)
99	43	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
100	95	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑋 ∈ ℝ)
101	98, 100	resubcld 11666	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
102	99, 100	resubcld 11666	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
103		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
104		eliccre 46335	. . . . . . . . . 10 ⊢ ((((𝑄‘𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ)
105	101, 102, 103, 104	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ)
106	100, 105	readdcld 11262	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ℝ)
107		elicc2 13464	. . . . . . . . . . . 12 ⊢ ((((𝑄‘𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))))
108	101, 102, 107	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))))
109	103, 108	mpbid 235	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))
110	109	simp2d 1161	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘𝑖) − 𝑋) ≤ 𝑡)
111	98, 100, 105	lesubadd2d 11837	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ↔ (𝑄‘𝑖) ≤ (𝑋 + 𝑡)))
112	110, 111	mpbid 235	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘𝑖) ≤ (𝑋 + 𝑡))
113	109	simp3d 1162	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))
114	100, 105, 99	leaddsub2d 11840	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)) ↔ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))
115	113, 114	mpbird 260	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)))
116	98, 99, 106, 112, 115	eliccd 46334	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
117		fvres 6897	. . . . . . 7 ⊢ ((𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
118	116, 117	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
119	118	itgeq2dv 26009	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
120	80, 97, 119	3eqtrd 2799	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
121	120	sumeq2dv 15789	. . 3 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
122		oveq2 7421	. . . . . . 7 ⊢ (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
123	122	fveq2d 6882	. . . . . 6 ⊢ (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
124	123	cbvitgv 26004	. . . . 5 ⊢ ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡
125	124	a1i 11	. . . 4 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
126		fourierdlem93.2	. . . . . . . . 9 ⊢ 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋))
127	126	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)))
128		fveq2 6878	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
129	128	oveq1d 7428	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
130	129	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
131	2	nnzd 12641	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
132		0le0 12366	. . . . . . . . . 10 ⊢ 0 ≤ 0
133	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 0)
134		0red 11235	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
135	2	nnred 12272	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℝ)
136	2	nngt0d 12309	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
137	134, 135, 136	ltled 11382	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑀)
138	14, 131, 14, 133, 137	elfzd 13569	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
139	8, 23	eqeltrdi 2868	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
140	139, 95	resubcld 11666	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0) − 𝑋) ∈ ℝ)
141	127, 130, 138, 140	fvmptd 6994	. . . . . . 7 ⊢ (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋))
142	8	oveq1d 7428	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0) − 𝑋) = (-π − 𝑋))
143	141, 142	eqtr2d 2796	. . . . . 6 ⊢ (𝜑 → (-π − 𝑋) = (𝐻‘0))
144		fveq2 6878	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
145	144	oveq1d 7428	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑀) − 𝑋))
146	145	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 𝑀) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑀) − 𝑋))
147	135	leidd 11804	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
148	14, 131, 131, 137, 147	elfzd 13569	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
149	10, 22	eqeltrdi 2868	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
150	149, 95	resubcld 11666	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝑀) − 𝑋) ∈ ℝ)
151	127, 146, 148, 150	fvmptd 6994	. . . . . . 7 ⊢ (𝜑 → (𝐻‘𝑀) = ((𝑄‘𝑀) − 𝑋))
152	10	oveq1d 7428	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝑀) − 𝑋) = (π − 𝑋))
153	151, 152	eqtr2d 2796	. . . . . 6 ⊢ (𝜑 → (π − 𝑋) = (𝐻‘𝑀))
154	143, 153	oveq12d 7431	. . . . 5 ⊢ (𝜑 → ((-π − 𝑋)[,](π − 𝑋)) = ((𝐻‘0)[,](𝐻‘𝑀)))
155	154	itgeq1d 46785	. . . 4 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡)
156	27	ffvelcdmda 7077	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
157	95	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
158	156, 157	resubcld 11666	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
159	158, 126	fmptd 7107	. . . . . 6 ⊢ (𝜑 → 𝐻:(0...𝑀)⟶ℝ)
160	40, 43, 96, 29	ltsub1dd 11850	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − 𝑋) < ((𝑄‘(𝑖 + 1)) − 𝑋))
161	39, 158	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
162	126	fvmpt2 6998	. . . . . . . 8 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑄‘𝑖) − 𝑋) ∈ ℝ) → (𝐻‘𝑖) = ((𝑄‘𝑖) − 𝑋))
163	39, 161, 162	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) = ((𝑄‘𝑖) − 𝑋))
164		fveq2 6878	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
165	164	oveq1d 7428	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑗) − 𝑋))
166	165	cbvmptv 5209	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋))
167	126, 166	eqtri 2783	. . . . . . . . 9 ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋))
168	167	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋)))
169		fveq2 6878	. . . . . . . . . 10 ⊢ (𝑗 = (𝑖 + 1) → (𝑄‘𝑗) = (𝑄‘(𝑖 + 1)))
170	169	oveq1d 7428	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 + 1) → ((𝑄‘𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋))
171	170	adantl 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄‘𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋))
172	43, 96	resubcld 11666	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
173	168, 171, 42, 172	fvmptd 6994	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) − 𝑋))
174	160, 163, 173	3brtr4d 5137	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) < (𝐻‘(𝑖 + 1)))
175		frn 6710	. . . . . . . . 9 ⊢ (𝐹:(-π[,]π)⟶ℂ → ran 𝐹 ⊆ ℂ)
176	30, 175	syl 18	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 ⊆ ℂ)
177	176	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → ran 𝐹 ⊆ ℂ)
178		ffun 6705	. . . . . . . . . 10 ⊢ (𝐹:(-π[,]π)⟶ℂ → Fun 𝐹)
179	30, 178	syl 18	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐹)
180	179	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → Fun 𝐹)
181	23	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π ∈ ℝ)
182	22	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → π ∈ ℝ)
183	95	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑋 ∈ ℝ)
184	141, 140	eqeltrd 2860	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘0) ∈ ℝ)
185	184	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘0) ∈ ℝ)
186	151, 150	eqeltrd 2860	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘𝑀) ∈ ℝ)
187	186	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘𝑀) ∈ ℝ)
188		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)))
189		eliccre 46335	. . . . . . . . . . . 12 ⊢ (((𝐻‘0) ∈ ℝ ∧ (𝐻‘𝑀) ∈ ℝ ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ℝ)
190	185, 187, 188, 189	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ℝ)
191	183, 190	readdcld 11262	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ ℝ)
192	128	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑄‘𝑖) = (𝑄‘0))
193	192	oveq1d 7428	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
194	127, 193, 138, 140	fvmptd 6994	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋))
195	194	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (𝐻‘0)) = (𝑋 + ((𝑄‘0) − 𝑋)))
196	95	recnd 11261	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ ℂ)
197	139	recnd 11261	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄‘0) ∈ ℂ)
198	196, 197	pncan3d 11596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + ((𝑄‘0) − 𝑋)) = (𝑄‘0))
199	195, 198, 8	3eqtrrd 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → -π = (𝑋 + (𝐻‘0)))
200	199	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π = (𝑋 + (𝐻‘0)))
201		elicc2 13464	. . . . . . . . . . . . . . 15 ⊢ (((𝐻‘0) ∈ ℝ ∧ (𝐻‘𝑀) ∈ ℝ) → (𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀))))
202	185, 187, 201	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀))))
203	188, 202	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀)))
204	203	simp2d 1161	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘0) ≤ 𝑡)
205	185, 190, 183, 204	leadd2dd 11853	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + (𝐻‘0)) ≤ (𝑋 + 𝑡))
206	200, 205	eqbrtrd 5127	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π ≤ (𝑋 + 𝑡))
207	203	simp3d 1162	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ≤ (𝐻‘𝑀))
208	190, 187, 183, 207	leadd2dd 11853	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ≤ (𝑋 + (𝐻‘𝑀)))
209	151	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (𝐻‘𝑀)) = (𝑋 + ((𝑄‘𝑀) − 𝑋)))
210	149	recnd 11261	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℂ)
211	196, 210	pncan3d 11596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + ((𝑄‘𝑀) − 𝑋)) = (𝑄‘𝑀))
212	209, 211, 10	3eqtrrd 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → π = (𝑋 + (𝐻‘𝑀)))
213	212	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → π = (𝑋 + (𝐻‘𝑀)))
214	208, 213	breqtrrd 5133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ≤ π)
215	181, 182, 191, 206, 214	eliccd 46334	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ (-π[,]π))
216		fdm 6712	. . . . . . . . . . . 12 ⊢ (𝐹:(-π[,]π)⟶ℂ → dom 𝐹 = (-π[,]π))
217	30, 216	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = (-π[,]π))
218	217	eqcomd 2766	. . . . . . . . . 10 ⊢ (𝜑 → (-π[,]π) = dom 𝐹)
219	218	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (-π[,]π) = dom 𝐹)
220	215, 219	eleqtrd 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ dom 𝐹)
221		fvelrn 7069	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ (𝑋 + 𝑡) ∈ dom 𝐹) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
222	180, 220, 221	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
223	177, 222	sseldd 3932	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
224	163, 161	eqeltrd 2860	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℝ)
225	173, 172	eqeltrd 2860	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
226	82, 60	fssresd 6742	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
227	40	rexrd 11283	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
228	227	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
229	43	rexrd 11283	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
230	229	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
231	95	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232		elioore 13428	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑡 ∈ ℝ)
233	232	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
234	231, 233	readdcld 11262	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ℝ)
235	163	oveq2d 7429	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + ((𝑄‘𝑖) − 𝑋)))
236	196	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
237	40	recnd 11261	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
238	236, 237	pncan3d 11596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘𝑖) − 𝑋)) = (𝑄‘𝑖))
239		eqidd 2761	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (𝑄‘𝑖))
240	235, 238, 239	3eqtrrd 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
241	240	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
242	224	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) ∈ ℝ)
243		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
244	242	rexrd 11283	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) ∈ ℝ^*)
245	225	rexrd 11283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ^*)
246	245	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ^*)
247		elioo2 13439	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^*) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1)))))
248	244, 246, 247	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1)))))
249	243, 248	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1))))
250	249	simp2d 1161	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) < 𝑡)
251	242, 233, 231, 250	ltadd2dd 11393	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘𝑖)) < (𝑋 + 𝑡))
252	241, 251	eqbrtrd 5127	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑋 + 𝑡))
253	225	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
254	249	simp3d 1162	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 < (𝐻‘(𝑖 + 1)))
255	233, 253, 231, 254	ltadd2dd 11393	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑋 + (𝐻‘(𝑖 + 1))))
256	173	oveq2d 7429	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)))
257	43	recnd 11261	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
258	236, 257	pncan3d 11596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)) = (𝑄‘(𝑖 + 1)))
259	256, 258	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1)))
260	259	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1)))
261	255, 260	breqtrd 5131	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1)))
262	228, 230, 234, 252, 261	eliood 46328	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
263		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
264	262, 263	fmptd 7107	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
265		fcompt 7127	. . . . . . . . . . 11 ⊢ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))))
266	226, 264, 265	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))))
267		oveq2 7421	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑟 → (𝑋 + 𝑡) = (𝑋 + 𝑟))
268	267	cbvmptv 5209	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))
269	268	fveq1i 6879	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)
270	269	fveq2i 6881	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))
271	270	mpteq2i 5201	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)))
272	271	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))))
273		fveq2 6878	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠) = ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))
274	273	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))
275	274	cbvmptv 5209	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))
276	275	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))))
277		eqidd 2761	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)) = (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)))
278		oveq2 7421	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑡 → (𝑋 + 𝑟) = (𝑋 + 𝑡))
279	278	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) ∧ 𝑟 = 𝑡) → (𝑋 + 𝑟) = (𝑋 + 𝑡))
280	277, 279, 243, 234	fvmptd 6994	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡) = (𝑋 + 𝑡))
281	280	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)))
282		fvres 6897	. . . . . . . . . . . . . 14 ⊢ ((𝑋 + 𝑡) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
283	262, 282	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
284	281, 283	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = (𝐹‘(𝑋 + 𝑡)))
285	284	mpteq2dva 5198	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
286	272, 276, 285	3eqtrd 2799	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
287	266, 286	eqtr2d 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))))
288		eqid 2760	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡))
289		ssid 3953	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
290	289	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → ℂ ⊆ ℂ)
291		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → 𝑋 ∈ ℂ)
292	290, 291, 290	constcncfg 46700	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑋) ∈ (ℂ–cn→ℂ))
293		cncfmptid 25141	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ))
294	289, 289, 293	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)
295	294	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ))
296	292, 295	addcncf 25672	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ))
297	236, 296	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ))
298		ioosscn 13461	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ
299	298	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ)
300		ioosscn 13461	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
301	300	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
302	288, 297, 299, 301, 262	cncfmptssg 46699	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
303	302, 64	cncfco 25135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
304	287, 303	eqeltrd 2860	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
305	227	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) ∈ ℝ^*)
306	229	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
307		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
308		vex 3454	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑟 ∈ V
309	263	elrnmpt 5942	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡)))
310	308, 309	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))
311	307, 310	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))
312		nfv 1947	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0..^𝑀))
313		nfmpt1 5204	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
314	313	nfrn 5936	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
315	314	nfcri 2914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
316	312, 315	nfan 1932	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
317		nfv 1947	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑟 ∈ ℝ
318		simp3 1156	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡))
319	95	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑋 ∈ ℝ)
320	232	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑡 ∈ ℝ)
321	319, 320	readdcld 11262	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) ∈ ℝ)
322	318, 321	eqeltrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 ∈ ℝ)
323	322	3exp 1137	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)))
324	323	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)))
325	316, 317, 324	rexlimd 3269	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ))
326	311, 325	mpd 16	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ℝ)
327		nfv 1947	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝑄‘𝑖) < 𝑟
328	252	3adant3 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄‘𝑖) < (𝑋 + 𝑡))
329		simp3 1156	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡))
330	328, 329	breqtrrd 5133	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄‘𝑖) < 𝑟)
331	330	3exp 1137	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟)))
332	331	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟)))
333	316, 327, 332	rexlimd 3269	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟))
334	311, 333	mpd 16	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) < 𝑟)
335		nfv 1947	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑟 < (𝑄‘(𝑖 + 1))
336	261	3adant3 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1)))
337	329, 336	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 < (𝑄‘(𝑖 + 1)))
338	337	3exp 1137	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))))
339	338	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))))
340	316, 335, 339	rexlimd 3269	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1))))
341	311, 340	mpd 16	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 < (𝑄‘(𝑖 + 1)))
342	305, 306, 326, 334, 341	eliood 46328	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
343	217	ineq2d 4166	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
344	343	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
345		dmres 6005	. . . . . . . . . . . . . . . . 17 ⊢ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹)
346	345	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹))
347		dfss 3918	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
348	60, 347	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
349	344, 346, 348	3eqtr4d 2805	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
350	349	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
351	342, 350	eleqtrrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
352	326, 341	ltned 11370	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘(𝑖 + 1)))
353	352	neneqd 2960	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘(𝑖 + 1)))
354		velsn 4600	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {(𝑄‘(𝑖 + 1))} ↔ 𝑟 = (𝑄‘(𝑖 + 1)))
355	353, 354	sylnibr 332	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘(𝑖 + 1))})
356	351, 355	eldifd 3910	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
357	356	ralrimiva 3154	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
358		dfss3 3920	. . . . . . . . . . 11 ⊢ (ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
359	357, 358	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
360		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠))
361	196	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑋 ∈ ℂ)
362		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑠 ∈ ℂ)
363	361, 362	addcomd 11436	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → (𝑋 + 𝑠) = (𝑠 + 𝑋))
364	363	mpteq2dva 5198	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)))
365		eqid 2760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋))
366	365	addccncf 25145	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 ∈ ℂ → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ))
367	196, 366	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ))
368	364, 367	eqeltrd 2860	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ))
369	368	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ))
370	224	rexrd 11283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℝ^*)
371		iocssre 13480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ)
372	370, 225, 371	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ)
373		ax-resscn 11181	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℂ
374	372, 373	sstrdi 3943	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ)
375	289	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℂ ⊆ ℂ)
376	196	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ)
377	374	sselda 3931	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
378	376, 377	addcld 11252	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ)
379	360, 369, 374, 375, 378	cncfmptssg 46699	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ))
380		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
381		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
382	380	cnfldtop 25009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (TopOpen‘ℂ_fld) ∈ Top
383		unicntop 25011	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
384	383	restid 17518	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
385	382, 384	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
386	385	eqcomi 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
387	380, 381, 386	cncfcn 25138	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
388	374, 375, 387	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
389	379, 388	eleqtrd 2862	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
390	380	cnfldtopon 25008	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
391	390	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
392		resttopon 23386	. . . . . . . . . . . . . . . . 17 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
393	391, 374, 392	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
394		cncnp 23505	. . . . . . . . . . . . . . . 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 596	. . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡)))
397	396	simprd 501	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))
398		ubioc1 13452	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
399	370, 245, 174, 398	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
400		fveq2 6878	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (𝐻‘(𝑖 + 1)) → ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
401	400	eleq2d 2846	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝐻‘(𝑖 + 1)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1)))))
402	401	rspccva 3575	. . . . . . . . . . . . 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 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
404		ioounsn 13530	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
405	370, 245, 174, 404	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
406	259	eqcomd 2766	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1))))
407	406	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1))))
408		iftrue 4488	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1)))
409	408	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1)))
410		oveq2 7421	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝐻‘(𝑖 + 1)) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1))))
411	410	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1))))
412	407, 409, 411	3eqtr4d 2805	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
413		iffalse 4491	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
414	413	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
415		eqidd 2761	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
416		oveq2 7421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑠 → (𝑋 + 𝑡) = (𝑋 + 𝑠))
417	416	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠))
418		velsn 4600	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ 𝑠 = (𝐻‘(𝑖 + 1)))
419	418	notbii 323	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ ¬ 𝑠 = (𝐻‘(𝑖 + 1)))
420		elun 4100	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}))
421	420	biimpi 219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}))
422	421	orcomd 885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ∨ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
423	422	ord 878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
424	419, 423	biimtrrid 246	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 = (𝐻‘(𝑖 + 1)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
425	424	imp 412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
426	425	adantll 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
427	95	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑋 ∈ ℝ)
428		elioore 13428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
429	428	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
430		elsni 4601	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 = (𝐻‘(𝑖 + 1)))
431	430	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 = (𝐻‘(𝑖 + 1)))
432	225	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
433	431, 432	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 ∈ ℝ)
434	429, 433	jaodan 972	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ)
435	420, 434	sylan2b 606	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ)
436	427, 435	readdcld 11262	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → (𝑋 + 𝑠) ∈ ℝ)
437	436	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) ∈ ℝ)
438	415, 417, 426, 437	fvmptd 6994	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠))
439	414, 438	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
440	412, 439	pm2.61dan 825	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
441	405, 440	mpteq12dva 5191	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)))
442	405	oveq2d 7429	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
443	442	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld)))
444	443	fveq1d 6880	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
445	403, 441, 444	3eltr4d 2875	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
446		eqid 2760	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}))
447		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))
448	264, 301	fssd 6720	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶ℂ)
449	225	recnd 11261	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℂ)
450	446, 380, 447, 448, 299, 449	ellimc 26100	. . . . . . . . . . 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 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘(𝑖 + 1))))
452	359, 451, 66	limccog 46450	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
453	266, 286	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
454	453	oveq1d 7428	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
455	452, 454	eleqtrd 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
456	40	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) ∈ ℝ)
457	456, 334	gtned 11369	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘𝑖))
458	457	neneqd 2960	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘𝑖))
459		velsn 4600	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {(𝑄‘𝑖)} ↔ 𝑟 = (𝑄‘𝑖))
460	458, 459	sylnibr 332	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘𝑖)})
461	351, 460	eldifd 3910	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
462	461	ralrimiva 3154	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
463		dfss3 3920	. . . . . . . . . . 11 ⊢ (ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
464	462, 463	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
465		icossre 13481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻‘𝑖) ∈ ℝ ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^*) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ)
466	224, 245, 465	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ)
467	466, 373	sstrdi 3943	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ)
468	196	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ)
469	467	sselda 3931	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
470	468, 469	addcld 11252	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ)
471	360, 369, 467, 375, 470	cncfmptssg 46699	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
472		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
473	380, 472, 386	cncfcn 25138	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
474	467, 375, 473	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
475	471, 474	eleqtrd 2862	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
476		resttopon 23386	. . . . . . . . . . . . . . . . 17 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
477	391, 467, 476	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
478		cncnp 23505	. . . . . . . . . . . . . . . 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 596	. . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡)))
481	480	simprd 501	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))
482		lbico1 13453	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
483	370, 245, 174, 482	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
484		fveq2 6878	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (𝐻‘𝑖) → ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
485	484	eleq2d 2846	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝐻‘𝑖) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ↔ (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖))))
486	485	rspccva 3575	. . . . . . . . . . . . 13 ⊢ ((∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ∧ (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
487	481, 483, 486	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
488		uncom 4105	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) = ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
489		snunioo 13531	. . . . . . . . . . . . . . 15 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
490	370, 245, 174, 489	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
491	488, 490	eqtrid 2807	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
492		iftrue 4488	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝐻‘𝑖) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘𝑖))
493	492	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘𝑖))
494	240	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
495		oveq2 7421	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (𝐻‘𝑖) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘𝑖)))
496	495	eqcomd 2766	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝐻‘𝑖) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + 𝑠))
497	496	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + 𝑠))
498	493, 494, 497	3eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
499	498	adantlr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
500		iffalse 4491	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑠 = (𝐻‘𝑖) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
501	500	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
502		eqidd 2761	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
503	416	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠))
504		velsn 4600	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ {(𝐻‘𝑖)} ↔ 𝑠 = (𝐻‘𝑖))
505	504	notbii 323	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑠 ∈ {(𝐻‘𝑖)} ↔ ¬ 𝑠 = (𝐻‘𝑖))
506		elun 4100	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)}))
507	506	biimpi 219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)}))
508	507	orcomd 885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (𝑠 ∈ {(𝐻‘𝑖)} ∨ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
509	508	ord 878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (¬ 𝑠 ∈ {(𝐻‘𝑖)} → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
510	505, 509	biimtrrid 246	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (¬ 𝑠 = (𝐻‘𝑖) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
511	510	imp 412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
512	511	adantll 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
513	95	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → 𝑋 ∈ ℝ)
514		elsni 4601	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ {(𝐻‘𝑖)} → 𝑠 = (𝐻‘𝑖))
515	514	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → 𝑠 = (𝐻‘𝑖))
516	224	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → (𝐻‘𝑖) ∈ ℝ)
517	515, 516	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → 𝑠 ∈ ℝ)
518	429, 517	jaodan 972	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)})) → 𝑠 ∈ ℝ)
519	506, 518	sylan2b 606	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → 𝑠 ∈ ℝ)
520	513, 519	readdcld 11262	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → (𝑋 + 𝑠) ∈ ℝ)
521	520	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → (𝑋 + 𝑠) ∈ ℝ)
522	502, 503, 512, 521	fvmptd 6994	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠))
523	501, 522	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
524	499, 523	pm2.61dan 825	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
525	491, 524	mpteq12dva 5191	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)))
526	491	oveq2d 7429	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
527	526	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld)))
528	527	fveq1d 6880	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
529	487, 525, 528	3eltr4d 2875	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
530		eqid 2760	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) = ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}))
531		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))
532	224	recnd 11261	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℂ)
533	530, 380, 531, 448, 299, 532	ellimc 26100	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘𝑖)) ↔ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖))))
534	529, 533	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘𝑖)))
535	464, 534, 69	limccog 46450	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
536	453	oveq1d 7428	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
537	535, 536	eleqtrd 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
538	224, 225, 304, 455, 537	iblcncfioo 46806	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ 𝐿¹)
539	30	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ)
540	49	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → -π ∈ ℝ^*)
541	51	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → π ∈ ℝ^*)
542	21	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π))
543		simplr 781	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
544		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))))
545	163, 173	oveq12d 7431	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
546	545	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
547	544, 546	eleqtrd 2862	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
548	547, 116	syldan 603	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
549	540, 541, 542, 543, 548	fourierdlem1 46936	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ (-π[,]π))
550	539, 549	ffvelcdmd 7078	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
551	224, 225, 538, 550	ibliooicc 46799	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ 𝐿¹)
552	14, 20, 159, 174, 223, 551	itgspltprt 46807	. . . . 5 ⊢ (𝜑 → ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡)
553	545	itgeq1d 46785	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
554	553	sumeq2dv 15789	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
555	552, 554	eqtrd 2795	. . . 4 ⊢ (𝜑 → ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
556	125, 155, 555	3eqtrd 2799	. . 3 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
557	121, 556	eqtr4d 2798	. 2 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)
558	13, 76, 557	3eqtrd 2799	1 ⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ifcif 4482 {csn 4584 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5655 ran crn 5656 ↾ cres 5657 ∘ ccom 5659 Fun wfun 6527 ⟶wf 6529 ‘cfv 6533 (class class class)co 7413 ↑_m cmap 8826 ℂcc 11122 ℝcr 11123 0cc0 11124 1c1 11125 + caddc 11127 ℝ^*cxr 11266 < clt 11267 ≤ cle 11268 − cmin 11465 -cneg 11466 ℕcn 12257 ℤ_≥cuz 12887 (,)cioo 13398 (,]cioc 13399 [,)cico 13400 [,]cicc 13401 ...cfz 13561 ..^cfzo 13709 Σcsu 15773 πcpi 16152 ↾_t crest 17505 TopOpenctopn 17506 ℂ_fldccnfld 21585 Topctop 23118 TopOnctopon 23135 Cn ccn 23449 CnP ccnp 23450 –cn→ccncf 25104 ∫citg 25846 lim_ℂ climc 26089

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-inf2 9620 ax-cc 10437 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201 ax-pre-sup 11202 ax-addf 11203

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-symdif 4199 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7678 df-ofr 7679 df-om 7863 df-1st 7986 df-2nd 7987 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-oadd 8459 df-omul 8460 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8905 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-fsupp 9332 df-fi 9381 df-sup 9412 df-inf 9413 df-oi 9482 df-dju 9906 df-card 9944 df-acn 9947 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11467 df-neg 11468 df-div 11896 df-nn 12258 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12529 df-z 12616 df-dec 12737 df-uz 12888 df-q 12998 df-rp 13043 df-xneg 13163 df-xadd 13164 df-xmul 13165 df-ioo 13402 df-ioc 13403 df-ico 13404 df-icc 13405 df-fz 13562 df-fzo 13710 df-fl 13853 df-mod 13931 df-seq 14066 df-exp 14126 df-fac 14338 df-bc 14367 df-hash 14395 df-shft 15140 df-cj 15186 df-re 15187 df-im 15188 df-sqrt 15322 df-abs 15323 df-limsup 15558 df-clim 15575 df-rlim 15576 df-sum 15774 df-ef 16153 df-sin 16155 df-cos 16156 df-pi 16158 df-struct 17239 df-sets 17256 df-slot 17274 df-ndx 17286 df-base 17302 df-ress 17323 df-plusg 17355 df-mulr 17356 df-starv 17357 df-sca 17358 df-vsca 17359 df-ip 17360 df-tset 17361 df-ple 17362 df-ds 17364 df-unif 17365 df-hom 17366 df-cco 17367 df-rest 17507 df-topn 17508 df-0g 17526 df-gsum 17527 df-topgen 17528 df-pt 17529 df-prds 17532 df-xrs 17588 df-qtop 17593 df-imas 17594 df-xps 17596 df-mre 17670 df-mrc 17671 df-acs 17673 df-mgm 18730 df-sgrp 18821 df-mnd 18837 df-submnd 18892 df-mulg 19191 df-cntz 19444 df-cmn 19909 df-psmet 21577 df-xmet 21578 df-met 21579 df-bl 21580 df-mopn 21581 df-fbas 21582 df-fg 21583 df-cnfld 21586 df-top 23119 df-topon 23136 df-topsp 23158 df-bases 23171 df-cld 23244 df-ntr 23245 df-cls 23246 df-nei 23323 df-lp 23361 df-perf 23362 df-cn 23452 df-cnp 23453 df-haus 23540 df-cmp 23612 df-tx 23788 df-hmeo 23981 df-fil 24072 df-fm 24164 df-flim 24165 df-flf 24166 df-xms 24546 df-ms 24547 df-tms 24548 df-cncf 25106 df-ovol 25692 df-vol 25693 df-mbf 25847 df-itg1 25848 df-itg2 25849 df-ibl 25850 df-itg 25851 df-0p 25898 df-ditg 26074 df-limc 26093 df-dv 26094

This theorem is used by: fourierdlem101 47035

W3C validator