Step |
Hyp |
Ref |
Expression |
1 |
|
rlim2.1 |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ ) |
2 |
|
rlim2.2 |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
3 |
|
rlim2.3 |
⊢ ( 𝜑 → 𝐶 ∈ ℂ ) |
4 |
1 2 3
|
rlim2 |
⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
5 |
|
simplr |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑦 ∈ ℝ ) |
6 |
|
simpl |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) → 𝐴 ⊆ ℝ ) |
7 |
6
|
sselda |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ ) |
8 |
|
ltle |
⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 < 𝑧 → 𝑦 ≤ 𝑧 ) ) |
9 |
5 7 8
|
syl2anc |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 < 𝑧 → 𝑦 ≤ 𝑧 ) ) |
10 |
9
|
imim1d |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
11 |
10
|
ralimdva |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
12 |
2 11
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
13 |
12
|
reximdva |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
14 |
13
|
ralimdv |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
15 |
4 14
|
sylbid |
⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
16 |
|
peano2re |
⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 1 ) ∈ ℝ ) |
17 |
16
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + 1 ) ∈ ℝ ) |
18 |
|
ltp1 |
⊢ ( 𝑦 ∈ ℝ → 𝑦 < ( 𝑦 + 1 ) ) |
19 |
18
|
ad2antlr |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑦 < ( 𝑦 + 1 ) ) |
20 |
16
|
ad2antlr |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 + 1 ) ∈ ℝ ) |
21 |
|
ltletr |
⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑦 < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) ≤ 𝑧 ) → 𝑦 < 𝑧 ) ) |
22 |
5 20 7 21
|
syl3anc |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) ≤ 𝑧 ) → 𝑦 < 𝑧 ) ) |
23 |
19 22
|
mpand |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 + 1 ) ≤ 𝑧 → 𝑦 < 𝑧 ) ) |
24 |
23
|
imim1d |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ( ( 𝑦 + 1 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
25 |
24
|
ralimdva |
⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 + 1 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
26 |
2 25
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 + 1 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
27 |
|
breq1 |
⊢ ( 𝑤 = ( 𝑦 + 1 ) → ( 𝑤 ≤ 𝑧 ↔ ( 𝑦 + 1 ) ≤ 𝑧 ) ) |
28 |
27
|
rspceaimv |
⊢ ( ( ( 𝑦 + 1 ) ∈ ℝ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 + 1 ) ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) |
29 |
17 26 28
|
syl6an |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
30 |
29
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
31 |
30
|
ralimdv |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
32 |
1 2 3
|
rlim2 |
⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
33 |
31 32
|
sylibrd |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ) ) |
34 |
15 33
|
impbid |
⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 < 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |