Axiom ax-pre-ltadd

Description: Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by theorem axpre-ltadd . Normally new proofs would use axltadd . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

	Ref	Expression
Assertion	ax-pre-ltadd	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)\to \left(A{<}_{ℝ}B\to C+A{<}_{ℝ}C+B\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cr	$$classℝ$$
2	0 1	wcel	$$wffA\in ℝ$$
3		cB	$$classB$$
4	3 1	wcel	$$wffB\in ℝ$$
5		cC	$$classC$$
6	5 1	wcel	$$wffC\in ℝ$$
7	2 4 6	w3a	$$wff\left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)$$
8		cltrr	$$class{<}_{ℝ}$$
9	0 3 8	wbr	$$wffA{<}_{ℝ}B$$
10		caddc	$$class+$$
11	5 0 10	co	$$class\left(C+A\right)$$
12	5 3 10	co	$$class\left(C+B\right)$$
13	11 12 8	wbr	$$wffC+A{<}_{ℝ}C+B$$
14	9 13	wi	$$wff\left(A{<}_{ℝ}B\to C+A{<}_{ℝ}C+B\right)$$
15	7 14	wi	$$wff\left(\left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)\to \left(A{<}_{ℝ}B\to C+A{<}_{ℝ}C+B\right)\right)$$