Proof of Theorem xrge0adddir
| Step | Hyp | Ref
| Expression |
| 1 | | iccssxr 13470 |
. . . 4
⊢
(0[,]+∞) ⊆ ℝ* |
| 2 | | simpl1 1192 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐴 ∈ (0[,]+∞)) |
| 3 | 1, 2 | sselid 3981 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐴 ∈
ℝ*) |
| 4 | | simpl2 1193 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐵 ∈ (0[,]+∞)) |
| 5 | 1, 4 | sselid 3981 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐵 ∈
ℝ*) |
| 6 | | rge0ssre 13496 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ |
| 7 | | simpr 484 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐶 ∈ (0[,)+∞)) |
| 8 | 6, 7 | sselid 3981 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐶 ∈ ℝ) |
| 9 | | xadddir 13338 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ) → ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 ·e
𝐶) +𝑒
(𝐵 ·e
𝐶))) |
| 10 | 3, 5, 8, 9 | syl3anc 1373 |
. 2
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) |
| 11 | | simpll1 1213 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 𝐴 ∈
(0[,]+∞)) |
| 12 | 1, 11 | sselid 3981 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 𝐴 ∈
ℝ*) |
| 13 | | simpll2 1214 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 𝐵 ∈
(0[,]+∞)) |
| 14 | 1, 13 | sselid 3981 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 𝐵 ∈
ℝ*) |
| 15 | 12, 14 | xaddcld 13343 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐴
+𝑒 𝐵)
∈ ℝ*) |
| 16 | | simpr 484 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 0 < 𝐴) |
| 17 | | xrge0addgt0 33022 |
. . . . . . 7
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞))
∧ 0 < 𝐴) → 0
< (𝐴
+𝑒 𝐵)) |
| 18 | 11, 13, 16, 17 | syl21anc 838 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 0 < (𝐴
+𝑒 𝐵)) |
| 19 | | xmulpnf1 13316 |
. . . . . 6
⊢ (((𝐴 +𝑒 𝐵) ∈ ℝ*
∧ 0 < (𝐴
+𝑒 𝐵))
→ ((𝐴
+𝑒 𝐵)
·e +∞) = +∞) |
| 20 | 15, 18, 19 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ ((𝐴
+𝑒 𝐵)
·e +∞) = +∞) |
| 21 | | oveq2 7439 |
. . . . . 6
⊢ (𝐶 = +∞ → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 +𝑒 𝐵) ·e
+∞)) |
| 22 | 21 | ad2antlr 727 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 +𝑒
𝐵) ·e
+∞)) |
| 23 | | simpll3 1215 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 𝐶 ∈
(0[,]+∞)) |
| 24 | | ge0xmulcl 13503 |
. . . . . . . 8
⊢ ((𝐵 ∈ (0[,]+∞) ∧
𝐶 ∈ (0[,]+∞))
→ (𝐵
·e 𝐶)
∈ (0[,]+∞)) |
| 25 | 13, 23, 24 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐵
·e 𝐶)
∈ (0[,]+∞)) |
| 26 | 1, 25 | sselid 3981 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐵
·e 𝐶)
∈ ℝ*) |
| 27 | | xrge0neqmnf 13492 |
. . . . . . 7
⊢ ((𝐵 ·e 𝐶) ∈ (0[,]+∞) →
(𝐵 ·e
𝐶) ≠
-∞) |
| 28 | 25, 27 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐵
·e 𝐶)
≠ -∞) |
| 29 | | xaddpnf2 13269 |
. . . . . 6
⊢ (((𝐵 ·e 𝐶) ∈ ℝ*
∧ (𝐵
·e 𝐶)
≠ -∞) → (+∞ +𝑒 (𝐵 ·e 𝐶)) = +∞) |
| 30 | 26, 28, 29 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (+∞ +𝑒 (𝐵 ·e 𝐶)) = +∞) |
| 31 | 20, 22, 30 | 3eqtr4d 2787 |
. . . 4
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ ((𝐴
+𝑒 𝐵)
·e 𝐶) =
(+∞ +𝑒 (𝐵 ·e 𝐶))) |
| 32 | | oveq2 7439 |
. . . . . . 7
⊢ (𝐶 = +∞ → (𝐴 ·e 𝐶) = (𝐴 ·e
+∞)) |
| 33 | 32 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐴
·e 𝐶) =
(𝐴 ·e
+∞)) |
| 34 | | xmulpnf1 13316 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
+∞) = +∞) |
| 35 | 12, 16, 34 | syl2anc 584 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐴
·e +∞) = +∞) |
| 36 | 33, 35 | eqtrd 2777 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐴
·e 𝐶) =
+∞) |
| 37 | 36 | oveq1d 7446 |
. . . 4
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ ((𝐴
·e 𝐶)
+𝑒 (𝐵
·e 𝐶)) =
(+∞ +𝑒 (𝐵 ·e 𝐶))) |
| 38 | 31, 37 | eqtr4d 2780 |
. . 3
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 ·e
𝐶) +𝑒
(𝐵 ·e
𝐶))) |
| 39 | | simpll3 1215 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ 𝐶 ∈
(0[,]+∞)) |
| 40 | 1, 39 | sselid 3981 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ 𝐶 ∈
ℝ*) |
| 41 | | xmul02 13310 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ*
→ (0 ·e 𝐶) = 0) |
| 42 | 40, 41 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ (0 ·e 𝐶) = 0) |
| 43 | 42 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((0 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶)) = (0 +𝑒 (𝐵 ·e 𝐶))) |
| 44 | | oveq1 7438 |
. . . . . . 7
⊢ (0 =
𝐴 → (0
·e 𝐶) =
(𝐴 ·e
𝐶)) |
| 45 | 44 | adantl 481 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ (0 ·e 𝐶) = (𝐴 ·e 𝐶)) |
| 46 | 45 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((0 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶)) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) |
| 47 | | simpll2 1214 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ 𝐵 ∈
(0[,]+∞)) |
| 48 | 1, 47 | sselid 3981 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ 𝐵 ∈
ℝ*) |
| 49 | 48, 40 | xmulcld 13344 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ (𝐵
·e 𝐶)
∈ ℝ*) |
| 50 | | xaddlid 13284 |
. . . . . 6
⊢ ((𝐵 ·e 𝐶) ∈ ℝ*
→ (0 +𝑒 (𝐵 ·e 𝐶)) = (𝐵 ·e 𝐶)) |
| 51 | 49, 50 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ (0 +𝑒 (𝐵 ·e 𝐶)) = (𝐵 ·e 𝐶)) |
| 52 | 43, 46, 51 | 3eqtr3d 2785 |
. . . 4
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((𝐴
·e 𝐶)
+𝑒 (𝐵
·e 𝐶)) =
(𝐵 ·e
𝐶)) |
| 53 | | xaddlid 13284 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ (0 +𝑒 𝐵) = 𝐵) |
| 54 | 48, 53 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ (0 +𝑒 𝐵) = 𝐵) |
| 55 | 54 | oveq1d 7446 |
. . . 4
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((0 +𝑒 𝐵) ·e 𝐶) = (𝐵 ·e 𝐶)) |
| 56 | | oveq1 7438 |
. . . . . 6
⊢ (0 =
𝐴 → (0
+𝑒 𝐵) =
(𝐴 +𝑒
𝐵)) |
| 57 | 56 | oveq1d 7446 |
. . . . 5
⊢ (0 =
𝐴 → ((0
+𝑒 𝐵)
·e 𝐶) =
((𝐴 +𝑒
𝐵) ·e
𝐶)) |
| 58 | 57 | adantl 481 |
. . . 4
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((0 +𝑒 𝐵) ·e 𝐶) = ((𝐴 +𝑒 𝐵) ·e 𝐶)) |
| 59 | 52, 55, 58 | 3eqtr2rd 2784 |
. . 3
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 ·e
𝐶) +𝑒
(𝐵 ·e
𝐶))) |
| 60 | | 0xr 11308 |
. . . . 5
⊢ 0 ∈
ℝ* |
| 61 | 60 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → 0 ∈ ℝ*) |
| 62 | | simpl1 1192 |
. . . . 5
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → 𝐴 ∈
(0[,]+∞)) |
| 63 | 1, 62 | sselid 3981 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → 𝐴 ∈
ℝ*) |
| 64 | | pnfxr 11315 |
. . . . . 6
⊢ +∞
∈ ℝ* |
| 65 | 64 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → +∞ ∈ ℝ*) |
| 66 | | iccgelb 13443 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐴 ∈ (0[,]+∞))
→ 0 ≤ 𝐴) |
| 67 | 61, 65, 62, 66 | syl3anc 1373 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → 0 ≤ 𝐴) |
| 68 | | xrleloe 13186 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (0 ≤
𝐴 ↔ (0 < 𝐴 ∨ 0 = 𝐴))) |
| 69 | 68 | biimpa 476 |
. . . 4
⊢ (((0
∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ 0 ≤
𝐴) → (0 < 𝐴 ∨ 0 = 𝐴)) |
| 70 | 61, 63, 67, 69 | syl21anc 838 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → (0 < 𝐴
∨ 0 = 𝐴)) |
| 71 | 38, 59, 70 | mpjaodan 961 |
. 2
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 ·e
𝐶) +𝑒
(𝐵 ·e
𝐶))) |
| 72 | | 0lepnf 13175 |
. . . . 5
⊢ 0 ≤
+∞ |
| 73 | | eliccelico 32779 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
≤ +∞) → (𝐶
∈ (0[,]+∞) ↔ (𝐶 ∈ (0[,)+∞) ∨ 𝐶 = +∞))) |
| 74 | 60, 64, 72, 73 | mp3an 1463 |
. . . 4
⊢ (𝐶 ∈ (0[,]+∞) ↔
(𝐶 ∈ (0[,)+∞)
∨ 𝐶 =
+∞)) |
| 75 | 74 | 3anbi3i 1160 |
. . 3
⊢ ((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ↔ (𝐴
∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ (𝐶 ∈ (0[,)+∞) ∨
𝐶 =
+∞))) |
| 76 | 75 | simp3bi 1148 |
. 2
⊢ ((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) → (𝐶
∈ (0[,)+∞) ∨ 𝐶 = +∞)) |
| 77 | 10, 71, 76 | mpjaodan 961 |
1
⊢ ((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) → ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 ·e
𝐶) +𝑒
(𝐵 ·e
𝐶))) |