Theorem lep1

Description: A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006)

	Ref	Expression
Assertion	lep1	$$⊢A\in ℝ\to A\le A+1$$

Proof

Step	Hyp	Ref	Expression
1		ltp1	$$⊢A\in ℝ\to A<A+1$$
2		peano2re	$$⊢A\in ℝ\to A+1\in ℝ$$
3		ltle	$$⊢\left(A\in ℝ\wedge A+1\in ℝ\right)\to \left(A<A+1\to A\le A+1\right)$$
4	2 3	mpdan	$$⊢A\in ℝ\to \left(A<A+1\to A\le A+1\right)$$
5	1 4	mpd	$$⊢A\in ℝ\to A\le A+1$$