Step | Hyp | Ref
| Expression |
1 | | elreal 11074 |
. . 3
⊢ (𝐴 ∈ ℝ ↔
∃𝑥 ∈
R ⟨𝑥,
0R⟩ = 𝐴) |
2 | | elreal 11074 |
. . 3
⊢ (𝐵 ∈ ℝ ↔
∃𝑦 ∈
R ⟨𝑦,
0R⟩ = 𝐵) |
3 | | elreal 11074 |
. . 3
⊢ (𝐶 ∈ ℝ ↔
∃𝑧 ∈
R ⟨𝑧,
0R⟩ = 𝐶) |
4 | | breq1 5113 |
. . . 4
⊢
(⟨𝑥,
0R⟩ = 𝐴 → (⟨𝑥, 0R⟩
<ℝ ⟨𝑦, 0R⟩ ↔
𝐴 <ℝ
⟨𝑦,
0R⟩)) |
5 | | oveq2 7370 |
. . . . 5
⊢
(⟨𝑥,
0R⟩ = 𝐴 → (⟨𝑧, 0R⟩ +
⟨𝑥,
0R⟩) = (⟨𝑧, 0R⟩ + 𝐴)) |
6 | 5 | breq1d 5120 |
. . . 4
⊢
(⟨𝑥,
0R⟩ = 𝐴 → ((⟨𝑧, 0R⟩ +
⟨𝑥,
0R⟩) <ℝ (⟨𝑧,
0R⟩ + ⟨𝑦, 0R⟩) ↔
(⟨𝑧,
0R⟩ + 𝐴) <ℝ (⟨𝑧,
0R⟩ + ⟨𝑦,
0R⟩))) |
7 | 4, 6 | bibi12d 346 |
. . 3
⊢
(⟨𝑥,
0R⟩ = 𝐴 → ((⟨𝑥, 0R⟩
<ℝ ⟨𝑦, 0R⟩ ↔
(⟨𝑧,
0R⟩ + ⟨𝑥, 0R⟩)
<ℝ (⟨𝑧, 0R⟩ +
⟨𝑦,
0R⟩)) ↔ (𝐴 <ℝ ⟨𝑦,
0R⟩ ↔ (⟨𝑧, 0R⟩ + 𝐴) <ℝ
(⟨𝑧,
0R⟩ + ⟨𝑦,
0R⟩)))) |
8 | | breq2 5114 |
. . . 4
⊢
(⟨𝑦,
0R⟩ = 𝐵 → (𝐴 <ℝ ⟨𝑦,
0R⟩ ↔ 𝐴 <ℝ 𝐵)) |
9 | | oveq2 7370 |
. . . . 5
⊢
(⟨𝑦,
0R⟩ = 𝐵 → (⟨𝑧, 0R⟩ +
⟨𝑦,
0R⟩) = (⟨𝑧, 0R⟩ + 𝐵)) |
10 | 9 | breq2d 5122 |
. . . 4
⊢
(⟨𝑦,
0R⟩ = 𝐵 → ((⟨𝑧, 0R⟩ + 𝐴) <ℝ
(⟨𝑧,
0R⟩ + ⟨𝑦, 0R⟩) ↔
(⟨𝑧,
0R⟩ + 𝐴) <ℝ (⟨𝑧,
0R⟩ + 𝐵))) |
11 | 8, 10 | bibi12d 346 |
. . 3
⊢
(⟨𝑦,
0R⟩ = 𝐵 → ((𝐴 <ℝ ⟨𝑦,
0R⟩ ↔ (⟨𝑧, 0R⟩ + 𝐴) <ℝ
(⟨𝑧,
0R⟩ + ⟨𝑦, 0R⟩)) ↔
(𝐴 <ℝ
𝐵 ↔ (⟨𝑧,
0R⟩ + 𝐴) <ℝ (⟨𝑧,
0R⟩ + 𝐵)))) |
12 | | oveq1 7369 |
. . . . 5
⊢
(⟨𝑧,
0R⟩ = 𝐶 → (⟨𝑧, 0R⟩ + 𝐴) = (𝐶 + 𝐴)) |
13 | | oveq1 7369 |
. . . . 5
⊢
(⟨𝑧,
0R⟩ = 𝐶 → (⟨𝑧, 0R⟩ + 𝐵) = (𝐶 + 𝐵)) |
14 | 12, 13 | breq12d 5123 |
. . . 4
⊢
(⟨𝑧,
0R⟩ = 𝐶 → ((⟨𝑧, 0R⟩ + 𝐴) <ℝ
(⟨𝑧,
0R⟩ + 𝐵) ↔ (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) |
15 | 14 | bibi2d 343 |
. . 3
⊢
(⟨𝑧,
0R⟩ = 𝐶 → ((𝐴 <ℝ 𝐵 ↔ (⟨𝑧, 0R⟩ + 𝐴) <ℝ
(⟨𝑧,
0R⟩ + 𝐵)) ↔ (𝐴 <ℝ 𝐵 ↔ (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))) |
16 | | ltasr 11043 |
. . . . . . 7
⊢ (𝑧 ∈ R →
(𝑥
<R 𝑦 ↔ (𝑧 +R 𝑥) <R
(𝑧
+R 𝑦))) |
17 | 16 | adantr 482 |
. . . . . 6
⊢ ((𝑧 ∈ R ∧
(𝑥 ∈ R
∧ 𝑦 ∈
R)) → (𝑥
<R 𝑦 ↔ (𝑧 +R 𝑥) <R
(𝑧
+R 𝑦))) |
18 | | ltresr 11083 |
. . . . . . 7
⊢
(⟨𝑥,
0R⟩ <ℝ ⟨𝑦,
0R⟩ ↔ 𝑥 <R 𝑦) |
19 | 18 | a1i 11 |
. . . . . 6
⊢ ((𝑧 ∈ R ∧
(𝑥 ∈ R
∧ 𝑦 ∈
R)) → (⟨𝑥, 0R⟩
<ℝ ⟨𝑦, 0R⟩ ↔
𝑥
<R 𝑦)) |
20 | | addresr 11081 |
. . . . . . . . 9
⊢ ((𝑧 ∈ R ∧
𝑥 ∈ R)
→ (⟨𝑧,
0R⟩ + ⟨𝑥, 0R⟩) =
⟨(𝑧
+R 𝑥),
0R⟩) |
21 | | addresr 11081 |
. . . . . . . . 9
⊢ ((𝑧 ∈ R ∧
𝑦 ∈ R)
→ (⟨𝑧,
0R⟩ + ⟨𝑦, 0R⟩) =
⟨(𝑧
+R 𝑦),
0R⟩) |
22 | 20, 21 | breqan12d 5126 |
. . . . . . . 8
⊢ (((𝑧 ∈ R ∧
𝑥 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑦
∈ R)) → ((⟨𝑧, 0R⟩ +
⟨𝑥,
0R⟩) <ℝ (⟨𝑧,
0R⟩ + ⟨𝑦, 0R⟩) ↔
⟨(𝑧
+R 𝑥), 0R⟩
<ℝ ⟨(𝑧 +R 𝑦),
0R⟩)) |
23 | 22 | anandis 677 |
. . . . . . 7
⊢ ((𝑧 ∈ R ∧
(𝑥 ∈ R
∧ 𝑦 ∈
R)) → ((⟨𝑧, 0R⟩ +
⟨𝑥,
0R⟩) <ℝ (⟨𝑧,
0R⟩ + ⟨𝑦, 0R⟩) ↔
⟨(𝑧
+R 𝑥), 0R⟩
<ℝ ⟨(𝑧 +R 𝑦),
0R⟩)) |
24 | | ltresr 11083 |
. . . . . . 7
⊢
(⟨(𝑧
+R 𝑥), 0R⟩
<ℝ ⟨(𝑧 +R 𝑦),
0R⟩ ↔ (𝑧 +R 𝑥) <R
(𝑧
+R 𝑦)) |
25 | 23, 24 | bitrdi 287 |
. . . . . 6
⊢ ((𝑧 ∈ R ∧
(𝑥 ∈ R
∧ 𝑦 ∈
R)) → ((⟨𝑧, 0R⟩ +
⟨𝑥,
0R⟩) <ℝ (⟨𝑧,
0R⟩ + ⟨𝑦, 0R⟩) ↔
(𝑧
+R 𝑥) <R (𝑧 +R
𝑦))) |
26 | 17, 19, 25 | 3bitr4d 311 |
. . . . 5
⊢ ((𝑧 ∈ R ∧
(𝑥 ∈ R
∧ 𝑦 ∈
R)) → (⟨𝑥, 0R⟩
<ℝ ⟨𝑦, 0R⟩ ↔
(⟨𝑧,
0R⟩ + ⟨𝑥, 0R⟩)
<ℝ (⟨𝑧, 0R⟩ +
⟨𝑦,
0R⟩))) |
27 | 26 | ancoms 460 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ 𝑧 ∈
R) → (⟨𝑥, 0R⟩
<ℝ ⟨𝑦, 0R⟩ ↔
(⟨𝑧,
0R⟩ + ⟨𝑥, 0R⟩)
<ℝ (⟨𝑧, 0R⟩ +
⟨𝑦,
0R⟩))) |
28 | 27 | 3impa 1111 |
. . 3
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → (⟨𝑥, 0R⟩
<ℝ ⟨𝑦, 0R⟩ ↔
(⟨𝑧,
0R⟩ + ⟨𝑥, 0R⟩)
<ℝ (⟨𝑧, 0R⟩ +
⟨𝑦,
0R⟩))) |
29 | 1, 2, 3, 7, 11, 15, 28 | 3gencl 3490 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) |
30 | 29 | biimpd 228 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) |