Proof of Theorem xleadd1a
| Step | Hyp | Ref
| Expression |
| 1 | | simplrr 778 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ) |
| 2 | | simpr 484 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ) |
| 3 | | simplrl 777 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐶 ∈ ℝ) |
| 4 | | simpllr 776 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ 𝐵) |
| 5 | 1, 2, 3, 4 | leadd1dd 11877 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)) |
| 6 | 1, 3 | rexaddd 13276 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) = (𝐴 + 𝐶)) |
| 7 | 2, 3 | rexaddd 13276 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
| 8 | 5, 6, 7 | 3brtr4d 5175 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 9 | | simpl1 1192 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈
ℝ*) |
| 10 | | simpl3 1194 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐶 ∈
ℝ*) |
| 11 | | xaddcl 13281 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
| 12 | 9, 10, 11 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
| 13 | 12 | ad2antrr 726 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
| 14 | | pnfge 13172 |
. . . . . . 7
⊢ ((𝐴 +𝑒 𝐶) ∈ ℝ*
→ (𝐴
+𝑒 𝐶)
≤ +∞) |
| 15 | 13, 14 | syl 17 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ≤ +∞) |
| 16 | | oveq1 7438 |
. . . . . . 7
⊢ (𝐵 = +∞ → (𝐵 +𝑒 𝐶) = (+∞
+𝑒 𝐶)) |
| 17 | | rexr 11307 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℝ*) |
| 18 | | renemnf 11310 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ → 𝐶 ≠ -∞) |
| 19 | | xaddpnf2 13269 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ -∞)
→ (+∞ +𝑒 𝐶) = +∞) |
| 20 | 17, 18, 19 | syl2anc 584 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ → (+∞
+𝑒 𝐶) =
+∞) |
| 21 | 20 | ad2antrl 728 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (+∞
+𝑒 𝐶) =
+∞) |
| 22 | 16, 21 | sylan9eqr 2799 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = +∞) |
| 23 | 15, 22 | breqtrrd 5171 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 24 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
| 25 | 24 | xrleidd 13194 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶)) |
| 26 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐴 ≤ 𝐵) |
| 27 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐵 = -∞) |
| 28 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐴 ∈
ℝ*) |
| 29 | | mnfle 13177 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ*
→ -∞ ≤ 𝐴) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → -∞ ≤ 𝐴) |
| 31 | 27, 30 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐵 ≤ 𝐴) |
| 32 | | simpl2 1193 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈
ℝ*) |
| 33 | | xrletri3 13196 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
| 34 | 9, 32, 33 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
| 35 | 34 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
| 36 | 26, 31, 35 | mpbir2and 713 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐴 = 𝐵) |
| 37 | 36 | oveq1d 7446 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) = (𝐵 +𝑒 𝐶)) |
| 38 | 25, 37 | breqtrd 5169 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 39 | 38 | adantlr 715 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 40 | | elxr 13158 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
| 41 | 32, 40 | sylib 218 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
| 42 | 41 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
| 43 | 8, 23, 39, 42 | mpjao3dan 1434 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 44 | 43 | anassrs 467 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 45 | 12 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
| 46 | 45 | xrleidd 13194 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶)) |
| 47 | | simplr 769 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐴 ≤ 𝐵) |
| 48 | | pnfge 13172 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) |
| 49 | 32, 48 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐵 ≤ +∞) |
| 50 | 49 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐵 ≤ +∞) |
| 51 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
| 52 | 50, 51 | breqtrrd 5171 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐵 ≤ 𝐴) |
| 53 | 34 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
| 54 | 47, 52, 53 | mpbir2and 713 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐴 = 𝐵) |
| 55 | 54 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) = (𝐵 +𝑒 𝐶)) |
| 56 | 46, 55 | breqtrd 5169 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 57 | 56 | adantlr 715 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 58 | | oveq1 7438 |
. . . . 5
⊢ (𝐴 = -∞ → (𝐴 +𝑒 𝐶) = (-∞
+𝑒 𝐶)) |
| 59 | | renepnf 11309 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ → 𝐶 ≠ +∞) |
| 60 | | xaddmnf2 13271 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ +∞)
→ (-∞ +𝑒 𝐶) = -∞) |
| 61 | 17, 59, 60 | syl2anc 584 |
. . . . . 6
⊢ (𝐶 ∈ ℝ → (-∞
+𝑒 𝐶) =
-∞) |
| 62 | 61 | adantl 481 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) → (-∞
+𝑒 𝐶) =
-∞) |
| 63 | 58, 62 | sylan9eqr 2799 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐶) = -∞) |
| 64 | | xaddcl 13281 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 65 | 32, 10, 64 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 66 | 65 | ad2antrr 726 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 67 | | mnfle 13177 |
. . . . 5
⊢ ((𝐵 +𝑒 𝐶) ∈ ℝ*
→ -∞ ≤ (𝐵
+𝑒 𝐶)) |
| 68 | 66, 67 | syl 17 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → -∞ ≤ (𝐵 +𝑒 𝐶)) |
| 69 | 63, 68 | eqbrtrd 5165 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 70 | | elxr 13158 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
| 71 | 9, 70 | sylib 218 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
| 72 | 71 | adantr 480 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
| 73 | 44, 57, 69, 72 | mpjao3dan 1434 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 74 | 38 | adantlr 715 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 75 | 12 | ad2antrr 726 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
| 76 | 75, 14 | syl 17 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ +∞) |
| 77 | | simplr 769 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → 𝐶 = +∞) |
| 78 | 77 | oveq2d 7447 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 𝐶) = (𝐵 +𝑒
+∞)) |
| 79 | 32 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) → 𝐵 ∈
ℝ*) |
| 80 | | xaddpnf1 13268 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (𝐵
+𝑒 +∞) = +∞) |
| 81 | 79, 80 | sylan 580 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 +∞) =
+∞) |
| 82 | 78, 81 | eqtrd 2777 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 𝐶) = +∞) |
| 83 | 76, 82 | breqtrrd 5171 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 84 | 74, 83 | pm2.61dane 3029 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 85 | 56 | adantlr 715 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 86 | | simplr 769 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → 𝐶 = -∞) |
| 87 | 86 | oveq2d 7447 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) = (𝐴 +𝑒
-∞)) |
| 88 | 9 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) → 𝐴 ∈
ℝ*) |
| 89 | | xaddmnf1 13270 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
→ (𝐴
+𝑒 -∞) = -∞) |
| 90 | 88, 89 | sylan 580 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) =
-∞) |
| 91 | 87, 90 | eqtrd 2777 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) = -∞) |
| 92 | 65 | ad2antrr 726 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 93 | 92, 67 | syl 17 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → -∞ ≤ (𝐵 +𝑒 𝐶)) |
| 94 | 91, 93 | eqbrtrd 5165 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 95 | 85, 94 | pm2.61dane 3029 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
| 96 | | elxr 13158 |
. . 3
⊢ (𝐶 ∈ ℝ*
↔ (𝐶 ∈ ℝ
∨ 𝐶 = +∞ ∨
𝐶 =
-∞)) |
| 97 | 10, 96 | sylib 218 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
| 98 | 73, 84, 95, 97 | mpjao3dan 1434 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |