Metamath Proof Explorer


Theorem fourierdlem93

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

Ref Expression
Hypotheses fourierdlem93.1 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem93.2 𝐻 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑖 ) − 𝑋 ) )
fourierdlem93.3 ( 𝜑𝑀 ∈ ℕ )
fourierdlem93.4 ( 𝜑𝑄 ∈ ( 𝑃𝑀 ) )
fourierdlem93.5 ( 𝜑𝑋 ∈ ℝ )
fourierdlem93.6 ( 𝜑𝐹 : ( - π [,] π ) ⟶ ℂ )
fourierdlem93.7 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem93.8 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
fourierdlem93.9 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
Assertion fourierdlem93 ( 𝜑 → ∫ ( - π [,] π ) ( 𝐹𝑡 ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 )

Proof

Step Hyp Ref Expression
1 fourierdlem93.1 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem93.2 𝐻 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑖 ) − 𝑋 ) )
3 fourierdlem93.3 ( 𝜑𝑀 ∈ ℕ )
4 fourierdlem93.4 ( 𝜑𝑄 ∈ ( 𝑃𝑀 ) )
5 fourierdlem93.5 ( 𝜑𝑋 ∈ ℝ )
6 fourierdlem93.6 ( 𝜑𝐹 : ( - π [,] π ) ⟶ ℂ )
7 fourierdlem93.7 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
8 fourierdlem93.8 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
9 fourierdlem93.9 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
10 1 fourierdlem2 ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
11 3 10 syl ( 𝜑 → ( 𝑄 ∈ ( 𝑃𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
12 4 11 mpbid ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
13 12 simprd ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
14 13 simplld ( 𝜑 → ( 𝑄 ‘ 0 ) = - π )
15 14 eqcomd ( 𝜑 → - π = ( 𝑄 ‘ 0 ) )
16 13 simplrd ( 𝜑 → ( 𝑄𝑀 ) = π )
17 16 eqcomd ( 𝜑 → π = ( 𝑄𝑀 ) )
18 15 17 oveq12d ( 𝜑 → ( - π [,] π ) = ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
19 18 itgeq1d ( 𝜑 → ∫ ( - π [,] π ) ( 𝐹𝑡 ) d 𝑡 = ∫ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ( 𝐹𝑡 ) d 𝑡 )
20 0zd ( 𝜑 → 0 ∈ ℤ )
21 nnuz ℕ = ( ℤ ‘ 1 )
22 3 21 eleqtrdi ( 𝜑𝑀 ∈ ( ℤ ‘ 1 ) )
23 1e0p1 1 = ( 0 + 1 )
24 23 a1i ( 𝜑 → 1 = ( 0 + 1 ) )
25 24 fveq2d ( 𝜑 → ( ℤ ‘ 1 ) = ( ℤ ‘ ( 0 + 1 ) ) )
26 22 25 eleqtrd ( 𝜑𝑀 ∈ ( ℤ ‘ ( 0 + 1 ) ) )
27 1 3 4 fourierdlem15 ( 𝜑𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
28 pire π ∈ ℝ
29 28 renegcli - π ∈ ℝ
30 iccssre ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
31 29 28 30 mp2an ( - π [,] π ) ⊆ ℝ
32 31 a1i ( 𝜑 → ( - π [,] π ) ⊆ ℝ )
33 27 32 fssd ( 𝜑𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
34 13 simprd ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
35 34 r19.21bi ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
36 6 adantr ( ( 𝜑𝑡 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ) → 𝐹 : ( - π [,] π ) ⟶ ℂ )
37 simpr ( ( 𝜑𝑡 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
38 18 eqcomd ( 𝜑 → ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) = ( - π [,] π ) )
39 38 adantr ( ( 𝜑𝑡 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ) → ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) = ( - π [,] π ) )
40 37 39 eleqtrd ( ( 𝜑𝑡 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ) → 𝑡 ∈ ( - π [,] π ) )
41 36 40 ffvelrnd ( ( 𝜑𝑡 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ) → ( 𝐹𝑡 ) ∈ ℂ )
42 33 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
43 elfzofz ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
44 43 adantl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
45 42 44 ffvelrnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℝ )
46 fzofzp1 ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
47 46 adantl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
48 42 47 ffvelrnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
49 6 feqmptd ( 𝜑𝐹 = ( 𝑡 ∈ ( - π [,] π ) ↦ ( 𝐹𝑡 ) ) )
50 49 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 = ( 𝑡 ∈ ( - π [,] π ) ↦ ( 𝐹𝑡 ) ) )
51 50 reseq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑡 ∈ ( - π [,] π ) ↦ ( 𝐹𝑡 ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
52 ioossicc ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
53 52 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
54 29 rexri - π ∈ ℝ*
55 54 a1i ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → - π ∈ ℝ* )
56 28 rexri π ∈ ℝ*
57 56 a1i ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → π ∈ ℝ* )
58 27 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
59 simplr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
60 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
61 55 57 58 59 60 fourierdlem1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( - π [,] π ) )
62 61 ralrimiva ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑡 ∈ ( - π [,] π ) )
63 dfss3 ( ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) ↔ ∀ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑡 ∈ ( - π [,] π ) )
64 62 63 sylibr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
65 53 64 sstrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
66 65 resmptd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( - π [,] π ) ↦ ( 𝐹𝑡 ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑡 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑡 ) ) )
67 51 66 eqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑡 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑡 ) ) )
68 67 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑡 ) ) = ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
69 68 7 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑡 ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
70 67 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑡 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑡 ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
71 9 70 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝑡 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑡 ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
72 67 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) = ( ( 𝑡 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑡 ) ) lim ( 𝑄𝑖 ) ) )
73 8 72 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝑡 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑡 ) ) lim ( 𝑄𝑖 ) ) )
74 45 48 69 71 73 iblcncfioo ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 )
75 6 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐹 : ( - π [,] π ) ⟶ ℂ )
76 75 61 ffvelrnd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹𝑡 ) ∈ ℂ )
77 45 48 74 76 ibliooicc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑡 ) ) ∈ 𝐿1 )
78 20 26 33 35 41 77 itgspltprt ( 𝜑 → ∫ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ( 𝐹𝑡 ) d 𝑡 = Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑡 ) d 𝑡 )
79 fvres ( 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) = ( 𝐹𝑡 ) )
80 79 eqcomd ( 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐹𝑡 ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) )
81 80 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹𝑡 ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) )
82 81 itgeq2dv ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑡 ) d 𝑡 = ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) d 𝑡 )
83 eqid ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
84 6 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : ( - π [,] π ) ⟶ ℂ )
85 84 64 fssresd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
86 53 resabs1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
87 86 7 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
88 86 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
89 45 48 35 85 limcicciooub ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
90 88 89 eqtr3d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
91 9 90 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
92 86 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
93 92 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) = ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
94 45 48 35 85 limciccioolb ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
95 93 94 eqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
96 8 95 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
97 5 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
98 83 45 48 35 85 87 91 96 97 fourierdlem82 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) d 𝑡 = ∫ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
99 45 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( 𝑄𝑖 ) ∈ ℝ )
100 48 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
101 5 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → 𝑋 ∈ ℝ )
102 99 101 resubcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( ( 𝑄𝑖 ) − 𝑋 ) ∈ ℝ )
103 100 101 resubcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ )
104 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
105 eliccre ( ( ( ( 𝑄𝑖 ) − 𝑋 ) ∈ ℝ ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → 𝑡 ∈ ℝ )
106 102 103 104 105 syl3anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → 𝑡 ∈ ℝ )
107 101 106 readdcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ℝ )
108 elicc2 ( ( ( ( 𝑄𝑖 ) − 𝑋 ) ∈ ℝ ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ ) → ( 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( ( 𝑄𝑖 ) − 𝑋 ) ≤ 𝑡𝑡 ≤ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) )
109 102 103 108 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( ( 𝑄𝑖 ) − 𝑋 ) ≤ 𝑡𝑡 ≤ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) )
110 104 109 mpbid ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( 𝑡 ∈ ℝ ∧ ( ( 𝑄𝑖 ) − 𝑋 ) ≤ 𝑡𝑡 ≤ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
111 110 simp2d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( ( 𝑄𝑖 ) − 𝑋 ) ≤ 𝑡 )
112 99 101 106 lesubadd2d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( ( ( 𝑄𝑖 ) − 𝑋 ) ≤ 𝑡 ↔ ( 𝑄𝑖 ) ≤ ( 𝑋 + 𝑡 ) ) )
113 111 112 mpbid ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( 𝑄𝑖 ) ≤ ( 𝑋 + 𝑡 ) )
114 110 simp3d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → 𝑡 ≤ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
115 101 106 100 leaddsub2d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( ( 𝑋 + 𝑡 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ 𝑡 ≤ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
116 114 115 mpbird ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
117 99 100 107 113 116 eliccd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
118 fvres ( ( 𝑋 + 𝑡 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑡 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
119 117 118 syl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑡 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
120 119 itgeq2dv ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ∫ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
121 82 98 120 3eqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑡 ) d 𝑡 = ∫ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
122 121 sumeq2dv ( 𝜑 → Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑡 ) d 𝑡 = Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
123 oveq2 ( 𝑠 = 𝑡 → ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝑡 ) )
124 123 fveq2d ( 𝑠 = 𝑡 → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
125 124 cbvitgv ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡
126 125 a1i ( 𝜑 → ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
127 2 a1i ( 𝜑𝐻 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑖 ) − 𝑋 ) ) )
128 fveq2 ( 𝑖 = 0 → ( 𝑄𝑖 ) = ( 𝑄 ‘ 0 ) )
129 128 oveq1d ( 𝑖 = 0 → ( ( 𝑄𝑖 ) − 𝑋 ) = ( ( 𝑄 ‘ 0 ) − 𝑋 ) )
130 129 adantl ( ( 𝜑𝑖 = 0 ) → ( ( 𝑄𝑖 ) − 𝑋 ) = ( ( 𝑄 ‘ 0 ) − 𝑋 ) )
131 3 nnzd ( 𝜑𝑀 ∈ ℤ )
132 0le0 0 ≤ 0
133 132 a1i ( 𝜑 → 0 ≤ 0 )
134 0red ( 𝜑 → 0 ∈ ℝ )
135 3 nnred ( 𝜑𝑀 ∈ ℝ )
136 3 nngt0d ( 𝜑 → 0 < 𝑀 )
137 134 135 136 ltled ( 𝜑 → 0 ≤ 𝑀 )
138 20 131 20 133 137 elfzd ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
139 14 29 eqeltrdi ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
140 139 5 resubcld ( 𝜑 → ( ( 𝑄 ‘ 0 ) − 𝑋 ) ∈ ℝ )
141 127 130 138 140 fvmptd ( 𝜑 → ( 𝐻 ‘ 0 ) = ( ( 𝑄 ‘ 0 ) − 𝑋 ) )
142 14 oveq1d ( 𝜑 → ( ( 𝑄 ‘ 0 ) − 𝑋 ) = ( - π − 𝑋 ) )
143 141 142 eqtr2d ( 𝜑 → ( - π − 𝑋 ) = ( 𝐻 ‘ 0 ) )
144 fveq2 ( 𝑖 = 𝑀 → ( 𝑄𝑖 ) = ( 𝑄𝑀 ) )
145 144 oveq1d ( 𝑖 = 𝑀 → ( ( 𝑄𝑖 ) − 𝑋 ) = ( ( 𝑄𝑀 ) − 𝑋 ) )
146 145 adantl ( ( 𝜑𝑖 = 𝑀 ) → ( ( 𝑄𝑖 ) − 𝑋 ) = ( ( 𝑄𝑀 ) − 𝑋 ) )
147 135 leidd ( 𝜑𝑀𝑀 )
148 20 131 131 137 147 elfzd ( 𝜑𝑀 ∈ ( 0 ... 𝑀 ) )
149 16 28 eqeltrdi ( 𝜑 → ( 𝑄𝑀 ) ∈ ℝ )
150 149 5 resubcld ( 𝜑 → ( ( 𝑄𝑀 ) − 𝑋 ) ∈ ℝ )
151 127 146 148 150 fvmptd ( 𝜑 → ( 𝐻𝑀 ) = ( ( 𝑄𝑀 ) − 𝑋 ) )
152 16 oveq1d ( 𝜑 → ( ( 𝑄𝑀 ) − 𝑋 ) = ( π − 𝑋 ) )
153 151 152 eqtr2d ( 𝜑 → ( π − 𝑋 ) = ( 𝐻𝑀 ) )
154 143 153 oveq12d ( 𝜑 → ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) = ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) )
155 154 itgeq1d ( 𝜑 → ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ∫ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
156 33 ffvelrnda ( ( 𝜑𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℝ )
157 5 adantr ( ( 𝜑𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ℝ )
158 156 157 resubcld ( ( 𝜑𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑄𝑖 ) − 𝑋 ) ∈ ℝ )
159 158 2 fmptd ( 𝜑𝐻 : ( 0 ... 𝑀 ) ⟶ ℝ )
160 45 48 97 35 ltsub1dd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) − 𝑋 ) < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
161 44 158 syldan ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) − 𝑋 ) ∈ ℝ )
162 2 fvmpt2 ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑄𝑖 ) − 𝑋 ) ∈ ℝ ) → ( 𝐻𝑖 ) = ( ( 𝑄𝑖 ) − 𝑋 ) )
163 44 161 162 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻𝑖 ) = ( ( 𝑄𝑖 ) − 𝑋 ) )
164 fveq2 ( 𝑖 = 𝑗 → ( 𝑄𝑖 ) = ( 𝑄𝑗 ) )
165 164 oveq1d ( 𝑖 = 𝑗 → ( ( 𝑄𝑖 ) − 𝑋 ) = ( ( 𝑄𝑗 ) − 𝑋 ) )
166 165 cbvmptv ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑖 ) − 𝑋 ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑗 ) − 𝑋 ) )
167 2 166 eqtri 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑗 ) − 𝑋 ) )
168 167 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑗 ) − 𝑋 ) ) )
169 fveq2 ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑄𝑗 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
170 169 oveq1d ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝑄𝑗 ) − 𝑋 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
171 170 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( ( 𝑄𝑗 ) − 𝑋 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
172 48 97 resubcld ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ )
173 168 171 47 172 fvmptd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
174 160 163 173 3brtr4d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻𝑖 ) < ( 𝐻 ‘ ( 𝑖 + 1 ) ) )
175 frn ( 𝐹 : ( - π [,] π ) ⟶ ℂ → ran 𝐹 ⊆ ℂ )
176 6 175 syl ( 𝜑 → ran 𝐹 ⊆ ℂ )
177 176 adantr ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ran 𝐹 ⊆ ℂ )
178 ffun ( 𝐹 : ( - π [,] π ) ⟶ ℂ → Fun 𝐹 )
179 6 178 syl ( 𝜑 → Fun 𝐹 )
180 179 adantr ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → Fun 𝐹 )
181 29 a1i ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → - π ∈ ℝ )
182 28 a1i ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → π ∈ ℝ )
183 5 adantr ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → 𝑋 ∈ ℝ )
184 141 140 eqeltrd ( 𝜑 → ( 𝐻 ‘ 0 ) ∈ ℝ )
185 184 adantr ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝐻 ‘ 0 ) ∈ ℝ )
186 151 150 eqeltrd ( 𝜑 → ( 𝐻𝑀 ) ∈ ℝ )
187 186 adantr ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝐻𝑀 ) ∈ ℝ )
188 simpr ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → 𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) )
189 eliccre ( ( ( 𝐻 ‘ 0 ) ∈ ℝ ∧ ( 𝐻𝑀 ) ∈ ℝ ∧ 𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → 𝑡 ∈ ℝ )
190 185 187 188 189 syl3anc ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → 𝑡 ∈ ℝ )
191 183 190 readdcld ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ℝ )
192 128 adantl ( ( 𝜑𝑖 = 0 ) → ( 𝑄𝑖 ) = ( 𝑄 ‘ 0 ) )
193 192 oveq1d ( ( 𝜑𝑖 = 0 ) → ( ( 𝑄𝑖 ) − 𝑋 ) = ( ( 𝑄 ‘ 0 ) − 𝑋 ) )
194 127 193 138 140 fvmptd ( 𝜑 → ( 𝐻 ‘ 0 ) = ( ( 𝑄 ‘ 0 ) − 𝑋 ) )
195 194 oveq2d ( 𝜑 → ( 𝑋 + ( 𝐻 ‘ 0 ) ) = ( 𝑋 + ( ( 𝑄 ‘ 0 ) − 𝑋 ) ) )
196 5 recnd ( 𝜑𝑋 ∈ ℂ )
197 139 recnd ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℂ )
198 196 197 pncan3d ( 𝜑 → ( 𝑋 + ( ( 𝑄 ‘ 0 ) − 𝑋 ) ) = ( 𝑄 ‘ 0 ) )
199 195 198 14 3eqtrrd ( 𝜑 → - π = ( 𝑋 + ( 𝐻 ‘ 0 ) ) )
200 199 adantr ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → - π = ( 𝑋 + ( 𝐻 ‘ 0 ) ) )
201 elicc2 ( ( ( 𝐻 ‘ 0 ) ∈ ℝ ∧ ( 𝐻𝑀 ) ∈ ℝ ) → ( 𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐻 ‘ 0 ) ≤ 𝑡𝑡 ≤ ( 𝐻𝑀 ) ) ) )
202 185 187 201 syl2anc ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐻 ‘ 0 ) ≤ 𝑡𝑡 ≤ ( 𝐻𝑀 ) ) ) )
203 188 202 mpbid ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝑡 ∈ ℝ ∧ ( 𝐻 ‘ 0 ) ≤ 𝑡𝑡 ≤ ( 𝐻𝑀 ) ) )
204 203 simp2d ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝐻 ‘ 0 ) ≤ 𝑡 )
205 185 190 183 204 leadd2dd ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝑋 + ( 𝐻 ‘ 0 ) ) ≤ ( 𝑋 + 𝑡 ) )
206 200 205 eqbrtrd ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → - π ≤ ( 𝑋 + 𝑡 ) )
207 203 simp3d ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → 𝑡 ≤ ( 𝐻𝑀 ) )
208 190 187 183 207 leadd2dd ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝑋 + 𝑡 ) ≤ ( 𝑋 + ( 𝐻𝑀 ) ) )
209 151 oveq2d ( 𝜑 → ( 𝑋 + ( 𝐻𝑀 ) ) = ( 𝑋 + ( ( 𝑄𝑀 ) − 𝑋 ) ) )
210 149 recnd ( 𝜑 → ( 𝑄𝑀 ) ∈ ℂ )
211 196 210 pncan3d ( 𝜑 → ( 𝑋 + ( ( 𝑄𝑀 ) − 𝑋 ) ) = ( 𝑄𝑀 ) )
212 209 211 16 3eqtrrd ( 𝜑 → π = ( 𝑋 + ( 𝐻𝑀 ) ) )
213 212 adantr ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → π = ( 𝑋 + ( 𝐻𝑀 ) ) )
214 208 213 breqtrrd ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝑋 + 𝑡 ) ≤ π )
215 181 182 191 206 214 eliccd ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝑋 + 𝑡 ) ∈ ( - π [,] π ) )
216 fdm ( 𝐹 : ( - π [,] π ) ⟶ ℂ → dom 𝐹 = ( - π [,] π ) )
217 6 216 syl ( 𝜑 → dom 𝐹 = ( - π [,] π ) )
218 217 eqcomd ( 𝜑 → ( - π [,] π ) = dom 𝐹 )
219 218 adantr ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( - π [,] π ) = dom 𝐹 )
220 215 219 eleqtrd ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝑋 + 𝑡 ) ∈ dom 𝐹 )
221 fvelrn ( ( Fun 𝐹 ∧ ( 𝑋 + 𝑡 ) ∈ dom 𝐹 ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ran 𝐹 )
222 180 220 221 syl2anc ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ran 𝐹 )
223 177 222 sseldd ( ( 𝜑𝑡 ∈ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ℂ )
224 163 161 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻𝑖 ) ∈ ℝ )
225 173 172 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
226 84 65 fssresd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
227 45 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
228 227 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
229 48 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
230 229 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
231 5 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
232 elioore ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → 𝑡 ∈ ℝ )
233 232 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ℝ )
234 231 233 readdcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑡 ) ∈ ℝ )
235 163 oveq2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( 𝐻𝑖 ) ) = ( 𝑋 + ( ( 𝑄𝑖 ) − 𝑋 ) ) )
236 196 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℂ )
237 45 recnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℂ )
238 236 237 pncan3d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( ( 𝑄𝑖 ) − 𝑋 ) ) = ( 𝑄𝑖 ) )
239 eqidd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) = ( 𝑄𝑖 ) )
240 235 238 239 3eqtrrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) = ( 𝑋 + ( 𝐻𝑖 ) ) )
241 240 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) = ( 𝑋 + ( 𝐻𝑖 ) ) )
242 224 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻𝑖 ) ∈ ℝ )
243 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
244 242 rexrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻𝑖 ) ∈ ℝ* )
245 225 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
246 245 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
247 elioo2 ( ( ( 𝐻𝑖 ) ∈ ℝ* ∧ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐻𝑖 ) < 𝑡𝑡 < ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
248 244 246 247 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝐻𝑖 ) < 𝑡𝑡 < ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
249 243 248 mpbid ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑡 ∈ ℝ ∧ ( 𝐻𝑖 ) < 𝑡𝑡 < ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
250 249 simp2d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻𝑖 ) < 𝑡 )
251 242 233 231 250 ltadd2dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + ( 𝐻𝑖 ) ) < ( 𝑋 + 𝑡 ) )
252 241 251 eqbrtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) < ( 𝑋 + 𝑡 ) )
253 225 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
254 249 simp3d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 < ( 𝐻 ‘ ( 𝑖 + 1 ) ) )
255 233 253 231 254 ltadd2dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑡 ) < ( 𝑋 + ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
256 173 oveq2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑋 + ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
257 48 recnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
258 236 257 pncan3d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
259 256 258 eqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
260 259 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
261 255 260 breqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑡 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
262 228 230 234 252 261 eliood ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑡 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
263 eqid ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) = ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) )
264 262 263 fmptd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) : ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⟶ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
265 fcompt ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ∧ ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) : ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⟶ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∘ ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) = ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) )
266 226 264 265 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∘ ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) = ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) )
267 oveq2 ( 𝑡 = 𝑟 → ( 𝑋 + 𝑡 ) = ( 𝑋 + 𝑟 ) )
268 267 cbvmptv ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) = ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) )
269 268 fveq1i ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) = ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑠 )
270 269 fveq2i ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑠 ) )
271 270 mpteq2i ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑠 ) ) )
272 271 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑠 ) ) ) )
273 fveq2 ( 𝑠 = 𝑡 → ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑠 ) = ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑡 ) )
274 273 fveq2d ( 𝑠 = 𝑡 → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑡 ) ) )
275 274 cbvmptv ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑠 ) ) ) = ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑡 ) ) )
276 275 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑠 ) ) ) = ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑡 ) ) ) )
277 eqidd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) = ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) )
278 oveq2 ( 𝑟 = 𝑡 → ( 𝑋 + 𝑟 ) = ( 𝑋 + 𝑡 ) )
279 278 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑟 = 𝑡 ) → ( 𝑋 + 𝑟 ) = ( 𝑋 + 𝑡 ) )
280 277 279 243 234 fvmptd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑡 ) = ( 𝑋 + 𝑡 ) )
281 280 fveq2d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑡 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑡 ) ) )
282 fvres ( ( 𝑋 + 𝑡 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑡 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
283 262 282 syl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑡 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
284 281 283 eqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑡 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
285 284 mpteq2dva ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑟 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑟 ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) )
286 272 276 285 3eqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) = ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) )
287 266 286 eqtr2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∘ ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) )
288 eqid ( 𝑡 ∈ ℂ ↦ ( 𝑋 + 𝑡 ) ) = ( 𝑡 ∈ ℂ ↦ ( 𝑋 + 𝑡 ) )
289 ssid ℂ ⊆ ℂ
290 289 a1i ( 𝑋 ∈ ℂ → ℂ ⊆ ℂ )
291 id ( 𝑋 ∈ ℂ → 𝑋 ∈ ℂ )
292 290 291 290 constcncfg ( 𝑋 ∈ ℂ → ( 𝑡 ∈ ℂ ↦ 𝑋 ) ∈ ( ℂ –cn→ ℂ ) )
293 cncfmptid ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( ℂ –cn→ ℂ ) )
294 289 289 293 mp2an ( 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( ℂ –cn→ ℂ )
295 294 a1i ( 𝑋 ∈ ℂ → ( 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( ℂ –cn→ ℂ ) )
296 292 295 addcncf ( 𝑋 ∈ ℂ → ( 𝑡 ∈ ℂ ↦ ( 𝑋 + 𝑡 ) ) ∈ ( ℂ –cn→ ℂ ) )
297 236 296 syl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ℂ ↦ ( 𝑋 + 𝑡 ) ) ∈ ( ℂ –cn→ ℂ ) )
298 ioosscn ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
299 298 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
300 ioosscn ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
301 300 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
302 288 297 299 301 262 cncfmptssg ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) –cn→ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
303 302 7 cncfco ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∘ ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
304 287 303 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
305 227 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
306 229 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
307 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) )
308 vex 𝑟 ∈ V
309 263 elrnmpt ( 𝑟 ∈ V → ( 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ↔ ∃ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) 𝑟 = ( 𝑋 + 𝑡 ) ) )
310 308 309 ax-mp ( 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ↔ ∃ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) 𝑟 = ( 𝑋 + 𝑡 ) )
311 307 310 sylib ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ∃ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) 𝑟 = ( 𝑋 + 𝑡 ) )
312 nfv 𝑡 ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) )
313 nfmpt1 𝑡 ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) )
314 313 nfrn 𝑡 ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) )
315 314 nfcri 𝑡 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) )
316 312 315 nfan 𝑡 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) )
317 nfv 𝑡 𝑟 ∈ ℝ
318 simp3 ( ( 𝜑𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑟 = ( 𝑋 + 𝑡 ) ) → 𝑟 = ( 𝑋 + 𝑡 ) )
319 5 3ad2ant1 ( ( 𝜑𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑟 = ( 𝑋 + 𝑡 ) ) → 𝑋 ∈ ℝ )
320 232 3ad2ant2 ( ( 𝜑𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑟 = ( 𝑋 + 𝑡 ) ) → 𝑡 ∈ ℝ )
321 319 320 readdcld ( ( 𝜑𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑟 = ( 𝑋 + 𝑡 ) ) → ( 𝑋 + 𝑡 ) ∈ ℝ )
322 318 321 eqeltrd ( ( 𝜑𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑟 = ( 𝑋 + 𝑡 ) ) → 𝑟 ∈ ℝ )
323 322 3exp ( 𝜑 → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑟 = ( 𝑋 + 𝑡 ) → 𝑟 ∈ ℝ ) ) )
324 323 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑟 = ( 𝑋 + 𝑡 ) → 𝑟 ∈ ℝ ) ) )
325 316 317 324 rexlimd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ( ∃ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) 𝑟 = ( 𝑋 + 𝑡 ) → 𝑟 ∈ ℝ ) )
326 311 325 mpd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → 𝑟 ∈ ℝ )
327 nfv 𝑡 ( 𝑄𝑖 ) < 𝑟
328 252 3adant3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑟 = ( 𝑋 + 𝑡 ) ) → ( 𝑄𝑖 ) < ( 𝑋 + 𝑡 ) )
329 simp3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑟 = ( 𝑋 + 𝑡 ) ) → 𝑟 = ( 𝑋 + 𝑡 ) )
330 328 329 breqtrrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑟 = ( 𝑋 + 𝑡 ) ) → ( 𝑄𝑖 ) < 𝑟 )
331 330 3exp ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑟 = ( 𝑋 + 𝑡 ) → ( 𝑄𝑖 ) < 𝑟 ) ) )
332 331 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑟 = ( 𝑋 + 𝑡 ) → ( 𝑄𝑖 ) < 𝑟 ) ) )
333 316 327 332 rexlimd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ( ∃ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) 𝑟 = ( 𝑋 + 𝑡 ) → ( 𝑄𝑖 ) < 𝑟 ) )
334 311 333 mpd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ( 𝑄𝑖 ) < 𝑟 )
335 nfv 𝑡 𝑟 < ( 𝑄 ‘ ( 𝑖 + 1 ) )
336 261 3adant3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑟 = ( 𝑋 + 𝑡 ) ) → ( 𝑋 + 𝑡 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
337 329 336 eqbrtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑟 = ( 𝑋 + 𝑡 ) ) → 𝑟 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
338 337 3exp ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑟 = ( 𝑋 + 𝑡 ) → 𝑟 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
339 338 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑟 = ( 𝑋 + 𝑡 ) → 𝑟 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
340 316 335 339 rexlimd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ( ∃ 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) 𝑟 = ( 𝑋 + 𝑡 ) → 𝑟 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
341 311 340 mpd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → 𝑟 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
342 305 306 326 334 341 eliood ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → 𝑟 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
343 217 ineq2d ( 𝜑 → ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∩ dom 𝐹 ) = ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∩ ( - π [,] π ) ) )
344 343 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∩ dom 𝐹 ) = ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∩ ( - π [,] π ) ) )
345 dmres dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∩ dom 𝐹 )
346 345 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∩ dom 𝐹 ) )
347 dfss ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) ↔ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∩ ( - π [,] π ) ) )
348 65 347 sylib ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∩ ( - π [,] π ) ) )
349 344 346 348 3eqtr4d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
350 349 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
351 342 350 eleqtrrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → 𝑟 ∈ dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
352 326 341 ltned ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → 𝑟 ≠ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
353 352 neneqd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ¬ 𝑟 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
354 velsn ( 𝑟 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ 𝑟 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
355 353 354 sylnibr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ¬ 𝑟 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } )
356 351 355 eldifd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → 𝑟 ∈ ( dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∖ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
357 356 ralrimiva ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) 𝑟 ∈ ( dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∖ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
358 dfss3 ( ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ⊆ ( dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∖ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↔ ∀ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) 𝑟 ∈ ( dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∖ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
359 357 358 sylibr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ⊆ ( dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∖ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
360 eqid ( 𝑠 ∈ ℂ ↦ ( 𝑋 + 𝑠 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑋 + 𝑠 ) )
361 196 adantr ( ( 𝜑𝑠 ∈ ℂ ) → 𝑋 ∈ ℂ )
362 simpr ( ( 𝜑𝑠 ∈ ℂ ) → 𝑠 ∈ ℂ )
363 361 362 addcomd ( ( 𝜑𝑠 ∈ ℂ ) → ( 𝑋 + 𝑠 ) = ( 𝑠 + 𝑋 ) )
364 363 mpteq2dva ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑋 + 𝑠 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 + 𝑋 ) ) )
365 eqid ( 𝑠 ∈ ℂ ↦ ( 𝑠 + 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 + 𝑋 ) )
366 365 addccncf ( 𝑋 ∈ ℂ → ( 𝑠 ∈ ℂ ↦ ( 𝑠 + 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
367 196 366 syl ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 + 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
368 364 367 eqeltrd ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ℂ –cn→ ℂ ) )
369 368 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ℂ ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ℂ –cn→ ℂ ) )
370 224 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻𝑖 ) ∈ ℝ* )
371 iocssre ( ( ( 𝐻𝑖 ) ∈ ℝ* ∧ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ) → ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
372 370 225 371 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
373 ax-resscn ℝ ⊆ ℂ
374 372 373 sstrdi ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
375 289 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℂ ⊆ ℂ )
376 196 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℂ )
377 374 sselda ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℂ )
378 376 377 addcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℂ )
379 360 369 374 375 378 cncfmptssg ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
380 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
381 eqid ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
382 380 cnfldtop ( TopOpen ‘ ℂfld ) ∈ Top
383 unicntop ℂ = ( TopOpen ‘ ℂfld )
384 383 restid ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
385 382 384 ax-mp ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
386 385 eqcomi ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
387 380 381 386 cncfcn ( ( ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
388 374 375 387 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
389 379 388 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
390 380 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
391 390 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
392 resttopon ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( TopOn ‘ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
393 391 374 392 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( TopOn ‘ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
394 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 ) ) ‘ 𝑡 ) ) ) )
395 393 391 394 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) : ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ∧ ∀ 𝑡 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) ) ) )
396 389 395 mpbid ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) : ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ∧ ∀ 𝑡 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) ) )
397 396 simprd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑡 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) )
398 ubioc1 ( ( ( 𝐻𝑖 ) ∈ ℝ* ∧ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ ( 𝐻𝑖 ) < ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
399 370 245 174 398 syl3anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
400 fveq2 ( 𝑡 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
401 400 eleq2d ( 𝑡 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) ↔ ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
402 401 rspccva ( ( ∀ 𝑡 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) ∧ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
403 397 399 402 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
404 ioounsn ( ( ( 𝐻𝑖 ) ∈ ℝ* ∧ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ ( 𝐻𝑖 ) < ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) = ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
405 370 245 174 404 syl3anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) = ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
406 259 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑋 + ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
407 406 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑋 + ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
408 iftrue ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) → if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
409 408 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
410 oveq2 ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) → ( 𝑋 + 𝑠 ) = ( 𝑋 + ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
411 410 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑋 + 𝑠 ) = ( 𝑋 + ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
412 407 409 411 3eqtr4d ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑋 + 𝑠 ) )
413 iffalse ( ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) → if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) )
414 413 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) )
415 eqidd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) = ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) )
416 oveq2 ( 𝑡 = 𝑠 → ( 𝑋 + 𝑡 ) = ( 𝑋 + 𝑠 ) )
417 416 adantl ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑡 = 𝑠 ) → ( 𝑋 + 𝑡 ) = ( 𝑋 + 𝑠 ) )
418 velsn ( 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ↔ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) )
419 418 notbii ( ¬ 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ↔ ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) )
420 elun ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) )
421 420 biimpi ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) )
422 421 orcomd ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ∨ 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
423 422 ord ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) → ( ¬ 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } → 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
424 419 423 syl5bir ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) → ( ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) → 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
425 424 imp ( ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ∧ ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
426 425 adantll ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
427 5 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑋 ∈ ℝ )
428 elioore ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ )
429 428 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
430 elsni ( 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } → 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) )
431 430 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) → 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) )
432 225 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
433 431 432 eqeltrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) → 𝑠 ∈ ℝ )
434 429 433 jaodan ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑠 ∈ ℝ )
435 420 434 sylan2b ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑠 ∈ ℝ )
436 427 435 readdcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
437 436 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
438 415 417 426 437 fvmptd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) = ( 𝑋 + 𝑠 ) )
439 414 438 eqtrd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑋 + 𝑠 ) )
440 412 439 pm2.61dan ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) → if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑋 + 𝑠 ) )
441 405 440 mpteq12dva ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) )
442 405 oveq2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
443 442 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) )
444 443 fveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) (,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
445 403 441 444 3eltr4d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
446 eqid ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) )
447 eqid ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) )
448 264 301 fssd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) : ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
449 225 recnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
450 446 380 447 448 299 449 ellimc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) lim ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑠 = ( 𝐻 ‘ ( 𝑖 + 1 ) ) , ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
451 445 450 mpbird ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) lim ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
452 359 451 9 limccog ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∘ ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) lim ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
453 266 286 eqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∘ ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) = ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) )
454 453 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∘ ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) lim ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) lim ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
455 452 454 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) lim ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
456 45 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ( 𝑄𝑖 ) ∈ ℝ )
457 456 334 gtned ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → 𝑟 ≠ ( 𝑄𝑖 ) )
458 457 neneqd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ¬ 𝑟 = ( 𝑄𝑖 ) )
459 velsn ( 𝑟 ∈ { ( 𝑄𝑖 ) } ↔ 𝑟 = ( 𝑄𝑖 ) )
460 458 459 sylnibr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → ¬ 𝑟 ∈ { ( 𝑄𝑖 ) } )
461 351 460 eldifd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) → 𝑟 ∈ ( dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∖ { ( 𝑄𝑖 ) } ) )
462 461 ralrimiva ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) 𝑟 ∈ ( dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∖ { ( 𝑄𝑖 ) } ) )
463 dfss3 ( ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ⊆ ( dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∖ { ( 𝑄𝑖 ) } ) ↔ ∀ 𝑟 ∈ ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) 𝑟 ∈ ( dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∖ { ( 𝑄𝑖 ) } ) )
464 462 463 sylibr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ran ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ⊆ ( dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∖ { ( 𝑄𝑖 ) } ) )
465 icossre ( ( ( 𝐻𝑖 ) ∈ ℝ ∧ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ) → ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
466 224 245 465 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
467 466 373 sstrdi ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
468 196 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℂ )
469 467 sselda ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℂ )
470 468 469 addcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℂ )
471 360 369 467 375 470 cncfmptssg ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
472 eqid ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
473 380 472 386 cncfcn ( ( ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
474 467 375 473 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
475 471 474 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
476 resttopon ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( TopOn ‘ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
477 391 467 476 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( TopOn ‘ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
478 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 ) ) ‘ 𝑡 ) ) ) )
479 477 391 478 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) : ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ∧ ∀ 𝑡 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) ) ) )
480 475 479 mpbid ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) : ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ∧ ∀ 𝑡 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) ) )
481 480 simprd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑡 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) )
482 lbico1 ( ( ( 𝐻𝑖 ) ∈ ℝ* ∧ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ ( 𝐻𝑖 ) < ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐻𝑖 ) ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
483 370 245 174 482 syl3anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻𝑖 ) ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
484 fveq2 ( 𝑡 = ( 𝐻𝑖 ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻𝑖 ) ) )
485 484 eleq2d ( 𝑡 = ( 𝐻𝑖 ) → ( ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) ↔ ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻𝑖 ) ) ) )
486 485 rspccva ( ( ∀ 𝑡 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑡 ) ∧ ( 𝐻𝑖 ) ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻𝑖 ) ) )
487 481 483 486 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻𝑖 ) ) )
488 uncom ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) = ( { ( 𝐻𝑖 ) } ∪ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
489 snunioo ( ( ( 𝐻𝑖 ) ∈ ℝ* ∧ ( 𝐻 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ ( 𝐻𝑖 ) < ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) → ( { ( 𝐻𝑖 ) } ∪ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
490 370 245 174 489 syl3anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( { ( 𝐻𝑖 ) } ∪ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
491 488 490 syl5eq ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) = ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
492 iftrue ( 𝑠 = ( 𝐻𝑖 ) → if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑄𝑖 ) )
493 492 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 = ( 𝐻𝑖 ) ) → if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑄𝑖 ) )
494 240 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 = ( 𝐻𝑖 ) ) → ( 𝑄𝑖 ) = ( 𝑋 + ( 𝐻𝑖 ) ) )
495 oveq2 ( 𝑠 = ( 𝐻𝑖 ) → ( 𝑋 + 𝑠 ) = ( 𝑋 + ( 𝐻𝑖 ) ) )
496 495 eqcomd ( 𝑠 = ( 𝐻𝑖 ) → ( 𝑋 + ( 𝐻𝑖 ) ) = ( 𝑋 + 𝑠 ) )
497 496 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 = ( 𝐻𝑖 ) ) → ( 𝑋 + ( 𝐻𝑖 ) ) = ( 𝑋 + 𝑠 ) )
498 493 494 497 3eqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 = ( 𝐻𝑖 ) ) → if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑋 + 𝑠 ) )
499 498 adantlr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) ∧ 𝑠 = ( 𝐻𝑖 ) ) → if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑋 + 𝑠 ) )
500 iffalse ( ¬ 𝑠 = ( 𝐻𝑖 ) → if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) )
501 500 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) ∧ ¬ 𝑠 = ( 𝐻𝑖 ) ) → if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) )
502 eqidd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) ∧ ¬ 𝑠 = ( 𝐻𝑖 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) = ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) )
503 416 adantl ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) ∧ ¬ 𝑠 = ( 𝐻𝑖 ) ) ∧ 𝑡 = 𝑠 ) → ( 𝑋 + 𝑡 ) = ( 𝑋 + 𝑠 ) )
504 velsn ( 𝑠 ∈ { ( 𝐻𝑖 ) } ↔ 𝑠 = ( 𝐻𝑖 ) )
505 504 notbii ( ¬ 𝑠 ∈ { ( 𝐻𝑖 ) } ↔ ¬ 𝑠 = ( 𝐻𝑖 ) )
506 elun ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ↔ ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝐻𝑖 ) } ) )
507 506 biimpi ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) → ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝐻𝑖 ) } ) )
508 507 orcomd ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) → ( 𝑠 ∈ { ( 𝐻𝑖 ) } ∨ 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
509 508 ord ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) → ( ¬ 𝑠 ∈ { ( 𝐻𝑖 ) } → 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
510 505 509 syl5bir ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) → ( ¬ 𝑠 = ( 𝐻𝑖 ) → 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
511 510 imp ( ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ∧ ¬ 𝑠 = ( 𝐻𝑖 ) ) → 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
512 511 adantll ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) ∧ ¬ 𝑠 = ( 𝐻𝑖 ) ) → 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
513 5 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) → 𝑋 ∈ ℝ )
514 elsni ( 𝑠 ∈ { ( 𝐻𝑖 ) } → 𝑠 = ( 𝐻𝑖 ) )
515 514 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝐻𝑖 ) } ) → 𝑠 = ( 𝐻𝑖 ) )
516 224 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝐻𝑖 ) } ) → ( 𝐻𝑖 ) ∈ ℝ )
517 515 516 eqeltrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝐻𝑖 ) } ) → 𝑠 ∈ ℝ )
518 429 517 jaodan ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝑠 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝐻𝑖 ) } ) ) → 𝑠 ∈ ℝ )
519 506 518 sylan2b ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) → 𝑠 ∈ ℝ )
520 513 519 readdcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
521 520 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) ∧ ¬ 𝑠 = ( 𝐻𝑖 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
522 502 503 512 521 fvmptd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) ∧ ¬ 𝑠 = ( 𝐻𝑖 ) ) → ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) = ( 𝑋 + 𝑠 ) )
523 501 522 eqtrd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) ∧ ¬ 𝑠 = ( 𝐻𝑖 ) ) → if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑋 + 𝑠 ) )
524 499 523 pm2.61dan ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) → if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) = ( 𝑋 + 𝑠 ) )
525 491 524 mpteq12dva ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ↦ if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑠 ) ) )
526 491 oveq2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) )
527 526 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) )
528 527 fveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻𝑖 ) ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐻𝑖 ) [,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻𝑖 ) ) )
529 487 525 528 3eltr4d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ↦ if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻𝑖 ) ) )
530 eqid ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) )
531 eqid ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ↦ if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ↦ if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) )
532 224 recnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻𝑖 ) ∈ ℂ )
533 530 380 531 448 299 532 ellimc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) ∈ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) lim ( 𝐻𝑖 ) ) ↔ ( 𝑠 ∈ ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ↦ if ( 𝑠 = ( 𝐻𝑖 ) , ( 𝑄𝑖 ) , ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ‘ 𝑠 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝐻𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐻𝑖 ) ) ) )
534 529 533 mpbird ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) lim ( 𝐻𝑖 ) ) )
535 464 534 8 limccog ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∘ ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) lim ( 𝐻𝑖 ) ) )
536 453 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∘ ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑋 + 𝑡 ) ) ) lim ( 𝐻𝑖 ) ) = ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) lim ( 𝐻𝑖 ) ) )
537 535 536 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) lim ( 𝐻𝑖 ) ) )
538 224 225 304 455 537 iblcncfioo ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) ∈ 𝐿1 )
539 6 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐹 : ( - π [,] π ) ⟶ ℂ )
540 54 a1i ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → - π ∈ ℝ* )
541 56 a1i ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → π ∈ ℝ* )
542 27 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
543 simplr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
544 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) )
545 163 173 oveq12d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
546 545 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
547 544 546 eleqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
548 547 117 syldan ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑡 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
549 540 541 542 543 548 fourierdlem1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑡 ) ∈ ( - π [,] π ) )
550 539 549 ffvelrnd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ∈ ℂ )
551 224 225 538 550 ibliooicc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) ) ∈ 𝐿1 )
552 20 26 159 174 223 551 itgspltprt ( 𝜑 → ∫ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
553 545 itgeq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = ∫ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
554 553 sumeq2dv ( 𝜑 → Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( 𝐻𝑖 ) [,] ( 𝐻 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
555 552 554 eqtrd ( 𝜑 → ∫ ( ( 𝐻 ‘ 0 ) [,] ( 𝐻𝑀 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 = Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
556 126 155 555 3eqtrd ( 𝜑 → ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 = Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( ( 𝑄𝑖 ) − 𝑋 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) d 𝑡 )
557 122 556 eqtr4d ( 𝜑 → Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑡 ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 )
558 19 78 557 3eqtrd ( 𝜑 → ∫ ( - π [,] π ) ( 𝐹𝑡 ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 )