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

Theorem fourierdlem93 45853
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.
StepHypRef Expression
1 fourierdlem93.4 . . . . . . . 8 (𝜑𝑄 ∈ (𝑃𝑀))
2 fourierdlem93.3 . . . . . . . . 9 (𝜑𝑀 ∈ ℕ)
3 fourierdlem93.1 . . . . . . . . . 10 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
43fourierdlem2 45763 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
52, 4syl 17 . . . . . . . 8 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
61, 5mpbid 231 . . . . . . 7 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
76simprd 494 . . . . . 6 (𝜑 → (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))
87simplld 766 . . . . 5 (𝜑 → (𝑄‘0) = -π)
98eqcomd 2732 . . . 4 (𝜑 → -π = (𝑄‘0))
107simplrd 768 . . . . 5 (𝜑 → (𝑄𝑀) = π)
1110eqcomd 2732 . . . 4 (𝜑 → π = (𝑄𝑀))
129, 11oveq12d 7431 . . 3 (𝜑 → (-π[,]π) = ((𝑄‘0)[,](𝑄𝑀)))
1312itgeq1d 45611 . 2 (𝜑 → ∫(-π[,]π)(𝐹𝑡) d𝑡 = ∫((𝑄‘0)[,](𝑄𝑀))(𝐹𝑡) d𝑡)
14 0zd 12613 . . 3 (𝜑 → 0 ∈ ℤ)
15 nnuz 12908 . . . . 5 ℕ = (ℤ‘1)
162, 15eleqtrdi 2836 . . . 4 (𝜑𝑀 ∈ (ℤ‘1))
17 1e0p1 12762 . . . . . 6 1 = (0 + 1)
1817a1i 11 . . . . 5 (𝜑 → 1 = (0 + 1))
1918fveq2d 6894 . . . 4 (𝜑 → (ℤ‘1) = (ℤ‘(0 + 1)))
2016, 19eleqtrd 2828 . . 3 (𝜑𝑀 ∈ (ℤ‘(0 + 1)))
213, 2, 1fourierdlem15 45776 . . . 4 (𝜑𝑄:(0...𝑀)⟶(-π[,]π))
22 pire 26480 . . . . . . 7 π ∈ ℝ
2322renegcli 11559 . . . . . 6 -π ∈ ℝ
24 iccssre 13451 . . . . . 6 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
2523, 22, 24mp2an 690 . . . . 5 (-π[,]π) ⊆ ℝ
2625a1i 11 . . . 4 (𝜑 → (-π[,]π) ⊆ ℝ)
2721, 26fssd 6734 . . 3 (𝜑𝑄:(0...𝑀)⟶ℝ)
287simprd 494 . . . 4 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
2928r19.21bi 3239 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
30 fourierdlem93.6 . . . . 5 (𝜑𝐹:(-π[,]π)⟶ℂ)
3130adantr 479 . . . 4 ((𝜑𝑡 ∈ ((𝑄‘0)[,](𝑄𝑀))) → 𝐹:(-π[,]π)⟶ℂ)
32 simpr 483 . . . . 5 ((𝜑𝑡 ∈ ((𝑄‘0)[,](𝑄𝑀))) → 𝑡 ∈ ((𝑄‘0)[,](𝑄𝑀)))
3312eqcomd 2732 . . . . . 6 (𝜑 → ((𝑄‘0)[,](𝑄𝑀)) = (-π[,]π))
3433adantr 479 . . . . 5 ((𝜑𝑡 ∈ ((𝑄‘0)[,](𝑄𝑀))) → ((𝑄‘0)[,](𝑄𝑀)) = (-π[,]π))
3532, 34eleqtrd 2828 . . . 4 ((𝜑𝑡 ∈ ((𝑄‘0)[,](𝑄𝑀))) → 𝑡 ∈ (-π[,]π))
3631, 35ffvelcdmd 7088 . . 3 ((𝜑𝑡 ∈ ((𝑄‘0)[,](𝑄𝑀))) → (𝐹𝑡) ∈ ℂ)
3727adantr 479 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
38 elfzofz 13693 . . . . . 6 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
3938adantl 480 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
4037, 39ffvelcdmd 7088 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
41 fzofzp1 13775 . . . . . 6 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
4241adantl 480 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
4337, 42ffvelcdmd 7088 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
4430feqmptd 6960 . . . . . . . . . 10 (𝜑𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹𝑡)))
4544adantr 479 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹𝑡)))
4645reseq1d 5978 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑡 ∈ (-π[,]π) ↦ (𝐹𝑡)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
47 ioossicc 13455 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
4847a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
4923rexri 11310 . . . . . . . . . . . . . 14 -π ∈ ℝ*
5049a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) → -π ∈ ℝ*)
5122rexri 11310 . . . . . . . . . . . . . 14 π ∈ ℝ*
5251a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) → π ∈ ℝ*)
5321ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π))
54 simplr 767 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
55 simpr 483 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
5650, 52, 53, 54, 55fourierdlem1 45762 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ (-π[,]π))
5756ralrimiva 3136 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π))
58 dfss3 3967 . . . . . . . . . . 11 (((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ∀𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π))
5957, 58sylibr 233 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
6048, 59sstrd 3989 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
6160resmptd 6039 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑡 ∈ (-π[,]π) ↦ (𝐹𝑡)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹𝑡)))
6246, 61eqtrd 2766 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹𝑡)))
6362eqcomd 2732 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹𝑡)) = (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
64 fourierdlem93.7 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
6563, 64eqeltrd 2826 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹𝑡)) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
66 fourierdlem93.9 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
6762oveq1d 7428 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹𝑡)) lim (𝑄‘(𝑖 + 1))))
6866, 67eleqtrd 2828 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹𝑡)) lim (𝑄‘(𝑖 + 1))))
69 fourierdlem93.8 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
7062oveq1d 7428 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)) = ((𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹𝑡)) lim (𝑄𝑖)))
7169, 70eleqtrd 2828 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹𝑡)) lim (𝑄𝑖)))
7240, 43, 65, 68, 71iblcncfioo 45632 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹𝑡)) ∈ 𝐿1)
7330ad2antrr 724 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ)
7473, 56ffvelcdmd 7088 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹𝑡) ∈ ℂ)
7540, 43, 72, 74ibliooicc 45625 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ (𝐹𝑡)) ∈ 𝐿1)
7614, 20, 27, 29, 36, 75itgspltprt 45633 . 2 (𝜑 → ∫((𝑄‘0)[,](𝑄𝑀))(𝐹𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹𝑡) d𝑡)
77 fvres 6909 . . . . . . . 8 (𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) = (𝐹𝑡))
7877eqcomd 2732 . . . . . . 7 (𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) → (𝐹𝑡) = ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡))
7978adantl 480 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹𝑡) = ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡))
8079itgeq2dv 25796 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → ∫((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹𝑡) d𝑡 = ∫((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡)
81 eqid 2726 . . . . . 6 (𝑥 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))) = (𝑥 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
8230adantr 479 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:(-π[,]π)⟶ℂ)
8382, 59fssresd 6758 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))):((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))⟶ℂ)
8448resabs1d 6007 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
8584, 64eqeltrd 2826 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
8684oveq1d 7428 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
8740, 43, 29, 83limcicciooub 45291 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
8886, 87eqtr3d 2768 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
8966, 88eleqtrd 2828 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
9084eqcomd 2732 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
9190oveq1d 7428 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)) = (((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
9240, 43, 29, 83limciccioolb 45275 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)) = ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
9391, 92eqtrd 2766 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)) = ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
9469, 93eleqtrd 2828 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
95 fourierdlem93.5 . . . . . . 7 (𝜑𝑋 ∈ ℝ)
9695adantr 479 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
9781, 40, 43, 29, 83, 85, 89, 94, 96fourierdlem82 45842 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → ∫((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡 = ∫(((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡)
9840adantr 479 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄𝑖) ∈ ℝ)
9943adantr 479 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
10095ad2antrr 724 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑋 ∈ ℝ)
10198, 100resubcld 11680 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄𝑖) − 𝑋) ∈ ℝ)
10299, 100resubcld 11680 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
103 simpr 483 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
104 eliccre 45156 . . . . . . . . . 10 ((((𝑄𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ)
105101, 102, 103, 104syl3anc 1368 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ)
106100, 105readdcld 11281 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ℝ)
107 elicc2 13434 . . . . . . . . . . . 12 ((((𝑄𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄𝑖) − 𝑋) ≤ 𝑡𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))))
108101, 102, 107syl2anc 582 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄𝑖) − 𝑋) ≤ 𝑡𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))))
109103, 108mpbid 231 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ ℝ ∧ ((𝑄𝑖) − 𝑋) ≤ 𝑡𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))
110109simp2d 1140 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄𝑖) − 𝑋) ≤ 𝑡)
11198, 100, 105lesubadd2d 11851 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (((𝑄𝑖) − 𝑋) ≤ 𝑡 ↔ (𝑄𝑖) ≤ (𝑋 + 𝑡)))
112110, 111mpbid 231 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄𝑖) ≤ (𝑋 + 𝑡))
113109simp3d 1141 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))
114100, 105, 99leaddsub2d 11854 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)) ↔ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))
115113, 114mpbird 256 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)))
11698, 99, 106, 112, 115eliccd 45155 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
117 fvres 6909 . . . . . . 7 ((𝑋 + 𝑡) ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
118116, 117syl 17 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
119118itgeq2dv 25796 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → ∫(((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
12080, 97, 1193eqtrd 2770 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → ∫((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹𝑡) d𝑡 = ∫(((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
121120sumeq2dv 15699 . . 3 (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
122 oveq2 7421 . . . . . . 7 (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
123122fveq2d 6894 . . . . . 6 (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
124123cbvitgv 25791 . . . . 5 ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡
125124a1i 11 . . . 4 (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
126 fourierdlem93.2 . . . . . . . . 9 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) − 𝑋))
127126a1i 11 . . . . . . . 8 (𝜑𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) − 𝑋)))
128 fveq2 6890 . . . . . . . . . 10 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
129128oveq1d 7428 . . . . . . . . 9 (𝑖 = 0 → ((𝑄𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
130129adantl 480 . . . . . . . 8 ((𝜑𝑖 = 0) → ((𝑄𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
1312nnzd 12628 . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
132 0le0 12356 . . . . . . . . . 10 0 ≤ 0
133132a1i 11 . . . . . . . . 9 (𝜑 → 0 ≤ 0)
134 0red 11255 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
1352nnred 12270 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
1362nngt0d 12304 . . . . . . . . . 10 (𝜑 → 0 < 𝑀)
137134, 135, 136ltled 11400 . . . . . . . . 9 (𝜑 → 0 ≤ 𝑀)
13814, 131, 14, 133, 137elfzd 13537 . . . . . . . 8 (𝜑 → 0 ∈ (0...𝑀))
1398, 23eqeltrdi 2834 . . . . . . . . 9 (𝜑 → (𝑄‘0) ∈ ℝ)
140139, 95resubcld 11680 . . . . . . . 8 (𝜑 → ((𝑄‘0) − 𝑋) ∈ ℝ)
141127, 130, 138, 140fvmptd 7005 . . . . . . 7 (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋))
1428oveq1d 7428 . . . . . . 7 (𝜑 → ((𝑄‘0) − 𝑋) = (-π − 𝑋))
143141, 142eqtr2d 2767 . . . . . 6 (𝜑 → (-π − 𝑋) = (𝐻‘0))
144 fveq2 6890 . . . . . . . . . 10 (𝑖 = 𝑀 → (𝑄𝑖) = (𝑄𝑀))
145144oveq1d 7428 . . . . . . . . 9 (𝑖 = 𝑀 → ((𝑄𝑖) − 𝑋) = ((𝑄𝑀) − 𝑋))
146145adantl 480 . . . . . . . 8 ((𝜑𝑖 = 𝑀) → ((𝑄𝑖) − 𝑋) = ((𝑄𝑀) − 𝑋))
147135leidd 11818 . . . . . . . . 9 (𝜑𝑀𝑀)
14814, 131, 131, 137, 147elfzd 13537 . . . . . . . 8 (𝜑𝑀 ∈ (0...𝑀))
14910, 22eqeltrdi 2834 . . . . . . . . 9 (𝜑 → (𝑄𝑀) ∈ ℝ)
150149, 95resubcld 11680 . . . . . . . 8 (𝜑 → ((𝑄𝑀) − 𝑋) ∈ ℝ)
151127, 146, 148, 150fvmptd 7005 . . . . . . 7 (𝜑 → (𝐻𝑀) = ((𝑄𝑀) − 𝑋))
15210oveq1d 7428 . . . . . . 7 (𝜑 → ((𝑄𝑀) − 𝑋) = (π − 𝑋))
153151, 152eqtr2d 2767 . . . . . 6 (𝜑 → (π − 𝑋) = (𝐻𝑀))
154143, 153oveq12d 7431 . . . . 5 (𝜑 → ((-π − 𝑋)[,](π − 𝑋)) = ((𝐻‘0)[,](𝐻𝑀)))
155154itgeq1d 45611 . . . 4 (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐻‘0)[,](𝐻𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡)
15627ffvelcdmda 7087 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) ∈ ℝ)
15795adantr 479 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
158156, 157resubcld 11680 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑄𝑖) − 𝑋) ∈ ℝ)
159158, 126fmptd 7117 . . . . . 6 (𝜑𝐻:(0...𝑀)⟶ℝ)
16040, 43, 96, 29ltsub1dd 11864 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − 𝑋) < ((𝑄‘(𝑖 + 1)) − 𝑋))
16139, 158syldan 589 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) − 𝑋) ∈ ℝ)
162126fvmpt2 7009 . . . . . . . 8 ((𝑖 ∈ (0...𝑀) ∧ ((𝑄𝑖) − 𝑋) ∈ ℝ) → (𝐻𝑖) = ((𝑄𝑖) − 𝑋))
16339, 161, 162syl2anc 582 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻𝑖) = ((𝑄𝑖) − 𝑋))
164 fveq2 6890 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (𝑄𝑖) = (𝑄𝑗))
165164oveq1d 7428 . . . . . . . . . . 11 (𝑖 = 𝑗 → ((𝑄𝑖) − 𝑋) = ((𝑄𝑗) − 𝑋))
166165cbvmptv 5256 . . . . . . . . . 10 (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) − 𝑋))
167126, 166eqtri 2754 . . . . . . . . 9 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) − 𝑋))
168167a1i 11 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) − 𝑋)))
169 fveq2 6890 . . . . . . . . . 10 (𝑗 = (𝑖 + 1) → (𝑄𝑗) = (𝑄‘(𝑖 + 1)))
170169oveq1d 7428 . . . . . . . . 9 (𝑗 = (𝑖 + 1) → ((𝑄𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋))
171170adantl 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋))
17243, 96resubcld 11680 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
173168, 171, 42, 172fvmptd 7005 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) − 𝑋))
174160, 163, 1733brtr4d 5175 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻𝑖) < (𝐻‘(𝑖 + 1)))
175 frn 6724 . . . . . . . . 9 (𝐹:(-π[,]π)⟶ℂ → ran 𝐹 ⊆ ℂ)
17630, 175syl 17 . . . . . . . 8 (𝜑 → ran 𝐹 ⊆ ℂ)
177176adantr 479 . . . . . . 7 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → ran 𝐹 ⊆ ℂ)
178 ffun 6720 . . . . . . . . . 10 (𝐹:(-π[,]π)⟶ℂ → Fun 𝐹)
17930, 178syl 17 . . . . . . . . 9 (𝜑 → Fun 𝐹)
180179adantr 479 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → Fun 𝐹)
18123a1i 11 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → -π ∈ ℝ)
18222a1i 11 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → π ∈ ℝ)
18395adantr 479 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → 𝑋 ∈ ℝ)
184141, 140eqeltrd 2826 . . . . . . . . . . . . 13 (𝜑 → (𝐻‘0) ∈ ℝ)
185184adantr 479 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝐻‘0) ∈ ℝ)
186151, 150eqeltrd 2826 . . . . . . . . . . . . 13 (𝜑 → (𝐻𝑀) ∈ ℝ)
187186adantr 479 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝐻𝑀) ∈ ℝ)
188 simpr 483 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → 𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀)))
189 eliccre 45156 . . . . . . . . . . . 12 (((𝐻‘0) ∈ ℝ ∧ (𝐻𝑀) ∈ ℝ ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → 𝑡 ∈ ℝ)
190185, 187, 188, 189syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → 𝑡 ∈ ℝ)
191183, 190readdcld 11281 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝑋 + 𝑡) ∈ ℝ)
192128adantl 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 = 0) → (𝑄𝑖) = (𝑄‘0))
193192oveq1d 7428 . . . . . . . . . . . . . . 15 ((𝜑𝑖 = 0) → ((𝑄𝑖) − 𝑋) = ((𝑄‘0) − 𝑋))
194127, 193, 138, 140fvmptd 7005 . . . . . . . . . . . . . 14 (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋))
195194oveq2d 7429 . . . . . . . . . . . . 13 (𝜑 → (𝑋 + (𝐻‘0)) = (𝑋 + ((𝑄‘0) − 𝑋)))
19695recnd 11280 . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ ℂ)
197139recnd 11280 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ∈ ℂ)
198196, 197pncan3d 11612 . . . . . . . . . . . . 13 (𝜑 → (𝑋 + ((𝑄‘0) − 𝑋)) = (𝑄‘0))
199195, 198, 83eqtrrd 2771 . . . . . . . . . . . 12 (𝜑 → -π = (𝑋 + (𝐻‘0)))
200199adantr 479 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → -π = (𝑋 + (𝐻‘0)))
201 elicc2 13434 . . . . . . . . . . . . . . 15 (((𝐻‘0) ∈ ℝ ∧ (𝐻𝑀) ∈ ℝ) → (𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡𝑡 ≤ (𝐻𝑀))))
202185, 187, 201syl2anc 582 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡𝑡 ≤ (𝐻𝑀))))
203188, 202mpbid 231 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡𝑡 ≤ (𝐻𝑀)))
204203simp2d 1140 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝐻‘0) ≤ 𝑡)
205185, 190, 183, 204leadd2dd 11867 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝑋 + (𝐻‘0)) ≤ (𝑋 + 𝑡))
206200, 205eqbrtrd 5165 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → -π ≤ (𝑋 + 𝑡))
207203simp3d 1141 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → 𝑡 ≤ (𝐻𝑀))
208190, 187, 183, 207leadd2dd 11867 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝑋 + 𝑡) ≤ (𝑋 + (𝐻𝑀)))
209151oveq2d 7429 . . . . . . . . . . . . 13 (𝜑 → (𝑋 + (𝐻𝑀)) = (𝑋 + ((𝑄𝑀) − 𝑋)))
210149recnd 11280 . . . . . . . . . . . . . 14 (𝜑 → (𝑄𝑀) ∈ ℂ)
211196, 210pncan3d 11612 . . . . . . . . . . . . 13 (𝜑 → (𝑋 + ((𝑄𝑀) − 𝑋)) = (𝑄𝑀))
212209, 211, 103eqtrrd 2771 . . . . . . . . . . . 12 (𝜑 → π = (𝑋 + (𝐻𝑀)))
213212adantr 479 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → π = (𝑋 + (𝐻𝑀)))
214208, 213breqtrrd 5171 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝑋 + 𝑡) ≤ π)
215181, 182, 191, 206, 214eliccd 45155 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝑋 + 𝑡) ∈ (-π[,]π))
216 fdm 6726 . . . . . . . . . . . 12 (𝐹:(-π[,]π)⟶ℂ → dom 𝐹 = (-π[,]π))
21730, 216syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = (-π[,]π))
218217eqcomd 2732 . . . . . . . . . 10 (𝜑 → (-π[,]π) = dom 𝐹)
219218adantr 479 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (-π[,]π) = dom 𝐹)
220215, 219eleqtrd 2828 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝑋 + 𝑡) ∈ dom 𝐹)
221 fvelrn 7079 . . . . . . . 8 ((Fun 𝐹 ∧ (𝑋 + 𝑡) ∈ dom 𝐹) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
222180, 220, 221syl2anc 582 . . . . . . 7 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹)
223177, 222sseldd 3979 . . . . . 6 ((𝜑𝑡 ∈ ((𝐻‘0)[,](𝐻𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
224163, 161eqeltrd 2826 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻𝑖) ∈ ℝ)
225173, 172eqeltrd 2826 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
22682, 60fssresd 6758 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
22740rexrd 11302 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
228227adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ*)
22943rexrd 11302 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
230229adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
23195ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232 elioore 13399 . . . . . . . . . . . . . . 15 (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑡 ∈ ℝ)
233232adantl 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
234231, 233readdcld 11281 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ℝ)
235163oveq2d 7429 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻𝑖)) = (𝑋 + ((𝑄𝑖) − 𝑋)))
236196adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
23740recnd 11280 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
238236, 237pncan3d 11612 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄𝑖) − 𝑋)) = (𝑄𝑖))
239 eqidd 2727 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (𝑄𝑖))
240235, 238, 2393eqtrrd 2771 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (𝑋 + (𝐻𝑖)))
241240adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄𝑖) = (𝑋 + (𝐻𝑖)))
242224adantr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻𝑖) ∈ ℝ)
243 simpr 483 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))))
244242rexrd 11302 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻𝑖) ∈ ℝ*)
245225rexrd 11302 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ*)
246245adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ*)
247 elioo2 13410 . . . . . . . . . . . . . . . . . 18 (((𝐻𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ*) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻𝑖) < 𝑡𝑡 < (𝐻‘(𝑖 + 1)))))
248244, 246, 247syl2anc 582 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻𝑖) < 𝑡𝑡 < (𝐻‘(𝑖 + 1)))))
249243, 248mpbid 231 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ℝ ∧ (𝐻𝑖) < 𝑡𝑡 < (𝐻‘(𝑖 + 1))))
250249simp2d 1140 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻𝑖) < 𝑡)
251242, 233, 231, 250ltadd2dd 11411 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻𝑖)) < (𝑋 + 𝑡))
252241, 251eqbrtrd 5165 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄𝑖) < (𝑋 + 𝑡))
253225adantr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
254249simp3d 1141 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 < (𝐻‘(𝑖 + 1)))
255233, 253, 231, 254ltadd2dd 11411 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑋 + (𝐻‘(𝑖 + 1))))
256173oveq2d 7429 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)))
25743recnd 11280 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
258236, 257pncan3d 11612 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)) = (𝑄‘(𝑖 + 1)))
259256, 258eqtrd 2766 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1)))
260259adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1)))
261255, 260breqtrd 5169 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1)))
262228, 230, 234, 252, 261eliood 45149 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
263 eqid 2726 . . . . . . . . . . . 12 (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
264262, 263fmptd 7117 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
265 fcompt 7136 . . . . . . . . . . 11 (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))))
266226, 264, 265syl2anc 582 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))))
267 oveq2 7421 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑟 → (𝑋 + 𝑡) = (𝑋 + 𝑟))
268267cbvmptv 5256 . . . . . . . . . . . . . . 15 (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))
269268fveq1i 6891 . . . . . . . . . . . . . 14 ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = ((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)
270269fveq2i 6893 . . . . . . . . . . . . 13 ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))
271270mpteq2i 5248 . . . . . . . . . . . 12 (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)))
272271a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))))
273 fveq2 6890 . . . . . . . . . . . . . 14 (𝑠 = 𝑡 → ((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠) = ((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))
274273fveq2d 6894 . . . . . . . . . . . . 13 (𝑠 = 𝑡 → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))
275274cbvmptv 5256 . . . . . . . . . . . 12 (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))
276275a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))))
277 eqidd 2727 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)) = (𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)))
278 oveq2 7421 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑡 → (𝑋 + 𝑟) = (𝑋 + 𝑡))
279278adantl 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) ∧ 𝑟 = 𝑡) → (𝑋 + 𝑟) = (𝑋 + 𝑡))
280277, 279, 243, 234fvmptd 7005 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡) = (𝑋 + 𝑡))
281280fveq2d 6894 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)))
282 fvres 6909 . . . . . . . . . . . . . 14 ((𝑋 + 𝑡) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
283262, 282syl 17 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡)))
284281, 283eqtrd 2766 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = (𝐹‘(𝑋 + 𝑡)))
285284mpteq2dva 5243 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))) = (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
286272, 276, 2853eqtrd 2770 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
287266, 286eqtr2d 2767 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))))
288 eqid 2726 . . . . . . . . . . 11 (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡))
289 ssid 4001 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
290289a1i 11 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → ℂ ⊆ ℂ)
291 id 22 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → 𝑋 ∈ ℂ)
292290, 291, 290constcncfg 45526 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑋) ∈ (ℂ–cn→ℂ))
293 cncfmptid 24918 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ))
294289, 289, 293mp2an 690 . . . . . . . . . . . . . 14 (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)
295294a1i 11 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ))
296292, 295addcncf 25457 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ))
297236, 296syl 17 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ))
298 ioosscn 13431 . . . . . . . . . . . 12 ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ
299298a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ)
300 ioosscn 13431 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
301300a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
302288, 297, 299, 301, 262cncfmptssg 45525 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
303302, 64cncfco 24912 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
304287, 303eqeltrd 2826 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
305227adantr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄𝑖) ∈ ℝ*)
306229adantr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
307 simpr 483 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
308 vex 3466 . . . . . . . . . . . . . . . . . 18 𝑟 ∈ V
309263elrnmpt 5952 . . . . . . . . . . . . . . . . . 18 (𝑟 ∈ V → (𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡)))
310308, 309ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))
311307, 310sylib 217 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ∃𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))
312 nfv 1910 . . . . . . . . . . . . . . . . . 18 𝑡(𝜑𝑖 ∈ (0..^𝑀))
313 nfmpt1 5251 . . . . . . . . . . . . . . . . . . . 20 𝑡(𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
314313nfrn 5948 . . . . . . . . . . . . . . . . . . 19 𝑡ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
315314nfcri 2883 . . . . . . . . . . . . . . . . . 18 𝑡 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))
316312, 315nfan 1895 . . . . . . . . . . . . . . . . 17 𝑡((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
317 nfv 1910 . . . . . . . . . . . . . . . . 17 𝑡 𝑟 ∈ ℝ
318 simp3 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡))
319953ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑋 ∈ ℝ)
3202323ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑡 ∈ ℝ)
321319, 320readdcld 11281 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) ∈ ℝ)
322318, 321eqeltrd 2826 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 ∈ ℝ)
3233223exp 1116 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)))
324323ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)))
325316, 317, 324rexlimd 3254 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ))
326311, 325mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ℝ)
327 nfv 1910 . . . . . . . . . . . . . . . . 17 𝑡(𝑄𝑖) < 𝑟
3282523adant3 1129 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄𝑖) < (𝑋 + 𝑡))
329 simp3 1135 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡))
330328, 329breqtrrd 5171 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄𝑖) < 𝑟)
3313303exp 1116 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄𝑖) < 𝑟)))
332331adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄𝑖) < 𝑟)))
333316, 327, 332rexlimd 3254 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → (𝑄𝑖) < 𝑟))
334311, 333mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄𝑖) < 𝑟)
335 nfv 1910 . . . . . . . . . . . . . . . . 17 𝑡 𝑟 < (𝑄‘(𝑖 + 1))
3362613adant3 1129 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1)))
337329, 336eqbrtrd 5165 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 < (𝑄‘(𝑖 + 1)))
3383373exp 1116 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))))
339338adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))))
340316, 335, 339rexlimd 3254 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1))))
341311, 340mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 < (𝑄‘(𝑖 + 1)))
342305, 306, 326, 334, 341eliood 45149 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
343217ineq2d 4210 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
344343adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
345 dmres 6011 . . . . . . . . . . . . . . . . 17 dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹)
346345a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹))
347 dfss 3965 . . . . . . . . . . . . . . . . 17 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
34860, 347sylib 217 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ (-π[,]π)))
349344, 346, 3483eqtr4d 2776 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
350349adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
351342, 350eleqtrrd 2829 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
352326, 341ltned 11388 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘(𝑖 + 1)))
353352neneqd 2935 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘(𝑖 + 1)))
354 velsn 4639 . . . . . . . . . . . . . 14 (𝑟 ∈ {(𝑄‘(𝑖 + 1))} ↔ 𝑟 = (𝑄‘(𝑖 + 1)))
355353, 354sylnibr 328 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘(𝑖 + 1))})
356351, 355eldifd 3957 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
357356ralrimiva 3136 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
358 dfss3 3967 . . . . . . . . . . 11 (ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
359357, 358sylibr 233 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}))
360 eqid 2726 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠))
361196adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑠 ∈ ℂ) → 𝑋 ∈ ℂ)
362 simpr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑠 ∈ ℂ) → 𝑠 ∈ ℂ)
363361, 362addcomd 11454 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑠 ∈ ℂ) → (𝑋 + 𝑠) = (𝑠 + 𝑋))
364363mpteq2dva 5243 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)))
365 eqid 2726 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋))
366365addccncf 24922 . . . . . . . . . . . . . . . . . . . 20 (𝑋 ∈ ℂ → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ))
367196, 366syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ))
368364, 367eqeltrd 2826 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ))
369368adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ))
370224rexrd 11302 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻𝑖) ∈ ℝ*)
371 iocssre 13449 . . . . . . . . . . . . . . . . . . 19 (((𝐻𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ) → ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ)
372370, 225, 371syl2anc 582 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ)
373 ax-resscn 11203 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℂ
374372, 373sstrdi 3991 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ)
375289a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → ℂ ⊆ ℂ)
376196ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ)
377374sselda 3978 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
378376, 377addcld 11271 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ)
379360, 369, 374, 375, 378cncfmptssg 45525 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ))
380 eqid 2726 . . . . . . . . . . . . . . . . . 18 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
381 eqid 2726 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) = ((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))))
382380cnfldtop 24785 . . . . . . . . . . . . . . . . . . . 20 (TopOpen‘ℂfld) ∈ Top
383 unicntop 24787 . . . . . . . . . . . . . . . . . . . . 21 ℂ = (TopOpen‘ℂfld)
384383restid 17440 . . . . . . . . . . . . . . . . . . . 20 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
385382, 384ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
386385eqcomi 2735 . . . . . . . . . . . . . . . . . 18 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
387380, 381, 386cncfcn 24915 . . . . . . . . . . . . . . . . 17 ((((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂfld)))
388374, 375, 387syl2anc 582 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂfld)))
389379, 388eleqtrd 2828 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂfld)))
390380cnfldtopon 24784 . . . . . . . . . . . . . . . . . 18 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
391390a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
392 resttopon 23150 . . . . . . . . . . . . . . . . 17 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))))
393391, 374, 392syl2anc 582 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))))
394 cncnp 23269 . . . . . . . . . . . . . . . 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))‘𝑡))))
395393, 391, 394syl2anc 582 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂfld)) ↔ ((𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡))))
396389, 395mpbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡)))
397396simprd 494 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡))
398 ubioc1 13422 . . . . . . . . . . . . . 14 (((𝐻𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐻𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))))
399370, 245, 174, 398syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))))
400 fveq2 6890 . . . . . . . . . . . . . . 15 (𝑡 = (𝐻‘(𝑖 + 1)) → ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡) = ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1))))
401400eleq2d 2812 . . . . . . . . . . . . . 14 (𝑡 = (𝐻‘(𝑖 + 1)) → ((𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡) ↔ (𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1)))))
402401rspccva 3606 . . . . . . . . . . . . 13 ((∀𝑡 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡) ∧ (𝐻‘(𝑖 + 1)) ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) → (𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1))))
403397, 399, 402syl2anc 582 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1))))
404 ioounsn 13499 . . . . . . . . . . . . . 14 (((𝐻𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐻𝑖) < (𝐻‘(𝑖 + 1))) → (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))))
405370, 245, 174, 404syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))))
406259eqcomd 2732 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1))))
407406ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1))))
408 iftrue 4529 . . . . . . . . . . . . . . . 16 (𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1)))
409408adantl 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1)))
410 oveq2 7421 . . . . . . . . . . . . . . . 16 (𝑠 = (𝐻‘(𝑖 + 1)) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1))))
411410adantl 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1))))
412407, 409, 4113eqtr4d 2776 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
413 iffalse 4532 . . . . . . . . . . . . . . . 16 𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
414413adantl 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
415 eqidd 2727 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
416 oveq2 7421 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑠 → (𝑋 + 𝑡) = (𝑋 + 𝑠))
417416adantl 480 . . . . . . . . . . . . . . . 16 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠))
418 velsn 4639 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ 𝑠 = (𝐻‘(𝑖 + 1)))
419418notbii 319 . . . . . . . . . . . . . . . . . . 19 𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ ¬ 𝑠 = (𝐻‘(𝑖 + 1)))
420 elun 4145 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↔ (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}))
421420biimpi 215 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}))
422421orcomd 869 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ∨ 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))))
423422ord 862 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))))
424419, 423biimtrrid 242 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 = (𝐻‘(𝑖 + 1)) → 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))))
425424imp 405 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))))
426425adantll 712 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))))
42795ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑋 ∈ ℝ)
428 elioore 13399 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
429428adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
430 elsni 4640 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 = (𝐻‘(𝑖 + 1)))
431430adantl 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 = (𝐻‘(𝑖 + 1)))
432225adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → (𝐻‘(𝑖 + 1)) ∈ ℝ)
433431, 432eqeltrd 2826 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 ∈ ℝ)
434429, 433jaodan 955 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ)
435420, 434sylan2b 592 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ)
436427, 435readdcld 11281 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → (𝑋 + 𝑠) ∈ ℝ)
437436adantr 479 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) ∈ ℝ)
438415, 417, 426, 437fvmptd 7005 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠))
439414, 438eqtrd 2766 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
440412, 439pm2.61dan 811 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
441405, 440mpteq12dva 5232 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)))
442405oveq2d 7429 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))))
443442oveq1d 7428 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld)))
444443fveq1d 6892 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1))) = ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)(,](𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1))))
445403, 441, 4443eltr4d 2841 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1))))
446 eqid 2726 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) = ((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}))
447 eqid 2726 . . . . . . . . . . . 12 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))
448264, 301fssd 6734 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))⟶ℂ)
449225recnd 11280 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℂ)
450446, 380, 447, 448, 299, 449ellimc 25887 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) ∈ ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim (𝐻‘(𝑖 + 1))) ↔ (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP (TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1)))))
451445, 450mpbird 256 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim (𝐻‘(𝑖 + 1))))
452359, 451, 66limccog 45274 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim (𝐻‘(𝑖 + 1))))
453266, 286eqtrd 2766 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))))
454453oveq1d 7428 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim (𝐻‘(𝑖 + 1))) = ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim (𝐻‘(𝑖 + 1))))
455452, 454eleqtrd 2828 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim (𝐻‘(𝑖 + 1))))
45640adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄𝑖) ∈ ℝ)
457456, 334gtned 11387 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄𝑖))
458457neneqd 2935 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄𝑖))
459 velsn 4639 . . . . . . . . . . . . . 14 (𝑟 ∈ {(𝑄𝑖)} ↔ 𝑟 = (𝑄𝑖))
460458, 459sylnibr 328 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄𝑖)})
461351, 460eldifd 3957 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄𝑖)}))
462461ralrimiva 3136 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄𝑖)}))
463 dfss3 3967 . . . . . . . . . . 11 (ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄𝑖)}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄𝑖)}))
464462, 463sylibr 233 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄𝑖)}))
465 icossre 13450 . . . . . . . . . . . . . . . . . . 19 (((𝐻𝑖) ∈ ℝ ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ*) → ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ)
466224, 245, 465syl2anc 582 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ)
467466, 373sstrdi 3991 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ)
468196ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ)
469467sselda 3978 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
470468, 469addcld 11271 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ)
471360, 369, 467, 375, 470cncfmptssg 45525 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ))
472 eqid 2726 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) = ((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))))
473380, 472, 386cncfcn 24915 . . . . . . . . . . . . . . . . 17 ((((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂfld)))
474467, 375, 473syl2anc 582 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂfld)))
475471, 474eleqtrd 2828 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂfld)))
476 resttopon 23150 . . . . . . . . . . . . . . . . 17 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))))
477391, 467, 476syl2anc 582 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))))
478 cncnp 23269 . . . . . . . . . . . . . . . 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))‘𝑡))))
479477, 391, 478syl2anc 582 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn (TopOpen‘ℂfld)) ↔ ((𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡))))
480475, 479mpbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡)))
481480simprd 494 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡))
482 lbico1 13423 . . . . . . . . . . . . . 14 (((𝐻𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐻𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻𝑖) ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))))
483370, 245, 174, 482syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻𝑖) ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))))
484 fveq2 6890 . . . . . . . . . . . . . . 15 (𝑡 = (𝐻𝑖) → ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡) = ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘(𝐻𝑖)))
485484eleq2d 2812 . . . . . . . . . . . . . 14 (𝑡 = (𝐻𝑖) → ((𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡) ↔ (𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘(𝐻𝑖))))
486485rspccva 3606 . . . . . . . . . . . . 13 ((∀𝑡 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘𝑡) ∧ (𝐻𝑖) ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘(𝐻𝑖)))
487481, 483, 486syl2anc 582 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘(𝐻𝑖)))
488 uncom 4150 . . . . . . . . . . . . . 14 (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) = ({(𝐻𝑖)} ∪ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))))
489 snunioo 13500 . . . . . . . . . . . . . . 15 (((𝐻𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ* ∧ (𝐻𝑖) < (𝐻‘(𝑖 + 1))) → ({(𝐻𝑖)} ∪ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))))
490370, 245, 174, 489syl3anc 1368 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ({(𝐻𝑖)} ∪ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))))
491488, 490eqtrid 2778 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) = ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))))
492 iftrue 4529 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐻𝑖) → if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄𝑖))
493492adantl 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻𝑖)) → if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄𝑖))
494240adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻𝑖)) → (𝑄𝑖) = (𝑋 + (𝐻𝑖)))
495 oveq2 7421 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝐻𝑖) → (𝑋 + 𝑠) = (𝑋 + (𝐻𝑖)))
496495eqcomd 2732 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐻𝑖) → (𝑋 + (𝐻𝑖)) = (𝑋 + 𝑠))
497496adantl 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻𝑖)) → (𝑋 + (𝐻𝑖)) = (𝑋 + 𝑠))
498493, 494, 4973eqtrd 2770 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻𝑖)) → if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
499498adantlr 713 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) ∧ 𝑠 = (𝐻𝑖)) → if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
500 iffalse 4532 . . . . . . . . . . . . . . . 16 𝑠 = (𝐻𝑖) → if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
501500adantl 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) ∧ ¬ 𝑠 = (𝐻𝑖)) → if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))
502 eqidd 2727 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) ∧ ¬ 𝑠 = (𝐻𝑖)) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))
503416adantl 480 . . . . . . . . . . . . . . . 16 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) ∧ ¬ 𝑠 = (𝐻𝑖)) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠))
504 velsn 4639 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ {(𝐻𝑖)} ↔ 𝑠 = (𝐻𝑖))
505504notbii 319 . . . . . . . . . . . . . . . . . . 19 𝑠 ∈ {(𝐻𝑖)} ↔ ¬ 𝑠 = (𝐻𝑖))
506 elun 4145 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) ↔ (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻𝑖)}))
507506biimpi 215 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) → (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻𝑖)}))
508507orcomd 869 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) → (𝑠 ∈ {(𝐻𝑖)} ∨ 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))))
509508ord 862 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) → (¬ 𝑠 ∈ {(𝐻𝑖)} → 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))))
510505, 509biimtrrid 242 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) → (¬ 𝑠 = (𝐻𝑖) → 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1)))))
511510imp 405 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) ∧ ¬ 𝑠 = (𝐻𝑖)) → 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))))
512511adantll 712 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) ∧ ¬ 𝑠 = (𝐻𝑖)) → 𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))))
51395ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) → 𝑋 ∈ ℝ)
514 elsni 4640 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ {(𝐻𝑖)} → 𝑠 = (𝐻𝑖))
515514adantl 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻𝑖)}) → 𝑠 = (𝐻𝑖))
516224adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻𝑖)}) → (𝐻𝑖) ∈ ℝ)
517515, 516eqeltrd 2826 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻𝑖)}) → 𝑠 ∈ ℝ)
518429, 517jaodan 955 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻𝑖)})) → 𝑠 ∈ ℝ)
519506, 518sylan2b 592 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) → 𝑠 ∈ ℝ)
520513, 519readdcld 11281 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) → (𝑋 + 𝑠) ∈ ℝ)
521520adantr 479 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) ∧ ¬ 𝑠 = (𝐻𝑖)) → (𝑋 + 𝑠) ∈ ℝ)
522502, 503, 512, 521fvmptd 7005 . . . . . . . . . . . . . . 15 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) ∧ ¬ 𝑠 = (𝐻𝑖)) → ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠))
523501, 522eqtrd 2766 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) ∧ ¬ 𝑠 = (𝐻𝑖)) → if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
524499, 523pm2.61dan 811 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) → if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠))
525491, 524mpteq12dva 5232 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) ↦ if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)))
526491oveq2d 7429 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) = ((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))))
527526oveq1d 7428 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld)))
528527fveq1d 6892 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) CnP (TopOpen‘ℂfld))‘(𝐻𝑖)) = ((((TopOpen‘ℂfld) ↾t ((𝐻𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP (TopOpen‘ℂfld))‘(𝐻𝑖)))
529487, 525, 5283eltr4d 2841 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) ↦ if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) CnP (TopOpen‘ℂfld))‘(𝐻𝑖)))
530 eqid 2726 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) = ((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}))
531 eqid 2726 . . . . . . . . . . . 12 (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) ↦ if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) ↦ if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))
532224recnd 11280 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻𝑖) ∈ ℂ)
533530, 380, 531, 448, 299, 532ellimc 25887 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) ∈ ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim (𝐻𝑖)) ↔ (𝑠 ∈ (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)}) ↦ if(𝑠 = (𝐻𝑖), (𝑄𝑖), ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈ ((((TopOpen‘ℂfld) ↾t (((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻𝑖)})) CnP (TopOpen‘ℂfld))‘(𝐻𝑖))))
534529, 533mpbird 256 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) lim (𝐻𝑖)))
535464, 534, 69limccog 45274 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim (𝐻𝑖)))
536453oveq1d 7428 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) lim (𝐻𝑖)) = ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim (𝐻𝑖)))
537535, 536eleqtrd 2828 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) lim (𝐻𝑖)))
538224, 225, 304, 455, 537iblcncfioo 45632 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ 𝐿1)
53930ad2antrr 724 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ)
54049a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → -π ∈ ℝ*)
54151a1i 11 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → π ∈ ℝ*)
54221ad2antrr 724 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π))
543 simplr 767 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
544 simpr 483 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1))))
545163, 173oveq12d 7431 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐻𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
546545adantr 479 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → ((𝐻𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
547544, 546eleqtrd 2828 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ (((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)))
548547, 116syldan 589 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
549540, 541, 542, 543, 548fourierdlem1 45762 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ (-π[,]π))
550539, 549ffvelcdmd 7088 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ)
551224, 225, 538, 550ibliooicc 45625 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻𝑖)[,](𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ 𝐿1)
55214, 20, 159, 174, 223, 551itgspltprt 45633 . . . . 5 (𝜑 → ∫((𝐻‘0)[,](𝐻𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡)
553545itgeq1d 45611 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ∫((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
554553sumeq2dv 15699 . . . . 5 (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝐻𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
555552, 554eqtrd 2766 . . . 4 (𝜑 → ∫((𝐻‘0)[,](𝐻𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
556125, 155, 5553eqtrd 2770 . . 3 (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡)
557121, 556eqtr4d 2769 . 2 (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)
55813, 76, 5573eqtrd 2770 1 (𝜑 → ∫(-π[,]π)(𝐹𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845  w3a 1084   = wceq 1534  wcel 2099  wral 3051  wrex 3060  {crab 3419  Vcvv 3462  cdif 3943  cun 3944  cin 3945  wss 3946  ifcif 4523  {csn 4623   class class class wbr 5143  cmpt 5226  dom cdm 5672  ran crn 5673  cres 5674  ccom 5676  Fun wfun 6537  wf 6539  cfv 6543  (class class class)co 7413  m cmap 8844  cc 11144  cr 11145  0cc0 11146  1c1 11147   + caddc 11149  *cxr 11285   < clt 11286  cle 11287  cmin 11482  -cneg 11483  cn 12255  cuz 12865  (,)cioo 13369  (,]cioc 13370  [,)cico 13371  [,]cicc 13372  ...cfz 13529  ..^cfzo 13672  Σcsu 15682  πcpi 16060  t crest 17427  TopOpenctopn 17428  fldccnfld 21336  Topctop 22880  TopOnctopon 22897   Cn ccn 23213   CnP ccnp 23214  cnccncf 24881  citg 25632   lim climc 25876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7735  ax-inf2 9674  ax-cc 10466  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224  ax-addf 11225
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-symdif 4241  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6302  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-ofr 7680  df-om 7866  df-1st 7992  df-2nd 7993  df-supp 8164  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-2o 8486  df-oadd 8489  df-omul 8490  df-er 8723  df-map 8846  df-pm 8847  df-ixp 8916  df-en 8964  df-dom 8965  df-sdom 8966  df-fin 8967  df-fsupp 9396  df-fi 9444  df-sup 9475  df-inf 9476  df-oi 9543  df-dju 9934  df-card 9972  df-acn 9975  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12256  df-2 12318  df-3 12319  df-4 12320  df-5 12321  df-6 12322  df-7 12323  df-8 12324  df-9 12325  df-n0 12516  df-z 12602  df-dec 12721  df-uz 12866  df-q 12976  df-rp 13020  df-xneg 13137  df-xadd 13138  df-xmul 13139  df-ioo 13373  df-ioc 13374  df-ico 13375  df-icc 13376  df-fz 13530  df-fzo 13673  df-fl 13803  df-mod 13881  df-seq 14013  df-exp 14073  df-fac 14283  df-bc 14312  df-hash 14340  df-shft 15064  df-cj 15096  df-re 15097  df-im 15098  df-sqrt 15232  df-abs 15233  df-limsup 15465  df-clim 15482  df-rlim 15483  df-sum 15683  df-ef 16061  df-sin 16063  df-cos 16064  df-pi 16066  df-struct 17141  df-sets 17158  df-slot 17176  df-ndx 17188  df-base 17206  df-ress 17235  df-plusg 17271  df-mulr 17272  df-starv 17273  df-sca 17274  df-vsca 17275  df-ip 17276  df-tset 17277  df-ple 17278  df-ds 17280  df-unif 17281  df-hom 17282  df-cco 17283  df-rest 17429  df-topn 17430  df-0g 17448  df-gsum 17449  df-topgen 17450  df-pt 17451  df-prds 17454  df-xrs 17509  df-qtop 17514  df-imas 17515  df-xps 17517  df-mre 17591  df-mrc 17592  df-acs 17594  df-mgm 18625  df-sgrp 18704  df-mnd 18720  df-submnd 18766  df-mulg 19055  df-cntz 19304  df-cmn 19773  df-psmet 21328  df-xmet 21329  df-met 21330  df-bl 21331  df-mopn 21332  df-fbas 21333  df-fg 21334  df-cnfld 21337  df-top 22881  df-topon 22898  df-topsp 22920  df-bases 22934  df-cld 23008  df-ntr 23009  df-cls 23010  df-nei 23087  df-lp 23125  df-perf 23126  df-cn 23216  df-cnp 23217  df-haus 23304  df-cmp 23376  df-tx 23551  df-hmeo 23744  df-fil 23835  df-fm 23927  df-flim 23928  df-flf 23929  df-xms 24311  df-ms 24312  df-tms 24313  df-cncf 24883  df-ovol 25478  df-vol 25479  df-mbf 25633  df-itg1 25634  df-itg2 25635  df-ibl 25636  df-itg 25637  df-0p 25684  df-ditg 25861  df-limc 25880  df-dv 25881
This theorem is referenced by:  fourierdlem101  45861
  Copyright terms: Public domain W3C validator