Description: A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002) (Proof shortened by AV, 9-Sep-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nn0le2xi.1 | ⊢ 𝑁 ∈ ℕ0 | |
Assertion | nn0le2xi | ⊢ 𝑁 ≤ ( 2 · 𝑁 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0le2xi.1 | ⊢ 𝑁 ∈ ℕ0 | |
2 | nn0le2x | ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ ( 2 · 𝑁 ) ) | |
3 | 1 2 | ax-mp | ⊢ 𝑁 ≤ ( 2 · 𝑁 ) |