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