Metamath Proof Explorer


Theorem fourierdlem49

Description: The given periodic function F has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem49.a ( 𝜑𝐴 ∈ ℝ )
fourierdlem49.b ( 𝜑𝐵 ∈ ℝ )
fourierdlem49.altb ( 𝜑𝐴 < 𝐵 )
fourierdlem49.p 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem49.t 𝑇 = ( 𝐵𝐴 )
fourierdlem49.m ( 𝜑𝑀 ∈ ℕ )
fourierdlem49.q ( 𝜑𝑄 ∈ ( 𝑃𝑀 ) )
fourierdlem49.d ( 𝜑𝐷 ⊆ ℝ )
fourierdlem49.f ( 𝜑𝐹 : 𝐷 ⟶ ℝ )
fourierdlem49.dper ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 )
fourierdlem49.per ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) )
fourierdlem49.cn ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem49.l ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem49.x ( 𝜑𝑋 ∈ ℝ )
fourierdlem49.z 𝑍 = ( 𝑥 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) )
fourierdlem49.e 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( 𝑍𝑥 ) ) )
Assertion fourierdlem49 ( 𝜑 → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 fourierdlem49.a ( 𝜑𝐴 ∈ ℝ )
2 fourierdlem49.b ( 𝜑𝐵 ∈ ℝ )
3 fourierdlem49.altb ( 𝜑𝐴 < 𝐵 )
4 fourierdlem49.p 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
5 fourierdlem49.t 𝑇 = ( 𝐵𝐴 )
6 fourierdlem49.m ( 𝜑𝑀 ∈ ℕ )
7 fourierdlem49.q ( 𝜑𝑄 ∈ ( 𝑃𝑀 ) )
8 fourierdlem49.d ( 𝜑𝐷 ⊆ ℝ )
9 fourierdlem49.f ( 𝜑𝐹 : 𝐷 ⟶ ℝ )
10 fourierdlem49.dper ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 )
11 fourierdlem49.per ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) )
12 fourierdlem49.cn ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
13 fourierdlem49.l ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
14 fourierdlem49.x ( 𝜑𝑋 ∈ ℝ )
15 fourierdlem49.z 𝑍 = ( 𝑥 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) )
16 fourierdlem49.e 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( 𝑍𝑥 ) ) )
17 ovex ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ V
18 15 fvmpt2 ( ( 𝑥 ∈ ℝ ∧ ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ V ) → ( 𝑍𝑥 ) = ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) )
19 17 18 mpan2 ( 𝑥 ∈ ℝ → ( 𝑍𝑥 ) = ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) )
20 19 oveq2d ( 𝑥 ∈ ℝ → ( 𝑥 + ( 𝑍𝑥 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
21 20 mpteq2ia ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( 𝑍𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
22 16 21 eqtri 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
23 1 2 3 5 22 fourierdlem4 ( 𝜑𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
24 23 14 ffvelcdmd ( 𝜑 → ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) )
25 simpr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ( 𝐸𝑋 ) ∈ ran 𝑄 )
26 4 fourierdlem2 ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
27 6 26 syl ( 𝜑 → ( 𝑄 ∈ ( 𝑃𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
28 7 27 mpbid ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
29 28 simpld ( 𝜑𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
30 elmapi ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
31 29 30 syl ( 𝜑𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
32 31 ffnd ( 𝜑𝑄 Fn ( 0 ... 𝑀 ) )
33 32 ad2antrr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → 𝑄 Fn ( 0 ... 𝑀 ) )
34 fvelrnb ( 𝑄 Fn ( 0 ... 𝑀 ) → ( ( 𝐸𝑋 ) ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) )
35 33 34 syl ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ( ( 𝐸𝑋 ) ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) )
36 25 35 mpbid ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄𝑗 ) = ( 𝐸𝑋 ) )
37 fveq2 ( 𝑖 = ( 𝑗 − 1 ) → ( 𝑄𝑖 ) = ( 𝑄 ‘ ( 𝑗 − 1 ) ) )
38 fvoveq1 ( 𝑖 = ( 𝑗 − 1 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) )
39 37 38 oveq12d ( 𝑖 = ( 𝑗 − 1 ) → ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) )
40 39 eleq2d ( 𝑖 = ( 𝑗 − 1 ) → ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) ) )
41 nnuz ℕ = ( ℤ ‘ 1 )
42 1zzd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 1 ∈ ℤ )
43 elfzelz ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
44 43 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑗 ∈ ℤ )
45 1e0p1 1 = ( 0 + 1 )
46 44 zred ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑗 ∈ ℝ )
47 elfzle1 ( 𝑗 ∈ ( 0 ... 𝑀 ) → 0 ≤ 𝑗 )
48 47 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 0 ≤ 𝑗 )
49 id ( ( 𝑄𝑗 ) = ( 𝐸𝑋 ) → ( 𝑄𝑗 ) = ( 𝐸𝑋 ) )
50 49 eqcomd ( ( 𝑄𝑗 ) = ( 𝐸𝑋 ) → ( 𝐸𝑋 ) = ( 𝑄𝑗 ) )
51 50 ad2antlr ( ( ( 𝜑 ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝐸𝑋 ) = ( 𝑄𝑗 ) )
52 fveq2 ( 𝑗 = 0 → ( 𝑄𝑗 ) = ( 𝑄 ‘ 0 ) )
53 52 adantl ( ( ( 𝜑 ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝑄𝑗 ) = ( 𝑄 ‘ 0 ) )
54 28 simprld ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) )
55 54 simpld ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
56 55 ad2antrr ( ( ( 𝜑 ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝑄 ‘ 0 ) = 𝐴 )
57 51 53 56 3eqtrd ( ( ( 𝜑 ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝐸𝑋 ) = 𝐴 )
58 57 adantllr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝐸𝑋 ) = 𝐴 )
59 58 adantllr ( ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝐸𝑋 ) = 𝐴 )
60 1 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 ∈ ℝ )
61 1 rexrd ( 𝜑𝐴 ∈ ℝ* )
62 61 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 ∈ ℝ* )
63 2 rexrd ( 𝜑𝐵 ∈ ℝ* )
64 63 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐵 ∈ ℝ* )
65 simpr ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) )
66 62 64 65 iocgtlbd ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < ( 𝐸𝑋 ) )
67 60 66 gtned ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸𝑋 ) ≠ 𝐴 )
68 67 neneqd ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ¬ ( 𝐸𝑋 ) = 𝐴 )
69 68 ad3antrrr ( ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ¬ ( 𝐸𝑋 ) = 𝐴 )
70 59 69 pm2.65da ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ¬ 𝑗 = 0 )
71 70 neqned ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑗 ≠ 0 )
72 46 48 71 ne0gt0d ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 0 < 𝑗 )
73 0zd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 0 ∈ ℤ )
74 73 44 zltp1led ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 0 < 𝑗 ↔ ( 0 + 1 ) ≤ 𝑗 ) )
75 72 74 mpbid ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 0 + 1 ) ≤ 𝑗 )
76 45 75 eqbrtrid ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 1 ≤ 𝑗 )
77 41 42 44 76 eluzd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑗 ∈ ℕ )
78 nnm1nn0 ( 𝑗 ∈ ℕ → ( 𝑗 − 1 ) ∈ ℕ0 )
79 77 78 syl ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ∈ ℕ0 )
80 nn0uz 0 = ( ℤ ‘ 0 )
81 79 80 eleqtrdi ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ∈ ( ℤ ‘ 0 ) )
82 6 nnzd ( 𝜑𝑀 ∈ ℤ )
83 82 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑀 ∈ ℤ )
84 peano2zm ( 𝑗 ∈ ℤ → ( 𝑗 − 1 ) ∈ ℤ )
85 43 84 syl ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) ∈ ℤ )
86 85 zred ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) ∈ ℝ )
87 43 zred ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℝ )
88 elfzel2 ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℤ )
89 88 zred ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℝ )
90 87 ltm1d ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) < 𝑗 )
91 elfzle2 ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗𝑀 )
92 86 87 89 90 91 ltletrd ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) < 𝑀 )
93 92 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) < 𝑀 )
94 81 83 93 elfzod ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑀 ) )
95 31 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
96 44 84 syl ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ∈ ℤ )
97 79 nn0ge0d ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 0 ≤ ( 𝑗 − 1 ) )
98 86 89 92 ltled ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) ≤ 𝑀 )
99 98 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ≤ 𝑀 )
100 73 83 96 97 99 elfzd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ... 𝑀 ) )
101 95 100 ffvelcdmd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) ∈ ℝ )
102 101 rexrd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) ∈ ℝ* )
103 31 ffvelcdmda ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄𝑗 ) ∈ ℝ )
104 103 rexrd ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄𝑗 ) ∈ ℝ* )
105 104 adantlr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄𝑗 ) ∈ ℝ* )
106 105 adantr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄𝑗 ) ∈ ℝ* )
107 iocssre ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
108 61 2 107 syl2anc ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
109 108 sselda ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸𝑋 ) ∈ ℝ )
110 109 rexrd ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
111 110 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
112 simplll ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝜑 )
113 ovex ( 𝑗 − 1 ) ∈ V
114 eleq1 ( 𝑖 = ( 𝑗 − 1 ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑀 ) ) )
115 114 anbi2d ( 𝑖 = ( 𝑗 − 1 ) → ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑀 ) ) ) )
116 37 38 breq12d ( 𝑖 = ( 𝑗 − 1 ) → ( ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) )
117 115 116 imbi12d ( 𝑖 = ( 𝑗 − 1 ) → ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) ) )
118 28 simprrd ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
119 118 r19.21bi ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
120 113 117 119 vtocl ( ( 𝜑 ∧ ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) )
121 112 94 120 syl2anc ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) )
122 43 zcnd ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℂ )
123 1cnd ( 𝑗 ∈ ( 0 ... 𝑀 ) → 1 ∈ ℂ )
124 122 123 npcand ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
125 124 eqcomd ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 = ( ( 𝑗 − 1 ) + 1 ) )
126 125 fveq2d ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑄𝑗 ) = ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) )
127 126 eqcomd ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) = ( 𝑄𝑗 ) )
128 127 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) = ( 𝑄𝑗 ) )
129 121 128 breqtrd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝑄𝑗 ) )
130 simpr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄𝑗 ) = ( 𝐸𝑋 ) )
131 129 130 breqtrd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝐸𝑋 ) )
132 108 24 sseldd ( 𝜑 → ( 𝐸𝑋 ) ∈ ℝ )
133 132 leidd ( 𝜑 → ( 𝐸𝑋 ) ≤ ( 𝐸𝑋 ) )
134 133 ad2antrr ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ≤ ( 𝐸𝑋 ) )
135 50 adantl ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) = ( 𝑄𝑗 ) )
136 134 135 breqtrd ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ≤ ( 𝑄𝑗 ) )
137 136 adantllr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ≤ ( 𝑄𝑗 ) )
138 102 106 111 131 137 eliocd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄𝑗 ) ) )
139 126 oveq2d ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄𝑗 ) ) = ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) )
140 139 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄𝑗 ) ) = ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) )
141 138 140 eleqtrd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) )
142 40 94 141 rspcedvdw ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
143 142 ex ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑄𝑗 ) = ( 𝐸𝑋 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
144 143 adantlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑄𝑗 ) = ( 𝐸𝑋 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
145 144 rexlimdva ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄𝑗 ) = ( 𝐸𝑋 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
146 36 145 mpd ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
147 6 ad2antrr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → 𝑀 ∈ ℕ )
148 31 ad2antrr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
149 iocssicc ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
150 55 eqcomd ( 𝜑𝐴 = ( 𝑄 ‘ 0 ) )
151 54 simprd ( 𝜑 → ( 𝑄𝑀 ) = 𝐵 )
152 151 eqcomd ( 𝜑𝐵 = ( 𝑄𝑀 ) )
153 150 152 oveq12d ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
154 149 153 sseqtrid ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
155 154 sselda ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
156 155 adantr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
157 simpr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 )
158 fveq2 ( 𝑘 = 𝑗 → ( 𝑄𝑘 ) = ( 𝑄𝑗 ) )
159 158 breq1d ( 𝑘 = 𝑗 → ( ( 𝑄𝑘 ) < ( 𝐸𝑋 ) ↔ ( 𝑄𝑗 ) < ( 𝐸𝑋 ) ) )
160 159 cbvrabv { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) < ( 𝐸𝑋 ) } = { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) < ( 𝐸𝑋 ) }
161 160 supeq1i sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) < ( 𝐸𝑋 ) } , ℝ , < ) = sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) < ( 𝐸𝑋 ) } , ℝ , < )
162 147 148 156 157 161 fourierdlem25 ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
163 ioossioc ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
164 163 sseli ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
165 164 a1i ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
166 165 reximdva ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
167 162 166 mpd ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
168 146 167 pm2.61dan ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
169 24 168 mpdan ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
170 resindm ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) )
171 9 fdmd ( 𝜑 → dom 𝐹 = 𝐷 )
172 171 ineq2d ( 𝜑 → ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ dom 𝐹 ) = ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) )
173 172 reseq2d ( 𝜑 → ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ) )
174 170 173 eqtr3id ( 𝜑 → ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) ) = ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ) )
175 174 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) ) = ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ) )
176 175 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) = ( ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ) lim ( 𝐸𝑋 ) ) )
177 ax-resscn ℝ ⊆ ℂ
178 177 a1i ( 𝜑 → ℝ ⊆ ℂ )
179 9 178 fssd ( 𝜑𝐹 : 𝐷 ⟶ ℂ )
180 179 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐹 : 𝐷 ⟶ ℂ )
181 inss2 ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ⊆ 𝐷
182 181 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ⊆ 𝐷 )
183 180 182 fssresd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ) : ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ⟶ ℂ )
184 mnfxr -∞ ∈ ℝ*
185 31 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
186 elfzofz ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
187 186 adantl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
188 185 187 ffvelcdmd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℝ )
189 188 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
190 189 mnfled ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → -∞ ≤ ( 𝑄𝑖 ) )
191 iooss1 ( ( -∞ ∈ ℝ* ∧ -∞ ≤ ( 𝑄𝑖 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ ( -∞ (,) ( 𝐸𝑋 ) ) )
192 184 190 191 sylancr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ ( -∞ (,) ( 𝐸𝑋 ) ) )
193 192 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ ( -∞ (,) ( 𝐸𝑋 ) ) )
194 fzofzp1 ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
195 194 adantl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
196 185 195 ffvelcdmd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
197 196 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
198 197 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
199 188 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) ∈ ℝ )
200 199 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
201 simp3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
202 200 198 201 iocleubd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
203 iooss2 ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ ( 𝐸𝑋 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
204 198 202 203 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
205 cncff ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
206 fdm ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ → dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
207 12 205 206 3syl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
208 ssdmres ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
209 207 208 sylibr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
210 171 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom 𝐹 = 𝐷 )
211 209 210 sseqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ 𝐷 )
212 211 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ 𝐷 )
213 204 212 sstrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ 𝐷 )
214 193 213 ssind ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) )
215 8 178 sstrd ( 𝜑𝐷 ⊆ ℂ )
216 215 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐷 ⊆ ℂ )
217 216 ssinss2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ⊆ ℂ )
218 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
219 eqid ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) )
220 132 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ℝ )
221 220 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
222 200 198 201 iocgtlbd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) < ( 𝐸𝑋 ) )
223 220 leidd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ≤ ( 𝐸𝑋 ) )
224 200 221 221 222 223 eliocd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) )
225 ioounsn ( ( ( 𝑄𝑖 ) ∈ ℝ* ∧ ( 𝐸𝑋 ) ∈ ℝ* ∧ ( 𝑄𝑖 ) < ( 𝐸𝑋 ) ) → ( ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ∪ { ( 𝐸𝑋 ) } ) = ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) )
226 200 221 222 225 syl3anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ∪ { ( 𝐸𝑋 ) } ) = ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) )
227 226 fveq2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) ‘ ( ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ∪ { ( 𝐸𝑋 ) } ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) ‘ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) )
228 218 cnfldtop ( TopOpen ‘ ℂfld ) ∈ Top
229 ovex ( -∞ (,) ( 𝐸𝑋 ) ) ∈ V
230 229 inex1 ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∈ V
231 snex { ( 𝐸𝑋 ) } ∈ V
232 230 231 unex ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ∈ V
233 resttop ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ∈ V ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ∈ Top )
234 228 232 233 mp2an ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ∈ Top
235 retop ( topGen ‘ ran (,) ) ∈ Top
236 iooretop ( ( 𝑄𝑖 ) (,) +∞ ) ∈ ( topGen ‘ ran (,) )
237 236 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) (,) +∞ ) ∈ ( topGen ‘ ran (,) ) )
238 elrestr ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ∈ V ∧ ( ( 𝑄𝑖 ) (,) +∞ ) ∈ ( topGen ‘ ran (,) ) ) → ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
239 235 232 237 238 mp3an12i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
240 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 = ( 𝐸𝑋 ) )
241 pnfxr +∞ ∈ ℝ*
242 241 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → +∞ ∈ ℝ* )
243 220 ltpnfd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) < +∞ )
244 200 242 220 222 243 eliood ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,) +∞ ) )
245 snidg ( ( 𝐸𝑋 ) ∈ ℝ → ( 𝐸𝑋 ) ∈ { ( 𝐸𝑋 ) } )
246 elun2 ( ( 𝐸𝑋 ) ∈ { ( 𝐸𝑋 ) } → ( 𝐸𝑋 ) ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) )
247 132 245 246 3syl ( 𝜑 → ( 𝐸𝑋 ) ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) )
248 247 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) )
249 244 248 elind ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
250 249 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
251 240 250 eqeltrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
252 251 adantlr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
253 200 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
254 241 a1i ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → +∞ ∈ ℝ* )
255 189 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
256 132 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → ( 𝐸𝑋 ) ∈ ℝ )
257 iocssre ( ( ( 𝑄𝑖 ) ∈ ℝ* ∧ ( 𝐸𝑋 ) ∈ ℝ ) → ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ⊆ ℝ )
258 255 256 257 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ⊆ ℝ )
259 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) )
260 258 259 sseldd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → 𝑥 ∈ ℝ )
261 260 3adantl3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → 𝑥 ∈ ℝ )
262 256 rexrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
263 255 262 259 iocgtlbd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → ( 𝑄𝑖 ) < 𝑥 )
264 263 3adantl3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → ( 𝑄𝑖 ) < 𝑥 )
265 261 ltpnfd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → 𝑥 < +∞ )
266 253 254 261 264 265 eliood ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) (,) +∞ ) )
267 266 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) (,) +∞ ) )
268 184 a1i ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → -∞ ∈ ℝ* )
269 262 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
270 260 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ℝ )
271 270 mnfltd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → -∞ < 𝑥 )
272 132 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ∈ ℝ )
273 255 262 259 iocleubd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → 𝑥 ≤ ( 𝐸𝑋 ) )
274 273 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ≤ ( 𝐸𝑋 ) )
275 neqne ( ¬ 𝑥 = ( 𝐸𝑋 ) → 𝑥 ≠ ( 𝐸𝑋 ) )
276 275 necomd ( ¬ 𝑥 = ( 𝐸𝑋 ) → ( 𝐸𝑋 ) ≠ 𝑥 )
277 276 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ≠ 𝑥 )
278 270 272 274 277 leneltd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 < ( 𝐸𝑋 ) )
279 268 269 270 271 278 eliood ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) )
280 279 3adantll3 ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) )
281 212 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ 𝐷 )
282 200 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
283 198 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
284 261 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ℝ )
285 264 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → ( 𝑄𝑖 ) < 𝑥 )
286 220 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ∈ ℝ )
287 197 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
288 278 3adantll3 ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 < ( 𝐸𝑋 ) )
289 202 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
290 284 286 287 288 289 ltletrd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
291 282 283 284 285 290 eliood ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
292 281 291 sseldd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥𝐷 )
293 280 292 elind ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) )
294 elun1 ( 𝑥 ∈ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) → 𝑥 ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) )
295 293 294 syl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) )
296 267 295 elind ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) ∧ ¬ 𝑥 = ( 𝐸𝑋 ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
297 252 296 pm2.61dan ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
298 200 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
299 221 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
300 elinel1 ( 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) (,) +∞ ) )
301 elioore ( 𝑥 ∈ ( ( 𝑄𝑖 ) (,) +∞ ) → 𝑥 ∈ ℝ )
302 301 rexrd ( 𝑥 ∈ ( ( 𝑄𝑖 ) (,) +∞ ) → 𝑥 ∈ ℝ* )
303 300 302 syl ( 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) → 𝑥 ∈ ℝ* )
304 303 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → 𝑥 ∈ ℝ* )
305 189 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
306 241 a1i ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → +∞ ∈ ℝ* )
307 300 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) (,) +∞ ) )
308 305 306 307 ioogtlbd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → ( 𝑄𝑖 ) < 𝑥 )
309 308 3adantl3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → ( 𝑄𝑖 ) < 𝑥 )
310 elinel2 ( 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) → 𝑥 ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) )
311 elsni ( 𝑥 ∈ { ( 𝐸𝑋 ) } → 𝑥 = ( 𝐸𝑋 ) )
312 311 adantl ( ( 𝜑𝑥 ∈ { ( 𝐸𝑋 ) } ) → 𝑥 = ( 𝐸𝑋 ) )
313 133 adantr ( ( 𝜑𝑥 ∈ { ( 𝐸𝑋 ) } ) → ( 𝐸𝑋 ) ≤ ( 𝐸𝑋 ) )
314 312 313 eqbrtrd ( ( 𝜑𝑥 ∈ { ( 𝐸𝑋 ) } ) → 𝑥 ≤ ( 𝐸𝑋 ) )
315 314 adantlr ( ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ∧ 𝑥 ∈ { ( 𝐸𝑋 ) } ) → 𝑥 ≤ ( 𝐸𝑋 ) )
316 simpll ( ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ∧ ¬ 𝑥 ∈ { ( 𝐸𝑋 ) } ) → 𝜑 )
317 elunnel2 ( ( 𝑥 ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ∧ ¬ 𝑥 ∈ { ( 𝐸𝑋 ) } ) → 𝑥 ∈ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) )
318 317 adantll ( ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ∧ ¬ 𝑥 ∈ { ( 𝐸𝑋 ) } ) → 𝑥 ∈ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) )
319 elinel1 ( 𝑥 ∈ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) → 𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) )
320 elioore ( 𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) → 𝑥 ∈ ℝ )
321 320 adantl ( ( 𝜑𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) ) → 𝑥 ∈ ℝ )
322 132 adantr ( ( 𝜑𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) ) → ( 𝐸𝑋 ) ∈ ℝ )
323 184 a1i ( ( 𝜑𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) ) → -∞ ∈ ℝ* )
324 322 rexrd ( ( 𝜑𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
325 simpr ( ( 𝜑𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) ) → 𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) )
326 323 324 325 iooltubd ( ( 𝜑𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) ) → 𝑥 < ( 𝐸𝑋 ) )
327 321 322 326 ltled ( ( 𝜑𝑥 ∈ ( -∞ (,) ( 𝐸𝑋 ) ) ) → 𝑥 ≤ ( 𝐸𝑋 ) )
328 319 327 sylan2 ( ( 𝜑𝑥 ∈ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ) → 𝑥 ≤ ( 𝐸𝑋 ) )
329 316 318 328 syl2anc ( ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ∧ ¬ 𝑥 ∈ { ( 𝐸𝑋 ) } ) → 𝑥 ≤ ( 𝐸𝑋 ) )
330 315 329 pm2.61dan ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) → 𝑥 ≤ ( 𝐸𝑋 ) )
331 330 adantlr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) → 𝑥 ≤ ( 𝐸𝑋 ) )
332 310 331 sylan2 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → 𝑥 ≤ ( 𝐸𝑋 ) )
333 332 3adantl3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → 𝑥 ≤ ( 𝐸𝑋 ) )
334 298 299 304 309 333 eliocd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) )
335 297 334 impbida ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥 ∈ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ↔ 𝑥 ∈ ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) )
336 335 eqrdv ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) = ( ( ( 𝑄𝑖 ) (,) +∞ ) ∩ ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
337 ioossre ( -∞ (,) ( 𝐸𝑋 ) ) ⊆ ℝ
338 ssinss1 ( ( -∞ (,) ( 𝐸𝑋 ) ) ⊆ ℝ → ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ⊆ ℝ )
339 337 338 mp1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ⊆ ℝ )
340 220 snssd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → { ( 𝐸𝑋 ) } ⊆ ℝ )
341 339 340 unssd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ⊆ ℝ )
342 eqid ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
343 218 342 rerest ( ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
344 341 343 syl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
345 239 336 344 3eltr4d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) )
346 isopn3i ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ∈ Top ∧ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) ‘ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) = ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) )
347 234 345 346 sylancr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) ‘ ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) ) = ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) )
348 227 347 eqtr2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) (,] ( 𝐸𝑋 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) ‘ ( ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ∪ { ( 𝐸𝑋 ) } ) ) )
349 224 348 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ∪ { ( 𝐸𝑋 ) } ) ) ) ‘ ( ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ∪ { ( 𝐸𝑋 ) } ) ) )
350 183 214 217 218 219 349 limcres ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) = ( ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ) lim ( 𝐸𝑋 ) ) )
351 214 resabs1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) = ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) )
352 351 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ↾ ( ( -∞ (,) ( 𝐸𝑋 ) ) ∩ 𝐷 ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
353 176 350 352 3eqtr2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
354 179 ffdmd ( 𝜑𝐹 : dom 𝐹 ⟶ ℂ )
355 354 adantr ( ( 𝜑𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
356 355 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
357 ioosscn ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ ℂ
358 357 a1i ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ ℂ )
359 171 eqcomd ( 𝜑𝐷 = dom 𝐹 )
360 359 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐷 = dom 𝐹 )
361 213 360 sseqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ dom 𝐹 )
362 361 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ dom 𝐹 )
363 oveq2 ( 𝑥 = 𝑋 → ( 𝐵𝑥 ) = ( 𝐵𝑋 ) )
364 363 fvoveq1d ( 𝑥 = 𝑋 → ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) )
365 364 oveq1d ( 𝑥 = 𝑋 → ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
366 2 14 resubcld ( 𝜑 → ( 𝐵𝑋 ) ∈ ℝ )
367 2 1 resubcld ( 𝜑 → ( 𝐵𝐴 ) ∈ ℝ )
368 5 367 eqeltrid ( 𝜑𝑇 ∈ ℝ )
369 1 2 posdifd ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵𝐴 ) ) )
370 3 369 mpbid ( 𝜑 → 0 < ( 𝐵𝐴 ) )
371 370 5 breqtrrdi ( 𝜑 → 0 < 𝑇 )
372 371 gt0ne0d ( 𝜑𝑇 ≠ 0 )
373 366 368 372 redivcld ( 𝜑 → ( ( 𝐵𝑋 ) / 𝑇 ) ∈ ℝ )
374 373 flcld ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ )
375 374 zred ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℝ )
376 375 368 remulcld ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
377 15 365 14 376 fvmptd3 ( 𝜑 → ( 𝑍𝑋 ) = ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
378 377 376 eqeltrd ( 𝜑 → ( 𝑍𝑋 ) ∈ ℝ )
379 378 recnd ( 𝜑 → ( 𝑍𝑋 ) ∈ ℂ )
380 379 adantr ( ( 𝜑𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → ( 𝑍𝑋 ) ∈ ℂ )
381 380 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → ( 𝑍𝑋 ) ∈ ℂ )
382 381 negcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → - ( 𝑍𝑋 ) ∈ ℂ )
383 eqid { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } = { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) }
384 ioosscn ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ⊆ ℂ
385 384 sseli ( 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) → 𝑦 ∈ ℂ )
386 385 adantl ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑦 ∈ ℂ )
387 379 adantr ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑍𝑋 ) ∈ ℂ )
388 386 387 pncand ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( 𝑍𝑋 ) ) = 𝑦 )
389 388 eqcomd ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑦 = ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( 𝑍𝑋 ) ) )
390 389 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑦 = ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( 𝑍𝑋 ) ) )
391 377 oveq2d ( 𝜑 → ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( 𝑍𝑋 ) ) = ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
392 391 adantr ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( 𝑍𝑋 ) ) = ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
393 386 387 addcld ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑦 + ( 𝑍𝑋 ) ) ∈ ℂ )
394 376 recnd ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
395 394 adantr ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
396 393 395 negsubd ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) + - ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
397 374 zcnd ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℂ )
398 368 recnd ( 𝜑𝑇 ∈ ℂ )
399 397 398 mulneg1d ( 𝜑 → ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) = - ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
400 399 eqcomd ( 𝜑 → - ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) = ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
401 400 oveq2d ( 𝜑 → ( ( 𝑦 + ( 𝑍𝑋 ) ) + - ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
402 401 adantr ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) + - ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
403 392 396 402 3eqtr2d ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( 𝑍𝑋 ) ) = ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
404 403 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( 𝑍𝑋 ) ) = ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
405 374 znegcld ( 𝜑 → - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ )
406 405 adantr ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ )
407 406 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ )
408 simpl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝜑 )
409 213 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ⊆ 𝐷 )
410 189 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
411 132 rexrd ( 𝜑 → ( 𝐸𝑋 ) ∈ ℝ* )
412 411 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
413 elioore ( 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) → 𝑦 ∈ ℝ )
414 413 adantl ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑦 ∈ ℝ )
415 378 adantr ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑍𝑋 ) ∈ ℝ )
416 414 415 readdcld ( ( 𝜑𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑦 + ( 𝑍𝑋 ) ) ∈ ℝ )
417 416 adantlr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑦 + ( 𝑍𝑋 ) ) ∈ ℝ )
418 378 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑍𝑋 ) ∈ ℝ )
419 188 418 resubcld ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ∈ ℝ )
420 419 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ∈ ℝ* )
421 420 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ∈ ℝ* )
422 14 rexrd ( 𝜑𝑋 ∈ ℝ* )
423 422 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑋 ∈ ℝ* )
424 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) )
425 421 423 424 ioogtlbd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) < 𝑦 )
426 188 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑄𝑖 ) ∈ ℝ )
427 378 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑍𝑋 ) ∈ ℝ )
428 413 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑦 ∈ ℝ )
429 426 427 428 ltsubaddd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) < 𝑦 ↔ ( 𝑄𝑖 ) < ( 𝑦 + ( 𝑍𝑋 ) ) ) )
430 425 429 mpbid ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑄𝑖 ) < ( 𝑦 + ( 𝑍𝑋 ) ) )
431 14 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑋 ∈ ℝ )
432 421 423 424 iooltubd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑦 < 𝑋 )
433 428 431 427 432 ltadd1dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑦 + ( 𝑍𝑋 ) ) < ( 𝑋 + ( 𝑍𝑋 ) ) )
434 id ( 𝑥 = 𝑋𝑥 = 𝑋 )
435 fveq2 ( 𝑥 = 𝑋 → ( 𝑍𝑥 ) = ( 𝑍𝑋 ) )
436 434 435 oveq12d ( 𝑥 = 𝑋 → ( 𝑥 + ( 𝑍𝑥 ) ) = ( 𝑋 + ( 𝑍𝑋 ) ) )
437 14 378 readdcld ( 𝜑 → ( 𝑋 + ( 𝑍𝑋 ) ) ∈ ℝ )
438 16 436 14 437 fvmptd3 ( 𝜑 → ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑍𝑋 ) ) )
439 438 eqcomd ( 𝜑 → ( 𝑋 + ( 𝑍𝑋 ) ) = ( 𝐸𝑋 ) )
440 439 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑋 + ( 𝑍𝑋 ) ) = ( 𝐸𝑋 ) )
441 433 440 breqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑦 + ( 𝑍𝑋 ) ) < ( 𝐸𝑋 ) )
442 410 412 417 430 441 eliood ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑦 + ( 𝑍𝑋 ) ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) )
443 442 3adantl3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑦 + ( 𝑍𝑋 ) ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) )
444 409 443 sseldd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷 )
445 408 444 407 3jca ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝜑 ∧ ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷 ∧ - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) )
446 eleq1 ( 𝑘 = - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( 𝑘 ∈ ℤ ↔ - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) )
447 446 3anbi3d ( 𝑘 = - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( 𝜑 ∧ ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷𝑘 ∈ ℤ ) ↔ ( 𝜑 ∧ ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷 ∧ - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) ) )
448 oveq1 ( 𝑘 = - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( 𝑘 · 𝑇 ) = ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
449 448 oveq2d ( 𝑘 = - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( 𝑘 · 𝑇 ) ) = ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
450 449 eleq1d ( 𝑘 = - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ↔ ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ 𝐷 ) )
451 447 450 imbi12d ( 𝑘 = - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( ( 𝜑 ∧ ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷𝑘 ∈ ℤ ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ) ↔ ( ( 𝜑 ∧ ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷 ∧ - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ 𝐷 ) ) )
452 ovex ( 𝑦 + ( 𝑍𝑋 ) ) ∈ V
453 eleq1 ( 𝑥 = ( 𝑦 + ( 𝑍𝑋 ) ) → ( 𝑥𝐷 ↔ ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷 ) )
454 453 3anbi2d ( 𝑥 = ( 𝑦 + ( 𝑍𝑋 ) ) → ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) ↔ ( 𝜑 ∧ ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷𝑘 ∈ ℤ ) ) )
455 oveq1 ( 𝑥 = ( 𝑦 + ( 𝑍𝑋 ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( 𝑘 · 𝑇 ) ) )
456 455 eleq1d ( 𝑥 = ( 𝑦 + ( 𝑍𝑋 ) ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ↔ ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ) )
457 454 456 imbi12d ( 𝑥 = ( 𝑦 + ( 𝑍𝑋 ) ) → ( ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ) ↔ ( ( 𝜑 ∧ ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷𝑘 ∈ ℤ ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ) ) )
458 452 457 10 vtocl ( ( 𝜑 ∧ ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷𝑘 ∈ ℤ ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 )
459 451 458 vtoclg ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ → ( ( 𝜑 ∧ ( 𝑦 + ( 𝑍𝑋 ) ) ∈ 𝐷 ∧ - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ 𝐷 ) )
460 407 445 459 sylc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ 𝐷 )
461 404 460 eqeltrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ( 𝑦 + ( 𝑍𝑋 ) ) − ( 𝑍𝑋 ) ) ∈ 𝐷 )
462 390 461 eqeltrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑦𝐷 )
463 462 ssd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ⊆ 𝐷 )
464 188 recnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℂ )
465 379 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑍𝑋 ) ∈ ℂ )
466 464 465 negsubd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) + - ( 𝑍𝑋 ) ) = ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) )
467 466 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) = ( ( 𝑄𝑖 ) + - ( 𝑍𝑋 ) ) )
468 438 oveq1d ( 𝜑 → ( ( 𝐸𝑋 ) + - ( 𝑍𝑋 ) ) = ( ( 𝑋 + ( 𝑍𝑋 ) ) + - ( 𝑍𝑋 ) ) )
469 437 recnd ( 𝜑 → ( 𝑋 + ( 𝑍𝑋 ) ) ∈ ℂ )
470 469 379 negsubd ( 𝜑 → ( ( 𝑋 + ( 𝑍𝑋 ) ) + - ( 𝑍𝑋 ) ) = ( ( 𝑋 + ( 𝑍𝑋 ) ) − ( 𝑍𝑋 ) ) )
471 14 recnd ( 𝜑𝑋 ∈ ℂ )
472 471 379 pncand ( 𝜑 → ( ( 𝑋 + ( 𝑍𝑋 ) ) − ( 𝑍𝑋 ) ) = 𝑋 )
473 468 470 472 3eqtrrd ( 𝜑𝑋 = ( ( 𝐸𝑋 ) + - ( 𝑍𝑋 ) ) )
474 473 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 = ( ( 𝐸𝑋 ) + - ( 𝑍𝑋 ) ) )
475 467 474 oveq12d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) = ( ( ( 𝑄𝑖 ) + - ( 𝑍𝑋 ) ) (,) ( ( 𝐸𝑋 ) + - ( 𝑍𝑋 ) ) ) )
476 132 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐸𝑋 ) ∈ ℝ )
477 418 renegcld ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → - ( 𝑍𝑋 ) ∈ ℝ )
478 188 476 477 iooshift ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄𝑖 ) + - ( 𝑍𝑋 ) ) (,) ( ( 𝐸𝑋 ) + - ( 𝑍𝑋 ) ) ) = { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } )
479 475 478 eqtr2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } = ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) )
480 479 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } = ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) )
481 171 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → dom 𝐹 = 𝐷 )
482 463 480 481 3sstr4d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } ⊆ dom 𝐹 )
483 482 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } ⊆ dom 𝐹 )
484 377 negeqd ( 𝜑 → - ( 𝑍𝑋 ) = - ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
485 484 400 eqtrd ( 𝜑 → - ( 𝑍𝑋 ) = ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
486 485 oveq2d ( 𝜑 → ( 𝑥 + - ( 𝑍𝑋 ) ) = ( 𝑥 + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
487 486 fveq2d ( 𝜑 → ( 𝐹 ‘ ( 𝑥 + - ( 𝑍𝑋 ) ) ) = ( 𝐹 ‘ ( 𝑥 + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) )
488 487 adantr ( ( 𝜑𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑥 + - ( 𝑍𝑋 ) ) ) = ( 𝐹 ‘ ( 𝑥 + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) )
489 488 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑥 + - ( 𝑍𝑋 ) ) ) = ( 𝐹 ‘ ( 𝑥 + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) )
490 405 adantr ( ( 𝜑𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) → - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ )
491 490 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) → - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ )
492 simpl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) → 𝜑 )
493 213 sselda ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) → 𝑥𝐷 )
494 492 493 491 3jca ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) → ( 𝜑𝑥𝐷 ∧ - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) )
495 446 3anbi3d ( 𝑘 = - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) ↔ ( 𝜑𝑥𝐷 ∧ - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) ) )
496 448 oveq2d ( 𝑘 = - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = ( 𝑥 + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
497 496 fveqeq2d ( 𝑘 = - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ↔ ( 𝐹 ‘ ( 𝑥 + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) )
498 495 497 imbi12d ( 𝑘 = - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) ↔ ( ( 𝜑𝑥𝐷 ∧ - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) ) )
499 498 11 vtoclg ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ → ( ( 𝜑𝑥𝐷 ∧ - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) )
500 491 494 499 sylc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑥 + ( - ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹𝑥 ) )
501 489 500 eqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑥 + - ( 𝑍𝑋 ) ) ) = ( 𝐹𝑥 ) )
502 501 adantlr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑥 + - ( 𝑍𝑋 ) ) ) = ( 𝐹𝑥 ) )
503 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
504 356 358 362 382 383 483 502 503 limcperiod ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → 𝑦 ∈ ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } ) lim ( ( 𝐸𝑋 ) + - ( 𝑍𝑋 ) ) ) )
505 479 reseq2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } ) = ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) )
506 474 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐸𝑋 ) + - ( 𝑍𝑋 ) ) = 𝑋 )
507 505 506 oveq12d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } ) lim ( ( 𝐸𝑋 ) + - ( 𝑍𝑋 ) ) ) = ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) )
508 507 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } ) lim ( ( 𝐸𝑋 ) + - ( 𝑍𝑋 ) ) ) = ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) )
509 508 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) 𝑧 = ( 𝑥 + - ( 𝑍𝑋 ) ) } ) lim ( ( 𝐸𝑋 ) + - ( 𝑍𝑋 ) ) ) = ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) )
510 504 509 eleqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) → 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) )
511 354 adantr ( ( 𝜑𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
512 511 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
513 384 a1i ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ⊆ ℂ )
514 463 481 sseqtrrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ⊆ dom 𝐹 )
515 514 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ⊆ dom 𝐹 )
516 379 adantr ( ( 𝜑𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → ( 𝑍𝑋 ) ∈ ℂ )
517 516 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → ( 𝑍𝑋 ) ∈ ℂ )
518 eqid { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } = { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) }
519 464 465 npcand ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) + ( 𝑍𝑋 ) ) = ( 𝑄𝑖 ) )
520 519 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) = ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) + ( 𝑍𝑋 ) ) )
521 438 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑍𝑋 ) ) )
522 520 521 oveq12d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) = ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) + ( 𝑍𝑋 ) ) (,) ( 𝑋 + ( 𝑍𝑋 ) ) ) )
523 14 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
524 419 523 418 iooshift ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) + ( 𝑍𝑋 ) ) (,) ( 𝑋 + ( 𝑍𝑋 ) ) ) = { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } )
525 522 524 eqtr2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } = ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) )
526 525 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } = ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) )
527 213 526 481 3sstr4d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } ⊆ dom 𝐹 )
528 527 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } ⊆ dom 𝐹 )
529 377 oveq2d ( 𝜑 → ( 𝑥 + ( 𝑍𝑋 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
530 529 fveq2d ( 𝜑 → ( 𝐹 ‘ ( 𝑥 + ( 𝑍𝑋 ) ) ) = ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) )
531 530 adantr ( ( 𝜑𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑍𝑋 ) ) ) = ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) )
532 531 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑍𝑋 ) ) ) = ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) )
533 374 adantr ( ( 𝜑𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ )
534 533 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ )
535 simpl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝜑 )
536 463 sselda ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑥𝐷 )
537 535 536 534 3jca ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝜑𝑥𝐷 ∧ ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) )
538 eleq1 ( 𝑘 = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( 𝑘 ∈ ℤ ↔ ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) )
539 538 3anbi3d ( 𝑘 = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) ↔ ( 𝜑𝑥𝐷 ∧ ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) ) )
540 oveq1 ( 𝑘 = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( 𝑘 · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
541 540 oveq2d ( 𝑘 = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
542 541 fveqeq2d ( 𝑘 = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ↔ ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) )
543 539 542 imbi12d ( 𝑘 = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) ↔ ( ( 𝜑𝑥𝐷 ∧ ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) ) )
544 543 11 vtoclg ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ → ( ( 𝜑𝑥𝐷 ∧ ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) )
545 534 537 544 sylc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝐹𝑥 ) )
546 532 545 eqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑍𝑋 ) ) ) = ( 𝐹𝑥 ) )
547 546 adantlr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑍𝑋 ) ) ) = ( 𝐹𝑥 ) )
548 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) )
549 512 513 515 517 518 528 547 548 limcperiod ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → 𝑦 ∈ ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } ) lim ( 𝑋 + ( 𝑍𝑋 ) ) ) )
550 525 reseq2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } ) = ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) )
551 439 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑋 + ( 𝑍𝑋 ) ) = ( 𝐸𝑋 ) )
552 550 551 oveq12d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } ) lim ( 𝑋 + ( 𝑍𝑋 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
553 552 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } ) lim ( 𝑋 + ( 𝑍𝑋 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
554 553 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) 𝑧 = ( 𝑥 + ( 𝑍𝑋 ) ) } ) lim ( 𝑋 + ( 𝑍𝑋 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
555 549 554 eleqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) → 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
556 510 555 impbida ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ↔ 𝑦 ∈ ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) ) )
557 556 eqrdv ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) = ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) )
558 resindm ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( -∞ (,) 𝑋 ) )
559 171 ineq2d ( 𝜑 → ( ( -∞ (,) 𝑋 ) ∩ dom 𝐹 ) = ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) )
560 559 reseq2d ( 𝜑 → ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ) )
561 558 560 eqtr3id ( 𝜑 → ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) = ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ) )
562 561 oveq1d ( 𝜑 → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ) lim 𝑋 ) )
563 562 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ) lim 𝑋 ) )
564 inss2 ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ⊆ 𝐷
565 564 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ⊆ 𝐷 )
566 180 565 fssresd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ) : ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ⟶ ℂ )
567 420 mnfled ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → -∞ ≤ ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) )
568 iooss1 ( ( -∞ ∈ ℝ* ∧ -∞ ≤ ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ⊆ ( -∞ (,) 𝑋 ) )
569 184 567 568 sylancr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ⊆ ( -∞ (,) 𝑋 ) )
570 569 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ⊆ ( -∞ (,) 𝑋 ) )
571 570 463 ssind ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ⊆ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) )
572 216 ssinss2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ⊆ ℂ )
573 eqid ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
574 420 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ∈ ℝ* )
575 422 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ* )
576 438 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑍𝑋 ) ) )
577 222 576 breqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) < ( 𝑋 + ( 𝑍𝑋 ) ) )
578 378 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑍𝑋 ) ∈ ℝ )
579 14 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
580 199 578 579 ltsubaddd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) < 𝑋 ↔ ( 𝑄𝑖 ) < ( 𝑋 + ( 𝑍𝑋 ) ) ) )
581 577 580 mpbird ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) < 𝑋 )
582 14 leidd ( 𝜑𝑋𝑋 )
583 582 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋𝑋 )
584 574 575 575 581 583 eliocd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) )
585 ioounsn ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ∈ ℝ*𝑋 ∈ ℝ* ∧ ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) < 𝑋 ) → ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ∪ { 𝑋 } ) = ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) )
586 574 575 581 585 syl3anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ∪ { 𝑋 } ) = ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) )
587 586 fveq2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ∪ { 𝑋 } ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) )
588 ovex ( -∞ (,) 𝑋 ) ∈ V
589 588 inex1 ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∈ V
590 snex { 𝑋 } ∈ V
591 589 590 unex ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ∈ V
592 resttop ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ∈ V ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ Top )
593 228 591 592 mp2an ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ Top
594 iooretop ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∈ ( topGen ‘ ran (,) )
595 594 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∈ ( topGen ‘ ran (,) ) )
596 elrestr ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ∈ V ∧ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∈ ( topGen ‘ ran (,) ) ) → ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
597 235 591 595 596 mp3an12i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
598 420 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ∈ ℝ* )
599 241 a1i ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → +∞ ∈ ℝ* )
600 14 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → 𝑋 ∈ ℝ )
601 iocssre ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ∈ ℝ*𝑋 ∈ ℝ ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ⊆ ℝ )
602 598 600 601 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ⊆ ℝ )
603 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) )
604 602 603 sseldd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → 𝑥 ∈ ℝ )
605 422 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → 𝑋 ∈ ℝ* )
606 598 605 603 iocgtlbd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) < 𝑥 )
607 604 ltpnfd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → 𝑥 < +∞ )
608 598 599 604 606 607 eliood ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) )
609 608 3adantl3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) )
610 eqvisset ( 𝑥 = 𝑋𝑋 ∈ V )
611 snidg ( 𝑋 ∈ V → 𝑋 ∈ { 𝑋 } )
612 610 611 syl ( 𝑥 = 𝑋𝑋 ∈ { 𝑋 } )
613 434 612 eqeltrd ( 𝑥 = 𝑋𝑥 ∈ { 𝑋 } )
614 elun2 ( 𝑥 ∈ { 𝑋 } → 𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
615 613 614 syl ( 𝑥 = 𝑋𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
616 615 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ 𝑥 = 𝑋 ) → 𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
617 simpll ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
618 420 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ∈ ℝ* )
619 422 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑋 ∈ ℝ* )
620 604 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ℝ )
621 606 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) < 𝑥 )
622 14 ad3antrrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑋 ∈ ℝ )
623 598 605 603 iocleubd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → 𝑥𝑋 )
624 623 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥𝑋 )
625 434 eqcoms ( 𝑋 = 𝑥𝑥 = 𝑋 )
626 625 necon3bi ( ¬ 𝑥 = 𝑋𝑋𝑥 )
627 626 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑋𝑥 )
628 620 622 624 627 leneltd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 < 𝑋 )
629 618 619 620 621 628 eliood ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) )
630 629 3adantll3 ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) )
631 571 sselda ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑥 ∈ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) )
632 elun1 ( 𝑥 ∈ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) → 𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
633 631 632 syl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) → 𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
634 617 630 633 syl2anc ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
635 616 634 pm2.61dan ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → 𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
636 609 635 elind ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) → 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
637 574 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ∈ ℝ* )
638 575 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑋 ∈ ℝ* )
639 elinel1 ( 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) )
640 elioore ( 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) → 𝑥 ∈ ℝ )
641 639 640 syl ( 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) → 𝑥 ∈ ℝ )
642 641 rexrd ( 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) → 𝑥 ∈ ℝ* )
643 642 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑥 ∈ ℝ* )
644 420 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) ∈ ℝ* )
645 241 a1i ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → +∞ ∈ ℝ* )
646 639 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) )
647 644 645 646 ioogtlbd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) < 𝑥 )
648 647 3adantl3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) < 𝑥 )
649 elinel2 ( 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) → 𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
650 elsni ( 𝑥 ∈ { 𝑋 } → 𝑥 = 𝑋 )
651 650 adantl ( ( 𝜑𝑥 ∈ { 𝑋 } ) → 𝑥 = 𝑋 )
652 582 adantr ( ( 𝜑𝑥 ∈ { 𝑋 } ) → 𝑋𝑋 )
653 651 652 eqbrtrd ( ( 𝜑𝑥 ∈ { 𝑋 } ) → 𝑥𝑋 )
654 653 adantlr ( ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ 𝑥 ∈ { 𝑋 } ) → 𝑥𝑋 )
655 simpll ( ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 ∈ { 𝑋 } ) → 𝜑 )
656 elunnel2 ( ( 𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ∧ ¬ 𝑥 ∈ { 𝑋 } ) → 𝑥 ∈ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) )
657 656 adantll ( ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 ∈ { 𝑋 } ) → 𝑥 ∈ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) )
658 657 elin1d ( ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 ∈ { 𝑋 } ) → 𝑥 ∈ ( -∞ (,) 𝑋 ) )
659 elioore ( 𝑥 ∈ ( -∞ (,) 𝑋 ) → 𝑥 ∈ ℝ )
660 659 adantl ( ( 𝜑𝑥 ∈ ( -∞ (,) 𝑋 ) ) → 𝑥 ∈ ℝ )
661 14 adantr ( ( 𝜑𝑥 ∈ ( -∞ (,) 𝑋 ) ) → 𝑋 ∈ ℝ )
662 184 a1i ( ( 𝜑𝑥 ∈ ( -∞ (,) 𝑋 ) ) → -∞ ∈ ℝ* )
663 422 adantr ( ( 𝜑𝑥 ∈ ( -∞ (,) 𝑋 ) ) → 𝑋 ∈ ℝ* )
664 simpr ( ( 𝜑𝑥 ∈ ( -∞ (,) 𝑋 ) ) → 𝑥 ∈ ( -∞ (,) 𝑋 ) )
665 662 663 664 iooltubd ( ( 𝜑𝑥 ∈ ( -∞ (,) 𝑋 ) ) → 𝑥 < 𝑋 )
666 660 661 665 ltled ( ( 𝜑𝑥 ∈ ( -∞ (,) 𝑋 ) ) → 𝑥𝑋 )
667 655 658 666 syl2anc ( ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 ∈ { 𝑋 } ) → 𝑥𝑋 )
668 654 667 pm2.61dan ( ( 𝜑𝑥 ∈ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) → 𝑥𝑋 )
669 649 668 sylan2 ( ( 𝜑𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑥𝑋 )
670 669 3ad2antl1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑥𝑋 )
671 637 638 643 648 670 eliocd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) )
672 636 671 impbida ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥 ∈ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ↔ 𝑥 ∈ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) )
673 672 eqrdv ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) = ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) +∞ ) ∩ ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
674 8 ssinss2d ( 𝜑 → ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ⊆ ℝ )
675 14 snssd ( 𝜑 → { 𝑋 } ⊆ ℝ )
676 674 675 unssd ( 𝜑 → ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ⊆ ℝ )
677 676 3ad2ant1 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ⊆ ℝ )
678 218 342 rerest ( ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
679 677 678 syl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
680 597 673 679 3eltr4d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
681 isopn3i ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ Top ∧ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) = ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) )
682 593 680 681 sylancr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) ) = ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) )
683 587 682 eqtr2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,] 𝑋 ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ∪ { 𝑋 } ) ) )
684 584 683 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ∪ { 𝑋 } ) ) )
685 566 571 572 218 573 684 limcres ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ) ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ) lim 𝑋 ) )
686 571 resabs1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ) ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) = ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) )
687 686 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ↾ ( ( -∞ (,) 𝑋 ) ∩ 𝐷 ) ) ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) )
688 563 685 687 3eqtr2rd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( ( 𝑄𝑖 ) − ( 𝑍𝑋 ) ) (,) 𝑋 ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 ) )
689 353 557 688 3eqtrrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
690 689 rexlimdv3a ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ) )
691 169 690 mpd ( 𝜑 → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
692 119 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
693 12 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
694 13 3adant3 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
695 eqid if ( ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝐸𝑋 ) ) ) = if ( ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝐸𝑋 ) ) )
696 eqid ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
697 199 197 692 693 694 199 220 222 204 695 696 fourierdlem33 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝐸𝑋 ) ) ) ∈ ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
698 204 resabs1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) = ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) )
699 698 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
700 697 699 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝐸𝑋 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) )
701 700 ne0d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ≠ ∅ )
702 353 701 eqnetrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ≠ ∅ )
703 702 rexlimdv3a ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ≠ ∅ ) )
704 169 703 mpd ( 𝜑 → ( ( 𝐹 ↾ ( -∞ (,) ( 𝐸𝑋 ) ) ) lim ( 𝐸𝑋 ) ) ≠ ∅ )
705 691 704 eqnetrd ( 𝜑 → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim 𝑋 ) ≠ ∅ )