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