Step |
Hyp |
Ref |
Expression |
1 |
|
arch |
⊢ ( 𝑥 ∈ ℝ → ∃ 𝑘 ∈ ℕ 𝑥 < 𝑘 ) |
2 |
|
nnre |
⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ ) |
3 |
|
lelttr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝑘 ) → 𝐴 < 𝑘 ) ) |
4 |
|
ltle |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐴 < 𝑘 → 𝐴 ≤ 𝑘 ) ) |
5 |
4
|
3adant2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝐴 < 𝑘 → 𝐴 ≤ 𝑘 ) ) |
6 |
3 5
|
syld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝑘 ) → 𝐴 ≤ 𝑘 ) ) |
7 |
6
|
exp5o |
⊢ ( 𝐴 ∈ ℝ → ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ℝ → ( 𝐴 ≤ 𝑥 → ( 𝑥 < 𝑘 → 𝐴 ≤ 𝑘 ) ) ) ) ) |
8 |
7
|
com3l |
⊢ ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ℝ → ( 𝐴 ∈ ℝ → ( 𝐴 ≤ 𝑥 → ( 𝑥 < 𝑘 → 𝐴 ≤ 𝑘 ) ) ) ) ) |
9 |
8
|
imp4b |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → ( 𝑥 < 𝑘 → 𝐴 ≤ 𝑘 ) ) ) |
10 |
9
|
com23 |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑥 < 𝑘 → ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑘 ) ) ) |
11 |
2 10
|
sylan2 |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑥 < 𝑘 → ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑘 ) ) ) |
12 |
11
|
reximdva |
⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑘 ∈ ℕ 𝑥 < 𝑘 → ∃ 𝑘 ∈ ℕ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑘 ) ) ) |
13 |
1 12
|
mpd |
⊢ ( 𝑥 ∈ ℝ → ∃ 𝑘 ∈ ℕ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑘 ) ) |
14 |
|
r19.35 |
⊢ ( ∃ 𝑘 ∈ ℕ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑘 ) ↔ ( ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → ∃ 𝑘 ∈ ℕ 𝐴 ≤ 𝑘 ) ) |
15 |
13 14
|
sylib |
⊢ ( 𝑥 ∈ ℝ → ( ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → ∃ 𝑘 ∈ ℕ 𝐴 ≤ 𝑘 ) ) |
16 |
15
|
rexlimiv |
⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) → ∃ 𝑘 ∈ ℕ 𝐴 ≤ 𝑘 ) |