Theorem ltaddpos

Description: Adding a positive number to another number increases it. (Contributed by NM, 17-Nov-2004)

	Ref	Expression
Assertion	ltaddpos	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0<A\leftrightarrow B<B+A\right)$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		ltadd2	$$⊢\left(0\in ℝ\wedge A\in ℝ\wedge B\in ℝ\right)\to \left(0<A\leftrightarrow B+0<B+A\right)$$
3	1 2	mp3an1	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0<A\leftrightarrow B+0<B+A\right)$$
4		recn	$$⊢B\in ℝ\to B\in ℂ$$
5	4	addridd	$$⊢B\in ℝ\to B+0=B$$
6	5	adantl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B+0=B$$
7	6	breq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B+0<B+A\leftrightarrow B<B+A\right)$$
8	3 7	bitrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0<A\leftrightarrow B<B+A\right)$$