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 40896

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	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (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 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
4	3	fourierdlem2 40806	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 223	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simprd 485	. . . . . 6 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
8	7	simplld 775	. . . . 5 ⊢ (𝜑 → (𝑄‘0) = -π)
9	8	eqcomd 2819	. . . 4 ⊢ (𝜑 → -π = (𝑄‘0))
10	7	simplrd 777	. . . . 5 ⊢ (𝜑 → (𝑄‘𝑀) = π)
11	10	eqcomd 2819	. . . 4 ⊢ (𝜑 → π = (𝑄‘𝑀))
12	9, 11	oveq12d 6895	. . 3 ⊢ (𝜑 → (-π[,]π) = ((𝑄‘0)[,](𝑄‘𝑀)))
13	12	itgeq1d 40653	. 2 ⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑡) d𝑡)
14		0zd 11658	. . 3 ⊢ (𝜑 → 0 ∈ ℤ)
15		nnuz 11944	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
16	2, 15	syl6eleq 2902	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
17		1e0p1 11804	. . . . . 6 ⊢ 1 = (0 + 1)
18	17	a1i 11	. . . . 5 ⊢ (𝜑 → 1 = (0 + 1))
19	18	fveq2d 6415	. . . 4 ⊢ (𝜑 → (ℤ_≥‘1) = (ℤ_≥‘(0 + 1)))
20	16, 19	eleqtrd 2894	. . 3 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(0 + 1)))
21	3, 2, 1	fourierdlem15 40819	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
22		pire 24431	. . . . . . 7 ⊢ π ∈ ℝ
23	22	renegcli 10630	. . . . . 6 ⊢ -π ∈ ℝ
24		iccssre 12476	. . . . . 6 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
25	23, 22, 24	mp2an 675	. . . . 5 ⊢ (-π[,]π) ⊆ ℝ
26	25	a1i 11	. . . 4 ⊢ (𝜑 → (-π[,]π) ⊆ ℝ)
27	21, 26	fssd 6273	. . 3 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
28	7	simprd 485	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
29	28	r19.21bi 3127	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
30		fourierdlem93.6	. . . . 5 ⊢ (𝜑 → 𝐹:(-π[,]π)⟶ℂ)
31	30	adantr 468	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝐹:(-π[,]π)⟶ℂ)
32		simpr 473	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
33	12	eqcomd 2819	. . . . . 6 ⊢ (𝜑 → ((𝑄‘0)[,](𝑄‘𝑀)) = (-π[,]π))
34	33	adantr 468	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → ((𝑄‘0)[,](𝑄‘𝑀)) = (-π[,]π))
35	32, 34	eleqtrd 2894	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑡 ∈ (-π[,]π))
36	31, 35	ffvelrnd 6585	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝐹‘𝑡) ∈ ℂ)
37	27	adantr 468	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
38		elfzofz 12712	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
39	38	adantl 469	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
40	37, 39	ffvelrnd 6585	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
41		fzofzp1 12792	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
42	41	adantl 469	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
43	37, 42	ffvelrnd 6585	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
44	30	feqmptd 6473	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)))
45	44	adantr 468	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)))
46	45	reseq1d 5603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
47		ioossicc 12480	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
48	47	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
49	23	rexri 10385	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ^*
50	49	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → -π ∈ ℝ^*)
51	22	rexri 10385	. . . . . . . . . . . . . 14 ⊢ π ∈ ℝ^*
52	51	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → π ∈ ℝ^*)
53	21	ad2antrr 708	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π))
54		simplr 776	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
55		simpr 473	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
56	50, 52, 53, 54, 55	fourierdlem1 40805	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ (-π[,]π))
57	56	ralrimiva 3161	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π))
58		dfss3 3794	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ∀𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π))
59	57, 58	sylibr 225	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
60	48, 59	sstrd 3815	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
61	60	resmptd 5664	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)))
62	46, 61	eqtrd 2847	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)))
63	62	eqcomd 2819	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
64		fourierdlem93.7	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
65	63, 64	eqeltrd 2892	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
66		fourierdlem93.9	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
67	62	oveq1d 6892	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘(𝑖 + 1))))
68	66, 67	eleqtrd 2894	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘(𝑖 + 1))))
69		fourierdlem93.8	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
70	62	oveq1d 6892	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘𝑖)))
71	69, 70	eleqtrd 2894	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) lim_ℂ (𝑄‘𝑖)))
72	40, 43, 65, 68, 71	iblcncfioo 40674	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ 𝐿¹)
73	30	ad2antrr 708	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ)
74	73, 56	ffvelrnd 6585	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑡) ∈ ℂ)
75	40, 43, 72, 74	ibliooicc 40667	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ 𝐿¹)
76	14, 20, 27, 29, 36, 75	itgspltprt 40675	. 2 ⊢ (𝜑 → ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡)
77		fvres 6430	. . . . . . . 8 ⊢ (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) = (𝐹‘𝑡))
78	77	eqcomd 2819	. . . . . . 7 ⊢ (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → (𝐹‘𝑡) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡))
79	78	adantl 469	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑡) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡))
80	79	itgeq2dv 23768	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡)
81		eqid 2813	. . . . . 6 ⊢ (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))) = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
82	30	adantr 468	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:(-π[,]π)⟶ℂ)
83	82, 59	fssresd 6289	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))⟶ℂ)
84	48	resabs1d 5638	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
85	84, 64	eqeltrd 2892	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
86	84	oveq1d 6892	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
87	40, 43, 29, 83	limcicciooub 40350	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
88	86, 87	eqtr3d 2849	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
89	66, 88	eleqtrd 2894	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
90	84	eqcomd 2819	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
91	90	oveq1d 6892	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
92	40, 43, 29, 83	limciccioolb 40334	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
93	91, 92	eqtrd 2847	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
94	69, 93	eleqtrd 2894	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
95		fourierdlem93.5	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℝ)
96	95	adantr 468	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
97	81, 40, 43, 29, 83, 85, 89, 94, 96	fourierdlem82 40885	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡)
98	40	adantr 468	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘𝑖) ∈ ℝ)
99	43	adantr 468	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
100	95	ad2antrr 708	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑋 ∈ ℝ)
101	98, 100	resubcld 10746	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
102	99, 100	resubcld 10746	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
103		simpr 473	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
104		eliccre 40213	. . . . . . . . . 10 ⊢ ((((𝑄‘𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ)
105	101, 102, 103, 104	syl3anc 1483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ)
106	100, 105	readdcld 10357	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ℝ)
107		elicc2 12459	. . . . . . . . . . . 12 ⊢ ((((𝑄‘𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))))
108	101, 102, 107	syl2anc 575	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))))
109	103, 108	mpbid 223	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))
110	109	simp2d 1166	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘𝑖) − 𝑋) ≤ 𝑡)
111	98, 100, 105	lesubadd2d 10914	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ↔ (𝑄‘𝑖) ≤ (𝑋 + 𝑡)))
112	110, 111	mpbid 223	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘𝑖) ≤ (𝑋 + 𝑡))
113	109	simp3d 1167	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))
114	100, 105, 99	leaddsub2d 10917	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)) ↔ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))
115	113, 114	mpbird 248	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)))
116	98, 99, 106, 112, 115	eliccd 40211	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
117		fvres 6430	. . . . . . 7 ⊢ ((𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
118	116, 117	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
119	118	itgeq2dv 23768	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
120	80, 97, 119	3eqtrd 2851	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
121	120	sumeq2dv 14659	. . 3 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
122		oveq2 6885	. . . . . . 7 ⊢ (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
123	122	fveq2d 6415	. . . . . 6 ⊢ (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
124	123	cbvitgv 23763	. . . . 5 ⊢ ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡
125	124	a1i 11	. . . 4 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
126		fourierdlem93.2	. . . . . . . . 9 ⊢ 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋))
127	126	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)))
128		fveq2 6411	. . . . . . . . . 10 ⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
129	128	oveq1d 6892	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
130	129	adantl 469	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
131	2	nnzd 11750	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℤ)
132	14, 131, 14	3jca 1151	. . . . . . . . 9 ⊢ (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ))
133		0le0 11396	. . . . . . . . . . 11 ⊢ 0 ≤ 0
134	133	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 0)
135		0red 10331	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℝ)
136	2	nnred 11323	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
137	2	nngt0d 11353	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < 𝑀)
138	135, 136, 137	ltled 10473	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝑀)
139	134, 138	jca 503	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ 0 ∧ 0 ≤ 𝑀))
140		elfz2 12559	. . . . . . . . 9 ⊢ (0 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
141	132, 139, 140	sylanbrc 574	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (0...𝑀))
142	8, 23	syl6eqel 2900	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
143	142, 95	resubcld 10746	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘0) − 𝑋) ∈ ℝ)
144	127, 130, 141, 143	fvmptd 6512	. . . . . . 7 ⊢ (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋))
145	8	oveq1d 6892	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0) − 𝑋) = (-π − 𝑋))
146	144, 145	eqtr2d 2848	. . . . . 6 ⊢ (𝜑 → (-π − 𝑋) = (𝐻‘0))
147		fveq2 6411	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
148	147	oveq1d 6892	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑀) − 𝑋))
149	148	adantl 469	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 = 𝑀) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑀) − 𝑋))
150	14, 131, 131	3jca 1151	. . . . . . . . 9 ⊢ (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ))
151	136	leidd 10882	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
152	138, 151	jca 503	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀))
153		elfz2 12559	. . . . . . . . 9 ⊢ (𝑀 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑀)))
154	150, 152, 153	sylanbrc 574	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
155	10, 22	syl6eqel 2900	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
156	155, 95	resubcld 10746	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝑀) − 𝑋) ∈ ℝ)
157	127, 149, 154, 156	fvmptd 6512	. . . . . . 7 ⊢ (𝜑 → (𝐻‘𝑀) = ((𝑄‘𝑀) − 𝑋))
158	10	oveq1d 6892	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝑀) − 𝑋) = (π − 𝑋))
159	157, 158	eqtr2d 2848	. . . . . 6 ⊢ (𝜑 → (π − 𝑋) = (𝐻‘𝑀))
160	146, 159	oveq12d 6895	. . . . 5 ⊢ (𝜑 → ((-π − 𝑋)[,](π − 𝑋)) = ((𝐻‘0)[,](𝐻‘𝑀)))
161	160	itgeq1d 40653	. . . 4 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡)
162	27	ffvelrnda 6584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
163	95	adantr 468	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
164	162, 163	resubcld 10746	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
165	164, 126	fmptd 6609	. . . . . 6 ⊢ (𝜑 → 𝐻:(0...𝑀)⟶ℝ)
166	40, 43, 96, 29	ltsub1dd 10927	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − 𝑋) < ((𝑄‘(𝑖 + 1)) − 𝑋))
167	39, 164	syldan 581	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ)
168	126	fvmpt2 6515	. . . . . . . 8 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑄‘𝑖) − 𝑋) ∈ ℝ) → (𝐻‘𝑖) = ((𝑄‘𝑖) − 𝑋))
169	39, 167, 168	syl2anc 575	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) = ((𝑄‘𝑖) − 𝑋))
170		fveq2 6411	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
171	170	oveq1d 6892	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑗) − 𝑋))
172	171	cbvmptv 4951	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋))
173	126, 172	eqtri 2835	. . . . . . . . 9 ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋))
174	173	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋)))
175		fveq2 6411	. . . . . . . . . 10 ⊢ (𝑗 = (𝑖 + 1) → (𝑄‘𝑗) = (𝑄‘(𝑖 + 1)))
176	175	oveq1d 6892	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 + 1) → ((𝑄‘𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋))
177	176	adantl 469	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄‘𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋))
178	43, 96	resubcld 10746	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
179	174, 177, 42, 178	fvmptd 6512	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) − 𝑋))
180	166, 169, 179	3brtr4d 4883	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) < (𝐻‘(𝑖 + 1)))
181		frn 6265	. . . . . . . . 9 ⊢ (𝐹:(-π[,]π)⟶ℂ → ran 𝐹 ⊆ ℂ)
182	30, 181	syl 17	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 ⊆ ℂ)
183	182	adantr 468	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → ran 𝐹 ⊆ ℂ)
184		ffun 6262	. . . . . . . . . 10 ⊢ (𝐹:(-π[,]π)⟶ℂ → Fun 𝐹)
185	30, 184	syl 17	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐹)
186	185	adantr 468	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → Fun 𝐹)
187	23	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π ∈ ℝ)
188	22	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → π ∈ ℝ)
189	95	adantr 468	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑋 ∈ ℝ)
190	144, 143	eqeltrd 2892	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘0) ∈ ℝ)
191	190	adantr 468	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘0) ∈ ℝ)
192	157, 156	eqeltrd 2892	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻‘𝑀) ∈ ℝ)
193	192	adantr 468	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘𝑀) ∈ ℝ)
194		simpr 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)))
195		eliccre 40213	. . . . . . . . . . . 12 ⊢ (((𝐻‘0) ∈ ℝ ∧ (𝐻‘𝑀) ∈ ℝ ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ℝ)
196	191, 193, 194, 195	syl3anc 1483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ℝ)
197	189, 196	readdcld 10357	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ ℝ)
198	128	adantl 469	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑄‘𝑖) = (𝑄‘0))
199	198	oveq1d 6892	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
200	127, 199, 141, 143	fvmptd 6512	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋))
201	200	oveq2d 6893	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (𝐻‘0)) = (𝑋 + ((𝑄‘0) − 𝑋)))
202	95	recnd 10356	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ ℂ)
203	142	recnd 10356	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄‘0) ∈ ℂ)
204	202, 203	pncan3d 10683	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + ((𝑄‘0) − 𝑋)) = (𝑄‘0))
205	201, 204, 8	3eqtrrd 2852	. . . . . . . . . . . 12 ⊢ (𝜑 → -π = (𝑋 + (𝐻‘0)))
206	205	adantr 468	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π = (𝑋 + (𝐻‘0)))
207		elicc2 12459	. . . . . . . . . . . . . . 15 ⊢ (((𝐻‘0) ∈ ℝ ∧ (𝐻‘𝑀) ∈ ℝ) → (𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀))))
208	191, 193, 207	syl2anc 575	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀))))
209	194, 208	mpbid 223	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀)))
210	209	simp2d 1166	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘0) ≤ 𝑡)
211	191, 196, 189, 210	leadd2dd 10930	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + (𝐻‘0)) ≤ (𝑋 + 𝑡))
212	206, 211	eqbrtrd 4873	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π ≤ (𝑋 + 𝑡))
213	209	simp3d 1167	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ≤ (𝐻‘𝑀))
214	196, 193, 189, 213	leadd2dd 10930	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ≤ (𝑋 + (𝐻‘𝑀)))
215	157	oveq2d 6893	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (𝐻‘𝑀)) = (𝑋 + ((𝑄‘𝑀) − 𝑋)))
216	155	recnd 10356	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℂ)
217	202, 216	pncan3d 10683	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + ((𝑄‘𝑀) − 𝑋)) = (𝑄‘𝑀))
218	215, 217, 10	3eqtrrd 2852	. . . . . . . . . . . 12 ⊢ (𝜑 → π = (𝑋 + (𝐻‘𝑀)))
219	218	adantr 468	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → π = (𝑋 + (𝐻‘𝑀)))
220	214, 219	breqtrrd 4879	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ≤ π)
221	187, 188, 197, 212, 220	eliccd 40211	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ (-π[,]π))
222		fdm 6267	. . . . . . . . . . . 12 ⊢ (𝐹:(-π[,]π)⟶ℂ → dom 𝐹 = (-π[,]π))
223	30, 222	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = (-π[,]π))
224	223	eqcomd 2819	. . . . . . . . . 10 ⊢ (𝜑 → (-π[,]π) = dom 𝐹)
225	224	adantr 468	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (-π[,]π) = dom 𝐹)
226	221, 225	eleqtrd 2894	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ dom 𝐹)
227		fvelrn 6577	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ (𝑋 + 𝑡) ∈ dom 𝐹) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
228	186, 226, 227	syl2anc 575	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
229	183, 228	sseldd 3806	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
230	169, 167	eqeltrd 2892	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℝ)
231	179, 178	eqeltrd 2892	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
232	82, 60	fssresd 6289	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
233	40	rexrd 10377	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
234	233	adantr 468	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
235	43	rexrd 10377	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
236	235	adantr 468	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
237	95	ad2antrr 708	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
238		elioore 12426	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑡 ∈ ℝ)
239	238	adantl 469	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
240	237, 239	readdcld 10357	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ℝ)
241	169	oveq2d 6893	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + ((𝑄‘𝑖) − 𝑋)))
242	202	adantr 468	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
243	40	recnd 10356	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
244	242, 243	pncan3d 10683	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘𝑖) − 𝑋)) = (𝑄‘𝑖))
245		eqidd 2814	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (𝑄‘𝑖))
246	241, 244, 245	3eqtrrd 2852	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
247	246	adantr 468	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
248	230	adantr 468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) ∈ ℝ)
249		simpr 473	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
250	248	rexrd 10377	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) ∈ ℝ^*)
251	231	rexrd 10377	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ^*)
252	251	adantr 468	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ^*)
253		elioo2 12437	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^*) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1)))))
254	250, 252, 253	syl2anc 575	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1)))))
255	249, 254	mpbid 223	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1))))
256	255	simp2d 1166	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) < 𝑡)
257	248, 239, 237, 256	ltadd2dd 10484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘𝑖)) < (𝑋 + 𝑡))
258	247, 257	eqbrtrd 4873	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑋 + 𝑡))
259	231	adantr 468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
260	255	simp3d 1167	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 < (𝐻‘(𝑖 + 1)))
261	239, 259, 237, 260	ltadd2dd 10484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑋 + (𝐻‘(𝑖 + 1))))
262	179	oveq2d 6893	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)))
263	43	recnd 10356	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
264	242, 263	pncan3d 10683	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)) = (𝑄‘(𝑖 + 1)))
265	262, 264	eqtrd 2847	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1)))
266	265	adantr 468	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1)))
267	261, 266	breqtrd 4877	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1)))
268	234, 236, 240, 258, 267	eliood 40205	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
269		eqid 2813	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
270	268, 269	fmptd 6609	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
271		fcompt 6626	. . . . . . . . . . 11 ⊢ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))))
272	232, 270, 271	syl2anc 575	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))))
273		oveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑟 → (𝑋 + 𝑡) = (𝑋 + 𝑟))
274	273	cbvmptv 4951	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))
275	274	fveq1i 6412	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)
276	275	fveq2i 6414	. . . . . . . . . . . . 13 ⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))
277	276	mpteq2i 4942	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)))
278	277	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))))
279		fveq2 6411	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑡 → ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠) = ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))
280	279	fveq2d 6415	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))
281	280	cbvmptv 4951	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))
282	281	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))))
283		eqidd 2814	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)) = (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)))
284		oveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑡 → (𝑋 + 𝑟) = (𝑋 + 𝑡))
285	284	adantl 469	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) ∧ 𝑟 = 𝑡) → (𝑋 + 𝑟) = (𝑋 + 𝑡))
286	283, 285, 249, 240	fvmptd 6512	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡) = (𝑋 + 𝑡))
287	286	fveq2d 6415	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)))
288		fvres 6430	. . . . . . . . . . . . . 14 ⊢ ((𝑋 + 𝑡) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
289	268, 288	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
290	287, 289	eqtrd 2847	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = (𝐹‘(𝑋 + 𝑡)))
291	290	mpteq2dva 4945	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
292	278, 282, 291	3eqtrd 2851	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
293	272, 292	eqtr2d 2848	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))))
294		eqid 2813	. . . . . . . . . . 11 ⊢ (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡))
295		ssid 3827	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
296	295	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → ℂ ⊆ ℂ)
297		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → 𝑋 ∈ ℂ)
298	296, 297, 296	constcncfg 40565	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑋) ∈ (ℂ–cn→ℂ))
299		cncfmptid 22932	. . . . . . . . . . . . . . 15 ⊢ ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ))
300	295, 295, 299	mp2an 675	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)
301	300	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ))
302	298, 301	addcncf 40567	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ))
303	242, 302	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ))
304		ioosscn 40201	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ
305	304	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ)
306		ioosscn 40201	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
307	306	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
308	294, 303, 305, 307, 268	cncfmptssg 40564	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
309	308, 64	cncfco 22927	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
310	293, 309	eqeltrd 2892	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
311	233	adantr 468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) ∈ ℝ^*)
312	235	adantr 468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
313		simpr 473	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
314		vex 3401	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑟 ∈ V
315	269	elrnmpt 5580	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡)))
316	314, 315	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))
317	313, 316	sylib 209	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))
318		nfv 2005	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0..^𝑀))
319		nfmpt1 4948	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡(𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
320	319	nfrn 5576	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
321	320	nfcri 2949	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
322	318, 321	nfan 1990	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
323		nfv 2005	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑟 ∈ ℝ
324		simp3 1161	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡))
325	95	3ad2ant1 1156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑋 ∈ ℝ)
326	238	3ad2ant2 1157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑡 ∈ ℝ)
327	325, 326	readdcld 10357	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) ∈ ℝ)
328	324, 327	eqeltrd 2892	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 ∈ ℝ)
329	328	3exp 1141	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)))
330	329	ad2antrr 708	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)))
331	322, 323, 330	rexlimd 3221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ))
332	317, 331	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ℝ)
333		nfv 2005	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝑄‘𝑖) < 𝑟
334	258	3adant3 1155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄‘𝑖) < (𝑋 + 𝑡))
335		simp3 1161	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡))
336	334, 335	breqtrrd 4879	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄‘𝑖) < 𝑟)
337	336	3exp 1141	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟)))
338	337	adantr 468	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟)))
339	322, 333, 338	rexlimd 3221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟))
340	317, 339	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) < 𝑟)
341		nfv 2005	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡 𝑟 < (𝑄‘(𝑖 + 1))
342	267	3adant3 1155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1)))
343	335, 342	eqbrtrd 4873	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 < (𝑄‘(𝑖 + 1)))
344	343	3exp 1141	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))))
345	344	adantr 468	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))))
346	322, 341, 345	rexlimd 3221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1))))
347	317, 346	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 < (𝑄‘(𝑖 + 1)))
348	311, 312, 332, 340, 347	eliood 40205	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
349	223	ineq2d 4020	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
350	349	adantr 468	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
351		dmres 5629	. . . . . . . . . . . . . . . . 17 ⊢ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹)
352	351	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹))
353		dfss 3791	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
354	60, 353	sylib 209	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
355	350, 352, 354	3eqtr4d 2857	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
356	355	adantr 468	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
357	348, 356	eleqtrrd 2895	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
358	332, 347	ltned 10461	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘(𝑖 + 1)))
359	358	neneqd 2990	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘(𝑖 + 1)))
360		velsn 4393	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {(𝑄‘(𝑖 + 1))} ↔ 𝑟 = (𝑄‘(𝑖 + 1)))
361	359, 360	sylnibr 320	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘(𝑖 + 1))})
362	357, 361	eldifd 3787	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
363	362	ralrimiva 3161	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
364		dfss3 3794	. . . . . . . . . . 11 ⊢ (ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
365	363, 364	sylibr 225	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
366		eqid 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠))
367	202	adantr 468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑋 ∈ ℂ)
368		simpr 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑠 ∈ ℂ)
369	367, 368	addcomd 10526	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → (𝑋 + 𝑠) = (𝑠 + 𝑋))
370	369	mpteq2dva 4945	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)))
371		eqid 2813	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋))
372	371	addccncf 22936	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 ∈ ℂ → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ))
373	202, 372	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ))
374	370, 373	eqeltrd 2892	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ))
375	374	adantr 468	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ))
376	230	rexrd 10377	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℝ^*)
377		iocssre 12474	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ)
378	376, 231, 377	syl2anc 575	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ)
379		ax-resscn 10281	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℂ
380	378, 379	syl6ss 3817	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ)
381	295	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℂ ⊆ ℂ)
382	202	ad2antrr 708	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ)
383	380	sselda 3805	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
384	382, 383	addcld 10347	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ)
385	366, 375, 380, 381, 384	cncfmptssg 40564	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ))
386		eqid 2813	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
387		eqid 2813	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
388	386	cnfldtop 22804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (TopOpen‘ℂ_fld) ∈ Top
389		unicntop 22806	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
390	389	restid 16302	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
391	388, 390	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
392	391	eqcomi 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
393	386, 387, 392	cncfcn 22929	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
394	380, 381, 393	syl2anc 575	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
395	385, 394	eleqtrd 2894	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
396	386	cnfldtopon 22803	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
397	396	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ))
398		resttopon 21183	. . . . . . . . . . . . . . . . 17 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
399	397, 380, 398	syl2anc 575	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
400		cncnp 21302	. . . . . . . . . . . . . . . 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))‘𝑡))))
401	399, 397, 400	syl2anc 575	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)) ↔ ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))))
402	395, 401	mpbid 223	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡)))
403	402	simprd 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))
404		ubioc1 12448	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
405	376, 251, 180, 404	syl3anc 1483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
406		fveq2 6411	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (𝐻‘(𝑖 + 1)) → ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
407	406	eleq2d 2878	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝐻‘(𝑖 + 1)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1)))))
408	407	rspccva 3508	. . . . . . . . . . . . 13 ⊢ ((∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ∧ (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
409	403, 405, 408	syl2anc 575	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
410		ioounsn 12522	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
411	376, 251, 180, 410	syl3anc 1483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))
412	265	eqcomd 2819	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1))))
413	412	ad2antrr 708	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1))))
414		iftrue 4292	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1)))
415	414	adantl 469	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1)))
416		oveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝐻‘(𝑖 + 1)) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1))))
417	416	adantl 469	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1))))
418	413, 415, 417	3eqtr4d 2857	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
419		iffalse 4295	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
420	419	adantl 469	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
421		eqidd 2814	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
422		oveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑠 → (𝑋 + 𝑡) = (𝑋 + 𝑠))
423	422	adantl 469	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠))
424		velsn 4393	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ 𝑠 = (𝐻‘(𝑖 + 1)))
425	424	notbii 311	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ ¬ 𝑠 = (𝐻‘(𝑖 + 1)))
426		elun 3959	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}))
427	426	biimpi 207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}))
428	427	orcomd 889	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ∨ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
429	428	ord 882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
430	425, 429	syl5bir 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 = (𝐻‘(𝑖 + 1)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
431	430	imp 395	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
432	431	adantll 696	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
433	95	ad2antrr 708	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑋 ∈ ℝ)
434		elioore 12426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
435	434	adantl 469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
436		elsni 4394	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 = (𝐻‘(𝑖 + 1)))
437	436	adantl 469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 = (𝐻‘(𝑖 + 1)))
438	231	adantr 468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
439	437, 438	eqeltrd 2892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 ∈ ℝ)
440	435, 439	jaodan 971	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ)
441	426, 440	sylan2b 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ)
442	433, 441	readdcld 10357	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → (𝑋 + 𝑠) ∈ ℝ)
443	442	adantr 468	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) ∈ ℝ)
444	421, 423, 432, 443	fvmptd 6512	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠))
445	420, 444	eqtrd 2847	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
446	418, 445	pm2.61dan 838	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
447	411, 446	mpteq12dva 4933	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)))
448	411	oveq2d 6893	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))))
449	448	oveq1d 6892	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld)))
450	449	fveq1d 6413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
451	409, 447, 450	3eltr4d 2907	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1))))
452		eqid 2813	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}))
453		eqid 2813	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))
454	270, 307	fssd 6273	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶ℂ)
455	231	recnd 10356	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℂ)
456	452, 386, 453, 454, 305, 455	ellimc 23857	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘(𝑖 + 1))) ↔ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘(𝑖 + 1)))))
457	451, 456	mpbird 248	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘(𝑖 + 1))))
458	365, 457, 66	limccog 40333	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
459	272, 292	eqtrd 2847	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
460	459	oveq1d 6892	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
461	458, 460	eleqtrd 2894	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘(𝑖 + 1))))
462	40	adantr 468	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) ∈ ℝ)
463	462, 340	gtned 10460	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘𝑖))
464	463	neneqd 2990	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘𝑖))
465		velsn 4393	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {(𝑄‘𝑖)} ↔ 𝑟 = (𝑄‘𝑖))
466	464, 465	sylnibr 320	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘𝑖)})
467	357, 466	eldifd 3787	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
468	467	ralrimiva 3161	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
469		dfss3 3794	. . . . . . . . . . 11 ⊢ (ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
470	468, 469	sylibr 225	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}))
471		icossre 12475	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐻‘𝑖) ∈ ℝ ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^*) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ)
472	230, 251, 471	syl2anc 575	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ)
473	472, 379	syl6ss 3817	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ)
474	202	ad2antrr 708	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ)
475	473	sselda 3805	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
476	474, 475	addcld 10347	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ)
477	366, 375, 473, 381, 476	cncfmptssg 40564	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
478		eqid 2813	. . . . . . . . . . . . . . . . . 18 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
479	386, 478, 392	cncfcn 22929	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
480	473, 381, 479	syl2anc 575	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
481	477, 480	eleqtrd 2894	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)))
482		resttopon 21183	. . . . . . . . . . . . . . . . 17 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
483	397, 473, 482	syl2anc 575	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
484		cncnp 21302	. . . . . . . . . . . . . . . 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))‘𝑡))))
485	483, 397, 484	syl2anc 575	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂ_fld)) ↔ ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))))
486	481, 485	mpbid 223	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡)))
487	486	simprd 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡))
488		lbico1 12449	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
489	376, 251, 180, 488	syl3anc 1483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
490		fveq2 6411	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (𝐻‘𝑖) → ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
491	490	eleq2d 2878	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝐻‘𝑖) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ↔ (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖))))
492	491	rspccva 3508	. . . . . . . . . . . . 13 ⊢ ((∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘𝑡) ∧ (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
493	487, 489, 492	syl2anc 575	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
494		uncom 3963	. . . . . . . . . . . . . 14 ⊢ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) = ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
495		snunioo 12524	. . . . . . . . . . . . . . 15 ⊢ (((𝐻‘𝑖) ∈ ℝ^* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ^* ∧ (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
496	376, 251, 180, 495	syl3anc 1483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
497	494, 496	syl5eq 2859	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))
498		iftrue 4292	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝐻‘𝑖) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘𝑖))
499	498	adantl 469	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘𝑖))
500	246	adantr 468	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖)))
501		oveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (𝐻‘𝑖) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘𝑖)))
502	501	eqcomd 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝐻‘𝑖) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + 𝑠))
503	502	adantl 469	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + 𝑠))
504	499, 500, 503	3eqtrd 2851	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
505	504	adantlr 697	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
506		iffalse 4295	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑠 = (𝐻‘𝑖) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
507	506	adantl 469	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
508		eqidd 2814	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
509	422	adantl 469	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠))
510		velsn 4393	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ {(𝐻‘𝑖)} ↔ 𝑠 = (𝐻‘𝑖))
511	510	notbii 311	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑠 ∈ {(𝐻‘𝑖)} ↔ ¬ 𝑠 = (𝐻‘𝑖))
512		elun 3959	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)}))
513	512	biimpi 207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)}))
514	513	orcomd 889	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (𝑠 ∈ {(𝐻‘𝑖)} ∨ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
515	514	ord 882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (¬ 𝑠 ∈ {(𝐻‘𝑖)} → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
516	511, 515	syl5bir 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (¬ 𝑠 = (𝐻‘𝑖) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))))
517	516	imp 395	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
518	517	adantll 696	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))
519	95	ad2antrr 708	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → 𝑋 ∈ ℝ)
520		elsni 4394	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ {(𝐻‘𝑖)} → 𝑠 = (𝐻‘𝑖))
521	520	adantl 469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → 𝑠 = (𝐻‘𝑖))
522	230	adantr 468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → (𝐻‘𝑖) ∈ ℝ)
523	521, 522	eqeltrd 2892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → 𝑠 ∈ ℝ)
524	435, 523	jaodan 971	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)})) → 𝑠 ∈ ℝ)
525	512, 524	sylan2b 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → 𝑠 ∈ ℝ)
526	519, 525	readdcld 10357	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → (𝑋 + 𝑠) ∈ ℝ)
527	526	adantr 468	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → (𝑋 + 𝑠) ∈ ℝ)
528	508, 509, 518, 527	fvmptd 6512	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠))
529	507, 528	eqtrd 2847	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
530	505, 529	pm2.61dan 838	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
531	497, 530	mpteq12dva 4933	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)))
532	497	oveq2d 6893	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) = ((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))))
533	532	oveq1d 6892	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld)))
534	533	fveq1d 6413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)) = ((((TopOpen‘ℂ_fld) ↾_t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
535	493, 531, 534	3eltr4d 2907	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖)))
536		eqid 2813	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) = ((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}))
537		eqid 2813	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))
538	230	recnd 10356	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℂ)
539	536, 386, 537, 454, 305, 538	ellimc 23857	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘𝑖)) ↔ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂ_fld) ↾_t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP (TopOpen‘ℂ_fld))‘(𝐻‘𝑖))))
540	535, 539	mpbird 248	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim_ℂ (𝐻‘𝑖)))
541	470, 540, 69	limccog 40333	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
542	459	oveq1d 6892	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
543	541, 542	eleqtrd 2894	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim_ℂ (𝐻‘𝑖)))
544	230, 231, 310, 461, 543	iblcncfioo 40674	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ 𝐿¹)
545	30	ad2antrr 708	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ)
546	49	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → -π ∈ ℝ^*)
547	51	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → π ∈ ℝ^*)
548	21	ad2antrr 708	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π))
549		simplr 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
550		simpr 473	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))))
551	169, 179	oveq12d 6895	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
552	551	adantr 468	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
553	550, 552	eleqtrd 2894	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
554	553, 116	syldan 581	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
555	546, 547, 548, 549, 554	fourierdlem1 40805	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ (-π[,]π))
556	545, 555	ffvelrnd 6585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
557	230, 231, 544, 556	ibliooicc 40667	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ 𝐿¹)
558	14, 20, 165, 180, 229, 557	itgspltprt 40675	. . . . 5 ⊢ (𝜑 → ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡)
559	551	itgeq1d 40653	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
560	559	sumeq2dv 14659	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
561	558, 560	eqtrd 2847	. . . 4 ⊢ (𝜑 → ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
562	125, 161, 561	3eqtrd 2851	. . 3 ⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
563	121, 562	eqtr4d 2850	. 2 ⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)
564	13, 76, 563	3eqtrd 2851	1 ⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 ∨ wo 865 ∧ w3a 1100 = wceq 1637 ∈ wcel 2157 ∀wral 3103 ∃wrex 3104 {crab 3107 Vcvv 3398 ∖ cdif 3773 ∪ cun 3774 ∩ cin 3775 ⊆ wss 3776 ifcif 4286 {csn 4377 class class class wbr 4851 ↦ cmpt 4930 dom cdm 5318 ran crn 5319 ↾ cres 5320 ∘ ccom 5322 Fun wfun 6098 ⟶wf 6100 ‘cfv 6104 (class class class)co 6877 ↑_𝑚 cmap 8095 ℂcc 10222 ℝcr 10223 0cc0 10224 1c1 10225 + caddc 10227 ℝ^*cxr 10361 < clt 10362 ≤ cle 10363 − cmin 10554 -cneg 10555 ℕcn 11308 ℤcz 11646 ℤ_≥cuz 11907 (,)cioo 12396 (,]cioc 12397 [,)cico 12398 [,]cicc 12399 ...cfz 12552 ..^cfzo 12692 Σcsu 14642 πcpi 15020 ↾_t crest 16289 TopOpenctopn 16290 ℂ_fldccnfld 19957 Topctop 20915 TopOnctopon 20932 Cn ccn 21246 CnP ccnp 21247 –cn→ccncf 22896 ∫citg 23605 lim_ℂ climc 23846

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2069 ax-7 2105 ax-8 2159 ax-9 2166 ax-10 2186 ax-11 2202 ax-12 2215 ax-13 2422 ax-ext 2791 ax-rep 4971 ax-sep 4982 ax-nul 4990 ax-pow 5042 ax-pr 5103 ax-un 7182 ax-inf2 8788 ax-cc 9545 ax-cnex 10280 ax-resscn 10281 ax-1cn 10282 ax-icn 10283 ax-addcl 10284 ax-addrcl 10285 ax-mulcl 10286 ax-mulrcl 10287 ax-mulcom 10288 ax-addass 10289 ax-mulass 10290 ax-distr 10291 ax-i2m1 10292 ax-1ne0 10293 ax-1rid 10294 ax-rnegex 10295 ax-rrecex 10296 ax-cnre 10297 ax-pre-lttri 10298 ax-pre-lttrn 10299 ax-pre-ltadd 10300 ax-pre-mulgt0 10301 ax-pre-sup 10302 ax-addf 10303 ax-mulf 10304

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-fal 1651 df-ex 1860 df-nf 1864 df-sb 2062 df-mo 2635 df-eu 2638 df-clab 2800 df-cleq 2806 df-clel 2809 df-nfc 2944 df-ne 2986 df-nel 3089 df-ral 3108 df-rex 3109 df-reu 3110 df-rmo 3111 df-rab 3112 df-v 3400 df-sbc 3641 df-csb 3736 df-dif 3779 df-un 3781 df-in 3783 df-ss 3790 df-pss 3792 df-symdif 4049 df-nul 4124 df-if 4287 df-pw 4360 df-sn 4378 df-pr 4380 df-tp 4382 df-op 4384 df-uni 4638 df-int 4677 df-iun 4721 df-iin 4722 df-disj 4820 df-br 4852 df-opab 4914 df-mpt 4931 df-tr 4954 df-id 5226 df-eprel 5231 df-po 5239 df-so 5240 df-fr 5277 df-se 5278 df-we 5279 df-xp 5324 df-rel 5325 df-cnv 5326 df-co 5327 df-dm 5328 df-rn 5329 df-res 5330 df-ima 5331 df-pred 5900 df-ord 5946 df-on 5947 df-lim 5948 df-suc 5949 df-iota 6067 df-fun 6106 df-fn 6107 df-f 6108 df-f1 6109 df-fo 6110 df-f1o 6111 df-fv 6112 df-isom 6113 df-riota 6838 df-ov 6880 df-oprab 6881 df-mpt2 6882 df-of 7130 df-ofr 7131 df-om 7299 df-1st 7401 df-2nd 7402 df-supp 7533 df-wrecs 7645 df-recs 7707 df-rdg 7745 df-1o 7799 df-2o 7800 df-oadd 7803 df-omul 7804 df-er 7982 df-map 8097 df-pm 8098 df-ixp 8149 df-en 8196 df-dom 8197 df-sdom 8198 df-fin 8199 df-fsupp 8518 df-fi 8559 df-sup 8590 df-inf 8591 df-oi 8657 df-card 9051 df-acn 9054 df-cda 9278 df-pnf 10364 df-mnf 10365 df-xr 10366 df-ltxr 10367 df-le 10368 df-sub 10556 df-neg 10557 df-div 10973 df-nn 11309 df-2 11367 df-3 11368 df-4 11369 df-5 11370 df-6 11371 df-7 11372 df-8 11373 df-9 11374 df-n0 11563 df-z 11647 df-dec 11763 df-uz 11908 df-q 12011 df-rp 12050 df-xneg 12165 df-xadd 12166 df-xmul 12167 df-ioo 12400 df-ioc 12401 df-ico 12402 df-icc 12403 df-fz 12553 df-fzo 12693 df-fl 12820 df-mod 12896 df-seq 13028 df-exp 13087 df-fac 13284 df-bc 13313 df-hash 13341 df-shft 14033 df-cj 14065 df-re 14066 df-im 14067 df-sqrt 14201 df-abs 14202 df-limsup 14428 df-clim 14445 df-rlim 14446 df-sum 14643 df-ef 15021 df-sin 15023 df-cos 15024 df-pi 15026 df-struct 16073 df-ndx 16074 df-slot 16075 df-base 16077 df-sets 16078 df-ress 16079 df-plusg 16169 df-mulr 16170 df-starv 16171 df-sca 16172 df-vsca 16173 df-ip 16174 df-tset 16175 df-ple 16176 df-ds 16178 df-unif 16179 df-hom 16180 df-cco 16181 df-rest 16291 df-topn 16292 df-0g 16310 df-gsum 16311 df-topgen 16312 df-pt 16313 df-prds 16316 df-xrs 16370 df-qtop 16375 df-imas 16376 df-xps 16378 df-mre 16454 df-mrc 16455 df-acs 16457 df-mgm 17450 df-sgrp 17492 df-mnd 17503 df-submnd 17544 df-mulg 17749 df-cntz 17954 df-cmn 18399 df-psmet 19949 df-xmet 19950 df-met 19951 df-bl 19952 df-mopn 19953 df-fbas 19954 df-fg 19955 df-cnfld 19958 df-top 20916 df-topon 20933 df-topsp 20955 df-bases 20968 df-cld 21041 df-ntr 21042 df-cls 21043 df-nei 21120 df-lp 21158 df-perf 21159 df-cn 21249 df-cnp 21250 df-haus 21337 df-cmp 21408 df-tx 21583 df-hmeo 21776 df-fil 21867 df-fm 21959 df-flim 21960 df-flf 21961 df-xms 22342 df-ms 22343 df-tms 22344 df-cncf 22898 df-ovol 23451 df-vol 23452 df-mbf 23606 df-itg1 23607 df-itg2 23608 df-ibl 23609 df-itg 23610 df-0p 23657 df-ditg 23831 df-limc 23850 df-dv 23851

This theorem is referenced by: fourierdlem101 40904

W3C validator