This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: An integer greater than or equal to 4 is an integer greater than or equal
to 3. (Contributed by AV, 5-Sep-2025)
|
|
Ref |
Expression |
|
Assertion |
uzuzle34 |
⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ( ℤ≥ ‘ 3 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
3z |
⊢ 3 ∈ ℤ |
| 2 |
|
3re |
⊢ 3 ∈ ℝ |
| 3 |
|
4re |
⊢ 4 ∈ ℝ |
| 4 |
|
3lt4 |
⊢ 3 < 4 |
| 5 |
2 3 4
|
ltleii |
⊢ 3 ≤ 4 |
| 6 |
|
eluzuzle |
⊢ ( ( 3 ∈ ℤ ∧ 3 ≤ 4 ) → ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ( ℤ≥ ‘ 3 ) ) ) |
| 7 |
1 5 6
|
mp2an |
⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ( ℤ≥ ‘ 3 ) ) |