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

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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
42 33 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
43 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
44 43 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
45 42 44 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
46 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
48 42 47 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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 biimtrrid ⊢ ( 𝑠 ∈ ( ( ( 𝐻 ‘ 𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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 biimtrrid ⊢ ( 𝑠 ∈ ( ( ( 𝐻 ‘ 𝑖 ) (,) ( 𝐻 ‘ ( 𝑖 + 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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 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 𝑠 )