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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 → ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cr	⊢ ℝ
2	0 1	wcel	⊢ 𝐴 ∈ ℝ
3		cB	⊢ 𝐵
4	3 1	wcel	⊢ 𝐵 ∈ ℝ
5		cC	⊢ 𝐶
6	5 1	wcel	⊢ 𝐶 ∈ ℝ
7	2 4 6	w3a	⊢ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ )
8		cltrr	⊢ <ℝ
9	0 3 8	wbr	⊢ 𝐴 <ℝ 𝐵
10		caddc	⊢ +
11	5 0 10	co	⊢ ( 𝐶 + 𝐴 )
12	5 3 10	co	⊢ ( 𝐶 + 𝐵 )
13	11 12 8	wbr	⊢ ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 )
14	9 13	wi	⊢ ( 𝐴 <ℝ 𝐵 → ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) )
15	7 14	wi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 → ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )