This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 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 cncfcdm ⊢ ( ( ℂ ⊆ ℂ ∧ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 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 elun ⊢ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↔ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
175 174 bilani ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
176 elsni ⊢ ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 = ( 𝑄 ‘ 𝑖 ) )
177 176 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 = ( 𝑄 ‘ 𝑖 ) )
178 160 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
179 177 178 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 ∈ ℝ )
180 179 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 ∈ ℝ ) )
181 180 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 ∈ ℝ ) )
182 pm3.44 ⊢ ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ ) ∧ ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 ∈ ℝ ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 ∈ ℝ ) )
183 131 181 182 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 ∈ ℝ ) )
184 175 183 mpd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑠 ∈ ℝ )
185 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑋 ∈ ℝ )
186 184 185 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 − 𝑋 ) ∈ ℝ )
187 eqid ⊢ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) )
188 186 187 fmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℝ )
189 fcompt ⊢ ( ( ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ ∧ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) ) )
190 173 188 189 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) ) )
191 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) )
192 146 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ 𝑠 = 𝑡 ) → ( 𝑠 − 𝑋 ) = ( 𝑡 − 𝑋 ) )
193 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
194 191 192 193 167 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) = ( 𝑡 − 𝑋 ) )
195 194 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
196 195 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
197 190 196 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) )
198 eqid ⊢ ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) )
199 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → 𝑠 ∈ ℂ )
200 94 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → 𝑋 ∈ ℂ )
201 199 200 negsubd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → ( 𝑠 + - 𝑋 ) = ( 𝑠 − 𝑋 ) )
202 201 eqcomd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → ( 𝑠 − 𝑋 ) = ( 𝑠 + - 𝑋 ) )
203 202 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) )
204 eqid ⊢ ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) )
205 204 addccncf ⊢ ( - 𝑋 ∈ ℂ → ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
206 99 205 syl ⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
207 203 206 eqeltrd ⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
208 207 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
209 160 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
210 209 snssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { ( 𝑄 ‘ 𝑖 ) } ⊆ ℂ )
211 108 210 unssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⊆ ℂ )
212 198 208 211 109 186 cncfmptssg ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ∈ ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℝ ) )
213 116 122 eqeltrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℂ ) )
214 213 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℂ ) )
215 212 214 cncfco ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) ∈ ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℂ ) )
216 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
217 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
218 216 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
219 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
220 219 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
221 218 220 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
222 221 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
223 216 217 222 cncfcn ⊢ ( ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
224 211 113 223 sylancl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
225 215 224 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
226 197 225 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
227 216 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
228 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) )
229 227 211 228 sylancr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) )
230 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 ) ) ‘ 𝑠 ) ) ) )
231 229 227 230 sylancl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) ) )
232 226 231 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) )
233 232 simprd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
234 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) )
235 elsng ⊢ ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ → ( ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ↔ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) ) )
236 160 235 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ↔ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) ) )
237 234 236 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } )
238 237 olcd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
239 elun ⊢ ( ( 𝑄 ‘ 𝑖 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↔ ( ( 𝑄 ‘ 𝑖 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
240 238 239 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
241 fveq2 ⊢ ( 𝑠 = ( 𝑄 ‘ 𝑖 ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
242 241 eleq2d ⊢ ( 𝑠 = ( 𝑄 ‘ 𝑖 ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) ) )
243 242 rspccva ⊢ ( ( ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ∧ ( 𝑄 ‘ 𝑖 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
244 233 240 243 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
245 172 244 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
246 eqid ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
247 217 216 246 139 108 209 ellimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) ) )
248 245 247 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
249 129 139 140 10 248 mullimcf ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
250 fvres ⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
251 250 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
252 251 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
253 252 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) )
254 253 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
255 249 254 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
256 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) )
257 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 𝑡 ) → 𝑠 = 𝑡 )
258 257 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 𝑡 ) → ( 𝑠 − 𝑋 ) = ( 𝑡 − 𝑋 ) )
259 258 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 𝑡 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
260 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
261 115 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
262 261 71 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
263 256 259 260 262 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
264 263 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
265 264 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) )
266 265 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
267 255 266 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
268 48 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
269 268 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
270 267 269 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
271 iftrue ⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
272 oveq1 ⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( 𝑡 − 𝑋 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
273 272 eqcomd ⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) = ( 𝑡 − 𝑋 ) )
274 273 fveq2d ⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
275 271 274 eqtrd ⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
276 275 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
277 iffalse ⊢ ( ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) )
278 277 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) )
279 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) )
280 147 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 = 𝑡 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
281 elun ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
282 281 biimpi ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
283 282 orcomd ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ∨ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
284 283 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ∨ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
285 velsn ⊢ ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
286 285 notbii ⊢ ( ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
287 286 bilanri ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } )
288 pm2.53 ⊢ ( ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ∨ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
289 284 287 288 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
290 173 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
291 289 67 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑡 ∈ ℝ )
292 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑋 ∈ ℝ )
293 291 292 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
294 290 293 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
295 279 280 289 294 fvmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
296 278 295 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
297 276 296 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
298 297 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
299 eqid ⊢ ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
300 106 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
301 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
302 7 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑋 ∈ ℝ )
303 301 302 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
304 92 103 300 300 303 cncfmptssg ⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ℝ –cn→ ℝ ) )
305 304 213 cncfcompt ⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ℝ –cn→ ℂ ) )
306 305 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ℝ –cn→ ℂ ) )
307 105 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
308 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
309 308 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
310 43 309 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( - π [,] π ) )
311 156 310 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
312 311 snssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ⊆ ℝ )
313 307 312 unssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℝ )
314 113 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℂ ⊆ ℂ )
315 173 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
316 313 sselda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑡 ∈ ℝ )
317 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑋 ∈ ℝ )
318 316 317 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
319 315 318 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
320 319 recnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℂ )
321 299 306 313 314 320 cncfmptssg ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) –cn→ ℂ ) )
322 156 106 sstri ⊢ ( - π [,] π ) ⊆ ℂ
323 322 310 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
324 323 snssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ⊆ ℂ )
325 108 324 unssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℂ )
326 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
327 216 326 222 cncfcn ⊢ ( ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
328 325 113 327 sylancl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
329 321 328 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
330 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) )
331 227 325 330 sylancr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) )
332 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 ) ) ‘ 𝑠 ) ) ) )
333 331 227 332 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 ) ) ‘ 𝑠 ) ) ) )
334 329 333 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) )
335 334 simprd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
336 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
337 elsng ⊢ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
338 311 337 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
339 336 338 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } )
340 339 olcd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
341 elun ⊢ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
342 340 341 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
343 fveq2 ⊢ ( 𝑠 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
344 343 eleq2d ⊢ ( 𝑠 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
345 344 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 ) ) ) )
346 335 342 345 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
347 298 346 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
348 eqid ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
349 326 216 348 139 108 323 ellimc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
350 347 349 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
351 129 139 140 11 350 mullimcf ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐿 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
352 265 253 48 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
353 352 oveq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
354 351 353 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐿 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) ∈ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
355 2 32 5 4 7 33 127 270 354 fourierdlem93 ⊢ ( 𝜑 → ∫ ( - π [,] π ) ( 𝐺 ‘ 𝑡 ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐺 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 )
356 3 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝐺 = ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) )
357 fveq2 ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
358 357 oveq1d ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
359 358 adantl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
360 oveq1 ⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( 𝑡 − 𝑋 ) = ( ( 𝑋 + 𝑠 ) − 𝑋 ) )
361 94 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑋 ∈ ℂ )
362 36 7 resubcld ⊢ ( 𝜑 → ( - π − 𝑋 ) ∈ ℝ )
363 362 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( - π − 𝑋 ) ∈ ℝ )
364 39 7 resubcld ⊢ ( 𝜑 → ( π − 𝑋 ) ∈ ℝ )
365 364 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( π − 𝑋 ) ∈ ℝ )
366 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) )
367 eliccre ⊢ ( ( ( - π − 𝑋 ) ∈ ℝ ∧ ( π − 𝑋 ) ∈ ℝ ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ℝ )
368 363 365 366 367 syl3anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ℝ )
369 368 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ℂ )
370 361 369 pncan2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( ( 𝑋 + 𝑠 ) − 𝑋 ) = 𝑠 )
371 360 370 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( 𝑡 − 𝑋 ) = 𝑠 )
372 371 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) )
373 372 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
374 359 373 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
375 16 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → - π ∈ ℝ )
376 15 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → π ∈ ℝ )
377 7 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑋 ∈ ℝ )
378 377 368 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
379 36 recnd ⊢ ( 𝜑 → - π ∈ ℂ )
380 94 379 pncan3d ⊢ ( 𝜑 → ( 𝑋 + ( - π − 𝑋 ) ) = - π )
381 380 eqcomd ⊢ ( 𝜑 → - π = ( 𝑋 + ( - π − 𝑋 ) ) )
382 381 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → - π = ( 𝑋 + ( - π − 𝑋 ) ) )
383 elicc2 ⊢ ( ( ( - π − 𝑋 ) ∈ ℝ ∧ ( π − 𝑋 ) ∈ ℝ ) → ( 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ↔ ( 𝑠 ∈ ℝ ∧ ( - π − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( π − 𝑋 ) ) ) )
384 363 365 383 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ↔ ( 𝑠 ∈ ℝ ∧ ( - π − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( π − 𝑋 ) ) ) )
385 366 384 mpbid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑠 ∈ ℝ ∧ ( - π − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( π − 𝑋 ) ) )
386 385 simp2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( - π − 𝑋 ) ≤ 𝑠 )
387 363 368 377 386 leadd2dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + ( - π − 𝑋 ) ) ≤ ( 𝑋 + 𝑠 ) )
388 382 387 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → - π ≤ ( 𝑋 + 𝑠 ) )
389 385 simp3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ≤ ( π − 𝑋 ) )
390 368 365 377 389 leadd2dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ≤ ( 𝑋 + ( π − 𝑋 ) ) )
391 picn ⊢ π ∈ ℂ
392 391 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → π ∈ ℂ )
393 361 392 pncan3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + ( π − 𝑋 ) ) = π )
394 390 393 breqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ≤ π )
395 375 376 378 388 394 eliccd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( - π [,] π ) )
396 8 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝐹 : ( - π [,] π ) ⟶ ℂ )
397 396 395 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
398 368 111 syldan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ∈ ℂ )
399 397 398 mulcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ℂ )
400 356 374 395 399 fvmptd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝐺 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
401 400 itgeq2dv ⊢ ( 𝜑 → ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐺 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) d 𝑠 )
402 29 355 401 3eqtrd ⊢ ( 𝜑 → ∫ ( - π [,] π ) ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) d 𝑠 )