| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elreal 11171 | . . 3
⊢ (𝐴 ∈ ℝ ↔
∃𝑥 ∈
R 〈𝑥,
0R〉 = 𝐴) | 
| 2 |  | elreal 11171 | . . 3
⊢ (𝐵 ∈ ℝ ↔
∃𝑦 ∈
R 〈𝑦,
0R〉 = 𝐵) | 
| 3 |  | elreal 11171 | . . 3
⊢ (𝐶 ∈ ℝ ↔
∃𝑧 ∈
R 〈𝑧,
0R〉 = 𝐶) | 
| 4 |  | breq1 5146 | . . . 4
⊢
(〈𝑥,
0R〉 = 𝐴 → (〈𝑥, 0R〉
<ℝ 〈𝑦, 0R〉 ↔
𝐴 <ℝ
〈𝑦,
0R〉)) | 
| 5 |  | oveq2 7439 | . . . . 5
⊢
(〈𝑥,
0R〉 = 𝐴 → (〈𝑧, 0R〉 +
〈𝑥,
0R〉) = (〈𝑧, 0R〉 + 𝐴)) | 
| 6 | 5 | breq1d 5153 | . . . 4
⊢
(〈𝑥,
0R〉 = 𝐴 → ((〈𝑧, 0R〉 +
〈𝑥,
0R〉) <ℝ (〈𝑧,
0R〉 + 〈𝑦, 0R〉) ↔
(〈𝑧,
0R〉 + 𝐴) <ℝ (〈𝑧,
0R〉 + 〈𝑦,
0R〉))) | 
| 7 | 4, 6 | bibi12d 345 | . . 3
⊢
(〈𝑥,
0R〉 = 𝐴 → ((〈𝑥, 0R〉
<ℝ 〈𝑦, 0R〉 ↔
(〈𝑧,
0R〉 + 〈𝑥, 0R〉)
<ℝ (〈𝑧, 0R〉 +
〈𝑦,
0R〉)) ↔ (𝐴 <ℝ 〈𝑦,
0R〉 ↔ (〈𝑧, 0R〉 + 𝐴) <ℝ
(〈𝑧,
0R〉 + 〈𝑦,
0R〉)))) | 
| 8 |  | breq2 5147 | . . . 4
⊢
(〈𝑦,
0R〉 = 𝐵 → (𝐴 <ℝ 〈𝑦,
0R〉 ↔ 𝐴 <ℝ 𝐵)) | 
| 9 |  | oveq2 7439 | . . . . 5
⊢
(〈𝑦,
0R〉 = 𝐵 → (〈𝑧, 0R〉 +
〈𝑦,
0R〉) = (〈𝑧, 0R〉 + 𝐵)) | 
| 10 | 9 | breq2d 5155 | . . . 4
⊢
(〈𝑦,
0R〉 = 𝐵 → ((〈𝑧, 0R〉 + 𝐴) <ℝ
(〈𝑧,
0R〉 + 〈𝑦, 0R〉) ↔
(〈𝑧,
0R〉 + 𝐴) <ℝ (〈𝑧,
0R〉 + 𝐵))) | 
| 11 | 8, 10 | bibi12d 345 | . . 3
⊢
(〈𝑦,
0R〉 = 𝐵 → ((𝐴 <ℝ 〈𝑦,
0R〉 ↔ (〈𝑧, 0R〉 + 𝐴) <ℝ
(〈𝑧,
0R〉 + 〈𝑦, 0R〉)) ↔
(𝐴 <ℝ
𝐵 ↔ (〈𝑧,
0R〉 + 𝐴) <ℝ (〈𝑧,
0R〉 + 𝐵)))) | 
| 12 |  | oveq1 7438 | . . . . 5
⊢
(〈𝑧,
0R〉 = 𝐶 → (〈𝑧, 0R〉 + 𝐴) = (𝐶 + 𝐴)) | 
| 13 |  | oveq1 7438 | . . . . 5
⊢
(〈𝑧,
0R〉 = 𝐶 → (〈𝑧, 0R〉 + 𝐵) = (𝐶 + 𝐵)) | 
| 14 | 12, 13 | breq12d 5156 | . . . 4
⊢
(〈𝑧,
0R〉 = 𝐶 → ((〈𝑧, 0R〉 + 𝐴) <ℝ
(〈𝑧,
0R〉 + 𝐵) ↔ (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | 
| 15 | 14 | bibi2d 342 | . . 3
⊢
(〈𝑧,
0R〉 = 𝐶 → ((𝐴 <ℝ 𝐵 ↔ (〈𝑧, 0R〉 + 𝐴) <ℝ
(〈𝑧,
0R〉 + 𝐵)) ↔ (𝐴 <ℝ 𝐵 ↔ (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))) | 
| 16 |  | ltasr 11140 | . . . . . . 7
⊢ (𝑧 ∈ R →
(𝑥
<R 𝑦 ↔ (𝑧 +R 𝑥) <R
(𝑧
+R 𝑦))) | 
| 17 | 16 | adantr 480 | . . . . . 6
⊢ ((𝑧 ∈ R ∧
(𝑥 ∈ R
∧ 𝑦 ∈
R)) → (𝑥
<R 𝑦 ↔ (𝑧 +R 𝑥) <R
(𝑧
+R 𝑦))) | 
| 18 |  | ltresr 11180 | . . . . . . 7
⊢
(〈𝑥,
0R〉 <ℝ 〈𝑦,
0R〉 ↔ 𝑥 <R 𝑦) | 
| 19 | 18 | a1i 11 | . . . . . 6
⊢ ((𝑧 ∈ R ∧
(𝑥 ∈ R
∧ 𝑦 ∈
R)) → (〈𝑥, 0R〉
<ℝ 〈𝑦, 0R〉 ↔
𝑥
<R 𝑦)) | 
| 20 |  | addresr 11178 | . . . . . . . . 9
⊢ ((𝑧 ∈ R ∧
𝑥 ∈ R)
→ (〈𝑧,
0R〉 + 〈𝑥, 0R〉) =
〈(𝑧
+R 𝑥),
0R〉) | 
| 21 |  | addresr 11178 | . . . . . . . . 9
⊢ ((𝑧 ∈ R ∧
𝑦 ∈ R)
→ (〈𝑧,
0R〉 + 〈𝑦, 0R〉) =
〈(𝑧
+R 𝑦),
0R〉) | 
| 22 | 20, 21 | breqan12d 5159 | . . . . . . . 8
⊢ (((𝑧 ∈ R ∧
𝑥 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑦
∈ R)) → ((〈𝑧, 0R〉 +
〈𝑥,
0R〉) <ℝ (〈𝑧,
0R〉 + 〈𝑦, 0R〉) ↔
〈(𝑧
+R 𝑥), 0R〉
<ℝ 〈(𝑧 +R 𝑦),
0R〉)) | 
| 23 | 22 | anandis 678 | . . . . . . 7
⊢ ((𝑧 ∈ R ∧
(𝑥 ∈ R
∧ 𝑦 ∈
R)) → ((〈𝑧, 0R〉 +
〈𝑥,
0R〉) <ℝ (〈𝑧,
0R〉 + 〈𝑦, 0R〉) ↔
〈(𝑧
+R 𝑥), 0R〉
<ℝ 〈(𝑧 +R 𝑦),
0R〉)) | 
| 24 |  | ltresr 11180 | . . . . . . 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 458 | . . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ 𝑧 ∈
R) → (〈𝑥, 0R〉
<ℝ 〈𝑦, 0R〉 ↔
(〈𝑧,
0R〉 + 〈𝑥, 0R〉)
<ℝ (〈𝑧, 0R〉 +
〈𝑦,
0R〉))) | 
| 28 | 27 | 3impa 1110 | . . 3
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R
∧ 𝑧 ∈
R) → (〈𝑥, 0R〉
<ℝ 〈𝑦, 0R〉 ↔
(〈𝑧,
0R〉 + 〈𝑥, 0R〉)
<ℝ (〈𝑧, 0R〉 +
〈𝑦,
0R〉))) | 
| 29 | 1, 2, 3, 7, 11, 15, 28 | 3gencl 3525 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | 
| 30 | 29 | biimpd 229 | 1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) |