Step |
Hyp |
Ref |
Expression |
1 |
|
rlim0.1 |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ ) |
2 |
|
rlim0.2 |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
3 |
|
0cnd |
⊢ ( 𝜑 → 0 ∈ ℂ ) |
4 |
1 2 3
|
rlim2 |
⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ) ) |
5 |
|
subid1 |
⊢ ( 𝐵 ∈ ℂ → ( 𝐵 − 0 ) = 𝐵 ) |
6 |
5
|
fveq2d |
⊢ ( 𝐵 ∈ ℂ → ( abs ‘ ( 𝐵 − 0 ) ) = ( abs ‘ 𝐵 ) ) |
7 |
6
|
breq1d |
⊢ ( 𝐵 ∈ ℂ → ( ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ↔ ( abs ‘ 𝐵 ) < 𝑥 ) ) |
8 |
7
|
imbi2d |
⊢ ( 𝐵 ∈ ℂ → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) ) |
9 |
8
|
ralimi |
⊢ ( ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ → ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) ) |
10 |
|
ralbi |
⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) ) |
11 |
1 9 10
|
3syl |
⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) ) |
12 |
11
|
rexbidv |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) ) |
13 |
12
|
ralbidv |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) ) |
14 |
4 13
|
bitrd |
⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ 𝐵 ) < 𝑥 ) ) ) |