Theorem nn0addge2

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

	Ref	Expression
Assertion	nn0addge2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ≤ ( 𝑁 + 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
2		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
3	1 2	jca	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) )
4		addge02	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 ≤ 𝑁 ↔ 𝐴 ≤ ( 𝑁 + 𝐴 ) ) )
5	4	biimp3a	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) → 𝐴 ≤ ( 𝑁 + 𝐴 ) )
6	5	3expb	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ) → 𝐴 ≤ ( 𝑁 + 𝐴 ) )
7	3 6	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ≤ ( 𝑁 + 𝐴 ) )