Proof of Theorem xleadd1a
Step | Hyp | Ref
| Expression |
1 | | simplrr 531 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ) |
2 | | simpr 109 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ) |
3 | | simplrl 530 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐶 ∈ ℝ) |
4 | | simpllr 529 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ 𝐵) |
5 | 1, 2, 3, 4 | leadd1dd 8465 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)) |
6 | 1, 3 | rexaddd 9798 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) = (𝐴 + 𝐶)) |
7 | 2, 3 | rexaddd 9798 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
8 | 5, 6, 7 | 3brtr4d 4019 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
9 | | simpl1 995 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈
ℝ*) |
10 | | simpl3 997 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐶 ∈
ℝ*) |
11 | | xaddcl 9804 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
12 | 9, 10, 11 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
13 | 12 | ad2antrr 485 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
14 | | pnfge 9733 |
. . . . . . 7
⊢ ((𝐴 +𝑒 𝐶) ∈ ℝ*
→ (𝐴
+𝑒 𝐶)
≤ +∞) |
15 | 13, 14 | syl 14 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ≤ +∞) |
16 | | oveq1 5857 |
. . . . . . 7
⊢ (𝐵 = +∞ → (𝐵 +𝑒 𝐶) = (+∞
+𝑒 𝐶)) |
17 | | rexr 7952 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℝ*) |
18 | | renemnf 7955 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ → 𝐶 ≠ -∞) |
19 | | xaddpnf2 9791 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ -∞)
→ (+∞ +𝑒 𝐶) = +∞) |
20 | 17, 18, 19 | syl2anc 409 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ → (+∞
+𝑒 𝐶) =
+∞) |
21 | 20 | ad2antrl 487 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (+∞
+𝑒 𝐶) =
+∞) |
22 | 16, 21 | sylan9eqr 2225 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = +∞) |
23 | 15, 22 | breqtrrd 4015 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
24 | 12 | adantr 274 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
25 | 24 | xrleidd 9745 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶)) |
26 | | simplr 525 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐴 ≤ 𝐵) |
27 | | simpr 109 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐵 = -∞) |
28 | 9 | adantr 274 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐴 ∈
ℝ*) |
29 | | mnfle 9736 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ*
→ -∞ ≤ 𝐴) |
30 | 28, 29 | syl 14 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → -∞ ≤ 𝐴) |
31 | 27, 30 | eqbrtrd 4009 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐵 ≤ 𝐴) |
32 | | simpl2 996 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈
ℝ*) |
33 | | xrletri3 9748 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
34 | 9, 32, 33 | syl2anc 409 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
35 | 34 | adantr 274 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
36 | 26, 31, 35 | mpbir2and 939 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐴 = 𝐵) |
37 | 36 | oveq1d 5865 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) = (𝐵 +𝑒 𝐶)) |
38 | 25, 37 | breqtrd 4013 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
39 | 38 | adantlr 474 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
40 | | elxr 9720 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
41 | 32, 40 | sylib 121 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
42 | 41 | adantr 274 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
43 | 8, 23, 39, 42 | mpjao3dan 1302 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
44 | 43 | anassrs 398 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
45 | 12 | adantr 274 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
46 | 45 | xrleidd 9745 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶)) |
47 | | simplr 525 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐴 ≤ 𝐵) |
48 | | pnfge 9733 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) |
49 | 32, 48 | syl 14 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐵 ≤ +∞) |
50 | 49 | adantr 274 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐵 ≤ +∞) |
51 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
52 | 50, 51 | breqtrrd 4015 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐵 ≤ 𝐴) |
53 | 34 | adantr 274 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
54 | 47, 52, 53 | mpbir2and 939 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐴 = 𝐵) |
55 | 54 | oveq1d 5865 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) = (𝐵 +𝑒 𝐶)) |
56 | 46, 55 | breqtrd 4013 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
57 | 56 | adantlr 474 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
58 | | oveq1 5857 |
. . . . 5
⊢ (𝐴 = -∞ → (𝐴 +𝑒 𝐶) = (-∞
+𝑒 𝐶)) |
59 | | renepnf 7954 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ → 𝐶 ≠ +∞) |
60 | | xaddmnf2 9793 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ +∞)
→ (-∞ +𝑒 𝐶) = -∞) |
61 | 17, 59, 60 | syl2anc 409 |
. . . . . 6
⊢ (𝐶 ∈ ℝ → (-∞
+𝑒 𝐶) =
-∞) |
62 | 61 | adantl 275 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) → (-∞
+𝑒 𝐶) =
-∞) |
63 | 58, 62 | sylan9eqr 2225 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐶) = -∞) |
64 | | xaddcl 9804 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
65 | 32, 10, 64 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
66 | 65 | ad2antrr 485 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
67 | | mnfle 9736 |
. . . . 5
⊢ ((𝐵 +𝑒 𝐶) ∈ ℝ*
→ -∞ ≤ (𝐵
+𝑒 𝐶)) |
68 | 66, 67 | syl 14 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → -∞ ≤ (𝐵 +𝑒 𝐶)) |
69 | 63, 68 | eqbrtrd 4009 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
70 | | elxr 9720 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
71 | 9, 70 | sylib 121 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
72 | 71 | adantr 274 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
73 | 44, 57, 69, 72 | mpjao3dan 1302 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
74 | 38 | adantlr 474 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
75 | 12 | ad2antrr 485 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
76 | 75, 14 | syl 14 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ +∞) |
77 | | simplr 525 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → 𝐶 = +∞) |
78 | 77 | oveq2d 5866 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 𝐶) = (𝐵 +𝑒
+∞)) |
79 | 32 | adantr 274 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) → 𝐵 ∈
ℝ*) |
80 | | xaddpnf1 9790 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (𝐵
+𝑒 +∞) = +∞) |
81 | 79, 80 | sylan 281 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 +∞) =
+∞) |
82 | 78, 81 | eqtrd 2203 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 𝐶) = +∞) |
83 | 76, 82 | breqtrrd 4015 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
84 | | xrmnfdc 9787 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ DECID 𝐵 = -∞) |
85 | | exmiddc 831 |
. . . . . 6
⊢
(DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞)) |
86 | 84, 85 | syl 14 |
. . . . 5
⊢ (𝐵 ∈ ℝ*
→ (𝐵 = -∞ ∨
¬ 𝐵 =
-∞)) |
87 | | df-ne 2341 |
. . . . . 6
⊢ (𝐵 ≠ -∞ ↔ ¬
𝐵 =
-∞) |
88 | 87 | orbi2i 757 |
. . . . 5
⊢ ((𝐵 = -∞ ∨ 𝐵 ≠ -∞) ↔ (𝐵 = -∞ ∨ ¬ 𝐵 = -∞)) |
89 | 86, 88 | sylibr 133 |
. . . 4
⊢ (𝐵 ∈ ℝ*
→ (𝐵 = -∞ ∨
𝐵 ≠
-∞)) |
90 | 79, 89 | syl 14 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) → (𝐵 = -∞ ∨ 𝐵 ≠ -∞)) |
91 | 74, 83, 90 | mpjaodan 793 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
92 | 56 | adantlr 474 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
93 | | simplr 525 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → 𝐶 = -∞) |
94 | 93 | oveq2d 5866 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) = (𝐴 +𝑒
-∞)) |
95 | 9 | adantr 274 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) → 𝐴 ∈
ℝ*) |
96 | | xaddmnf1 9792 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
→ (𝐴
+𝑒 -∞) = -∞) |
97 | 95, 96 | sylan 281 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) =
-∞) |
98 | 94, 97 | eqtrd 2203 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) = -∞) |
99 | 65 | ad2antrr 485 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
100 | 99, 67 | syl 14 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → -∞ ≤ (𝐵 +𝑒 𝐶)) |
101 | 98, 100 | eqbrtrd 4009 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
102 | | xrpnfdc 9786 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ DECID 𝐴 = +∞) |
103 | | exmiddc 831 |
. . . . . 6
⊢
(DECID 𝐴 = +∞ → (𝐴 = +∞ ∨ ¬ 𝐴 = +∞)) |
104 | 102, 103 | syl 14 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ (𝐴 = +∞ ∨
¬ 𝐴 =
+∞)) |
105 | | df-ne 2341 |
. . . . . 6
⊢ (𝐴 ≠ +∞ ↔ ¬
𝐴 =
+∞) |
106 | 105 | orbi2i 757 |
. . . . 5
⊢ ((𝐴 = +∞ ∨ 𝐴 ≠ +∞) ↔ (𝐴 = +∞ ∨ ¬ 𝐴 = +∞)) |
107 | 104, 106 | sylibr 133 |
. . . 4
⊢ (𝐴 ∈ ℝ*
→ (𝐴 = +∞ ∨
𝐴 ≠
+∞)) |
108 | 95, 107 | syl 14 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) → (𝐴 = +∞ ∨ 𝐴 ≠ +∞)) |
109 | 92, 101, 108 | mpjaodan 793 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
110 | | elxr 9720 |
. . 3
⊢ (𝐶 ∈ ℝ*
↔ (𝐶 ∈ ℝ
∨ 𝐶 = +∞ ∨
𝐶 =
-∞)) |
111 | 10, 110 | sylib 121 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
112 | 73, 91, 109, 111 | mpjao3dan 1302 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |