Proof of Theorem xrge0npcan
| Step | Hyp | Ref
| Expression |
| 1 | | iccssxr 13470 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
| 2 | | simpl1 1192 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → 𝐴 ∈ (0[,]+∞)) |
| 3 | 1, 2 | sselid 3981 |
. . . . . . . 8
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → 𝐴 ∈
ℝ*) |
| 4 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → 𝐵 = +∞) |
| 5 | | simpl3 1194 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → 𝐵 ≤ 𝐴) |
| 6 | 4, 5 | eqbrtrrd 5167 |
. . . . . . . 8
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → +∞ ≤ 𝐴) |
| 7 | | xgepnf 13207 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ*
→ (+∞ ≤ 𝐴
↔ 𝐴 =
+∞)) |
| 8 | 7 | biimpa 476 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ +∞ ≤ 𝐴)
→ 𝐴 =
+∞) |
| 9 | 3, 6, 8 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → 𝐴 = +∞) |
| 10 | | xnegeq 13249 |
. . . . . . . 8
⊢ (𝐵 = +∞ →
-𝑒𝐵 =
-𝑒+∞) |
| 11 | 4, 10 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) →
-𝑒𝐵 =
-𝑒+∞) |
| 12 | 9, 11 | oveq12d 7449 |
. . . . . 6
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → (𝐴 +𝑒
-𝑒𝐵) =
(+∞ +𝑒
-𝑒+∞)) |
| 13 | | pnfxr 11315 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
| 14 | | xnegid 13280 |
. . . . . . 7
⊢ (+∞
∈ ℝ* → (+∞ +𝑒
-𝑒+∞) = 0) |
| 15 | 13, 14 | ax-mp 5 |
. . . . . 6
⊢ (+∞
+𝑒 -𝑒+∞) = 0 |
| 16 | 12, 15 | eqtrdi 2793 |
. . . . 5
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → (𝐴 +𝑒
-𝑒𝐵) =
0) |
| 17 | 16 | oveq1d 7446 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → ((𝐴 +𝑒
-𝑒𝐵)
+𝑒 𝐵) =
(0 +𝑒 𝐵)) |
| 18 | 4 | oveq2d 7447 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → (0 +𝑒
𝐵) = (0
+𝑒 +∞)) |
| 19 | | xaddlid 13284 |
. . . . 5
⊢ (+∞
∈ ℝ* → (0 +𝑒 +∞) =
+∞) |
| 20 | 13, 19 | mp1i 13 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → (0 +𝑒
+∞) = +∞) |
| 21 | 17, 18, 20 | 3eqtrd 2781 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → ((𝐴 +𝑒
-𝑒𝐵)
+𝑒 𝐵) =
+∞) |
| 22 | 21, 9 | eqtr4d 2780 |
. 2
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ 𝐵 = +∞) → ((𝐴 +𝑒
-𝑒𝐵)
+𝑒 𝐵) =
𝐴) |
| 23 | | simpl1 1192 |
. . . . 5
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) → 𝐴 ∈ (0[,]+∞)) |
| 24 | 1, 23 | sselid 3981 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) → 𝐴 ∈
ℝ*) |
| 25 | | xrge0neqmnf 13492 |
. . . . 5
⊢ (𝐴 ∈ (0[,]+∞) →
𝐴 ≠
-∞) |
| 26 | 23, 25 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) → 𝐴 ≠ -∞) |
| 27 | | simpl2 1193 |
. . . . . 6
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) → 𝐵 ∈ (0[,]+∞)) |
| 28 | 1, 27 | sselid 3981 |
. . . . 5
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) → 𝐵 ∈
ℝ*) |
| 29 | 28 | xnegcld 13342 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) →
-𝑒𝐵
∈ ℝ*) |
| 30 | | simpr 484 |
. . . . 5
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) → ¬ 𝐵 = +∞) |
| 31 | | xnegneg 13256 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ*
→ -𝑒-𝑒𝐵 = 𝐵) |
| 32 | | xnegeq 13249 |
. . . . . . . . 9
⊢
(-𝑒𝐵 = -∞ →
-𝑒-𝑒𝐵 =
-𝑒-∞) |
| 33 | 31, 32 | sylan9req 2798 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ -𝑒𝐵 = -∞) → 𝐵 =
-𝑒-∞) |
| 34 | | xnegmnf 13252 |
. . . . . . . 8
⊢
-𝑒-∞ = +∞ |
| 35 | 33, 34 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ -𝑒𝐵 = -∞) → 𝐵 = +∞) |
| 36 | 35 | stoic1a 1772 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ ¬ 𝐵 = +∞)
→ ¬ -𝑒𝐵 = -∞) |
| 37 | 36 | neqned 2947 |
. . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ ¬ 𝐵 = +∞)
→ -𝑒𝐵 ≠ -∞) |
| 38 | 28, 30, 37 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) →
-𝑒𝐵 ≠
-∞) |
| 39 | | xrge0neqmnf 13492 |
. . . . 5
⊢ (𝐵 ∈ (0[,]+∞) →
𝐵 ≠
-∞) |
| 40 | 27, 39 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) → 𝐵 ≠ -∞) |
| 41 | | xaddass 13291 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (-𝑒𝐵 ∈ ℝ* ∧
-𝑒𝐵 ≠
-∞) ∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞)) → ((𝐴
+𝑒 -𝑒𝐵) +𝑒 𝐵) = (𝐴 +𝑒
(-𝑒𝐵
+𝑒 𝐵))) |
| 42 | 24, 26, 29, 38, 28, 40, 41 | syl222anc 1388 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) → ((𝐴 +𝑒
-𝑒𝐵)
+𝑒 𝐵) =
(𝐴 +𝑒
(-𝑒𝐵
+𝑒 𝐵))) |
| 43 | | xnegcl 13255 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ -𝑒𝐵 ∈
ℝ*) |
| 44 | | xaddcom 13282 |
. . . . . . . 8
⊢
((-𝑒𝐵 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (-𝑒𝐵 +𝑒 𝐵) = (𝐵 +𝑒
-𝑒𝐵)) |
| 45 | 43, 44 | mpancom 688 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
→ (-𝑒𝐵 +𝑒 𝐵) = (𝐵 +𝑒
-𝑒𝐵)) |
| 46 | | xnegid 13280 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
→ (𝐵
+𝑒 -𝑒𝐵) = 0) |
| 47 | 45, 46 | eqtrd 2777 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ (-𝑒𝐵 +𝑒 𝐵) = 0) |
| 48 | 47 | oveq2d 7447 |
. . . . 5
⊢ (𝐵 ∈ ℝ*
→ (𝐴
+𝑒 (-𝑒𝐵 +𝑒 𝐵)) = (𝐴 +𝑒 0)) |
| 49 | | xaddrid 13283 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ (𝐴
+𝑒 0) = 𝐴) |
| 50 | 48, 49 | sylan9eqr 2799 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 +𝑒
(-𝑒𝐵
+𝑒 𝐵)) =
𝐴) |
| 51 | 24, 28, 50 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) → (𝐴 +𝑒
(-𝑒𝐵
+𝑒 𝐵)) =
𝐴) |
| 52 | 42, 51 | eqtrd 2777 |
. 2
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) ∧ ¬ 𝐵 = +∞) → ((𝐴 +𝑒
-𝑒𝐵)
+𝑒 𝐵) =
𝐴) |
| 53 | 22, 52 | pm2.61dan 813 |
1
⊢ ((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒
-𝑒𝐵)
+𝑒 𝐵) =
𝐴) |