Step |
Hyp |
Ref |
Expression |
1 |
|
uzubioo2.1 |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
2 |
|
uzubioo2.2 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
3 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑀 ∈ ℤ ) |
4 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ ) |
5 |
3 2 4
|
uzubioo |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∃ 𝑘 ∈ ( 𝑦 (,) +∞ ) 𝑘 ∈ 𝑍 ) |
6 |
5
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ( 𝑦 (,) +∞ ) 𝑘 ∈ 𝑍 ) |
7 |
|
oveq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 (,) +∞ ) = ( 𝑦 (,) +∞ ) ) |
8 |
7
|
rexeqdv |
⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑘 ∈ ( 𝑥 (,) +∞ ) 𝑘 ∈ 𝑍 ↔ ∃ 𝑘 ∈ ( 𝑦 (,) +∞ ) 𝑘 ∈ 𝑍 ) ) |
9 |
8
|
cbvralvw |
⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ( 𝑥 (,) +∞ ) 𝑘 ∈ 𝑍 ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ( 𝑦 (,) +∞ ) 𝑘 ∈ 𝑍 ) |
10 |
6 9
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ( 𝑥 (,) +∞ ) 𝑘 ∈ 𝑍 ) |