This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Construction and axiomatization of real and complex numbers Real and complex number postulates restated as axioms 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 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 → ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )