Step | Hyp | Ref
| Expression |
1 | | elreal 7777 |
. . 3
⊢ (𝐴 ∈ ℝ ↔
∃𝑥 ∈
R 〈𝑥,
0R〉 = 𝐴) |
2 | | elreal 7777 |
. . 3
⊢ (𝐵 ∈ ℝ ↔
∃𝑦 ∈
R 〈𝑦,
0R〉 = 𝐵) |
3 | | elreal 7777 |
. . 3
⊢ (𝐶 ∈ ℝ ↔
∃𝑧 ∈
R 〈𝑧,
0R〉 = 𝐶) |
4 | | breq1 3990 |
. . . 4
⊢
(〈𝑥,
0R〉 = 𝐴 → (〈𝑥, 0R〉
<ℝ 〈𝑦, 0R〉 ↔
𝐴 <ℝ
〈𝑦,
0R〉)) |
5 | | oveq2 5858 |
. . . . 5
⊢
(〈𝑥,
0R〉 = 𝐴 → (〈𝑧, 0R〉 +
〈𝑥,
0R〉) = (〈𝑧, 0R〉 + 𝐴)) |
6 | 5 | breq1d 3997 |
. . . 4
⊢
(〈𝑥,
0R〉 = 𝐴 → ((〈𝑧, 0R〉 +
〈𝑥,
0R〉) <ℝ (〈𝑧,
0R〉 + 〈𝑦, 0R〉) ↔
(〈𝑧,
0R〉 + 𝐴) <ℝ (〈𝑧,
0R〉 + 〈𝑦,
0R〉))) |
7 | 4, 6 | bibi12d 234 |
. . 3
⊢
(〈𝑥,
0R〉 = 𝐴 → ((〈𝑥, 0R〉
<ℝ 〈𝑦, 0R〉 ↔
(〈𝑧,
0R〉 + 〈𝑥, 0R〉)
<ℝ (〈𝑧, 0R〉 +
〈𝑦,
0R〉)) ↔ (𝐴 <ℝ 〈𝑦,
0R〉 ↔ (〈𝑧, 0R〉 + 𝐴) <ℝ
(〈𝑧,
0R〉 + 〈𝑦,
0R〉)))) |
8 | | breq2 3991 |
. . . 4
⊢
(〈𝑦,
0R〉 = 𝐵 → (𝐴 <ℝ 〈𝑦,
0R〉 ↔ 𝐴 <ℝ 𝐵)) |
9 | | oveq2 5858 |
. . . . 5
⊢
(〈𝑦,
0R〉 = 𝐵 → (〈𝑧, 0R〉 +
〈𝑦,
0R〉) = (〈𝑧, 0R〉 + 𝐵)) |
10 | 9 | breq2d 3999 |
. . . 4
⊢
(〈𝑦,
0R〉 = 𝐵 → ((〈𝑧, 0R〉 + 𝐴) <ℝ
(〈𝑧,
0R〉 + 〈𝑦, 0R〉) ↔
(〈𝑧,
0R〉 + 𝐴) <ℝ (〈𝑧,
0R〉 + 𝐵))) |
11 | 8, 10 | bibi12d 234 |
. . 3
⊢
(〈𝑦,
0R〉 = 𝐵 → ((𝐴 <ℝ 〈𝑦,
0R〉 ↔ (〈𝑧, 0R〉 + 𝐴) <ℝ
(〈𝑧,
0R〉 + 〈𝑦, 0R〉)) ↔
(𝐴 <ℝ
𝐵 ↔ (〈𝑧,
0R〉 + 𝐴) <ℝ (〈𝑧,
0R〉 + 𝐵)))) |
12 | | oveq1 5857 |
. . . . 5
⊢
(〈𝑧,
0R〉 = 𝐶 → (〈𝑧, 0R〉 + 𝐴) = (𝐶 + 𝐴)) |
13 | | oveq1 5857 |
. . . . 5
⊢
(〈𝑧,
0R〉 = 𝐶 → (〈𝑧, 0R〉 + 𝐵) = (𝐶 + 𝐵)) |
14 | 12, 13 | breq12d 4000 |
. . . 4
⊢
(〈𝑧,
0R〉 = 𝐶 → ((〈𝑧, 0R〉 + 𝐴) <ℝ
(〈𝑧,
0R〉 + 𝐵) ↔ (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) |
15 | 14 | bibi2d 231 |
. . 3
⊢
(〈𝑧,
0R〉 = 𝐶 → ((𝐴 <ℝ 𝐵 ↔ (〈𝑧, 0R〉 + 𝐴) <ℝ
(〈𝑧,
0R〉 + 𝐵)) ↔ (𝐴 <ℝ 𝐵 ↔ (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))) |
16 | | ltasrg 7719 |
. . . 4
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → (𝑥
<R 𝑦 ↔ (𝑧 +R 𝑥) <R
(𝑧
+R 𝑦))) |
17 | | ltresr 7788 |
. . . . 5
⊢
(〈𝑥,
0R〉 <ℝ 〈𝑦,
0R〉 ↔ 𝑥 <R 𝑦) |
18 | 17 | a1i 9 |
. . . 4
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → (〈𝑥, 0R〉
<ℝ 〈𝑦, 0R〉 ↔
𝑥
<R 𝑦)) |
19 | | simp3 994 |
. . . . . 6
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → 𝑧
∈ R) |
20 | | simp1 992 |
. . . . . 6
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → 𝑥
∈ R) |
21 | | simp2 993 |
. . . . . 6
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → 𝑦
∈ R) |
22 | | addresr 7786 |
. . . . . . 7
⊢ ((𝑧 ∈ R ∧
𝑥 ∈ R)
→ (〈𝑧,
0R〉 + 〈𝑥, 0R〉) =
〈(𝑧
+R 𝑥),
0R〉) |
23 | | addresr 7786 |
. . . . . . 7
⊢ ((𝑧 ∈ R ∧
𝑦 ∈ R)
→ (〈𝑧,
0R〉 + 〈𝑦, 0R〉) =
〈(𝑧
+R 𝑦),
0R〉) |
24 | 22, 23 | breqan12d 4003 |
. . . . . 6
⊢ (((𝑧 ∈ R ∧
𝑥 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑦
∈ R)) → ((〈𝑧, 0R〉 +
〈𝑥,
0R〉) <ℝ (〈𝑧,
0R〉 + 〈𝑦, 0R〉) ↔
〈(𝑧
+R 𝑥), 0R〉
<ℝ 〈(𝑧 +R 𝑦),
0R〉)) |
25 | 19, 20, 19, 21, 24 | syl22anc 1234 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → ((〈𝑧, 0R〉 +
〈𝑥,
0R〉) <ℝ (〈𝑧,
0R〉 + 〈𝑦, 0R〉) ↔
〈(𝑧
+R 𝑥), 0R〉
<ℝ 〈(𝑧 +R 𝑦),
0R〉)) |
26 | | ltresr 7788 |
. . . . 5
⊢
(〈(𝑧
+R 𝑥), 0R〉
<ℝ 〈(𝑧 +R 𝑦),
0R〉 ↔ (𝑧 +R 𝑥) <R
(𝑧
+R 𝑦)) |
27 | 25, 26 | bitrdi 195 |
. . . 4
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → ((〈𝑧, 0R〉 +
〈𝑥,
0R〉) <ℝ (〈𝑧,
0R〉 + 〈𝑦, 0R〉) ↔
(𝑧
+R 𝑥) <R (𝑧 +R
𝑦))) |
28 | 16, 18, 27 | 3bitr4d 219 |
. . 3
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → (〈𝑥, 0R〉
<ℝ 〈𝑦, 0R〉 ↔
(〈𝑧,
0R〉 + 〈𝑥, 0R〉)
<ℝ (〈𝑧, 0R〉 +
〈𝑦,
0R〉))) |
29 | 1, 2, 3, 7, 11, 15, 28 | 3gencl 2764 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) |
30 | 29 | biimpd 143 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) |