Step |
Hyp |
Ref |
Expression |
1 |
|
clim2d.k |
⊢ Ⅎ 𝑘 𝜑 |
2 |
|
clim2d.f |
⊢ Ⅎ 𝑘 𝐹 |
3 |
|
clim2d.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
4 |
|
clim2d.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
5 |
|
clim2d.c |
⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 ) |
6 |
|
clim2d.b |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 ) |
7 |
|
clim2d.x |
⊢ ( 𝜑 → 𝑋 ∈ ℝ+ ) |
8 |
|
climrel |
⊢ Rel ⇝ |
9 |
8
|
a1i |
⊢ ( 𝜑 → Rel ⇝ ) |
10 |
|
brrelex1 |
⊢ ( ( Rel ⇝ ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 ∈ V ) |
11 |
9 5 10
|
syl2anc |
⊢ ( 𝜑 → 𝐹 ∈ V ) |
12 |
1 2 4 3 11 6
|
clim2f2 |
⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) ) ) |
13 |
5 12
|
mpbid |
⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) ) |
14 |
13
|
simprd |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) |
15 |
|
breq2 |
⊢ ( 𝑥 = 𝑋 → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) |
16 |
15
|
anbi2d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) ) |
17 |
16
|
ralbidv |
⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) ) |
18 |
17
|
rexbidv |
⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) ) |
19 |
18
|
rspcva |
⊢ ( ( 𝑋 ∈ ℝ+ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) |
20 |
7 14 19
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) |