Metamath Proof Explorer

Theorem fourierdlem101

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

Ref Expression
Hypotheses fourierdlem101.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
fourierdlem101.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem101.g ⊢ 𝐺 = ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
fourierdlem101.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem101.6 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem101.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
fourierdlem101.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem101.f ⊢ ( 𝜑 → 𝐹 : ( - π [,] π ) ⟶ ℂ )
fourierdlem101.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem101.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
fourierdlem101.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
Assertion fourierdlem101 ( 𝜑 → ∫ ( - π [,] π ) ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) d 𝑠 )

Proof

Step Hyp Ref Expression
1 fourierdlem101.d ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
2 fourierdlem101.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
3 fourierdlem101.g ⊢ 𝐺 = ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
4 fourierdlem101.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5 fourierdlem101.6 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
6 fourierdlem101.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 fourierdlem101.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
8 fourierdlem101.f ⊢ ( 𝜑 → 𝐹 : ( - π [,] π ) ⟶ ℂ )
9 fourierdlem101.fcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
10 fourierdlem101.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
11 fourierdlem101.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → 𝑡 ∈ ( - π [,] π ) )
13 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
14 6 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → 𝑁 ∈ ℕ )
15 pire ⊢ π ∈ ℝ
16 15 renegcli ⊢ - π ∈ ℝ
17 eliccre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑡 ∈ ( - π [,] π ) ) → 𝑡 ∈ ℝ )
18 16 15 17 mp3an12 ⊢ ( 𝑡 ∈ ( - π [,] π ) → 𝑡 ∈ ℝ )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → 𝑡 ∈ ℝ )
20 7 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → 𝑋 ∈ ℝ )
21 19 20 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
22 1 dirkerre ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑡 − 𝑋 ) ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
23 14 21 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
24 23 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℂ )
25 13 24 mulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ℂ )
26 3 fvmpt2 ⊢ ( ( 𝑡 ∈ ( - π [,] π ) ∧ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ℂ ) → ( 𝐺 ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
27 12 25 26 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( 𝐺 ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
28 27 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( 𝐺 ‘ 𝑡 ) )
29 28 itgeq2dv ⊢ ( 𝜑 → ∫ ( - π [,] π ) ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) d 𝑡 = ∫ ( - π [,] π ) ( 𝐺 ‘ 𝑡 ) d 𝑡 )
30 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) )
31 30 oveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑄 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) )
32 31 cbvmptv ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) − 𝑋 ) ) = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) )
33 25 3 fmptd ⊢ ( 𝜑 → 𝐺 : ( - π [,] π ) ⟶ ℂ )
34 3 reseq1i ⊢ ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
35 ioossicc ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
36 16 a1i ⊢ ( 𝜑 → - π ∈ ℝ )
37 36 rexrd ⊢ ( 𝜑 → - π ∈ ℝ* )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → - π ∈ ℝ* )
39 15 a1i ⊢ ( 𝜑 → π ∈ ℝ )
40 39 rexrd ⊢ ( 𝜑 → π ∈ ℝ* )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → π ∈ ℝ* )
42 2 5 4 fourierdlem15 ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
44 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
45 38 41 43 44 fourierdlem8 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
46 35 45 sstrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
47 46 resmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) )
48 34 47 eqtrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) )
49 8 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : ( - π [,] π ) ⟶ ℂ )
50 49 46 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ 𝑡 ) ) )
51 50 9 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
52 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
53 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) → 𝑠 = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) )
54 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) )
55 oveq1 ⊢ ( 𝑡 = 𝑟 → ( 𝑡 − 𝑋 ) = ( 𝑟 − 𝑋 ) )
56 55 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑡 = 𝑟 ) → ( 𝑡 − 𝑋 ) = ( 𝑟 − 𝑋 ) )
57 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
58 elioore ⊢ ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑟 ∈ ℝ )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑟 ∈ ℝ )
60 7 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
61 59 60 resubcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑟 − 𝑋 ) ∈ ℝ )
62 61 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑟 − 𝑋 ) ∈ ℝ )
63 54 56 57 62 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) = ( 𝑟 − 𝑋 ) )
64 63 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) = ( 𝑟 − 𝑋 ) )
65 53 64 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) → 𝑠 = ( 𝑟 − 𝑋 ) )
66 65 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) )
67 elioore ⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑡 ∈ ℝ )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ℝ )
69 7 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
70 68 69 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
71 70 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
72 eqid ⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) )
73 71 72 fmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
74 73 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ∈ ℝ )
75 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑁 ∈ ℕ )
76 1 dirkerre ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑟 − 𝑋 ) ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) ∈ ℝ )
77 75 62 76 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) ∈ ℝ )
78 52 66 74 77 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ‘ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) )
79 78 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) = ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ‘ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) )
80 79 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) ) = ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ‘ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) ) )
81 55 fveq2d ⊢ ( 𝑡 = 𝑟 → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) )
82 81 cbvmptv ⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) )
83 82 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) ) )
84 1 dirkerre ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ∈ ℝ )
85 6 84 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ∈ ℝ )
86 eqid ⊢ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) )
87 85 86 fmptd ⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℝ )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℝ )
89 fcompt ⊢ ( ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℝ ∧ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ ) → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∘ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ) = ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ‘ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) ) )
90 88 73 89 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∘ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ) = ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ‘ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) ) )
91 80 83 90 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∘ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ) )
92 eqid ⊢ ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) = ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) )
93 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → 𝑡 ∈ ℂ )
94 7 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
95 94 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → 𝑋 ∈ ℂ )
96 93 95 negsubd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑡 + - 𝑋 ) = ( 𝑡 − 𝑋 ) )
97 96 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑡 − 𝑋 ) = ( 𝑡 + - 𝑋 ) )
98 97 mpteq2dva ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) = ( 𝑡 ∈ ℂ ↦ ( 𝑡 + - 𝑋 ) ) )
99 94 negcld ⊢ ( 𝜑 → - 𝑋 ∈ ℂ )
100 eqid ⊢ ( 𝑡 ∈ ℂ ↦ ( 𝑡 + - 𝑋 ) ) = ( 𝑡 ∈ ℂ ↦ ( 𝑡 + - 𝑋 ) )
101 100 addccncf ⊢ ( - 𝑋 ∈ ℂ → ( 𝑡 ∈ ℂ ↦ ( 𝑡 + - 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
102 99 101 syl ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 + - 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
103 98 102 eqeltrd ⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
104 103 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
105 ioossre ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
106 ax-resscn ⊢ ℝ ⊆ ℂ
107 105 106 sstri ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
108 107 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
109 106 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℝ ⊆ ℂ )
110 92 104 108 109 71 cncfmptssg ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℝ ) )
111 85 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ∈ ℂ )
112 111 86 fmptd ⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℂ )
113 ssid ⊢ ℂ ⊆ ℂ
114 1 dirkerf ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
115 6 114 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
116 115 feqmptd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
117 1 dirkercncf ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℝ ) )
118 6 117 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℝ ) )
119 116 118 eqeltrrd ⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℝ ) )
120 cncffvrn ⊢ ( ( ℂ ⊆ ℂ ∧ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℝ ) ) → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℂ ) ↔ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℂ ) )
121 113 119 120 sylancr ⊢ ( 𝜑 → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℂ ) ↔ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℂ ) )
122 112 121 mpbird ⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℂ ) )
123 122 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℂ ) )
124 110 123 cncfco ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∘ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
125 91 124 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
126 51 125 mulcncf ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
127 48 126 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
128 cncff ⊢ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
129 9 128 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
130 115 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
131 elioore ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ )
132 131 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
133 7 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
134 132 133 resubcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 − 𝑋 ) ∈ ℝ )
135 130 134 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ∈ ℝ )
136 135 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ∈ ℂ )
137 eqid ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) )
138 136 137 fmptd ⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
139 138 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
140 eqid ⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
141 oveq1 ⊢ ( 𝑡 = ( 𝑄 ‘ 𝑖 ) → ( 𝑡 − 𝑋 ) = ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) )
142 141 fveq2d ⊢ ( 𝑡 = ( 𝑄 ‘ 𝑖 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) )
143 142 eqcomd ⊢ ( 𝑡 = ( 𝑄 ‘ 𝑖 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
144 143 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
145 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) )
146 oveq1 ⊢ ( 𝑠 = 𝑡 → ( 𝑠 − 𝑋 ) = ( 𝑡 − 𝑋 ) )
147 146 fveq2d ⊢ ( 𝑠 = 𝑡 → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
148 147 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) ∧ 𝑠 = 𝑡 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
149 velsn ⊢ ( 𝑡 ∈ { ( 𝑄 ‘ 𝑖 ) } ↔ 𝑡 = ( 𝑄 ‘ 𝑖 ) )
150 149 notbii ⊢ ( ¬ 𝑡 ∈ { ( 𝑄 ‘ 𝑖 ) } ↔ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) )
151 elunnel2 ⊢ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ∧ ¬ 𝑡 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
152 150 151 sylan2br ⊢ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
153 152 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
154 115 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
155 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 = ( 𝑄 ‘ 𝑖 ) )
156 18 ssriv ⊢ ( - π [,] π ) ⊆ ℝ
157 fzossfz ⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
158 157 44 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
159 43 158 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( - π [,] π ) )
160 156 159 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
161 160 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
162 155 161 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 ∈ ℝ )
163 162 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 ∈ ℝ )
164 153 67 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 ∈ ℝ )
165 163 164 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑡 ∈ ℝ )
166 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑋 ∈ ℝ )
167 165 166 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
168 154 167 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
169 168 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
170 145 148 153 169 fvmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
171 144 170 ifeqda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
172 171 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
173 115 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
174 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
175 elun ⊢ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↔ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
176 174 175 sylib ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
177 176 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
178 elsni ⊢ ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 = ( 𝑄 ‘ 𝑖 ) )
179 178 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 = ( 𝑄 ‘ 𝑖 ) )
180 160 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
181 179 180 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 ∈ ℝ )
182 181 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 ∈ ℝ ) )
183 182 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 ∈ ℝ ) )
184 pm3.44 ⊢ ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ ) ∧ ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 ∈ ℝ ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 ∈ ℝ ) )
185 131 183 184 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 ∈ ℝ ) )
186 177 185 mpd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑠 ∈ ℝ )
187 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑋 ∈ ℝ )
188 186 187 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 − 𝑋 ) ∈ ℝ )
189 eqid ⊢ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) )
190 188 189 fmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℝ )
191 fcompt ⊢ ( ( ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ ∧ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) ) )
192 173 190 191 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) ) )
193 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) )
194 146 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ 𝑠 = 𝑡 ) → ( 𝑠 − 𝑋 ) = ( 𝑡 − 𝑋 ) )
195 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
196 193 194 195 167 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) = ( 𝑡 − 𝑋 ) )
197 196 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
198 197 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
199 192 198 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) )
200 eqid ⊢ ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) )
201 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → 𝑠 ∈ ℂ )
202 94 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → 𝑋 ∈ ℂ )
203 201 202 negsubd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → ( 𝑠 + - 𝑋 ) = ( 𝑠 − 𝑋 ) )
204 203 eqcomd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → ( 𝑠 − 𝑋 ) = ( 𝑠 + - 𝑋 ) )
205 204 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) )
206 eqid ⊢ ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) )
207 206 addccncf ⊢ ( - 𝑋 ∈ ℂ → ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
208 99 207 syl ⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
209 205 208 eqeltrd ⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
210 209 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
211 160 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
212 211 snssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { ( 𝑄 ‘ 𝑖 ) } ⊆ ℂ )
213 108 212 unssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⊆ ℂ )
214 200 210 213 109 188 cncfmptssg ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ∈ ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℝ ) )
215 116 122 eqeltrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℂ ) )
216 215 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℂ ) )
217 214 216 cncfco ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) ∈ ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℂ ) )
218 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
219 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
220 218 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
221 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
222 221 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
223 220 222 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
224 223 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
225 218 219 224 cncfcn ⊢ ( ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
226 213 113 225 sylancl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
227 217 226 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
228 199 227 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
229 218 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
230 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) )
231 229 213 230 sylancr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) )
232 cncnp ⊢ ( ( ( ( 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 ) ) ‘ 𝑠 ) ) ) )
233 231 229 232 sylancl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) ) )
234 228 233 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) )
235 234 simprd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
236 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) )
237 elsng ⊢ ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ → ( ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ↔ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) ) )
238 160 237 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ↔ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) ) )
239 236 238 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } )
240 239 olcd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
241 elun ⊢ ( ( 𝑄 ‘ 𝑖 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↔ ( ( 𝑄 ‘ 𝑖 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
242 240 241 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
243 fveq2 ⊢ ( 𝑠 = ( 𝑄 ‘ 𝑖 ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
244 243 eleq2d ⊢ ( 𝑠 = ( 𝑄 ‘ 𝑖 ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) ) )
245 244 rspccva ⊢ ( ( ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ∧ ( 𝑄 ‘ 𝑖 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
246 235 242 245 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
247 172 246 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
248 eqid ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
249 219 218 248 139 108 211 ellimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) ) )
250 247 249 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
251 129 139 140 10 250 mullimcf ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
252 fvres ⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
253 252 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
254 253 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
255 254 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) )
256 255 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
257 251 256 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
258 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) )
259 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 𝑡 ) → 𝑠 = 𝑡 )
260 259 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 𝑡 ) → ( 𝑠 − 𝑋 ) = ( 𝑡 − 𝑋 ) )
261 260 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 𝑡 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
262 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
263 115 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
264 263 71 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
265 258 261 262 264 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
266 265 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
267 266 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) )
268 267 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
269 257 268 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
270 48 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
271 270 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
272 269 271 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
273 iftrue ⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
274 oveq1 ⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( 𝑡 − 𝑋 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
275 274 eqcomd ⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) = ( 𝑡 − 𝑋 ) )
276 275 fveq2d ⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
277 273 276 eqtrd ⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
278 277 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
279 iffalse ⊢ ( ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) )
280 279 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) )
281 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) )
282 147 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 = 𝑡 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
283 elun ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
284 283 biimpi ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
285 284 orcomd ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ∨ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
286 285 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ∨ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
287 velsn ⊢ ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
288 287 notbii ⊢ ( ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
289 288 biimpri ⊢ ( ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } )
290 289 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } )
291 pm2.53 ⊢ ( ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ∨ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
292 286 290 291 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
293 173 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
294 292 67 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑡 ∈ ℝ )
295 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑋 ∈ ℝ )
296 294 295 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
297 293 296 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
298 281 282 292 297 fvmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
299 280 298 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
300 278 299 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
301 300 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
302 eqid ⊢ ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
303 106 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
304 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
305 7 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑋 ∈ ℝ )
306 304 305 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
307 92 103 303 303 306 cncfmptssg ⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ℝ –cn→ ℝ ) )
308 307 215 cncfcompt ⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ℝ –cn→ ℂ ) )
309 308 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ℝ –cn→ ℂ ) )
310 105 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
311 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
312 311 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
313 43 312 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( - π [,] π ) )
314 156 313 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
315 314 snssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ⊆ ℝ )
316 310 315 unssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℝ )
317 113 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℂ ⊆ ℂ )
318 173 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
319 316 sselda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑡 ∈ ℝ )
320 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑋 ∈ ℝ )
321 319 320 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
322 318 321 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
323 322 recnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℂ )
324 302 309 316 317 323 cncfmptssg ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) –cn→ ℂ ) )
325 156 106 sstri ⊢ ( - π [,] π ) ⊆ ℂ
326 325 313 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
327 326 snssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ⊆ ℂ )
328 108 327 unssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℂ )
329 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
330 218 329 224 cncfcn ⊢ ( ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
331 328 113 330 sylancl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
332 324 331 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
333 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) )
334 229 328 333 sylancr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) )
335 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) ) )
336 334 229 335 sylancl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) ) )
337 332 336 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) )
338 337 simprd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
339 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
340 elsng ⊢ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
341 314 340 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
342 339 341 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } )
343 342 olcd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
344 elun ⊢ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
345 343 344 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
346 fveq2 ⊢ ( 𝑠 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
347 346 eleq2d ⊢ ( 𝑠 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
348 347 rspccva ⊢ ( ( ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
349 338 345 348 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
350 301 349 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
351 eqid ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
352 329 218 351 139 108 326 ellimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
353 350 352 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
354 129 139 140 11 353 mullimcf ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐿 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
355 267 255 48 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
356 355 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
357 354 356 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐿 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) ∈ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
358 2 32 5 4 7 33 127 272 357 fourierdlem93 ⊢ ( 𝜑 → ∫ ( - π [,] π ) ( 𝐺 ‘ 𝑡 ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐺 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 )
359 3 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝐺 = ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) )
360 fveq2 ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
361 360 oveq1d ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
362 361 adantl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
363 oveq1 ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( 𝑡 − 𝑋 ) = ( ( 𝑋 + 𝑠 ) − 𝑋 ) )
364 94 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑋 ∈ ℂ )
365 36 7 resubcld ⊢ ( 𝜑 → ( - π − 𝑋 ) ∈ ℝ )
366 365 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( - π − 𝑋 ) ∈ ℝ )
367 39 7 resubcld ⊢ ( 𝜑 → ( π − 𝑋 ) ∈ ℝ )
368 367 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( π − 𝑋 ) ∈ ℝ )
369 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) )
370 eliccre ⊢ ( ( ( - π − 𝑋 ) ∈ ℝ ∧ ( π − 𝑋 ) ∈ ℝ ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ℝ )
371 366 368 369 370 syl3anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ℝ )
372 371 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ℂ )
373 364 372 pncan2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( ( 𝑋 + 𝑠 ) − 𝑋 ) = 𝑠 )
374 363 373 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( 𝑡 − 𝑋 ) = 𝑠 )
375 374 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) )
376 375 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
377 362 376 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
378 16 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → - π ∈ ℝ )
379 15 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → π ∈ ℝ )
380 7 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑋 ∈ ℝ )
381 380 371 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
382 36 recnd ⊢ ( 𝜑 → - π ∈ ℂ )
383 94 382 pncan3d ⊢ ( 𝜑 → ( 𝑋 + ( - π − 𝑋 ) ) = - π )
384 383 eqcomd ⊢ ( 𝜑 → - π = ( 𝑋 + ( - π − 𝑋 ) ) )
385 384 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → - π = ( 𝑋 + ( - π − 𝑋 ) ) )
386 elicc2 ⊢ ( ( ( - π − 𝑋 ) ∈ ℝ ∧ ( π − 𝑋 ) ∈ ℝ ) → ( 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ↔ ( 𝑠 ∈ ℝ ∧ ( - π − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( π − 𝑋 ) ) ) )
387 366 368 386 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ↔ ( 𝑠 ∈ ℝ ∧ ( - π − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( π − 𝑋 ) ) ) )
388 369 387 mpbid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑠 ∈ ℝ ∧ ( - π − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( π − 𝑋 ) ) )
389 388 simp2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( - π − 𝑋 ) ≤ 𝑠 )
390 366 371 380 389 leadd2dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + ( - π − 𝑋 ) ) ≤ ( 𝑋 + 𝑠 ) )
391 385 390 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → - π ≤ ( 𝑋 + 𝑠 ) )
392 388 simp3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ≤ ( π − 𝑋 ) )
393 371 368 380 392 leadd2dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ≤ ( 𝑋 + ( π − 𝑋 ) ) )
394 picn ⊢ π ∈ ℂ
395 394 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → π ∈ ℂ )
396 364 395 pncan3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + ( π − 𝑋 ) ) = π )
397 393 396 breqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ≤ π )
398 378 379 381 391 397 eliccd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( - π [,] π ) )
399 8 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝐹 : ( - π [,] π ) ⟶ ℂ )
400 399 398 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
401 371 111 syldan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ∈ ℂ )
402 400 401 mulcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ℂ )
403 359 377 398 402 fvmptd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝐺 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
404 403 itgeq2dv ⊢ ( 𝜑 → ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐺 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) d 𝑠 )
405 29 358 404 3eqtrd ⊢ ( 𝜑 → ∫ ( - π [,] π ) ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) d 𝑠 )