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

Metamath Proof Explorer

Theorem nn0addge2i

Description: A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005)

Ref Expression
Hypotheses nn0addge1i.1 ⊢ 𝐴 ∈ ℝ
nn0addge1i.2 ⊢ 𝑁 ∈ ℕ0
Assertion nn0addge2i 𝐴 ≤ ( 𝑁 + 𝐴 )

Proof

Step Hyp Ref Expression
1 nn0addge1i.1 ⊢ 𝐴 ∈ ℝ
2 nn0addge1i.2 ⊢ 𝑁 ∈ ℕ0
3 nn0addge2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ≤ ( 𝑁 + 𝐴 ) )
4 1 2 3 mp2an ⊢ 𝐴 ≤ ( 𝑁 + 𝐴 )