Metamath Proof Explorer


Theorem fourierdlem48

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

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

Proof

Step Hyp Ref Expression
1 fourierdlem48.a ( 𝜑𝐴 ∈ ℝ )
2 fourierdlem48.b ( 𝜑𝐵 ∈ ℝ )
3 fourierdlem48.altb ( 𝜑𝐴 < 𝐵 )
4 fourierdlem48.p 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
5 fourierdlem48.t 𝑇 = ( 𝐵𝐴 )
6 fourierdlem48.m ( 𝜑𝑀 ∈ ℕ )
7 fourierdlem48.q ( 𝜑𝑄 ∈ ( 𝑃𝑀 ) )
8 fourierdlem48.f ( 𝜑𝐹 : 𝐷 ⟶ ℝ )
9 fourierdlem48.dper ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 )
10 fourierdlem48.per ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) )
11 fourierdlem48.cn ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
12 fourierdlem48.r ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
13 fourierdlem48.x ( 𝜑𝑋 ∈ ℝ )
14 fourierdlem48.z 𝑍 = ( 𝑥 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) )
15 fourierdlem48.e 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( 𝑍𝑥 ) ) )
16 fourierdlem48.ch ( 𝜒 ↔ ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
17 simpl ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → 𝜑 )
18 fveq2 ( 𝑖 = 0 → ( 𝑄𝑖 ) = ( 𝑄 ‘ 0 ) )
19 fvoveq1 ( 𝑖 = 0 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 0 + 1 ) ) )
20 18 19 oveq12d ( 𝑖 = 0 → ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) )
21 20 eleq2d ( 𝑖 = 0 → ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) ) )
22 21 anbi1d ( 𝑖 = 0 → ( ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ↔ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) )
23 22 rexbidv ( 𝑖 = 0 → ( ∃ 𝑘 ∈ ℤ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ↔ ∃ 𝑘 ∈ ℤ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) )
24 0zd ( 𝜑 → 0 ∈ ℤ )
25 6 nnzd ( 𝜑𝑀 ∈ ℤ )
26 6 nngt0d ( 𝜑 → 0 < 𝑀 )
27 fzolb ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
28 24 25 26 27 syl3anbrc ( 𝜑 → 0 ∈ ( 0 ..^ 𝑀 ) )
29 28 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → 0 ∈ ( 0 ..^ 𝑀 ) )
30 2 13 resubcld ( 𝜑 → ( 𝐵𝑋 ) ∈ ℝ )
31 2 1 resubcld ( 𝜑 → ( 𝐵𝐴 ) ∈ ℝ )
32 5 31 eqeltrid ( 𝜑𝑇 ∈ ℝ )
33 1 2 posdifd ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵𝐴 ) ) )
34 3 33 mpbid ( 𝜑 → 0 < ( 𝐵𝐴 ) )
35 34 5 breqtrrdi ( 𝜑 → 0 < 𝑇 )
36 35 gt0ne0d ( 𝜑𝑇 ≠ 0 )
37 30 32 36 redivcld ( 𝜑 → ( ( 𝐵𝑋 ) / 𝑇 ) ∈ ℝ )
38 37 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → ( ( 𝐵𝑋 ) / 𝑇 ) ∈ ℝ )
39 38 flcld ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ )
40 1zzd ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → 1 ∈ ℤ )
41 39 40 zsubcld ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) ∈ ℤ )
42 id ( ( 𝐸𝑋 ) = 𝐵 → ( 𝐸𝑋 ) = 𝐵 )
43 5 a1i ( ( 𝐸𝑋 ) = 𝐵𝑇 = ( 𝐵𝐴 ) )
44 42 43 oveq12d ( ( 𝐸𝑋 ) = 𝐵 → ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝐵 − ( 𝐵𝐴 ) ) )
45 2 recnd ( 𝜑𝐵 ∈ ℂ )
46 1 recnd ( 𝜑𝐴 ∈ ℂ )
47 45 46 nncand ( 𝜑 → ( 𝐵 − ( 𝐵𝐴 ) ) = 𝐴 )
48 44 47 sylan9eqr ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → ( ( 𝐸𝑋 ) − 𝑇 ) = 𝐴 )
49 4 fourierdlem2 ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
50 6 49 syl ( 𝜑 → ( 𝑄 ∈ ( 𝑃𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
51 7 50 mpbid ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
52 51 simpld ( 𝜑𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
53 elmapi ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
54 52 53 syl ( 𝜑𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
55 6 nnnn0d ( 𝜑𝑀 ∈ ℕ0 )
56 nn0uz 0 = ( ℤ ‘ 0 )
57 55 56 eleqtrdi ( 𝜑𝑀 ∈ ( ℤ ‘ 0 ) )
58 eluzfz1 ( 𝑀 ∈ ( ℤ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
59 57 58 syl ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
60 54 59 ffvelcdmd ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
61 60 rexrd ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ* )
62 1zzd ( 𝜑 → 1 ∈ ℤ )
63 0le1 0 ≤ 1
64 63 a1i ( 𝜑 → 0 ≤ 1 )
65 6 nnge1d ( 𝜑 → 1 ≤ 𝑀 )
66 24 25 62 64 65 elfzd ( 𝜑 → 1 ∈ ( 0 ... 𝑀 ) )
67 54 66 ffvelcdmd ( 𝜑 → ( 𝑄 ‘ 1 ) ∈ ℝ )
68 67 rexrd ( 𝜑 → ( 𝑄 ‘ 1 ) ∈ ℝ* )
69 1 rexrd ( 𝜑𝐴 ∈ ℝ* )
70 51 simprd ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
71 70 simplld ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
72 1 leidd ( 𝜑𝐴𝐴 )
73 71 72 eqbrtrd ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ 𝐴 )
74 71 eqcomd ( 𝜑𝐴 = ( 𝑄 ‘ 0 ) )
75 18 19 breq12d ( 𝑖 = 0 → ( ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) ) )
76 51 simprrd ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
77 75 76 28 rspcdva ( 𝜑 → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) )
78 1e0p1 1 = ( 0 + 1 )
79 78 fveq2i ( 𝑄 ‘ 1 ) = ( 𝑄 ‘ ( 0 + 1 ) )
80 77 79 breqtrrdi ( 𝜑 → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ 1 ) )
81 74 80 eqbrtrd ( 𝜑𝐴 < ( 𝑄 ‘ 1 ) )
82 61 68 69 73 81 elicod ( 𝜑𝐴 ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ 1 ) ) )
83 79 oveq2i ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ 1 ) ) = ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) )
84 82 83 eleqtrdi ( 𝜑𝐴 ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) )
85 84 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → 𝐴 ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) )
86 48 85 eqeltrd ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) )
87 id ( 𝑥 = 𝑋𝑥 = 𝑋 )
88 fveq2 ( 𝑥 = 𝑋 → ( 𝑍𝑥 ) = ( 𝑍𝑋 ) )
89 87 88 oveq12d ( 𝑥 = 𝑋 → ( 𝑥 + ( 𝑍𝑥 ) ) = ( 𝑋 + ( 𝑍𝑋 ) ) )
90 oveq2 ( 𝑥 = 𝑋 → ( 𝐵𝑥 ) = ( 𝐵𝑋 ) )
91 90 fvoveq1d ( 𝑥 = 𝑋 → ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) )
92 91 oveq1d ( 𝑥 = 𝑋 → ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
93 37 flcld ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℤ )
94 93 zred ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℝ )
95 94 32 remulcld ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
96 14 92 13 95 fvmptd3 ( 𝜑 → ( 𝑍𝑋 ) = ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
97 96 95 eqeltrd ( 𝜑 → ( 𝑍𝑋 ) ∈ ℝ )
98 13 97 readdcld ( 𝜑 → ( 𝑋 + ( 𝑍𝑋 ) ) ∈ ℝ )
99 15 89 13 98 fvmptd3 ( 𝜑 → ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑍𝑋 ) ) )
100 96 oveq2d ( 𝜑 → ( 𝑋 + ( 𝑍𝑋 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
101 99 100 eqtrd ( 𝜑 → ( 𝐸𝑋 ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
102 101 oveq1d ( 𝜑 → ( ( 𝐸𝑋 ) − 𝑇 ) = ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑇 ) )
103 13 recnd ( 𝜑𝑋 ∈ ℂ )
104 95 recnd ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
105 32 recnd ( 𝜑𝑇 ∈ ℂ )
106 103 104 105 addsubassd ( 𝜑 → ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑇 ) = ( 𝑋 + ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) − 𝑇 ) ) )
107 93 zcnd ( 𝜑 → ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) ∈ ℂ )
108 107 105 mulsubfacd ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) − 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) )
109 108 oveq2d ( 𝜑 → ( 𝑋 + ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) − 𝑇 ) ) = ( 𝑋 + ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) )
110 102 106 109 3eqtrd ( 𝜑 → ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) )
111 110 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) )
112 oveq1 ( 𝑘 = ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) → ( 𝑘 · 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) )
113 112 oveq2d ( 𝑘 = ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) → ( 𝑋 + ( 𝑘 · 𝑇 ) ) = ( 𝑋 + ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) )
114 113 eqeq2d ( 𝑘 = ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) → ( ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ↔ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) ) )
115 114 anbi2d ( 𝑘 = ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) → ( ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ↔ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) ) ) )
116 115 rspcev ( ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) ∈ ℤ ∧ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) − 1 ) · 𝑇 ) ) ) ) → ∃ 𝑘 ∈ ℤ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
117 41 86 111 116 syl12anc ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → ∃ 𝑘 ∈ ℤ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄 ‘ 0 ) [,) ( 𝑄 ‘ ( 0 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
118 23 29 117 rspcedvdw ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
119 ovex ( ( 𝐸𝑋 ) − 𝑇 ) ∈ V
120 eleq1 ( 𝑦 = ( ( 𝐸𝑋 ) − 𝑇 ) → ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
121 eqeq1 ( 𝑦 = ( ( 𝐸𝑋 ) − 𝑇 ) → ( 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ↔ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
122 120 121 anbi12d ( 𝑦 = ( ( 𝐸𝑋 ) − 𝑇 ) → ( ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ↔ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) )
123 122 2rexbidv ( 𝑦 = ( ( 𝐸𝑋 ) − 𝑇 ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) )
124 123 anbi2d ( 𝑦 = ( ( 𝐸𝑋 ) − 𝑇 ) → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) ↔ ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) ) )
125 124 imbi1d ( 𝑦 = ( ( 𝐸𝑋 ) − 𝑇 ) → ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ ) ↔ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ ) ) )
126 simpr ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
127 nfv 𝑖 𝜑
128 nfre1 𝑖𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
129 127 128 nfan 𝑖 ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
130 nfv 𝑘 𝜑
131 nfcv 𝑘 ( 0 ..^ 𝑀 )
132 nfre1 𝑘𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
133 131 132 nfrexw 𝑘𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
134 130 133 nfan 𝑘 ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
135 simp1 ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → 𝜑 )
136 simp2l ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
137 simp3l ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
138 135 136 137 jca31 ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
139 simp2r ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → 𝑘 ∈ ℤ )
140 simp3r ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
141 resindm ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( 𝑋 (,) +∞ ) )
142 16 biimpi ( 𝜒 → ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
143 142 simplld ( 𝜒 → ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
144 143 simplld ( 𝜒𝜑 )
145 fdm ( 𝐹 : 𝐷 ⟶ ℝ → dom 𝐹 = 𝐷 )
146 144 8 145 3syl ( 𝜒 → dom 𝐹 = 𝐷 )
147 146 ineq2d ( 𝜒 → ( ( 𝑋 (,) +∞ ) ∩ dom 𝐹 ) = ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) )
148 147 reseq2d ( 𝜒 → ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ dom 𝐹 ) ) = ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ) )
149 141 148 eqtr3id ( 𝜒 → ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) = ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ) )
150 149 oveq1d ( 𝜒 → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ) lim 𝑋 ) )
151 144 8 syl ( 𝜒𝐹 : 𝐷 ⟶ ℝ )
152 ax-resscn ℝ ⊆ ℂ
153 152 a1i ( 𝜒 → ℝ ⊆ ℂ )
154 151 153 fssd ( 𝜒𝐹 : 𝐷 ⟶ ℂ )
155 inss2 ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ⊆ 𝐷
156 155 a1i ( 𝜒 → ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ⊆ 𝐷 )
157 154 156 fssresd ( 𝜒 → ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ) : ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ⟶ ℂ )
158 pnfxr +∞ ∈ ℝ*
159 158 a1i ( 𝜒 → +∞ ∈ ℝ* )
160 143 simplrd ( 𝜒𝑖 ∈ ( 0 ..^ 𝑀 ) )
161 54 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
162 fzofzp1 ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
163 162 adantl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
164 161 163 ffvelcdmd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
165 144 160 164 syl2anc ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
166 142 simplrd ( 𝜒𝑘 ∈ ℤ )
167 166 zred ( 𝜒𝑘 ∈ ℝ )
168 144 32 syl ( 𝜒𝑇 ∈ ℝ )
169 167 168 remulcld ( 𝜒 → ( 𝑘 · 𝑇 ) ∈ ℝ )
170 165 169 resubcld ( 𝜒 → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ∈ ℝ )
171 170 rexrd ( 𝜒 → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ∈ ℝ* )
172 171 pnfged ( 𝜒 → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ≤ +∞ )
173 iooss2 ( ( +∞ ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ≤ +∞ ) → ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ ( 𝑋 (,) +∞ ) )
174 159 172 173 syl2anc ( 𝜒 → ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ ( 𝑋 (,) +∞ ) )
175 166 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑘 ∈ ℤ )
176 175 zcnd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑘 ∈ ℂ )
177 168 recnd ( 𝜒𝑇 ∈ ℂ )
178 177 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑇 ∈ ℂ )
179 176 178 mulneg1d ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( - 𝑘 · 𝑇 ) = - ( 𝑘 · 𝑇 ) )
180 179 oveq2d ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) = ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + - ( 𝑘 · 𝑇 ) ) )
181 elioore ( 𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) → 𝑤 ∈ ℝ )
182 181 recnd ( 𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) → 𝑤 ∈ ℂ )
183 182 adantl ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑤 ∈ ℂ )
184 176 178 mulcld ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑘 · 𝑇 ) ∈ ℂ )
185 183 184 addcld ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ℂ )
186 185 184 negsubd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + - ( 𝑘 · 𝑇 ) ) = ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) − ( 𝑘 · 𝑇 ) ) )
187 183 184 pncand ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) − ( 𝑘 · 𝑇 ) ) = 𝑤 )
188 180 186 187 3eqtrrd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑤 = ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) )
189 144 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝜑 )
190 143 simpld ( 𝜒 → ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) )
191 cncff ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
192 fdm ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ → dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
193 11 191 192 3syl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
194 ssdmres ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
195 193 194 sylibr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
196 8 fdmd ( 𝜑 → dom 𝐹 = 𝐷 )
197 196 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom 𝐹 = 𝐷 )
198 195 197 sseqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ 𝐷 )
199 190 198 syl ( 𝜒 → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ 𝐷 )
200 199 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ 𝐷 )
201 elfzofz ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
202 201 adantl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
203 161 202 ffvelcdmd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℝ )
204 144 160 203 syl2anc ( 𝜒 → ( 𝑄𝑖 ) ∈ ℝ )
205 204 rexrd ( 𝜒 → ( 𝑄𝑖 ) ∈ ℝ* )
206 205 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
207 165 rexrd ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
208 207 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
209 181 adantl ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑤 ∈ ℝ )
210 175 zred ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑘 ∈ ℝ )
211 189 32 syl ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑇 ∈ ℝ )
212 210 211 remulcld ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
213 209 212 readdcld ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ℝ )
214 204 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑄𝑖 ) ∈ ℝ )
215 144 13 syl ( 𝜒𝑋 ∈ ℝ )
216 215 169 readdcld ( 𝜒 → ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ ℝ )
217 216 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ ℝ )
218 16 simprbi ( 𝜒𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
219 218 eqcomd ( 𝜒 → ( 𝑋 + ( 𝑘 · 𝑇 ) ) = 𝑦 )
220 143 simprd ( 𝜒𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
221 219 220 eqeltrd ( 𝜒 → ( 𝑋 + ( 𝑘 · 𝑇 ) ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
222 205 207 221 icogelbd ( 𝜒 → ( 𝑄𝑖 ) ≤ ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
223 222 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑄𝑖 ) ≤ ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
224 189 13 syl ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑋 ∈ ℝ )
225 224 rexrd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑋 ∈ ℝ* )
226 165 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
227 226 212 resubcld ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ∈ ℝ )
228 227 rexrd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ∈ ℝ* )
229 simpr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
230 225 228 229 ioogtlbd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑋 < 𝑤 )
231 224 209 212 230 ltadd1dd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑋 + ( 𝑘 · 𝑇 ) ) < ( 𝑤 + ( 𝑘 · 𝑇 ) ) )
232 214 217 213 223 231 lelttrd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑄𝑖 ) < ( 𝑤 + ( 𝑘 · 𝑇 ) ) )
233 225 228 229 iooltubd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑤 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) )
234 209 227 212 233 ltadd1dd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) < ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) )
235 165 recnd ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
236 169 recnd ( 𝜒 → ( 𝑘 · 𝑇 ) ∈ ℂ )
237 235 236 npcand ( 𝜒 → ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
238 237 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
239 234 238 breqtrd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
240 206 208 213 232 239 eliood ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
241 200 240 sseldd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 )
242 175 znegcld ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → - 𝑘 ∈ ℤ )
243 ovex ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ V
244 eleq1 ( 𝑥 = ( 𝑤 + ( 𝑘 · 𝑇 ) ) → ( 𝑥𝐷 ↔ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ) )
245 244 3anbi2d ( 𝑥 = ( 𝑤 + ( 𝑘 · 𝑇 ) ) → ( ( 𝜑𝑥𝐷 ∧ - 𝑘 ∈ ℤ ) ↔ ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ∧ - 𝑘 ∈ ℤ ) ) )
246 oveq1 ( 𝑥 = ( 𝑤 + ( 𝑘 · 𝑇 ) ) → ( 𝑥 + ( - 𝑘 · 𝑇 ) ) = ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) )
247 246 eleq1d ( 𝑥 = ( 𝑤 + ( 𝑘 · 𝑇 ) ) → ( ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 ↔ ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 ) )
248 245 247 imbi12d ( 𝑥 = ( 𝑤 + ( 𝑘 · 𝑇 ) ) → ( ( ( 𝜑𝑥𝐷 ∧ - 𝑘 ∈ ℤ ) → ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 ) ↔ ( ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ∧ - 𝑘 ∈ ℤ ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 ) ) )
249 negex - 𝑘 ∈ V
250 eleq1 ( 𝑗 = - 𝑘 → ( 𝑗 ∈ ℤ ↔ - 𝑘 ∈ ℤ ) )
251 250 3anbi3d ( 𝑗 = - 𝑘 → ( ( 𝜑𝑥𝐷𝑗 ∈ ℤ ) ↔ ( 𝜑𝑥𝐷 ∧ - 𝑘 ∈ ℤ ) ) )
252 oveq1 ( 𝑗 = - 𝑘 → ( 𝑗 · 𝑇 ) = ( - 𝑘 · 𝑇 ) )
253 252 oveq2d ( 𝑗 = - 𝑘 → ( 𝑥 + ( 𝑗 · 𝑇 ) ) = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) )
254 253 eleq1d ( 𝑗 = - 𝑘 → ( ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 ↔ ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 ) )
255 251 254 imbi12d ( 𝑗 = - 𝑘 → ( ( ( 𝜑𝑥𝐷𝑗 ∈ ℤ ) → ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 ) ↔ ( ( 𝜑𝑥𝐷 ∧ - 𝑘 ∈ ℤ ) → ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 ) ) )
256 eleq1 ( 𝑘 = 𝑗 → ( 𝑘 ∈ ℤ ↔ 𝑗 ∈ ℤ ) )
257 256 3anbi3d ( 𝑘 = 𝑗 → ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) ↔ ( 𝜑𝑥𝐷𝑗 ∈ ℤ ) ) )
258 oveq1 ( 𝑘 = 𝑗 → ( 𝑘 · 𝑇 ) = ( 𝑗 · 𝑇 ) )
259 258 oveq2d ( 𝑘 = 𝑗 → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = ( 𝑥 + ( 𝑗 · 𝑇 ) ) )
260 259 eleq1d ( 𝑘 = 𝑗 → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ↔ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 ) )
261 257 260 imbi12d ( 𝑘 = 𝑗 → ( ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ) ↔ ( ( 𝜑𝑥𝐷𝑗 ∈ ℤ ) → ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 ) ) )
262 261 9 chvarvv ( ( 𝜑𝑥𝐷𝑗 ∈ ℤ ) → ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 )
263 249 255 262 vtocl ( ( 𝜑𝑥𝐷 ∧ - 𝑘 ∈ ℤ ) → ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 )
264 243 248 263 vtocl ( ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ∧ - 𝑘 ∈ ℤ ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 )
265 189 241 242 264 syl3anc ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 )
266 188 265 eqeltrd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑤𝐷 )
267 266 ssd ( 𝜒 → ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ 𝐷 )
268 174 267 ssind ( 𝜒 → ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) )
269 ioosscn ( 𝑋 (,) +∞ ) ⊆ ℂ
270 ssinss1 ( ( 𝑋 (,) +∞ ) ⊆ ℂ → ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ⊆ ℂ )
271 269 270 mp1i ( 𝜒 → ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ⊆ ℂ )
272 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
273 eqid ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
274 215 rexrd ( 𝜒𝑋 ∈ ℝ* )
275 215 leidd ( 𝜒𝑋𝑋 )
276 218 oveq1d ( 𝜒 → ( 𝑦 − ( 𝑘 · 𝑇 ) ) = ( ( 𝑋 + ( 𝑘 · 𝑇 ) ) − ( 𝑘 · 𝑇 ) ) )
277 215 recnd ( 𝜒𝑋 ∈ ℂ )
278 277 236 pncand ( 𝜒 → ( ( 𝑋 + ( 𝑘 · 𝑇 ) ) − ( 𝑘 · 𝑇 ) ) = 𝑋 )
279 276 278 eqtr2d ( 𝜒𝑋 = ( 𝑦 − ( 𝑘 · 𝑇 ) ) )
280 icossre ( ( ( 𝑄𝑖 ) ∈ ℝ ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ) → ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
281 204 207 280 syl2anc ( 𝜒 → ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
282 281 220 sseldd ( 𝜒𝑦 ∈ ℝ )
283 205 207 220 icoltubd ( 𝜒𝑦 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
284 282 165 169 283 ltsub1dd ( 𝜒 → ( 𝑦 − ( 𝑘 · 𝑇 ) ) < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) )
285 279 284 eqbrtrd ( 𝜒𝑋 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) )
286 274 171 274 275 285 elicod ( 𝜒𝑋 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
287 snunioo1 ( ( 𝑋 ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ∈ ℝ*𝑋 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) → ( ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∪ { 𝑋 } ) = ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
288 274 171 285 287 syl3anc ( 𝜒 → ( ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∪ { 𝑋 } ) = ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
289 288 fveq2d ( 𝜒 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∪ { 𝑋 } ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) )
290 272 cnfldtop ( TopOpen ‘ ℂfld ) ∈ Top
291 ovex ( 𝑋 (,) +∞ ) ∈ V
292 291 inex1 ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∈ V
293 snex { 𝑋 } ∈ V
294 292 293 unex ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ∈ V
295 resttop ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ∈ V ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ Top )
296 290 294 295 mp2an ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ Top
297 296 a1i ( 𝜒 → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ Top )
298 retop ( topGen ‘ ran (,) ) ∈ Top
299 iooretop ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∈ ( topGen ‘ ran (,) )
300 299 a1i ( 𝜒 → ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∈ ( topGen ‘ ran (,) ) )
301 elrestr ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ∈ V ∧ ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∈ ( topGen ‘ ran (,) ) ) → ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
302 298 294 300 301 mp3an12i ( 𝜒 → ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
303 mnfxr -∞ ∈ ℝ*
304 303 a1i ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → -∞ ∈ ℝ* )
305 171 adantr ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ∈ ℝ* )
306 icossre ( ( 𝑋 ∈ ℝ ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ∈ ℝ* ) → ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ ℝ )
307 215 171 306 syl2anc ( 𝜒 → ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ ℝ )
308 307 sselda ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑥 ∈ ℝ )
309 308 mnfltd ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → -∞ < 𝑥 )
310 274 adantr ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑋 ∈ ℝ* )
311 simpr ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
312 310 305 311 icoltubd ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑥 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) )
313 304 305 308 309 312 eliood ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑥 ∈ ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
314 vsnid 𝑥 ∈ { 𝑥 }
315 sneq ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
316 314 315 eleqtrid ( 𝑥 = 𝑋𝑥 ∈ { 𝑋 } )
317 elun2 ( 𝑥 ∈ { 𝑋 } → 𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
318 316 317 syl ( 𝑥 = 𝑋𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
319 318 adantl ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ 𝑥 = 𝑋 ) → 𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
320 274 ad2antrr ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑋 ∈ ℝ* )
321 158 a1i ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → +∞ ∈ ℝ* )
322 308 adantr ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ℝ )
323 215 ad2antrr ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑋 ∈ ℝ )
324 310 305 311 icogelbd ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑋𝑥 )
325 324 adantr ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑋𝑥 )
326 neqne ( ¬ 𝑥 = 𝑋𝑥𝑋 )
327 326 adantl ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥𝑋 )
328 323 322 325 327 leneltd ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑋 < 𝑥 )
329 322 ltpnfd ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 < +∞ )
330 320 321 322 328 329 eliood ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ( 𝑋 (,) +∞ ) )
331 166 zcnd ( 𝜒𝑘 ∈ ℂ )
332 331 177 mulneg1d ( 𝜒 → ( - 𝑘 · 𝑇 ) = - ( 𝑘 · 𝑇 ) )
333 332 oveq2d ( 𝜒 → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) = ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + - ( 𝑘 · 𝑇 ) ) )
334 333 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) = ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + - ( 𝑘 · 𝑇 ) ) )
335 ioosscn ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ ℂ
336 335 sseli ( 𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) → 𝑤 ∈ ℂ )
337 336 adantl ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑤 ∈ ℂ )
338 236 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑘 · 𝑇 ) ∈ ℂ )
339 337 338 addcld ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ℂ )
340 339 338 negsubd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + - ( 𝑘 · 𝑇 ) ) = ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) − ( 𝑘 · 𝑇 ) ) )
341 337 338 pncand ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) − ( 𝑘 · 𝑇 ) ) = 𝑤 )
342 334 340 341 3eqtrrd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑤 = ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) )
343 169 adantr ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
344 209 343 readdcld ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ℝ )
345 206 208 344 232 239 eliood ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
346 200 345 sseldd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 )
347 250 3anbi3d ( 𝑗 = - 𝑘 → ( ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷𝑗 ∈ ℤ ) ↔ ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ∧ - 𝑘 ∈ ℤ ) ) )
348 252 oveq2d ( 𝑗 = - 𝑘 → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( 𝑗 · 𝑇 ) ) = ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) )
349 348 eleq1d ( 𝑗 = - 𝑘 → ( ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 ↔ ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 ) )
350 347 349 imbi12d ( 𝑗 = - 𝑘 → ( ( ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷𝑗 ∈ ℤ ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 ) ↔ ( ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ∧ - 𝑘 ∈ ℤ ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 ) ) )
351 244 3anbi2d ( 𝑥 = ( 𝑤 + ( 𝑘 · 𝑇 ) ) → ( ( 𝜑𝑥𝐷𝑗 ∈ ℤ ) ↔ ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷𝑗 ∈ ℤ ) ) )
352 oveq1 ( 𝑥 = ( 𝑤 + ( 𝑘 · 𝑇 ) ) → ( 𝑥 + ( 𝑗 · 𝑇 ) ) = ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( 𝑗 · 𝑇 ) ) )
353 352 eleq1d ( 𝑥 = ( 𝑤 + ( 𝑘 · 𝑇 ) ) → ( ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 ↔ ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 ) )
354 351 353 imbi12d ( 𝑥 = ( 𝑤 + ( 𝑘 · 𝑇 ) ) → ( ( ( 𝜑𝑥𝐷𝑗 ∈ ℤ ) → ( 𝑥 + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 ) ↔ ( ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷𝑗 ∈ ℤ ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 ) ) )
355 243 354 262 vtocl ( ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷𝑗 ∈ ℤ ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( 𝑗 · 𝑇 ) ) ∈ 𝐷 )
356 249 350 355 vtocl ( ( 𝜑 ∧ ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ∧ - 𝑘 ∈ ℤ ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 )
357 189 346 242 356 syl3anc ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 )
358 342 357 eqeltrd ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑤𝐷 )
359 358 ssd ( 𝜒 → ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ 𝐷 )
360 359 ad2antrr ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ 𝐷 )
361 171 ad2antrr ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ∈ ℝ* )
362 312 adantr ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) )
363 320 361 322 328 362 eliood ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
364 360 363 sseldd ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥𝐷 )
365 330 364 elind ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) )
366 elun1 ( 𝑥 ∈ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) → 𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
367 365 366 syl ( ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
368 319 367 pm2.61dan ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
369 313 368 elind ( ( 𝜒𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
370 274 adantr ( ( 𝜒𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑋 ∈ ℝ* )
371 171 adantr ( ( 𝜒𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ∈ ℝ* )
372 elinel1 ( 𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) → 𝑥 ∈ ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
373 372 elioored ( 𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) → 𝑥 ∈ ℝ )
374 373 rexrd ( 𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) → 𝑥 ∈ ℝ* )
375 374 adantl ( ( 𝜒𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑥 ∈ ℝ* )
376 elinel2 ( 𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) → 𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
377 215 adantr ( ( 𝜒𝑥 = 𝑋 ) → 𝑋 ∈ ℝ )
378 87 eqcomd ( 𝑥 = 𝑋𝑋 = 𝑥 )
379 378 adantl ( ( 𝜒𝑥 = 𝑋 ) → 𝑋 = 𝑥 )
380 377 379 eqled ( ( 𝜒𝑥 = 𝑋 ) → 𝑋𝑥 )
381 380 adantlr ( ( ( 𝜒𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ 𝑥 = 𝑋 ) → 𝑋𝑥 )
382 simpll ( ( ( 𝜒𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝜒 )
383 simplr ( ( ( 𝜒𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) )
384 id ( ¬ 𝑥 = 𝑋 → ¬ 𝑥 = 𝑋 )
385 velsn ( 𝑥 ∈ { 𝑋 } ↔ 𝑥 = 𝑋 )
386 384 385 sylnibr ( ¬ 𝑥 = 𝑋 → ¬ 𝑥 ∈ { 𝑋 } )
387 386 adantl ( ( ( 𝜒𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 = 𝑋 ) → ¬ 𝑥 ∈ { 𝑋 } )
388 elunnel2 ( ( 𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ∧ ¬ 𝑥 ∈ { 𝑋 } ) → 𝑥 ∈ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) )
389 383 387 388 syl2anc ( ( ( 𝜒𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) )
390 elinel1 ( 𝑥 ∈ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) → 𝑥 ∈ ( 𝑋 (,) +∞ ) )
391 389 390 syl ( ( ( 𝜒𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑥 ∈ ( 𝑋 (,) +∞ ) )
392 215 adantr ( ( 𝜒𝑥 ∈ ( 𝑋 (,) +∞ ) ) → 𝑋 ∈ ℝ )
393 elioore ( 𝑥 ∈ ( 𝑋 (,) +∞ ) → 𝑥 ∈ ℝ )
394 393 adantl ( ( 𝜒𝑥 ∈ ( 𝑋 (,) +∞ ) ) → 𝑥 ∈ ℝ )
395 274 adantr ( ( 𝜒𝑥 ∈ ( 𝑋 (,) +∞ ) ) → 𝑋 ∈ ℝ* )
396 158 a1i ( ( 𝜒𝑥 ∈ ( 𝑋 (,) +∞ ) ) → +∞ ∈ ℝ* )
397 simpr ( ( 𝜒𝑥 ∈ ( 𝑋 (,) +∞ ) ) → 𝑥 ∈ ( 𝑋 (,) +∞ ) )
398 395 396 397 ioogtlbd ( ( 𝜒𝑥 ∈ ( 𝑋 (,) +∞ ) ) → 𝑋 < 𝑥 )
399 392 394 398 ltled ( ( 𝜒𝑥 ∈ ( 𝑋 (,) +∞ ) ) → 𝑋𝑥 )
400 382 391 399 syl2anc ( ( ( 𝜒𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∧ ¬ 𝑥 = 𝑋 ) → 𝑋𝑥 )
401 381 400 pm2.61dan ( ( 𝜒𝑥 ∈ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) → 𝑋𝑥 )
402 376 401 sylan2 ( ( 𝜒𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑋𝑥 )
403 iooltub ( ( -∞ ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ∈ ℝ*𝑥 ∈ ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑥 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) )
404 303 171 372 403 mp3an3an ( ( 𝜒𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑥 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) )
405 370 371 375 402 404 elicod ( ( 𝜒𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → 𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
406 369 405 impbida ( 𝜒 → ( 𝑥 ∈ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ↔ 𝑥 ∈ ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) )
407 406 eqrdv ( 𝜒 → ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) = ( ( -∞ (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∩ ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
408 ioossre ( 𝑋 (,) +∞ ) ⊆ ℝ
409 ssinss1 ( ( 𝑋 (,) +∞ ) ⊆ ℝ → ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ⊆ ℝ )
410 408 409 mp1i ( 𝜒 → ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ⊆ ℝ )
411 215 snssd ( 𝜒 → { 𝑋 } ⊆ ℝ )
412 410 411 unssd ( 𝜒 → ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ⊆ ℝ )
413 eqid ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
414 272 413 rerest ( ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
415 412 414 syl ( 𝜒 → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
416 302 407 415 3eltr4d ( 𝜒 → ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) )
417 isopn3i ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ∈ Top ∧ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) = ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
418 297 416 417 syl2anc ( 𝜒 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) = ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
419 289 418 eqtr2d ( 𝜒 → ( 𝑋 [,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∪ { 𝑋 } ) ) )
420 286 419 eleqtrd ( 𝜒𝑋 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ∪ { 𝑋 } ) ) ) ‘ ( ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∪ { 𝑋 } ) ) )
421 157 268 271 272 273 420 limcres ( 𝜒 → ( ( ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ) ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ) lim 𝑋 ) )
422 268 resabs1d ( 𝜒 → ( ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ) ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) = ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) )
423 422 oveq1d ( 𝜒 → ( ( ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ) ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) )
424 152 a1i ( 𝜑 → ℝ ⊆ ℂ )
425 8 424 fssd ( 𝜑𝐹 : 𝐷 ⟶ ℂ )
426 425 ffdmd ( 𝜑𝐹 : dom 𝐹 ⟶ ℂ )
427 144 426 syl ( 𝜒𝐹 : dom 𝐹 ⟶ ℂ )
428 427 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
429 335 a1i ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ) → ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ ℂ )
430 359 146 sseqtrrd ( 𝜒 → ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ dom 𝐹 )
431 430 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ) → ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ⊆ dom 𝐹 )
432 236 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ) → ( 𝑘 · 𝑇 ) ∈ ℂ )
433 eqid { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } = { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) }
434 eqeq1 ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) ↔ 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) )
435 434 rexbidv ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) ↔ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) )
436 435 elrab ( 𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ↔ ( 𝑤 ∈ ℂ ∧ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) )
437 436 simprbi ( 𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } → ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
438 437 adantl ( ( 𝜒𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ) → ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
439 nfv 𝑥 𝜒
440 nfre1 𝑥𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) )
441 nfcv 𝑥
442 440 441 nfrabw 𝑥 { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) }
443 442 nfcri 𝑥 𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) }
444 439 443 nfan 𝑥 ( 𝜒𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } )
445 nfv 𝑥 𝑤𝐷
446 simp3 ( ( 𝜒𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∧ 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) → 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
447 eleq1 ( 𝑤 = 𝑥 → ( 𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ↔ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) )
448 447 anbi2d ( 𝑤 = 𝑥 → ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ↔ ( 𝜒𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) ) )
449 oveq1 ( 𝑤 = 𝑥 → ( 𝑤 + ( 𝑘 · 𝑇 ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
450 449 eleq1d ( 𝑤 = 𝑥 → ( ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ) )
451 448 450 imbi12d ( 𝑤 = 𝑥 → ( ( ( 𝜒𝑤 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑤 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ) ↔ ( ( 𝜒𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 ) ) )
452 451 241 chvarvv ( ( 𝜒𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 )
453 452 3adant3 ( ( 𝜒𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∧ 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ 𝐷 )
454 446 453 eqeltrd ( ( 𝜒𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ∧ 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) → 𝑤𝐷 )
455 454 3exp ( 𝜒 → ( 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) → ( 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) → 𝑤𝐷 ) ) )
456 455 adantr ( ( 𝜒𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ) → ( 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) → ( 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) → 𝑤𝐷 ) ) )
457 444 445 456 rexlimd ( ( 𝜒𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ) → ( ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑤 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) → 𝑤𝐷 ) )
458 438 457 mpd ( ( 𝜒𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ) → 𝑤𝐷 )
459 458 ssd ( 𝜒 → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ⊆ 𝐷 )
460 459 146 sseqtrrd ( 𝜒 → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ⊆ dom 𝐹 )
461 460 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ⊆ dom 𝐹 )
462 144 adantr ( ( 𝜒𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝜑 )
463 359 sselda ( ( 𝜒𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑥𝐷 )
464 166 adantr ( ( 𝜒𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → 𝑘 ∈ ℤ )
465 462 463 464 10 syl3anc ( ( 𝜒𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) )
466 465 adantlr ( ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ) ∧ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) )
467 simpr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ) → 𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) )
468 428 429 431 432 433 461 466 467 limcperiod ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ) → 𝑤 ∈ ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ) lim ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
469 237 eqcomd ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) )
470 218 469 oveq12d ( 𝜒 → ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑋 + ( 𝑘 · 𝑇 ) ) (,) ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) ) )
471 215 170 169 iooshift ( 𝜒 → ( ( 𝑋 + ( 𝑘 · 𝑇 ) ) (,) ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) + ( 𝑘 · 𝑇 ) ) ) = { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } )
472 470 471 eqtr2d ( 𝜒 → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } = ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
473 472 reseq2d ( 𝜒 → ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ) = ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
474 473 219 oveq12d ( 𝜒 → ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ) lim ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) = ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) )
475 474 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ) → ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) 𝑧 = ( 𝑥 + ( 𝑘 · 𝑇 ) ) } ) lim ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) = ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) )
476 468 475 eleqtrd ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ) → 𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) )
477 427 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
478 ioosscn ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
479 478 a1i ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
480 205 207 220 icogelbd ( 𝜒 → ( 𝑄𝑖 ) ≤ 𝑦 )
481 iooss1 ( ( ( 𝑄𝑖 ) ∈ ℝ* ∧ ( 𝑄𝑖 ) ≤ 𝑦 ) → ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
482 205 480 481 syl2anc ( 𝜒 → ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
483 482 199 sstrd ( 𝜒 → ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ 𝐷 )
484 483 146 sseqtrrd ( 𝜒 → ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
485 484 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
486 331 negcld ( 𝜒 → - 𝑘 ∈ ℂ )
487 486 177 mulcld ( 𝜒 → ( - 𝑘 · 𝑇 ) ∈ ℂ )
488 487 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → ( - 𝑘 · 𝑇 ) ∈ ℂ )
489 eqid { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } = { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) }
490 eqeq1 ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ↔ 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ) )
491 490 rexbidv ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ↔ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ) )
492 491 elrab ( 𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ↔ ( 𝑤 ∈ ℂ ∧ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ) )
493 492 simprbi ( 𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } → ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) )
494 493 adantl ( ( 𝜒𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ) → ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) )
495 nfre1 𝑥𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) )
496 495 441 nfrabw 𝑥 { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) }
497 496 nfcri 𝑥 𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) }
498 439 497 nfan 𝑥 ( 𝜒𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } )
499 simp3 ( ( 𝜒𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ) → 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) )
500 144 adantr ( ( 𝜒𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝜑 )
501 483 sselda ( ( 𝜒𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥𝐷 )
502 166 adantr ( ( 𝜒𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑘 ∈ ℤ )
503 502 znegcld ( ( 𝜒𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → - 𝑘 ∈ ℤ )
504 500 501 503 263 syl3anc ( ( 𝜒𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 )
505 504 3adant3 ( ( 𝜒𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ) → ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ∈ 𝐷 )
506 499 505 eqeltrd ( ( 𝜒𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ) → 𝑤𝐷 )
507 506 3exp ( 𝜒 → ( 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) → 𝑤𝐷 ) ) )
508 507 adantr ( ( 𝜒𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ) → ( 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) → 𝑤𝐷 ) ) )
509 498 445 508 rexlimd ( ( 𝜒𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ) → ( ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) → 𝑤𝐷 ) )
510 494 509 mpd ( ( 𝜒𝑤 ∈ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ) → 𝑤𝐷 )
511 510 ssd ( 𝜒 → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ⊆ 𝐷 )
512 511 146 sseqtrrd ( 𝜒 → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ⊆ dom 𝐹 )
513 512 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ⊆ dom 𝐹 )
514 144 ad2antrr ( ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) ∧ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝜑 )
515 501 adantlr ( ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) ∧ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥𝐷 )
516 503 adantlr ( ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) ∧ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → - 𝑘 ∈ ℤ )
517 253 fveqeq2d ( 𝑗 = - 𝑘 → ( ( 𝐹 ‘ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ↔ ( 𝐹 ‘ ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) )
518 251 517 imbi12d ( 𝑗 = - 𝑘 → ( ( ( 𝜑𝑥𝐷𝑗 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) ↔ ( ( 𝜑𝑥𝐷 ∧ - 𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) ) )
519 259 fveqeq2d ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ↔ ( 𝐹 ‘ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) )
520 257 519 imbi12d ( 𝑘 = 𝑗 → ( ( ( 𝜑𝑥𝐷𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) ↔ ( ( 𝜑𝑥𝐷𝑗 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ) = ( 𝐹𝑥 ) ) ) )
521 520 10 chvarvv ( ( 𝜑𝑥𝐷𝑗 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑗 · 𝑇 ) ) ) = ( 𝐹𝑥 ) )
522 249 518 521 vtocl ( ( 𝜑𝑥𝐷 ∧ - 𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) )
523 514 515 516 522 syl3anc ( ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) ∧ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑥 + ( - 𝑘 · 𝑇 ) ) ) = ( 𝐹𝑥 ) )
524 simpr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → 𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) )
525 477 479 485 488 489 513 523 524 limcperiod ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → 𝑤 ∈ ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ) lim ( 𝑦 + ( - 𝑘 · 𝑇 ) ) ) )
526 332 oveq2d ( 𝜒 → ( 𝑦 + ( - 𝑘 · 𝑇 ) ) = ( 𝑦 + - ( 𝑘 · 𝑇 ) ) )
527 282 recnd ( 𝜒𝑦 ∈ ℂ )
528 527 236 negsubd ( 𝜒 → ( 𝑦 + - ( 𝑘 · 𝑇 ) ) = ( 𝑦 − ( 𝑘 · 𝑇 ) ) )
529 279 eqcomd ( 𝜒 → ( 𝑦 − ( 𝑘 · 𝑇 ) ) = 𝑋 )
530 526 528 529 3eqtrd ( 𝜒 → ( 𝑦 + ( - 𝑘 · 𝑇 ) ) = 𝑋 )
531 530 eqcomd ( 𝜒𝑋 = ( 𝑦 + ( - 𝑘 · 𝑇 ) ) )
532 332 oveq2d ( 𝜒 → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( - 𝑘 · 𝑇 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + - ( 𝑘 · 𝑇 ) ) )
533 235 236 negsubd ( 𝜒 → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + - ( 𝑘 · 𝑇 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) )
534 532 533 eqtr2d ( 𝜒 → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( - 𝑘 · 𝑇 ) ) )
535 531 534 oveq12d ( 𝜒 → ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) = ( ( 𝑦 + ( - 𝑘 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( - 𝑘 · 𝑇 ) ) ) )
536 167 renegcld ( 𝜒 → - 𝑘 ∈ ℝ )
537 536 168 remulcld ( 𝜒 → ( - 𝑘 · 𝑇 ) ∈ ℝ )
538 282 165 537 iooshift ( 𝜒 → ( ( 𝑦 + ( - 𝑘 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( - 𝑘 · 𝑇 ) ) ) = { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } )
539 535 538 eqtr2d ( 𝜒 → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } = ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
540 539 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } = ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) )
541 540 reseq2d ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ) = ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) )
542 530 adantr ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → ( 𝑦 + ( - 𝑘 · 𝑇 ) ) = 𝑋 )
543 541 542 oveq12d ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → ( ( 𝐹 ↾ { 𝑧 ∈ ℂ ∣ ∃ 𝑥 ∈ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑧 = ( 𝑥 + ( - 𝑘 · 𝑇 ) ) } ) lim ( 𝑦 + ( - 𝑘 · 𝑇 ) ) ) = ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) )
544 525 543 eleqtrd ( ( 𝜒𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) → 𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) )
545 476 544 impbida ( 𝜒 → ( 𝑤 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) ↔ 𝑤 ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ) )
546 545 eqrdv ( 𝜒 → ( ( 𝐹 ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) )
547 423 546 eqtrd ( 𝜒 → ( ( ( 𝐹 ↾ ( ( 𝑋 (,) +∞ ) ∩ 𝐷 ) ) ↾ ( 𝑋 (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − ( 𝑘 · 𝑇 ) ) ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) )
548 150 421 547 3eqtr2d ( 𝜒 → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) = ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) )
549 76 r19.21bi ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
550 144 160 549 syl2anc ( 𝜒 → ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
551 144 160 11 syl2anc ( 𝜒 → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
552 144 160 12 syl2anc ( 𝜒𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
553 eqid if ( 𝑦 = ( 𝑄𝑖 ) , 𝑅 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑦 ) ) = if ( 𝑦 = ( 𝑄𝑖 ) , 𝑅 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑦 ) )
554 eqid ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
555 204 165 550 551 552 282 165 283 482 553 554 fourierdlem32 ( 𝜒 → if ( 𝑦 = ( 𝑄𝑖 ) , 𝑅 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑦 ) ) ∈ ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) )
556 482 resabs1d ( 𝜒 → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
557 556 oveq1d ( 𝜒 → ( ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) = ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) )
558 555 557 eleqtrd ( 𝜒 → if ( 𝑦 = ( 𝑄𝑖 ) , 𝑅 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑦 ) ) ∈ ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) )
559 558 ne0d ( 𝜒 → ( ( 𝐹 ↾ ( 𝑦 (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim 𝑦 ) ≠ ∅ )
560 548 559 eqnetrd ( 𝜒 → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ )
561 16 560 sylbir ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ )
562 138 139 140 561 syl21anc ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ )
563 562 3exp ( 𝜑 → ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ ) ) )
564 563 adantr ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ ) ) )
565 129 134 564 rexlim2d ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ ) )
566 126 565 mpd ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ )
567 119 125 566 vtocl ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( ( 𝐸𝑋 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( ( 𝐸𝑋 ) − 𝑇 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ )
568 17 118 567 syl2anc ( ( 𝜑 ∧ ( 𝐸𝑋 ) = 𝐵 ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ )
569 iocssre ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
570 69 2 569 syl2anc ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
571 ovex ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ V
572 14 fvmpt2 ( ( 𝑥 ∈ ℝ ∧ ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ V ) → ( 𝑍𝑥 ) = ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) )
573 571 572 mpan2 ( 𝑥 ∈ ℝ → ( 𝑍𝑥 ) = ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) )
574 573 oveq2d ( 𝑥 ∈ ℝ → ( 𝑥 + ( 𝑍𝑥 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
575 574 mpteq2ia ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( 𝑍𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
576 15 575 eqtri 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
577 1 2 3 5 576 fourierdlem4 ( 𝜑𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
578 577 13 ffvelcdmd ( 𝜑 → ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) )
579 570 578 sseldd ( 𝜑 → ( 𝐸𝑋 ) ∈ ℝ )
580 579 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) → ( 𝐸𝑋 ) ∈ ℝ )
581 simpl ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) → 𝜑 )
582 simpr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ( 𝐸𝑋 ) ∈ ran 𝑄 )
583 54 ffnd ( 𝜑𝑄 Fn ( 0 ... 𝑀 ) )
584 583 ad2antrr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → 𝑄 Fn ( 0 ... 𝑀 ) )
585 fvelrnb ( 𝑄 Fn ( 0 ... 𝑀 ) → ( ( 𝐸𝑋 ) ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) )
586 584 585 syl ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ( ( 𝐸𝑋 ) ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) )
587 582 586 mpbid ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄𝑗 ) = ( 𝐸𝑋 ) )
588 fveq2 ( 𝑖 = ( 𝑗 − 1 ) → ( 𝑄𝑖 ) = ( 𝑄 ‘ ( 𝑗 − 1 ) ) )
589 fvoveq1 ( 𝑖 = ( 𝑗 − 1 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) )
590 588 589 oveq12d ( 𝑖 = ( 𝑗 − 1 ) → ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) )
591 590 eleq2d ( 𝑖 = ( 𝑗 − 1 ) → ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) ) )
592 nnuz ℕ = ( ℤ ‘ 1 )
593 1zzd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 1 ∈ ℤ )
594 elfzelz ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
595 594 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑗 ∈ ℤ )
596 595 zred ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑗 ∈ ℝ )
597 elfzle1 ( 𝑗 ∈ ( 0 ... 𝑀 ) → 0 ≤ 𝑗 )
598 597 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 0 ≤ 𝑗 )
599 id ( ( 𝑄𝑗 ) = ( 𝐸𝑋 ) → ( 𝑄𝑗 ) = ( 𝐸𝑋 ) )
600 599 eqcomd ( ( 𝑄𝑗 ) = ( 𝐸𝑋 ) → ( 𝐸𝑋 ) = ( 𝑄𝑗 ) )
601 600 ad2antlr ( ( ( 𝜑 ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝐸𝑋 ) = ( 𝑄𝑗 ) )
602 fveq2 ( 𝑗 = 0 → ( 𝑄𝑗 ) = ( 𝑄 ‘ 0 ) )
603 602 adantl ( ( ( 𝜑 ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝑄𝑗 ) = ( 𝑄 ‘ 0 ) )
604 51 simprld ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) )
605 604 simpld ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
606 605 ad2antrr ( ( ( 𝜑 ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝑄 ‘ 0 ) = 𝐴 )
607 601 603 606 3eqtrd ( ( ( 𝜑 ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝐸𝑋 ) = 𝐴 )
608 607 adantllr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝐸𝑋 ) = 𝐴 )
609 608 adantllr ( ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ( 𝐸𝑋 ) = 𝐴 )
610 1 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 ∈ ℝ )
611 69 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 ∈ ℝ* )
612 2 rexrd ( 𝜑𝐵 ∈ ℝ* )
613 612 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐵 ∈ ℝ* )
614 simpr ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) )
615 611 613 614 iocgtlbd ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < ( 𝐸𝑋 ) )
616 610 615 gtned ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸𝑋 ) ≠ 𝐴 )
617 616 neneqd ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ¬ ( 𝐸𝑋 ) = 𝐴 )
618 617 ad3antrrr ( ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) ∧ 𝑗 = 0 ) → ¬ ( 𝐸𝑋 ) = 𝐴 )
619 609 618 pm2.65da ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ¬ 𝑗 = 0 )
620 619 neqned ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑗 ≠ 0 )
621 596 598 620 ne0gt0d ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 0 < 𝑗 )
622 0zd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 0 ∈ ℤ )
623 622 595 zltp1led ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 0 < 𝑗 ↔ ( 0 + 1 ) ≤ 𝑗 ) )
624 621 623 mpbid ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 0 + 1 ) ≤ 𝑗 )
625 78 624 eqbrtrid ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 1 ≤ 𝑗 )
626 592 593 595 625 eluzd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑗 ∈ ℕ )
627 nnm1nn0 ( 𝑗 ∈ ℕ → ( 𝑗 − 1 ) ∈ ℕ0 )
628 626 627 syl ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ∈ ℕ0 )
629 628 56 eleqtrdi ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ∈ ( ℤ ‘ 0 ) )
630 25 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑀 ∈ ℤ )
631 peano2zm ( 𝑗 ∈ ℤ → ( 𝑗 − 1 ) ∈ ℤ )
632 594 631 syl ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) ∈ ℤ )
633 632 zred ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) ∈ ℝ )
634 594 zred ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℝ )
635 elfzel2 ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℤ )
636 635 zred ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℝ )
637 634 ltm1d ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) < 𝑗 )
638 elfzle2 ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗𝑀 )
639 633 634 636 637 638 ltletrd ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) < 𝑀 )
640 639 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) < 𝑀 )
641 629 630 640 elfzod ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑀 ) )
642 54 ad3antrrr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
643 595 631 syl ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ∈ ℤ )
644 628 nn0ge0d ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 0 ≤ ( 𝑗 − 1 ) )
645 633 636 639 ltled ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 1 ) ≤ 𝑀 )
646 645 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ≤ 𝑀 )
647 622 630 643 644 646 elfzd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ... 𝑀 ) )
648 642 647 ffvelcdmd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) ∈ ℝ )
649 648 rexrd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) ∈ ℝ* )
650 54 ffvelcdmda ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄𝑗 ) ∈ ℝ )
651 650 rexrd ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄𝑗 ) ∈ ℝ* )
652 651 adantlr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄𝑗 ) ∈ ℝ* )
653 652 adantr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄𝑗 ) ∈ ℝ* )
654 570 sselda ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸𝑋 ) ∈ ℝ )
655 654 rexrd ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
656 655 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
657 simplll ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → 𝜑 )
658 ovex ( 𝑗 − 1 ) ∈ V
659 eleq1 ( 𝑖 = ( 𝑗 − 1 ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑀 ) ) )
660 659 anbi2d ( 𝑖 = ( 𝑗 − 1 ) → ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑀 ) ) ) )
661 588 589 breq12d ( 𝑖 = ( 𝑗 − 1 ) → ( ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) )
662 660 661 imbi12d ( 𝑖 = ( 𝑗 − 1 ) → ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) ) )
663 658 662 549 vtocl ( ( 𝜑 ∧ ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) )
664 657 641 663 syl2anc ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) )
665 594 zcnd ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℂ )
666 1cnd ( 𝑗 ∈ ( 0 ... 𝑀 ) → 1 ∈ ℂ )
667 665 666 npcand ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
668 667 fveq2d ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) = ( 𝑄𝑗 ) )
669 668 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) = ( 𝑄𝑗 ) )
670 664 669 breqtrd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝑄𝑗 ) )
671 simpr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄𝑗 ) = ( 𝐸𝑋 ) )
672 670 671 breqtrd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝑄 ‘ ( 𝑗 − 1 ) ) < ( 𝐸𝑋 ) )
673 579 leidd ( 𝜑 → ( 𝐸𝑋 ) ≤ ( 𝐸𝑋 ) )
674 673 ad2antrr ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ≤ ( 𝐸𝑋 ) )
675 600 adantl ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) = ( 𝑄𝑗 ) )
676 674 675 breqtrd ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ≤ ( 𝑄𝑗 ) )
677 676 adantllr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ≤ ( 𝑄𝑗 ) )
678 649 653 656 672 677 eliocd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄𝑗 ) ) )
679 667 eqcomd ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 = ( ( 𝑗 − 1 ) + 1 ) )
680 679 fveq2d ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑄𝑗 ) = ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) )
681 680 oveq2d ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄𝑗 ) ) = ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) )
682 681 ad2antlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄𝑗 ) ) = ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) )
683 678 682 eleqtrd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ ( 𝑗 − 1 ) ) (,] ( 𝑄 ‘ ( ( 𝑗 − 1 ) + 1 ) ) ) )
684 591 641 683 rspcedvdw ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ( 𝑄𝑗 ) = ( 𝐸𝑋 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
685 684 ex ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑄𝑗 ) = ( 𝐸𝑋 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
686 685 adantlr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑄𝑗 ) = ( 𝐸𝑋 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
687 686 rexlimdva ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑄𝑗 ) = ( 𝐸𝑋 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
688 587 687 mpd ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
689 6 ad2antrr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → 𝑀 ∈ ℕ )
690 54 ad2antrr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
691 iocssicc ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
692 605 eqcomd ( 𝜑𝐴 = ( 𝑄 ‘ 0 ) )
693 604 simprd ( 𝜑 → ( 𝑄𝑀 ) = 𝐵 )
694 693 eqcomd ( 𝜑𝐵 = ( 𝑄𝑀 ) )
695 692 694 oveq12d ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
696 691 695 sseqtrid ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
697 696 sselda ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
698 697 adantr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
699 simpr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 )
700 fveq2 ( 𝑘 = 𝑗 → ( 𝑄𝑘 ) = ( 𝑄𝑗 ) )
701 700 breq1d ( 𝑘 = 𝑗 → ( ( 𝑄𝑘 ) < ( 𝐸𝑋 ) ↔ ( 𝑄𝑗 ) < ( 𝐸𝑋 ) ) )
702 701 cbvrabv { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) < ( 𝐸𝑋 ) } = { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) < ( 𝐸𝑋 ) }
703 702 supeq1i sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) < ( 𝐸𝑋 ) } , ℝ , < ) = sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) < ( 𝐸𝑋 ) } , ℝ , < )
704 689 690 698 699 703 fourierdlem25 ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
705 ioossioc ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
706 705 sseli ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
707 706 a1i ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
708 707 reximdva ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
709 704 708 mpd ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) ∧ ¬ ( 𝐸𝑋 ) ∈ ran 𝑄 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
710 688 709 pm2.61dan ( ( 𝜑 ∧ ( 𝐸𝑋 ) ∈ ( 𝐴 (,] 𝐵 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
711 578 710 mpdan ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
712 fveq2 ( 𝑖 = 𝑗 → ( 𝑄𝑖 ) = ( 𝑄𝑗 ) )
713 fvoveq1 ( 𝑖 = 𝑗 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
714 712 713 oveq12d ( 𝑖 = 𝑗 → ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )
715 714 eleq2d ( 𝑖 = 𝑗 → ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) )
716 715 cbvrexvw ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) (,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑗 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )
717 711 716 sylib ( 𝜑 → ∃ 𝑗 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )
718 717 adantr ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )
719 fveq2 ( 𝑖 = ( 𝑗 + 1 ) → ( 𝑄𝑖 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
720 fvoveq1 ( 𝑖 = ( 𝑗 + 1 ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) )
721 719 720 oveq12d ( 𝑖 = ( 𝑗 + 1 ) → ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝑗 + 1 ) ) [,) ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) ) )
722 721 eleq2d ( 𝑖 = ( 𝑗 + 1 ) → ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ ( 𝑗 + 1 ) ) [,) ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) ) ) )
723 elfzonn0 ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℕ0 )
724 1nn0 1 ∈ ℕ0
725 724 a1i ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 1 ∈ ℕ0 )
726 723 725 nn0addcld ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑗 + 1 ) ∈ ℕ0 )
727 726 56 eleqtrdi ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑗 + 1 ) ∈ ( ℤ ‘ 0 ) )
728 727 adantr ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( ℤ ‘ 0 ) )
729 728 3ad2antl2 ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( ℤ ‘ 0 ) )
730 25 ad2antrr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 𝑀 ∈ ℤ )
731 730 3ad2antl1 ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 𝑀 ∈ ℤ )
732 723 nn0red ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℝ )
733 732 adantr ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 𝑗 ∈ ℝ )
734 733 3ad2antl2 ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 𝑗 ∈ ℝ )
735 1red ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 1 ∈ ℝ )
736 734 735 readdcld ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℝ )
737 731 zred ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 𝑀 ∈ ℝ )
738 elfzop1le2 ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑗 + 1 ) ≤ 𝑀 )
739 738 adantr ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑗 + 1 ) ≤ 𝑀 )
740 739 3ad2antl2 ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑗 + 1 ) ≤ 𝑀 )
741 simplr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝑀 = ( 𝑗 + 1 ) ) → ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
742 fveq2 ( 𝑀 = ( 𝑗 + 1 ) → ( 𝑄𝑀 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
743 742 eqcomd ( 𝑀 = ( 𝑗 + 1 ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) = ( 𝑄𝑀 ) )
744 743 adantl ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝑀 = ( 𝑗 + 1 ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) = ( 𝑄𝑀 ) )
745 693 ad2antrr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝑀 = ( 𝑗 + 1 ) ) → ( 𝑄𝑀 ) = 𝐵 )
746 741 744 745 3eqtrd ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝑀 = ( 𝑗 + 1 ) ) → ( 𝐸𝑋 ) = 𝐵 )
747 746 adantllr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝑀 = ( 𝑗 + 1 ) ) → ( 𝐸𝑋 ) = 𝐵 )
748 simpllr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝑀 = ( 𝑗 + 1 ) ) → ( 𝐸𝑋 ) ≠ 𝐵 )
749 748 neneqd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝑀 = ( 𝑗 + 1 ) ) → ¬ ( 𝐸𝑋 ) = 𝐵 )
750 747 749 pm2.65da ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ¬ 𝑀 = ( 𝑗 + 1 ) )
751 750 neqned ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 𝑀 ≠ ( 𝑗 + 1 ) )
752 751 3ad2antl1 ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 𝑀 ≠ ( 𝑗 + 1 ) )
753 736 737 740 752 leneltd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑗 + 1 ) < 𝑀 )
754 729 731 753 elfzod ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( 0 ..^ 𝑀 ) )
755 54 adantr ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
756 fzofzp1 ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
757 756 adantl ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
758 755 757 ffvelcdmd ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
759 758 rexrd ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
760 759 adantlr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
761 760 3adant3 ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
762 761 adantr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
763 simpl1l ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 𝜑 )
764 763 54 syl ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
765 fzofzp1 ( ( 𝑗 + 1 ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝑗 + 1 ) + 1 ) ∈ ( 0 ... 𝑀 ) )
766 754 765 syl ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( ( 𝑗 + 1 ) + 1 ) ∈ ( 0 ... 𝑀 ) )
767 764 766 ffvelcdmd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) ∈ ℝ )
768 767 rexrd ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) ∈ ℝ* )
769 579 rexrd ( 𝜑 → ( 𝐸𝑋 ) ∈ ℝ* )
770 769 ad2antrr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
771 770 3ad2antl1 ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
772 758 leidd ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
773 772 adantr ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
774 id ( ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) → ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
775 774 eqcomd ( ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) = ( 𝐸𝑋 ) )
776 775 adantl ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) = ( 𝐸𝑋 ) )
777 773 776 breqtrd ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐸𝑋 ) )
778 777 adantllr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐸𝑋 ) )
779 778 3adantl3 ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐸𝑋 ) )
780 simpr ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
781 simpr ( ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
782 ovex ( 𝑗 + 1 ) ∈ V
783 eleq1 ( 𝑖 = ( 𝑗 + 1 ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑗 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) )
784 783 anbi2d ( 𝑖 = ( 𝑗 + 1 ) → ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) ) )
785 719 720 breq12d ( 𝑖 = ( 𝑗 + 1 ) → ( ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ ( 𝑗 + 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) ) )
786 784 785 imbi12d ( 𝑖 = ( 𝑗 + 1 ) → ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) ) ) )
787 782 786 549 vtocl ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) )
788 787 adantr ( ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) < ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) )
789 781 788 eqbrtrd ( ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) < ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) )
790 763 754 780 789 syl21anc ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) < ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) )
791 762 768 771 779 790 elicod ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄 ‘ ( 𝑗 + 1 ) ) [,) ( 𝑄 ‘ ( ( 𝑗 + 1 ) + 1 ) ) ) )
792 722 754 791 rspcedvdw ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
793 712 713 oveq12d ( 𝑖 = 𝑗 → ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄𝑗 ) [,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )
794 793 eleq2d ( 𝑖 = 𝑗 → ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) [,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) )
795 simpl2 ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → 𝑗 ∈ ( 0 ..^ 𝑀 ) )
796 id ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) )
797 796 3adant1r ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) )
798 elfzofz ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
799 798 adantl ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
800 755 799 ffvelcdmd ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑗 ) ∈ ℝ )
801 800 rexrd ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑗 ) ∈ ℝ* )
802 801 adantr ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄𝑗 ) ∈ ℝ* )
803 802 3adantl3 ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄𝑗 ) ∈ ℝ* )
804 759 adantr ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
805 804 3adantl3 ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
806 769 adantr ( ( 𝜑 ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
807 806 3ad2antl1 ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ℝ* )
808 800 3adant3 ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄𝑗 ) ∈ ℝ )
809 579 3ad2ant1 ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ℝ )
810 801 3adant3 ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄𝑗 ) ∈ ℝ* )
811 759 3adant3 ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
812 simp3 ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )
813 810 811 812 iocgtlbd ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄𝑗 ) < ( 𝐸𝑋 ) )
814 808 809 813 ltled ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄𝑗 ) ≤ ( 𝐸𝑋 ) )
815 814 adantr ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄𝑗 ) ≤ ( 𝐸𝑋 ) )
816 809 adantr ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ℝ )
817 758 adantr ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
818 817 3adantl3 ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
819 810 811 812 iocleubd ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐸𝑋 ) ≤ ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
820 819 adantr ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) ≤ ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
821 neqne ( ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) → ( 𝐸𝑋 ) ≠ ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
822 821 necomd ( ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ≠ ( 𝐸𝑋 ) )
823 822 adantl ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ≠ ( 𝐸𝑋 ) )
824 816 818 820 823 leneltd ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) < ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
825 803 805 807 815 824 elicod ( ( ( 𝜑𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) [,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )
826 797 825 sylan ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) [,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )
827 794 795 826 rspcedvdw ( ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) ∧ ¬ ( 𝐸𝑋 ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
828 792 827 pm2.61dan ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
829 828 rexlimdv3a ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) → ( ∃ 𝑗 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑗 ) (,] ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
830 718 829 mpd ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
831 simpr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
832 oveq1 ( 𝑘 = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( 𝑘 · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) )
833 832 oveq2d ( 𝑘 = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( 𝑋 + ( 𝑘 · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
834 833 eqeq2d ( 𝑘 = ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) → ( ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ↔ ( 𝐸𝑋 ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ) )
835 834 93 101 rspcedvdw ( 𝜑 → ∃ 𝑘 ∈ ℤ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
836 835 ad2antrr ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑘 ∈ ℤ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) )
837 r19.42v ( ∃ 𝑘 ∈ ℤ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ↔ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ∃ 𝑘 ∈ ℤ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
838 831 836 837 sylanbrc ( ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) ∧ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑘 ∈ ℤ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
839 838 ex ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) → ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑘 ∈ ℤ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) )
840 839 reximdv ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) )
841 830 840 mpd ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
842 581 841 jca ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) → ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) )
843 eleq1 ( 𝑦 = ( 𝐸𝑋 ) → ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
844 eqeq1 ( 𝑦 = ( 𝐸𝑋 ) → ( 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ↔ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
845 843 844 anbi12d ( 𝑦 = ( 𝐸𝑋 ) → ( ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ↔ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) )
846 845 2rexbidv ( 𝑦 = ( 𝐸𝑋 ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) )
847 846 anbi2d ( 𝑦 = ( 𝐸𝑋 ) → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) ↔ ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) ) )
848 847 imbi1d ( 𝑦 = ( 𝐸𝑋 ) → ( ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( 𝑦 ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑦 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ ) ↔ ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ ) ) )
849 848 566 vtoclg ( ( 𝐸𝑋 ) ∈ ℝ → ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑘 ∈ ℤ ( ( 𝐸𝑋 ) ∈ ( ( 𝑄𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐸𝑋 ) = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ ) )
850 580 842 849 sylc ( ( 𝜑 ∧ ( 𝐸𝑋 ) ≠ 𝐵 ) → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ )
851 568 850 pm2.61dane ( 𝜑 → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim 𝑋 ) ≠ ∅ )