This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝑁 ∈ ℕ₀ → 𝑁 ≤ ( 2 · 𝑁 ) )

Proof

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