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

Metamath Proof Explorer

Theorem nn0addge1

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

		Ref	Expression
	Assertion	nn0addge1	$⊢ (A \in ℝ \land N \in ℕ_{0}) \to A \leq A + N$

Step	Hyp	Ref	Expression
1		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
2		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
3	1 2	jca	$⊢ N \in ℕ_{0} \to (N \in ℝ \land 0 \leq N)$
4		addge01	$⊢ (A \in ℝ \land N \in ℝ) \to (0 \leq N \leftrightarrow A \leq A + N)$
5	4	biimp3a	$⊢ (A \in ℝ \land N \in ℝ \land 0 \leq N) \to A \leq A + N$
6	5	3expb	$⊢ (A \in ℝ \land (N \in ℝ \land 0 \leq N)) \to A \leq A + N$
7	3 6	sylan2	$⊢ (A \in ℝ \land N \in ℕ_{0}) \to A \leq A + N$