Theorem nn0le2x

Description: A nonnegative integer is less than or equal to twice itself. Generalization of nn0le2xi . (Contributed by Raph Levien, 10-Dec-2002) (Revised by AV, 9-Sep-2025)

	Ref	Expression
Assertion	nn0le2x	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ ( 2 · 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
2		nn0addge1	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ≤ ( 𝑁 + 𝑁 ) )
3	1 2	mpancom	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ ( 𝑁 + 𝑁 ) )
4		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
5	4	2timesd	⊢ ( 𝑁 ∈ ℕ0 → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
6	3 5	breqtrrd	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ ( 2 · 𝑁 ) )