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 44902

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 44812	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simprd 497	. . . . . 6 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
8	7	simplld 767	. . . . 5 ⊢ (𝜑 → (𝑄‘0) = -π)
9	8	eqcomd 2739	. . . 4 ⊢ (𝜑 → -π = (𝑄‘0))
10	7	simplrd 769	. . . . 5 ⊢ (𝜑 → (𝑄‘𝑀) = π)
11	10	eqcomd 2739	. . . 4 ⊢ (𝜑 → π = (𝑄‘𝑀))
12	9, 11	oveq12d 7424	. . 3 ⊢ (𝜑 → (-π[,]π) = ((𝑄‘0)[,](𝑄‘𝑀)))
13	12	itgeq1d 44660	. 2 ⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑡) d𝑡)
14		0zd 12567	. . 3 ⊢ (𝜑 → 0 ∈ ℤ)
15		nnuz 12862	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
16	2, 15	eleqtrdi 2844	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
17		1e0p1 12716	. . . . . 6 ⊢ 1 = (0 + 1)
18	17	a1i 11	. . . . 5 ⊢ (𝜑 → 1 = (0 + 1))
19	18	fveq2d 6893	. . . 4 ⊢ (𝜑 → (ℤ_≥‘1) = (ℤ_≥‘(0 + 1)))
20	16, 19	eleqtrd 2836	. . 3 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(0 + 1)))
21	3, 2, 1	fourierdlem15 44825	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
22		pire 25960	. . . . . . 7 ⊢ π ∈ ℝ
23	22	renegcli 11518	. . . . . 6 ⊢ -π ∈ ℝ
24		iccssre 13403	. . . . . 6 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
25	23, 22, 24	mp2an 691	. . . . 5 ⊢ (-π[,]π) ⊆ ℝ
26	25	a1i 11	. . . 4 ⊢ (𝜑 → (-π[,]π) ⊆ ℝ)
27	21, 26	fssd 6733	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
28	7	simprd 497	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
29	28	r19.21bi 3249	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
30		fourierdlem93.6	. . . . 5 ⊢ (𝜑 → 𝐹:(-π[,]π)⟶ℂ)
31	30	adantr 482	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝐹:(-π[,]π)⟶ℂ)
32		simpr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
33	12	eqcomd 2739	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0)[,](𝑄‘𝑀)) = (-π[,]π))
34	33	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → ((𝑄‘0)[,](𝑄‘𝑀)) = (-π[,]π))
35	32, 34	eleqtrd 2836	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑡 ∈ (-π[,]π))
36	31, 35	ffvelcdmd 7085	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝐹‘𝑡) ∈ ℂ)
37	27	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
38		elfzofz 13645	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
39	38	adantl 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
40	37, 39	ffvelcdmd 7085	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
41		fzofzp1 13726	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
42	41	adantl 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
43	37, 42	ffvelcdmd 7085	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
44	30	feqmptd 6958	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)))
45	44	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)))
46	45	reseq1d 5979	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
47		ioossicc 13407	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
48	47	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
49	23	rexri 11269	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ^*
50	49	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → -π ∈ ℝ^*)
51	22	rexri 11269	. . . . . . . . . . . . . 14 ⊢ π ∈ ℝ^*
52	51	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → π ∈ ℝ^*)
53	21	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π))
54		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
55		simpr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
56	50, 52, 53, 54, 55	fourierdlem1 44811	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ (-π[,]π))
57	56	ralrimiva 3147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π))
58		dfss3 3970	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ∀𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π))
59	57, 58	sylibr 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
60	48, 59	sstrd 3992	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
61	60	resmptd 6039	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)))
62	46, 61	eqtrd 2773	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)))
63	62	eqcomd 2739	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
64		fourierdlem93.7	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
65	63, 64	eqeltrd 2834	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
66		fourierdlem93.9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
67	62	oveq1d 7421	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘(𝑖 + 1))))
68	66, 67	eleqtrd 2836	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘(𝑖 + 1))))
69		fourierdlem93.8	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
70	62	oveq1d 7421	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘𝑖)))
71	69, 70	eleqtrd 2836	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘𝑖)))
72	40, 43, 65, 68, 71	iblcncfioo 44681	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ 𝐿¹)
73	30	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ)
74	73, 56	ffvelcdmd 7085	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑡) ∈ ℂ)
75	40, 43, 72, 74	ibliooicc 44674	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ 𝐿¹)
76	14, 20, 27, 29, 36, 75	itgspltprt 44682	. 2 ⊢ (𝜑 → ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡)
77		fvres 6908	. . . . . . . 8 ⊢ (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) = (𝐹‘𝑡))
78	77	eqcomd 2739	. . . . . . 7 ⊢ (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → (𝐹‘𝑡) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡))
79	78	adantl 483	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑡) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡))
80	79	itgeq2dv 25291	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡)
81		eqid 2733	. . . . . 6 ⊢ (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))) = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
82	30	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:(-π[,]π)⟶ℂ)
83	82, 59	fssresd 6756	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))⟶ℂ)
84	48	resabs1d 6011	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
85	84, 64	eqeltrd 2834	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
86	84	oveq1d 7421	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
87	40, 43, 29, 83	limcicciooub 44340	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
88	86, 87	eqtr3d 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
89	66, 88	eleqtrd 2836	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
90	84	eqcomd 2739	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
91	90	oveq1d 7421	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
92	40, 43, 29, 83	limciccioolb 44324	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
93	91, 92	eqtrd 2773	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
94	69, 93	eleqtrd 2836	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
95		fourierdlem93.5	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℝ)
96	95	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
97	81, 40, 43, 29, 83, 85, 89, 94, 96	fourierdlem82 44891	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡)
98	40	adantr 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘𝑖) ∈ ℝ)
99	43	adantr 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
100	95	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑋 ∈ ℝ)
101	98, 100	resubcld 11639	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
102	99, 100	resubcld 11639	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
103		simpr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
104		eliccre 44205	. . . . . . . . . 10 ⊢ ((((𝑄‘𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ)
105	101, 102, 103, 104	syl3anc 1372	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ)
106	100, 105	readdcld 11240	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ℝ)
107		elicc2 13386	. . . . . . . . . . . 12 ⊢ ((((𝑄‘𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))))
108	101, 102, 107	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))))
109	103, 108	mpbid 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))
110	109	simp2d 1144	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘𝑖) − 𝑋) ≤ 𝑡)
111	98, 100, 105	lesubadd2d 11810	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ↔ (𝑄‘𝑖) ≤ (𝑋 + 𝑡)))
112	110, 111	mpbid 231	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘𝑖) ≤ (𝑋 + 𝑡))
113	109	simp3d 1145	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))
114	100, 105, 99	leaddsub2d 11813	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)) ↔ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))
115	113, 114	mpbird 257	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)))
116	98, 99, 106, 112, 115	eliccd 44204	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
117		fvres 6908	. . . . . . 7 ⊢ ((𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
118	116, 117	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
119	118	itgeq2dv 25291	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
120	80, 97, 119	3eqtrd 2777	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
121	120	sumeq2dv 15646	. . 3 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
122		oveq2 7414	. . . . . . 7 ⊢ (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
123	122	fveq2d 6893	. . . . . 6 ⊢ (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
124	123	cbvitgv 25286	. . . . 5 ⊢ ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡
125	124	a1i 11	. . . 4 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
126		fourierdlem93.2	. . . . . . . . 9 ⊢ 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋))
127	126	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)))
128		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
129	128	oveq1d 7421	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
130	129	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
131	2	nnzd 12582	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
132		0le0 12310	. . . . . . . . . 10 ⊢ 0 ≤ 0
133	132	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 0)
134		0red 11214	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
135	2	nnred 12224	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℝ)
136	2	nngt0d 12258	. . . . . . . . . 10 ⊢ (𝜑 → 0 < 𝑀)
137	134, 135, 136	ltled 11359	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑀)
138	14, 131, 14, 133, 137	elfzd 13489	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
139	8, 23	eqeltrdi 2842	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
140	139, 95	resubcld 11639	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0) − 𝑋) ∈ ℝ)
141	127, 130, 138, 140	fvmptd 7003	. . . . . . 7 ⊢ (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋))
142	8	oveq1d 7421	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0) − 𝑋) = (-π − 𝑋))
143	141, 142	eqtr2d 2774	. . . . . 6 ⊢ (𝜑 → (-π − 𝑋) = (𝐻‘0))
144		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
145	144	oveq1d 7421	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑀) − 𝑋))
146	145	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 𝑀) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑀) − 𝑋))
147	135	leidd 11777	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
148	14, 131, 131, 137, 147	elfzd 13489	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
149	10, 22	eqeltrdi 2842	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
150	149, 95	resubcld 11639	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝑀) − 𝑋) ∈ ℝ)
151	127, 146, 148, 150	fvmptd 7003	. . . . . . 7 ⊢ (𝜑 → (𝐻‘𝑀) = ((𝑄‘𝑀) − 𝑋))
152	10	oveq1d 7421	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝑀) − 𝑋) = (π − 𝑋))
153	151, 152	eqtr2d 2774	. . . . . 6 ⊢ (𝜑 → (π − 𝑋) = (𝐻‘𝑀))
154	143, 153	oveq12d 7424	. . . . 5 ⊢ (𝜑 → ((-π − 𝑋)[,](π − 𝑋)) = ((𝐻‘0)[,](𝐻‘𝑀)))
155	154	itgeq1d 44660	. . . 4 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡)
156	27	ffvelcdmda 7084	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
157	95	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
158	156, 157	resubcld 11639	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
159	158, 126	fmptd 7111	. . . . . 6 ⊢ (𝜑 → 𝐻:(0...𝑀)⟶ℝ)
160	40, 43, 96, 29	ltsub1dd 11823	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − 𝑋) < ((𝑄‘(𝑖 + 1)) − 𝑋))
161	39, 158	syldan 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
162	126	fvmpt2 7007	. . . . . . . 8 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑄‘𝑖) − 𝑋) ∈ ℝ) → (𝐻‘𝑖) = ((𝑄‘𝑖) − 𝑋))
163	39, 161, 162	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) = ((𝑄‘𝑖) − 𝑋))
164		fveq2 6889	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
165	164	oveq1d 7421	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑗) − 𝑋))
166	165	cbvmptv 5261	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋))
167	126, 166	eqtri 2761	. . . . . . . . 9 ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋))
168	167	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋)))
169		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑗 = (𝑖 + 1) → (𝑄‘𝑗) = (𝑄‘(𝑖 + 1)))
170	169	oveq1d 7421	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 + 1) → ((𝑄‘𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋))
171	170	adantl 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄‘𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋))
172	43, 96	resubcld 11639	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
173	168, 171, 42, 172	fvmptd 7003	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) − 𝑋))
174	160, 163, 173	3brtr4d 5180	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) < (𝐻‘(𝑖 + 1)))
175		frn 6722	. . . . . . . . 9 ⊢ (𝐹:(-π[,]π)⟶ℂ → ran 𝐹 ⊆ ℂ)
176	30, 175	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 ⊆ ℂ)
177	176	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → ran 𝐹 ⊆ ℂ)
178		ffun 6718	. . . . . . . . . 10 ⊢ (𝐹:(-π[,]π)⟶ℂ → Fun 𝐹)
179	30, 178	syl 17	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐹)
180	179	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → Fun 𝐹)
181	23	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π ∈ ℝ)
182	22	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → π ∈ ℝ)
183	95	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑋 ∈ ℝ)
184	141, 140	eqeltrd 2834	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘0) ∈ ℝ)
185	184	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘0) ∈ ℝ)
186	151, 150	eqeltrd 2834	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘𝑀) ∈ ℝ)
187	186	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘𝑀) ∈ ℝ)
188		simpr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)))
189		eliccre 44205	. . . . . . . . . . . 12 ⊢ (((𝐻‘0) ∈ ℝ ∧ (𝐻‘𝑀) ∈ ℝ ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ℝ)
190	185, 187, 188, 189	syl3anc 1372	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ℝ)
191	183, 190	readdcld 11240	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ ℝ)
192	128	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑄‘𝑖) = (𝑄‘0))
193	192	oveq1d 7421	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
194	127, 193, 138, 140	fvmptd 7003	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋))
195	194	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (𝐻‘0)) = (𝑋 + ((𝑄‘0) − 𝑋)))
196	95	recnd 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ ℂ)
197	139	recnd 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄‘0) ∈ ℂ)
198	196, 197	pncan3d 11571	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + ((𝑄‘0) − 𝑋)) = (𝑄‘0))
199	195, 198, 8	3eqtrrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → -π = (𝑋 + (𝐻‘0)))
200	199	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π = (𝑋 + (𝐻‘0)))
201		elicc2 13386	. . . . . . . . . . . . . . 15 ⊢ (((𝐻‘0) ∈ ℝ ∧ (𝐻‘𝑀) ∈ ℝ) → (𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀))))
202	185, 187, 201	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀))))
203	188, 202	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀)))
204	203	simp2d 1144	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘0) ≤ 𝑡)
205	185, 190, 183, 204	leadd2dd 11826	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + (𝐻‘0)) ≤ (𝑋 + 𝑡))
206	200, 205	eqbrtrd 5170	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π ≤ (𝑋 + 𝑡))
207	203	simp3d 1145	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ≤ (𝐻‘𝑀))
208	190, 187, 183, 207	leadd2dd 11826	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ≤ (𝑋 + (𝐻‘𝑀)))
209	151	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (𝐻‘𝑀)) = (𝑋 + ((𝑄‘𝑀) − 𝑋)))
210	149	recnd 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℂ)
211	196, 210	pncan3d 11571	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + ((𝑄‘𝑀) − 𝑋)) = (𝑄‘𝑀))
212	209, 211, 10	3eqtrrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → π = (𝑋 + (𝐻‘𝑀)))
213	212	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → π = (𝑋 + (𝐻‘𝑀)))
214	208, 213	breqtrrd 5176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ≤ π)
215	181, 182, 191, 206, 214	eliccd 44204	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ (-π[,]π))
216		fdm 6724	. . . . . . . . . . . 12 ⊢ (𝐹:(-π[,]π)⟶ℂ → dom 𝐹 = (-π[,]π))
217	30, 216	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = (-π[,]π))
218	217	eqcomd 2739	. . . . . . . . . 10 ⊢ (𝜑 → (-π[,]π) = dom 𝐹)
219	218	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (-π[,]π) = dom 𝐹)
220	215, 219	eleqtrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ dom 𝐹)
221		fvelrn 7076	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ (𝑋 + 𝑡) ∈ dom 𝐹) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
222	180, 220, 221	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
223	177, 222	sseldd 3983	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
224	163, 161	eqeltrd 2834	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℝ)
225	173, 172	eqeltrd 2834	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
226	82, 60	fssresd 6756	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
227	40	rexrd 11261	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
228	227	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
229	43	rexrd 11261	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
230	229	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
231	95	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232		elioore 13351	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑡 ∈ ℝ)
233	232	adantl 483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
234	231, 233	readdcld 11240	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ℝ)
235	163	oveq2d 7422	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + ((𝑄‘𝑖) − 𝑋)))
236	196	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
237	40	recnd 11239	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
238	236, 237	pncan3d 11571	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘𝑖) − 𝑋)) = (𝑄‘𝑖))
239		eqidd 2734	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (𝑄‘𝑖))
240	235, 238, 239	3eqtrrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
241	240	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
242	224	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) ∈ ℝ)
243		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
244	242	rexrd 11261	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) ∈ ℝ^*)
245	225	rexrd 11261	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ^*)
246	245	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ^*)
247		elioo2 13362	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^*) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1)))))
248	244, 246, 247	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1)))))
249	243, 248	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1))))
250	249	simp2d 1144	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) < 𝑡)
251	242, 233, 231, 250	ltadd2dd 11370	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘𝑖)) < (𝑋 + 𝑡))
252	241, 251	eqbrtrd 5170	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑋 + 𝑡))
253	225	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
254	249	simp3d 1145	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 < (𝐻‘(𝑖 + 1)))
255	233, 253, 231, 254	ltadd2dd 11370	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑋 + (𝐻‘(𝑖 + 1))))
256	173	oveq2d 7422	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)))
257	43	recnd 11239	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
258	236, 257	pncan3d 11571	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)) = (𝑄‘(𝑖 + 1)))
259	256, 258	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1)))
260	259	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1)))
261	255, 260	breqtrd 5174	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1)))
262	228, 230, 234, 252, 261	eliood 44198	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
263		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
264	262, 263	fmptd 7111	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
265		fcompt 7128	. . . . . . . . . . 11 ⊢ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))))
266	226, 264, 265	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))))
267		oveq2 7414	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑟 → (𝑋 + 𝑡) = (𝑋 + 𝑟))
268	267	cbvmptv 5261	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))
269	268	fveq1i 6890	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)
270	269	fveq2i 6892	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))
271	270	mpteq2i 5253	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)))
272	271	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))))
273		fveq2 6889	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠) = ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))
274	273	fveq2d 6893	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))
275	274	cbvmptv 5261	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))
276	275	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))))
277		eqidd 2734	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)) = (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)))
278		oveq2 7414	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑡 → (𝑋 + 𝑟) = (𝑋 + 𝑡))
279	278	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) ∧ 𝑟 = 𝑡) → (𝑋 + 𝑟) = (𝑋 + 𝑡))
280	277, 279, 243, 234	fvmptd 7003	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡) = (𝑋 + 𝑡))
281	280	fveq2d 6893	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)))
282		fvres 6908	. . . . . . . . . . . . . 14 ⊢ ((𝑋 + 𝑡) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
283	262, 282	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
284	281, 283	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = (𝐹‘(𝑋 + 𝑡)))
285	284	mpteq2dva 5248	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
286	272, 276, 285	3eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
287	266, 286	eqtr2d 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))))
288		eqid 2733	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡))
289		ssid 4004	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
290	289	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → ℂ ⊆ ℂ)
291		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → 𝑋 ∈ ℂ)
292	290, 291, 290	constcncfg 44575	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑋) ∈ (ℂ–cn→ℂ))
293		cncfmptid 24421	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ))
294	289, 289, 293	mp2an 691	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)
295	294	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ))
296	292, 295	addcncf 24953	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ))
297	236, 296	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ))
298		ioosscn 13383	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ
299	298	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ)
300		ioosscn 13383	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
301	300	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
302	288, 297, 299, 301, 262	cncfmptssg 44574	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
303	302, 64	cncfco 24415	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
304	287, 303	eqeltrd 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
305	227	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) ∈ ℝ^*)
306	229	adantr 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
307		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
308		vex 3479	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑟 ∈ V
309	263	elrnmpt 5954	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡)))
310	308, 309	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))
311	307, 310	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))
312		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0..^𝑀))
313		nfmpt1 5256	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
314	313	nfrn 5950	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
315	314	nfcri 2891	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
316	312, 315	nfan 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
317		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑟 ∈ ℝ
318		simp3 1139	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡))
319	95	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑋 ∈ ℝ)
320	232	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑡 ∈ ℝ)
321	319, 320	readdcld 11240	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) ∈ ℝ)
322	318, 321	eqeltrd 2834	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 ∈ ℝ)
323	322	3exp 1120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)))
324	323	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)))
325	316, 317, 324	rexlimd 3264	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ))
326	311, 325	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ℝ)
327		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝑄‘𝑖) < 𝑟
328	252	3adant3 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄‘𝑖) < (𝑋 + 𝑡))
329		simp3 1139	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡))
330	328, 329	breqtrrd 5176	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄‘𝑖) < 𝑟)
331	330	3exp 1120	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟)))
332	331	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟)))
333	316, 327, 332	rexlimd 3264	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟))
334	311, 333	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) < 𝑟)
335		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑟 < (𝑄‘(𝑖 + 1))
336	261	3adant3 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1)))
337	329, 336	eqbrtrd 5170	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 < (𝑄‘(𝑖 + 1)))
338	337	3exp 1120	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))))
339	338	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))))
340	316, 335, 339	rexlimd 3264	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1))))
341	311, 340	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 < (𝑄‘(𝑖 + 1)))
342	305, 306, 326, 334, 341	eliood 44198	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
343	217	ineq2d 4212	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
344	343	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
345		dmres 6002	. . . . . . . . . . . . . . . . 17 ⊢ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹)
346	345	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹))
347		dfss 3966	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
348	60, 347	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
349	344, 346, 348	3eqtr4d 2783	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
350	349	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
351	342, 350	eleqtrrd 2837	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
352	326, 341	ltned 11347	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘(𝑖 + 1)))
353	352	neneqd 2946	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘(𝑖 + 1)))
354		velsn 4644	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {(𝑄‘(𝑖 + 1))} ↔ 𝑟 = (𝑄‘(𝑖 + 1)))
355	353, 354	sylnibr 329	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘(𝑖 + 1))})
356	351, 355	eldifd 3959	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
357	356	ralrimiva 3147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
358		dfss3 3970	. . . . . . . . . . 11 ⊢ (ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
359	357, 358	sylibr 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
360		eqid 2733	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠))
361	196	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑋 ∈ ℂ)
362		simpr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑠 ∈ ℂ)
363	361, 362	addcomd 11413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → (𝑋 + 𝑠) = (𝑠 + 𝑋))
364	363	mpteq2dva 5248	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)))
365		eqid 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋))
366	365	addccncf 24425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 ∈ ℂ → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ))
367	196, 366	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ))
368	364, 367	eqeltrd 2834	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ))
369	368	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ))
370	224	rexrd 11261	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℝ^*)
371		iocssre 13401	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ)
372	370, 225, 371	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ)
373		ax-resscn 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℂ
374	372, 373	sstrdi 3994	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ)
375	289	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℂ ⊆ ℂ)
376	196	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ)
377	374	sselda 3982	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
378	376, 377	addcld 11230	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ)
379	360, 369, 374, 375, 378	cncfmptssg 44574	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ))
380		eqid 2733	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
381		eqid 2733	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
382	380	cnfldtop 24292	. . . . . . . . . . . . . . . . . . . 20 ⊢ (TopOpen‘ℂ_fld) ∈ Top
383		unicntop 24294	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
384	383	restid 17376	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
385	382, 384	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
386	385	eqcomi 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
387	380, 381, 386	cncfcn 24418	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
388	374, 375, 387	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
389	379, 388	eleqtrd 2836	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
390	380	cnfldtopon 24291	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
391	390	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
392		resttopon 22657	. . . . . . . . . . . . . . . . 17 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
393	391, 374, 392	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
394		cncnp 22776	. . . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . . 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 231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡)))
397	396	simprd 497	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))
398		ubioc1 13374	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
399	370, 245, 174, 398	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
400		fveq2 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (𝐻‘(𝑖 + 1)) → ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
401	400	eleq2d 2820	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝐻‘(𝑖 + 1)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1)))))
402	401	rspccva 3612	. . . . . . . . . . . . 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 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
404		ioounsn 13451	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
405	370, 245, 174, 404	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
406	259	eqcomd 2739	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1))))
407	406	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1))))
408		iftrue 4534	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1)))
409	408	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1)))
410		oveq2 7414	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝐻‘(𝑖 + 1)) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1))))
411	410	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1))))
412	407, 409, 411	3eqtr4d 2783	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
413		iffalse 4537	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
414	413	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
415		eqidd 2734	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
416		oveq2 7414	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑠 → (𝑋 + 𝑡) = (𝑋 + 𝑠))
417	416	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠))
418		velsn 4644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ 𝑠 = (𝐻‘(𝑖 + 1)))
419	418	notbii 320	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ ¬ 𝑠 = (𝐻‘(𝑖 + 1)))
420		elun 4148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}))
421	420	biimpi 215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}))
422	421	orcomd 870	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ∨ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
423	422	ord 863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
424	419, 423	biimtrrid 242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 = (𝐻‘(𝑖 + 1)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
425	424	imp 408	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
426	425	adantll 713	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
427	95	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑋 ∈ ℝ)
428		elioore 13351	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
429	428	adantl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
430		elsni 4645	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 = (𝐻‘(𝑖 + 1)))
431	430	adantl 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 = (𝐻‘(𝑖 + 1)))
432	225	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
433	431, 432	eqeltrd 2834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 ∈ ℝ)
434	429, 433	jaodan 957	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ)
435	420, 434	sylan2b 595	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ)
436	427, 435	readdcld 11240	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → (𝑋 + 𝑠) ∈ ℝ)
437	436	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) ∈ ℝ)
438	415, 417, 426, 437	fvmptd 7003	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠))
439	414, 438	eqtrd 2773	. . . . . . . . . . . . . 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 5237	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)))
442	405	oveq2d 7422	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
443	442	oveq1d 7421	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld)))
444	443	fveq1d 6891	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
445	403, 441, 444	3eltr4d 2849	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
446		eqid 2733	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}))
447		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))
448	264, 301	fssd 6733	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶ℂ)
449	225	recnd 11239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℂ)
450	446, 380, 447, 448, 299, 449	ellimc 25382	. . . . . . . . . . 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 44323	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
453	266, 286	eqtrd 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
454	453	oveq1d 7421	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
455	452, 454	eleqtrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
456	40	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) ∈ ℝ)
457	456, 334	gtned 11346	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘𝑖))
458	457	neneqd 2946	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘𝑖))
459		velsn 4644	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {(𝑄‘𝑖)} ↔ 𝑟 = (𝑄‘𝑖))
460	458, 459	sylnibr 329	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘𝑖)})
461	351, 460	eldifd 3959	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
462	461	ralrimiva 3147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
463		dfss3 3970	. . . . . . . . . . 11 ⊢ (ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
464	462, 463	sylibr 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
465		icossre 13402	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻‘𝑖) ∈ ℝ ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^*) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ)
466	224, 245, 465	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ)
467	466, 373	sstrdi 3994	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ)
468	196	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ)
469	467	sselda 3982	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
470	468, 469	addcld 11230	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ)
471	360, 369, 467, 375, 470	cncfmptssg 44574	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
472		eqid 2733	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
473	380, 472, 386	cncfcn 24418	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
474	467, 375, 473	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
475	471, 474	eleqtrd 2836	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
476		resttopon 22657	. . . . . . . . . . . . . . . . 17 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
477	391, 467, 476	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
478		cncnp 22776	. . . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . . 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 231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡)))
481	480	simprd 497	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))
482		lbico1 13375	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
483	370, 245, 174, 482	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
484		fveq2 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (𝐻‘𝑖) → ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
485	484	eleq2d 2820	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝐻‘𝑖) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ↔ (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖))))
486	485	rspccva 3612	. . . . . . . . . . . . 13 ⊢ ((∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ∧ (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
487	481, 483, 486	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
488		uncom 4153	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) = ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
489		snunioo 13452	. . . . . . . . . . . . . . 15 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
490	370, 245, 174, 489	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
491	488, 490	eqtrid 2785	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
492		iftrue 4534	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝐻‘𝑖) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘𝑖))
493	492	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘𝑖))
494	240	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
495		oveq2 7414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (𝐻‘𝑖) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘𝑖)))
496	495	eqcomd 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝐻‘𝑖) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + 𝑠))
497	496	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + 𝑠))
498	493, 494, 497	3eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
499	498	adantlr 714	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
500		iffalse 4537	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑠 = (𝐻‘𝑖) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
501	500	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
502		eqidd 2734	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
503	416	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠))
504		velsn 4644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ {(𝐻‘𝑖)} ↔ 𝑠 = (𝐻‘𝑖))
505	504	notbii 320	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑠 ∈ {(𝐻‘𝑖)} ↔ ¬ 𝑠 = (𝐻‘𝑖))
506		elun 4148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)}))
507	506	biimpi 215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)}))
508	507	orcomd 870	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (𝑠 ∈ {(𝐻‘𝑖)} ∨ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
509	508	ord 863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (¬ 𝑠 ∈ {(𝐻‘𝑖)} → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
510	505, 509	biimtrrid 242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (¬ 𝑠 = (𝐻‘𝑖) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
511	510	imp 408	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
512	511	adantll 713	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
513	95	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → 𝑋 ∈ ℝ)
514		elsni 4645	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ {(𝐻‘𝑖)} → 𝑠 = (𝐻‘𝑖))
515	514	adantl 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → 𝑠 = (𝐻‘𝑖))
516	224	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → (𝐻‘𝑖) ∈ ℝ)
517	515, 516	eqeltrd 2834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → 𝑠 ∈ ℝ)
518	429, 517	jaodan 957	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)})) → 𝑠 ∈ ℝ)
519	506, 518	sylan2b 595	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → 𝑠 ∈ ℝ)
520	513, 519	readdcld 11240	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → (𝑋 + 𝑠) ∈ ℝ)
521	520	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → (𝑋 + 𝑠) ∈ ℝ)
522	502, 503, 512, 521	fvmptd 7003	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠))
523	501, 522	eqtrd 2773	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
524	499, 523	pm2.61dan 812	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
525	491, 524	mpteq12dva 5237	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)))
526	491	oveq2d 7422	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
527	526	oveq1d 7421	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld)))
528	527	fveq1d 6891	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
529	487, 525, 528	3eltr4d 2849	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
530		eqid 2733	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) = ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}))
531		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))
532	224	recnd 11239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℂ)
533	530, 380, 531, 448, 299, 532	ellimc 25382	. . . . . . . . . . 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 44323	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
536	453	oveq1d 7421	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
537	535, 536	eleqtrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
538	224, 225, 304, 455, 537	iblcncfioo 44681	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ 𝐿¹)
539	30	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ)
540	49	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → -π ∈ ℝ^*)
541	51	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → π ∈ ℝ^*)
542	21	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π))
543		simplr 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
544		simpr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))))
545	163, 173	oveq12d 7424	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
546	545	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
547	544, 546	eleqtrd 2836	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
548	547, 116	syldan 592	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
549	540, 541, 542, 543, 548	fourierdlem1 44811	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ (-π[,]π))
550	539, 549	ffvelcdmd 7085	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
551	224, 225, 538, 550	ibliooicc 44674	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ 𝐿¹)
552	14, 20, 159, 174, 223, 551	itgspltprt 44682	. . . . 5 ⊢ (𝜑 → ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡)
553	545	itgeq1d 44660	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
554	553	sumeq2dv 15646	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
555	552, 554	eqtrd 2773	. . . 4 ⊢ (𝜑 → ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
556	125, 155, 555	3eqtrd 2777	. . 3 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
557	121, 556	eqtr4d 2776	. 2 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)
558	13, 76, 557	3eqtrd 2777	1 ⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 {crab 3433 Vcvv 3475 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 ⊆ wss 3948 ifcif 4528 {csn 4628 class class class wbr 5148 ↦ cmpt 5231 dom cdm 5676 ran crn 5677 ↾ cres 5678 ∘ ccom 5680 Fun wfun 6535 ⟶wf 6537 ‘cfv 6541 (class class class)co 7406 ↑_m cmap 8817 ℂcc 11105 ℝcr 11106 0cc0 11107 1c1 11108 + caddc 11110 ℝ^*cxr 11244 < clt 11245 ≤ cle 11246 − cmin 11441 -cneg 11442 ℕcn 12209 ℤ_≥cuz 12819 (,)cioo 13321 (,]cioc 13322 [,)cico 13323 [,]cicc 13324 ...cfz 13481 ..^cfzo 13624 Σcsu 15629 πcpi 16007 ↾_t crest 17363 TopOpenctopn 17364 ℂ_fldccnfld 20937 Topctop 22387 TopOnctopon 22404 Cn ccn 22720 CnP ccnp 22721 –cn→ccncf 24384 ∫citg 25127 lim_ℂ climc 25371

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cc 10427 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-symdif 4242 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-disj 5114 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-ofr 7668 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-oadd 8467 df-omul 8468 df-er 8700 df-map 8819 df-pm 8820 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-dju 9893 df-card 9931 df-acn 9934 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ioo 13325 df-ioc 13326 df-ico 13327 df-icc 13328 df-fz 13482 df-fzo 13625 df-fl 13754 df-mod 13832 df-seq 13964 df-exp 14025 df-fac 14231 df-bc 14260 df-hash 14288 df-shft 15011 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-limsup 15412 df-clim 15429 df-rlim 15430 df-sum 15630 df-ef 16008 df-sin 16010 df-cos 16011 df-pi 16013 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-rest 17365 df-topn 17366 df-0g 17384 df-gsum 17385 df-topgen 17386 df-pt 17387 df-prds 17390 df-xrs 17445 df-qtop 17450 df-imas 17451 df-xps 17453 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669 df-mulg 18946 df-cntz 19176 df-cmn 19645 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-fbas 20934 df-fg 20935 df-cnfld 20938 df-top 22388 df-topon 22405 df-topsp 22427 df-bases 22441 df-cld 22515 df-ntr 22516 df-cls 22517 df-nei 22594 df-lp 22632 df-perf 22633 df-cn 22723 df-cnp 22724 df-haus 22811 df-cmp 22883 df-tx 23058 df-hmeo 23251 df-fil 23342 df-fm 23434 df-flim 23435 df-flf 23436 df-xms 23818 df-ms 23819 df-tms 23820 df-cncf 24386 df-ovol 24973 df-vol 24974 df-mbf 25128 df-itg1 25129 df-itg2 25130 df-ibl 25131 df-itg 25132 df-0p 25179 df-ditg 25356 df-limc 25375 df-dv 25376

This theorem is referenced by: fourierdlem101 44910

W3C validator