Proof of Theorem xleadd1a
Step | Hyp | Ref
| Expression |
1 | | simplrr 797 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ) |
2 | | simpr 476 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ) |
3 | | simplrl 796 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐶 ∈ ℝ) |
4 | | simpllr 795 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ 𝐵) |
5 | 1, 2, 3, 4 | leadd1dd 10520 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)) |
6 | | rexadd 11937 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐶) = (𝐴 + 𝐶)) |
7 | 1, 3, 6 | syl2anc 691 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) = (𝐴 + 𝐶)) |
8 | | rexadd 11937 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
9 | 2, 3, 8 | syl2anc 691 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
10 | 5, 7, 9 | 3brtr4d 4615 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
11 | | simpl1 1057 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈
ℝ*) |
12 | | simpl3 1059 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐶 ∈
ℝ*) |
13 | | xaddcl 11944 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
14 | 11, 12, 13 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
15 | 14 | ad2antrr 758 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
16 | | pnfge 11840 |
. . . . . . 7
⊢ ((𝐴 +𝑒 𝐶) ∈ ℝ*
→ (𝐴
+𝑒 𝐶)
≤ +∞) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ≤ +∞) |
18 | | oveq1 6556 |
. . . . . . 7
⊢ (𝐵 = +∞ → (𝐵 +𝑒 𝐶) = (+∞
+𝑒 𝐶)) |
19 | | rexr 9964 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℝ*) |
20 | | renemnf 9967 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ → 𝐶 ≠ -∞) |
21 | | xaddpnf2 11932 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ -∞)
→ (+∞ +𝑒 𝐶) = +∞) |
22 | 19, 20, 21 | syl2anc 691 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ → (+∞
+𝑒 𝐶) =
+∞) |
23 | 22 | ad2antrl 760 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (+∞
+𝑒 𝐶) =
+∞) |
24 | 18, 23 | sylan9eqr 2666 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = +∞) |
25 | 17, 24 | breqtrrd 4611 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
26 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
27 | | xrleid 11859 |
. . . . . . . 8
⊢ ((𝐴 +𝑒 𝐶) ∈ ℝ*
→ (𝐴
+𝑒 𝐶)
≤ (𝐴
+𝑒 𝐶)) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶)) |
29 | | simplr 788 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐴 ≤ 𝐵) |
30 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐵 = -∞) |
31 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐴 ∈
ℝ*) |
32 | | mnfle 11845 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ*
→ -∞ ≤ 𝐴) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → -∞ ≤ 𝐴) |
34 | 30, 33 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐵 ≤ 𝐴) |
35 | | simpl2 1058 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈
ℝ*) |
36 | | xrletri3 11861 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
37 | 11, 35, 36 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
38 | 37 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
39 | 29, 34, 38 | mpbir2and 959 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → 𝐴 = 𝐵) |
40 | 39 | oveq1d 6564 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) = (𝐵 +𝑒 𝐶)) |
41 | 28, 40 | breqtrd 4609 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
42 | 41 | adantlr 747 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
43 | | elxr 11826 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
44 | 35, 43 | sylib 207 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
45 | 44 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
46 | 10, 25, 42, 45 | mpjao3dan 1387 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ)) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
47 | 46 | anassrs 678 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
48 | 14 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
49 | 48, 27 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐴 +𝑒 𝐶)) |
50 | | simplr 788 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐴 ≤ 𝐵) |
51 | | pnfge 11840 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) |
52 | 35, 51 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → 𝐵 ≤ +∞) |
53 | 52 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐵 ≤ +∞) |
54 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
55 | 53, 54 | breqtrrd 4611 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐵 ≤ 𝐴) |
56 | 37 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
57 | 50, 55, 56 | mpbir2and 959 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → 𝐴 = 𝐵) |
58 | 57 | oveq1d 6564 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) = (𝐵 +𝑒 𝐶)) |
59 | 49, 58 | breqtrd 4609 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
60 | 59 | adantlr 747 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
61 | | oveq1 6556 |
. . . . 5
⊢ (𝐴 = -∞ → (𝐴 +𝑒 𝐶) = (-∞
+𝑒 𝐶)) |
62 | | renepnf 9966 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ → 𝐶 ≠ +∞) |
63 | | xaddmnf2 11934 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ +∞)
→ (-∞ +𝑒 𝐶) = -∞) |
64 | 19, 62, 63 | syl2anc 691 |
. . . . . 6
⊢ (𝐶 ∈ ℝ → (-∞
+𝑒 𝐶) =
-∞) |
65 | 64 | adantl 481 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) → (-∞
+𝑒 𝐶) =
-∞) |
66 | 61, 65 | sylan9eqr 2666 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐶) = -∞) |
67 | | xaddcl 11944 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
68 | 35, 12, 67 | syl2anc 691 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
69 | 68 | ad2antrr 758 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
70 | | mnfle 11845 |
. . . . 5
⊢ ((𝐵 +𝑒 𝐶) ∈ ℝ*
→ -∞ ≤ (𝐵
+𝑒 𝐶)) |
71 | 69, 70 | syl 17 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → -∞ ≤ (𝐵 +𝑒 𝐶)) |
72 | 66, 71 | eqbrtrd 4605 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
73 | | elxr 11826 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
74 | 11, 73 | sylib 207 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
75 | 74 | adantr 480 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
76 | 47, 60, 72, 75 | mpjao3dan 1387 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
77 | 41 | adantlr 747 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
78 | 14 | ad2antrr 758 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ∈
ℝ*) |
79 | 78, 16 | syl 17 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ +∞) |
80 | | simplr 788 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → 𝐶 = +∞) |
81 | 80 | oveq2d 6565 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 𝐶) = (𝐵 +𝑒
+∞)) |
82 | 35 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) → 𝐵 ∈
ℝ*) |
83 | | xaddpnf1 11931 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (𝐵
+𝑒 +∞) = +∞) |
84 | 82, 83 | sylan 487 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 +∞) =
+∞) |
85 | 81, 84 | eqtrd 2644 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐵 +𝑒 𝐶) = +∞) |
86 | 79, 85 | breqtrrd 4611 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) ∧ 𝐵 ≠ -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
87 | 77, 86 | pm2.61dane 2869 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
88 | 59 | adantlr 747 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
89 | | simplr 788 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → 𝐶 = -∞) |
90 | 89 | oveq2d 6565 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) = (𝐴 +𝑒
-∞)) |
91 | 11 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) → 𝐴 ∈
ℝ*) |
92 | | xaddmnf1 11933 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
→ (𝐴
+𝑒 -∞) = -∞) |
93 | 91, 92 | sylan 487 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) =
-∞) |
94 | 90, 93 | eqtrd 2644 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) = -∞) |
95 | 68 | ad2antrr 758 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
96 | 95, 70 | syl 17 |
. . . 4
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → -∞ ≤ (𝐵 +𝑒 𝐶)) |
97 | 94, 96 | eqbrtrd 4605 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
98 | 88, 97 | pm2.61dane 2869 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 = -∞) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |
99 | | elxr 11826 |
. . 3
⊢ (𝐶 ∈ ℝ*
↔ (𝐶 ∈ ℝ
∨ 𝐶 = +∞ ∨
𝐶 =
-∞)) |
100 | 12, 99 | sylib 207 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
101 | 76, 87, 98, 100 | mpjao3dan 1387 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)) |