Step |
Hyp |
Ref |
Expression |
1 |
|
axltadd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 → ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ) ) |
2 |
|
oveq2 |
⊢ ( 𝐴 = 𝐵 → ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ) |
3 |
2
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 = 𝐵 → ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ) ) |
4 |
|
axltadd |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐴 → ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) ) |
5 |
4
|
3com12 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐴 → ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) ) |
6 |
3 5
|
orim12d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) → ( ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ∨ ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) ) ) |
7 |
6
|
con3d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ ( ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ∨ ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) → ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
8 |
|
simp3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ ) |
9 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ ) |
10 |
8 9
|
readdcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + 𝐴 ) ∈ ℝ ) |
11 |
|
simp2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ ) |
12 |
8 11
|
readdcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + 𝐵 ) ∈ ℝ ) |
13 |
|
axlttri |
⊢ ( ( ( 𝐶 + 𝐴 ) ∈ ℝ ∧ ( 𝐶 + 𝐵 ) ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ↔ ¬ ( ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ∨ ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) ) ) |
14 |
10 12 13
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ↔ ¬ ( ( 𝐶 + 𝐴 ) = ( 𝐶 + 𝐵 ) ∨ ( 𝐶 + 𝐵 ) < ( 𝐶 + 𝐴 ) ) ) ) |
15 |
|
axlttri |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
16 |
9 11 15
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
17 |
7 14 16
|
3imtr4d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) → 𝐴 < 𝐵 ) ) |
18 |
1 17
|
impbid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ) ) |