Proof of Theorem xrge0adddir
Step | Hyp | Ref
| Expression |
1 | | iccssxr 13018 |
. . . 4
⊢
(0[,]+∞) ⊆ ℝ* |
2 | | simpl1 1193 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐴 ∈ (0[,]+∞)) |
3 | 1, 2 | sseldi 3899 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐴 ∈
ℝ*) |
4 | | simpl2 1194 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐵 ∈ (0[,]+∞)) |
5 | 1, 4 | sseldi 3899 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐵 ∈
ℝ*) |
6 | | rge0ssre 13044 |
. . . 4
⊢
(0[,)+∞) ⊆ ℝ |
7 | | simpr 488 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐶 ∈ (0[,)+∞)) |
8 | 6, 7 | sseldi 3899 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → 𝐶 ∈ ℝ) |
9 | | xadddir 12886 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ) → ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 ·e
𝐶) +𝑒
(𝐵 ·e
𝐶))) |
10 | 3, 5, 8, 9 | syl3anc 1373 |
. 2
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶
∈ (0[,)+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) |
11 | | simpll1 1214 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 𝐴 ∈
(0[,]+∞)) |
12 | 1, 11 | sseldi 3899 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 𝐴 ∈
ℝ*) |
13 | | simpll2 1215 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 𝐵 ∈
(0[,]+∞)) |
14 | 1, 13 | sseldi 3899 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 𝐵 ∈
ℝ*) |
15 | 12, 14 | xaddcld 12891 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐴
+𝑒 𝐵)
∈ ℝ*) |
16 | | simpr 488 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 0 < 𝐴) |
17 | | xrge0addgt0 31019 |
. . . . . . 7
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞))
∧ 0 < 𝐴) → 0
< (𝐴
+𝑒 𝐵)) |
18 | 11, 13, 16, 17 | syl21anc 838 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 0 < (𝐴
+𝑒 𝐵)) |
19 | | xmulpnf1 12864 |
. . . . . 6
⊢ (((𝐴 +𝑒 𝐵) ∈ ℝ*
∧ 0 < (𝐴
+𝑒 𝐵))
→ ((𝐴
+𝑒 𝐵)
·e +∞) = +∞) |
20 | 15, 18, 19 | syl2anc 587 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ ((𝐴
+𝑒 𝐵)
·e +∞) = +∞) |
21 | | oveq2 7221 |
. . . . . 6
⊢ (𝐶 = +∞ → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 +𝑒 𝐵) ·e
+∞)) |
22 | 21 | ad2antlr 727 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 +𝑒
𝐵) ·e
+∞)) |
23 | | simpll3 1216 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ 𝐶 ∈
(0[,]+∞)) |
24 | | ge0xmulcl 13051 |
. . . . . . . 8
⊢ ((𝐵 ∈ (0[,]+∞) ∧
𝐶 ∈ (0[,]+∞))
→ (𝐵
·e 𝐶)
∈ (0[,]+∞)) |
25 | 13, 23, 24 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐵
·e 𝐶)
∈ (0[,]+∞)) |
26 | 1, 25 | sseldi 3899 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐵
·e 𝐶)
∈ ℝ*) |
27 | | xrge0neqmnf 13040 |
. . . . . . 7
⊢ ((𝐵 ·e 𝐶) ∈ (0[,]+∞) →
(𝐵 ·e
𝐶) ≠
-∞) |
28 | 25, 27 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐵
·e 𝐶)
≠ -∞) |
29 | | xaddpnf2 12817 |
. . . . . 6
⊢ (((𝐵 ·e 𝐶) ∈ ℝ*
∧ (𝐵
·e 𝐶)
≠ -∞) → (+∞ +𝑒 (𝐵 ·e 𝐶)) = +∞) |
30 | 26, 28, 29 | syl2anc 587 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (+∞ +𝑒 (𝐵 ·e 𝐶)) = +∞) |
31 | 20, 22, 30 | 3eqtr4d 2787 |
. . . 4
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ ((𝐴
+𝑒 𝐵)
·e 𝐶) =
(+∞ +𝑒 (𝐵 ·e 𝐶))) |
32 | | oveq2 7221 |
. . . . . . 7
⊢ (𝐶 = +∞ → (𝐴 ·e 𝐶) = (𝐴 ·e
+∞)) |
33 | 32 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐴
·e 𝐶) =
(𝐴 ·e
+∞)) |
34 | | xmulpnf1 12864 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
+∞) = +∞) |
35 | 12, 16, 34 | syl2anc 587 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐴
·e +∞) = +∞) |
36 | 33, 35 | eqtrd 2777 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ (𝐴
·e 𝐶) =
+∞) |
37 | 36 | oveq1d 7228 |
. . . 4
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ ((𝐴
·e 𝐶)
+𝑒 (𝐵
·e 𝐶)) =
(+∞ +𝑒 (𝐵 ·e 𝐶))) |
38 | 31, 37 | eqtr4d 2780 |
. . 3
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 < 𝐴)
→ ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 ·e
𝐶) +𝑒
(𝐵 ·e
𝐶))) |
39 | | simpll3 1216 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ 𝐶 ∈
(0[,]+∞)) |
40 | 1, 39 | sseldi 3899 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ 𝐶 ∈
ℝ*) |
41 | | xmul02 12858 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ*
→ (0 ·e 𝐶) = 0) |
42 | 40, 41 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ (0 ·e 𝐶) = 0) |
43 | 42 | oveq1d 7228 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((0 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶)) = (0 +𝑒 (𝐵 ·e 𝐶))) |
44 | | oveq1 7220 |
. . . . . . 7
⊢ (0 =
𝐴 → (0
·e 𝐶) =
(𝐴 ·e
𝐶)) |
45 | 44 | adantl 485 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ (0 ·e 𝐶) = (𝐴 ·e 𝐶)) |
46 | 45 | oveq1d 7228 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((0 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶)) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) |
47 | | simpll2 1215 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ 𝐵 ∈
(0[,]+∞)) |
48 | 1, 47 | sseldi 3899 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ 𝐵 ∈
ℝ*) |
49 | 48, 40 | xmulcld 12892 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ (𝐵
·e 𝐶)
∈ ℝ*) |
50 | | xaddid2 12832 |
. . . . . 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 | | xaddid2 12832 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ (0 +𝑒 𝐵) = 𝐵) |
54 | 48, 53 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ (0 +𝑒 𝐵) = 𝐵) |
55 | 54 | oveq1d 7228 |
. . . 4
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((0 +𝑒 𝐵) ·e 𝐶) = (𝐵 ·e 𝐶)) |
56 | | oveq1 7220 |
. . . . . 6
⊢ (0 =
𝐴 → (0
+𝑒 𝐵) =
(𝐴 +𝑒
𝐵)) |
57 | 56 | oveq1d 7228 |
. . . . 5
⊢ (0 =
𝐴 → ((0
+𝑒 𝐵)
·e 𝐶) =
((𝐴 +𝑒
𝐵) ·e
𝐶)) |
58 | 57 | adantl 485 |
. . . 4
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((0 +𝑒 𝐵) ·e 𝐶) = ((𝐴 +𝑒 𝐵) ·e 𝐶)) |
59 | 52, 55, 58 | 3eqtr2rd 2784 |
. . 3
⊢ ((((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) ∧ 0 = 𝐴)
→ ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 ·e
𝐶) +𝑒
(𝐵 ·e
𝐶))) |
60 | | 0xr 10880 |
. . . . 5
⊢ 0 ∈
ℝ* |
61 | 60 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → 0 ∈ ℝ*) |
62 | | simpl1 1193 |
. . . . 5
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → 𝐴 ∈
(0[,]+∞)) |
63 | 1, 62 | sseldi 3899 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → 𝐴 ∈
ℝ*) |
64 | | pnfxr 10887 |
. . . . . 6
⊢ +∞
∈ ℝ* |
65 | 64 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → +∞ ∈ ℝ*) |
66 | | iccgelb 12991 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐴 ∈ (0[,]+∞))
→ 0 ≤ 𝐴) |
67 | 61, 65, 62, 66 | syl3anc 1373 |
. . . 4
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → 0 ≤ 𝐴) |
68 | | xrleloe 12734 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (0 ≤
𝐴 ↔ (0 < 𝐴 ∨ 0 = 𝐴))) |
69 | 68 | biimpa 480 |
. . . 4
⊢ (((0
∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ 0 ≤
𝐴) → (0 < 𝐴 ∨ 0 = 𝐴)) |
70 | 61, 63, 67, 69 | syl21anc 838 |
. . 3
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → (0 < 𝐴
∨ 0 = 𝐴)) |
71 | 38, 59, 70 | mpjaodan 959 |
. 2
⊢ (((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ∧ 𝐶 =
+∞) → ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 ·e
𝐶) +𝑒
(𝐵 ·e
𝐶))) |
72 | | 0lepnf 12724 |
. . . . 5
⊢ 0 ≤
+∞ |
73 | | eliccelico 30818 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
≤ +∞) → (𝐶
∈ (0[,]+∞) ↔ (𝐶 ∈ (0[,)+∞) ∨ 𝐶 = +∞))) |
74 | 60, 64, 72, 73 | mp3an 1463 |
. . . 4
⊢ (𝐶 ∈ (0[,]+∞) ↔
(𝐶 ∈ (0[,)+∞)
∨ 𝐶 =
+∞)) |
75 | 74 | 3anbi3i 1161 |
. . 3
⊢ ((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) ↔ (𝐴
∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ (𝐶 ∈ (0[,)+∞) ∨
𝐶 =
+∞))) |
76 | 75 | simp3bi 1149 |
. 2
⊢ ((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) → (𝐶
∈ (0[,)+∞) ∨ 𝐶 = +∞)) |
77 | 10, 71, 76 | mpjaodan 959 |
1
⊢ ((𝐴 ∈ (0[,]+∞) ∧
𝐵 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) → ((𝐴
+𝑒 𝐵)
·e 𝐶) =
((𝐴 ·e
𝐶) +𝑒
(𝐵 ·e
𝐶))) |