Theorem ltm1

Description: A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006)

	Ref	Expression
Assertion	ltm1	$$⊢A\in ℝ\to A-1<A$$

Proof

Step	Hyp	Ref	Expression
1		0lt1	$$⊢0<1$$
2		0re	$$⊢0\in ℝ$$
3		1re	$$⊢1\in ℝ$$
4		ltsub2	$$⊢\left(0\in ℝ\wedge 1\in ℝ\wedge A\in ℝ\right)\to \left(0<1\leftrightarrow A-1<A-0\right)$$
5	2 3 4	mp3an12	$$⊢A\in ℝ\to \left(0<1\leftrightarrow A-1<A-0\right)$$
6	1 5	mpbii	$$⊢A\in ℝ\to A-1<A-0$$
7		recn	$$⊢A\in ℝ\to A\in ℂ$$
8	7	subid1d	$$⊢A\in ℝ\to A-0=A$$
9	6 8	breqtrd	$$⊢A\in ℝ\to A-1<A$$