Theorem xltadd2

Description: Extended real version of ltadd2 . (Contributed by Mario Carneiro, 23-Aug-2015)

	Ref	Expression
Assertion	xltadd2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in ℝ\right)\to \left(A<B\leftrightarrow C{+}_{𝑒}A<C{+}_{𝑒}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		xltadd1	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in ℝ\right)\to \left(A<B\leftrightarrow A{+}_{𝑒}C<B{+}_{𝑒}C\right)$$
2		rexr	$$⊢C\in ℝ\to C\in {ℝ}^{*}$$
3		xaddcom	$$⊢\left(A\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\right)\to A{+}_{𝑒}C=C{+}_{𝑒}A$$
4	3	3adant2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\right)\to A{+}_{𝑒}C=C{+}_{𝑒}A$$
5		xaddcom	$$⊢\left(B\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\right)\to B{+}_{𝑒}C=C{+}_{𝑒}B$$
6	5	3adant1	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\right)\to B{+}_{𝑒}C=C{+}_{𝑒}B$$
7	4 6	breq12d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\right)\to \left(A{+}_{𝑒}C<B{+}_{𝑒}C\leftrightarrow C{+}_{𝑒}A<C{+}_{𝑒}B\right)$$
8	2 7	syl3an3	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in ℝ\right)\to \left(A{+}_{𝑒}C<B{+}_{𝑒}C\leftrightarrow C{+}_{𝑒}A<C{+}_{𝑒}B\right)$$
9	1 8	bitrd	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in ℝ\right)\to \left(A<B\leftrightarrow C{+}_{𝑒}A<C{+}_{𝑒}B\right)$$