Proof of Theorem xadddilem
Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → 𝐴 ∈ ℝ) |
2 | | recn 10026 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
3 | | recn 10026 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
4 | | recn 10026 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) |
5 | | adddi 10025 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
6 | 2, 3, 4, 5 | syl3an 1368 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
7 | 6 | 3expa 1265 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
8 | | readdcl 10019 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 + 𝐶) ∈ ℝ) |
9 | | rexmul 12101 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 + 𝐶) ∈ ℝ) → (𝐴 ·e (𝐵 + 𝐶)) = (𝐴 · (𝐵 + 𝐶))) |
10 | 8, 9 | sylan2 491 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐴 ·e (𝐵 + 𝐶)) = (𝐴 · (𝐵 + 𝐶))) |
11 | 10 | anassrs 680 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e (𝐵 + 𝐶)) = (𝐴 · (𝐵 + 𝐶))) |
12 | | remulcl 10021 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
13 | 12 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
14 | | remulcl 10021 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℝ) |
15 | 14 | adantlr 751 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℝ) |
16 | | rexadd 12063 |
. . . . . . 7
⊢ (((𝐴 · 𝐵) ∈ ℝ ∧ (𝐴 · 𝐶) ∈ ℝ) → ((𝐴 · 𝐵) +𝑒 (𝐴 · 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
17 | 13, 15, 16 | syl2anc 693 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐵) +𝑒 (𝐴 · 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
18 | 7, 11, 17 | 3eqtr4d 2666 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e (𝐵 + 𝐶)) = ((𝐴 · 𝐵) +𝑒 (𝐴 · 𝐶))) |
19 | | rexadd 12063 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
20 | 19 | adantll 750 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
21 | 20 | oveq2d 6666 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e (𝐵 + 𝐶))) |
22 | | rexmul 12101 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵)) |
23 | 22 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵)) |
24 | | rexmul 12101 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ·e 𝐶) = (𝐴 · 𝐶)) |
25 | 24 | adantlr 751 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e 𝐶) = (𝐴 · 𝐶)) |
26 | 23, 25 | oveq12d 6668 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 · 𝐵) +𝑒 (𝐴 · 𝐶))) |
27 | 18, 21, 26 | 3eqtr4d 2666 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
28 | 1, 27 | sylanl1 682 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
29 | | rexr 10085 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
30 | 29 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → 𝐴 ∈
ℝ*) |
31 | | xmulpnf1 12104 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
+∞) = +∞) |
32 | 30, 31 | sylan 488 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → (𝐴 ·e +∞) =
+∞) |
33 | 32 | adantr 481 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) → (𝐴 ·e +∞) =
+∞) |
34 | 22, 12 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) ∈
ℝ) |
35 | 1, 34 | sylan 488 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) ∈ ℝ) |
36 | | rexr 10085 |
. . . . . . . 8
⊢ ((𝐴 ·e 𝐵) ∈ ℝ → (𝐴 ·e 𝐵) ∈
ℝ*) |
37 | | renemnf 10088 |
. . . . . . . 8
⊢ ((𝐴 ·e 𝐵) ∈ ℝ → (𝐴 ·e 𝐵) ≠
-∞) |
38 | | xaddpnf1 12057 |
. . . . . . . 8
⊢ (((𝐴 ·e 𝐵) ∈ ℝ*
∧ (𝐴
·e 𝐵)
≠ -∞) → ((𝐴
·e 𝐵)
+𝑒 +∞) = +∞) |
39 | 36, 37, 38 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐴 ·e 𝐵) ∈ ℝ → ((𝐴 ·e 𝐵) +𝑒
+∞) = +∞) |
40 | 35, 39 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) → ((𝐴 ·e 𝐵) +𝑒 +∞) =
+∞) |
41 | 33, 40 | eqtr4d 2659 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) → (𝐴 ·e +∞) = ((𝐴 ·e 𝐵) +𝑒
+∞)) |
42 | 41 | adantr 481 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = +∞) → (𝐴 ·e +∞) = ((𝐴 ·e 𝐵) +𝑒
+∞)) |
43 | | oveq2 6658 |
. . . . . 6
⊢ (𝐶 = +∞ → (𝐵 +𝑒 𝐶) = (𝐵 +𝑒
+∞)) |
44 | | rexr 10085 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
45 | | renemnf 10088 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ≠ -∞) |
46 | | xaddpnf1 12057 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (𝐵
+𝑒 +∞) = +∞) |
47 | 44, 45, 46 | syl2anc 693 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → (𝐵 +𝑒 +∞)
= +∞) |
48 | 47 | adantl 482 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 +∞) =
+∞) |
49 | 43, 48 | sylan9eqr 2678 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = +∞) → (𝐵 +𝑒 𝐶) = +∞) |
50 | 49 | oveq2d 6666 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e
+∞)) |
51 | | oveq2 6658 |
. . . . . 6
⊢ (𝐶 = +∞ → (𝐴 ·e 𝐶) = (𝐴 ·e
+∞)) |
52 | 51, 33 | sylan9eqr 2678 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = +∞) → (𝐴 ·e 𝐶) = +∞) |
53 | 52 | oveq2d 6666 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = +∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 ·e 𝐵) +𝑒
+∞)) |
54 | 42, 50, 53 | 3eqtr4d 2666 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
55 | | xmulmnf1 12106 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
-∞) = -∞) |
56 | 30, 55 | sylan 488 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → (𝐴 ·e -∞) =
-∞) |
57 | 56 | adantr 481 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) → (𝐴 ·e -∞) =
-∞) |
58 | 57 | adantr 481 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = -∞) → (𝐴 ·e -∞) =
-∞) |
59 | 35 | adantr 481 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = -∞) → (𝐴 ·e 𝐵) ∈ ℝ) |
60 | | renepnf 10087 |
. . . . . . 7
⊢ ((𝐴 ·e 𝐵) ∈ ℝ → (𝐴 ·e 𝐵) ≠
+∞) |
61 | | xaddmnf1 12059 |
. . . . . . 7
⊢ (((𝐴 ·e 𝐵) ∈ ℝ*
∧ (𝐴
·e 𝐵)
≠ +∞) → ((𝐴
·e 𝐵)
+𝑒 -∞) = -∞) |
62 | 36, 60, 61 | syl2anc 693 |
. . . . . 6
⊢ ((𝐴 ·e 𝐵) ∈ ℝ → ((𝐴 ·e 𝐵) +𝑒
-∞) = -∞) |
63 | 59, 62 | syl 17 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = -∞) → ((𝐴 ·e 𝐵) +𝑒 -∞) =
-∞) |
64 | 58, 63 | eqtr4d 2659 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = -∞) → (𝐴 ·e -∞) = ((𝐴 ·e 𝐵) +𝑒
-∞)) |
65 | | oveq2 6658 |
. . . . . 6
⊢ (𝐶 = -∞ → (𝐵 +𝑒 𝐶) = (𝐵 +𝑒
-∞)) |
66 | | renepnf 10087 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ≠ +∞) |
67 | | xaddmnf1 12059 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ (𝐵
+𝑒 -∞) = -∞) |
68 | 44, 66, 67 | syl2anc 693 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → (𝐵 +𝑒 -∞)
= -∞) |
69 | 68 | adantl 482 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 -∞) =
-∞) |
70 | 65, 69 | sylan9eqr 2678 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = -∞) → (𝐵 +𝑒 𝐶) = -∞) |
71 | 70 | oveq2d 6666 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e
-∞)) |
72 | | oveq2 6658 |
. . . . . 6
⊢ (𝐶 = -∞ → (𝐴 ·e 𝐶) = (𝐴 ·e
-∞)) |
73 | 72, 57 | sylan9eqr 2678 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = -∞) → (𝐴 ·e 𝐶) = -∞) |
74 | 73 | oveq2d 6666 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = -∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 ·e 𝐵) +𝑒
-∞)) |
75 | 64, 71, 74 | 3eqtr4d 2666 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) ∧ 𝐶 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
76 | | simpl3 1066 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → 𝐶 ∈
ℝ*) |
77 | | elxr 11950 |
. . . . 5
⊢ (𝐶 ∈ ℝ*
↔ (𝐶 ∈ ℝ
∨ 𝐶 = +∞ ∨
𝐶 =
-∞)) |
78 | 76, 77 | sylib 208 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
79 | 78 | adantr 481 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
80 | 28, 54, 75, 79 | mpjao3dan 1395 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
81 | 32 | ad2antrr 762 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e +∞) =
+∞) |
82 | 1 | adantr 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) → 𝐴 ∈ ℝ) |
83 | 24, 14 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ·e 𝐶) ∈
ℝ) |
84 | 82, 83 | sylan 488 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e 𝐶) ∈ ℝ) |
85 | | rexr 10085 |
. . . . . . 7
⊢ ((𝐴 ·e 𝐶) ∈ ℝ → (𝐴 ·e 𝐶) ∈
ℝ*) |
86 | | renemnf 10088 |
. . . . . . 7
⊢ ((𝐴 ·e 𝐶) ∈ ℝ → (𝐴 ·e 𝐶) ≠
-∞) |
87 | | xaddpnf2 12058 |
. . . . . . 7
⊢ (((𝐴 ·e 𝐶) ∈ ℝ*
∧ (𝐴
·e 𝐶)
≠ -∞) → (+∞ +𝑒 (𝐴 ·e 𝐶)) = +∞) |
88 | 85, 86, 87 | syl2anc 693 |
. . . . . 6
⊢ ((𝐴 ·e 𝐶) ∈ ℝ →
(+∞ +𝑒 (𝐴 ·e 𝐶)) = +∞) |
89 | 84, 88 | syl 17 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 ∈ ℝ) → (+∞
+𝑒 (𝐴
·e 𝐶)) =
+∞) |
90 | 81, 89 | eqtr4d 2659 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e +∞) = (+∞
+𝑒 (𝐴
·e 𝐶))) |
91 | | simpr 477 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) → 𝐵 = +∞) |
92 | 91 | oveq1d 6665 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = (+∞ +𝑒 𝐶)) |
93 | | rexr 10085 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℝ*) |
94 | | renemnf 10088 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ → 𝐶 ≠ -∞) |
95 | | xaddpnf2 12058 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ -∞)
→ (+∞ +𝑒 𝐶) = +∞) |
96 | 93, 94, 95 | syl2anc 693 |
. . . . . 6
⊢ (𝐶 ∈ ℝ → (+∞
+𝑒 𝐶) =
+∞) |
97 | 92, 96 | sylan9eq 2676 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = +∞) |
98 | 97 | oveq2d 6666 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e
+∞)) |
99 | | oveq2 6658 |
. . . . . . 7
⊢ (𝐵 = +∞ → (𝐴 ·e 𝐵) = (𝐴 ·e
+∞)) |
100 | 99, 32 | sylan9eqr 2678 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) → (𝐴 ·e 𝐵) = +∞) |
101 | 100 | adantr 481 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e 𝐵) = +∞) |
102 | 101 | oveq1d 6665 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 ∈ ℝ) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (+∞ +𝑒 (𝐴 ·e 𝐶))) |
103 | 90, 98, 102 | 3eqtr4d 2666 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
104 | | pnfxr 10092 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
105 | | pnfnemnf 10094 |
. . . . . . 7
⊢ +∞
≠ -∞ |
106 | | xaddpnf1 12057 |
. . . . . . 7
⊢
((+∞ ∈ ℝ* ∧ +∞ ≠ -∞)
→ (+∞ +𝑒 +∞) = +∞) |
107 | 104, 105,
106 | mp2an 708 |
. . . . . 6
⊢ (+∞
+𝑒 +∞) = +∞ |
108 | 32, 32 | oveq12d 6668 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → ((𝐴 ·e +∞)
+𝑒 (𝐴
·e +∞)) = (+∞ +𝑒
+∞)) |
109 | 107, 108,
32 | 3eqtr4a 2682 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → ((𝐴 ·e +∞)
+𝑒 (𝐴
·e +∞)) = (𝐴 ·e
+∞)) |
110 | 109 | ad2antrr 762 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → ((𝐴 ·e +∞)
+𝑒 (𝐴
·e +∞)) = (𝐴 ·e
+∞)) |
111 | 99, 51 | oveqan12d 6669 |
. . . . 5
⊢ ((𝐵 = +∞ ∧ 𝐶 = +∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 ·e +∞)
+𝑒 (𝐴
·e +∞))) |
112 | 111 | adantll 750 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 ·e +∞)
+𝑒 (𝐴
·e +∞))) |
113 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝐵 = +∞ ∧ 𝐶 = +∞) → (𝐵 +𝑒 𝐶) = (+∞
+𝑒 +∞)) |
114 | 113, 107 | syl6eq 2672 |
. . . . . 6
⊢ ((𝐵 = +∞ ∧ 𝐶 = +∞) → (𝐵 +𝑒 𝐶) = +∞) |
115 | 114 | oveq2d 6666 |
. . . . 5
⊢ ((𝐵 = +∞ ∧ 𝐶 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e
+∞)) |
116 | 115 | adantll 750 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e
+∞)) |
117 | 110, 112,
116 | 3eqtr4rd 2667 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
118 | | pnfaddmnf 12061 |
. . . . . 6
⊢ (+∞
+𝑒 -∞) = 0 |
119 | 32, 56 | oveq12d 6668 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → ((𝐴 ·e +∞)
+𝑒 (𝐴
·e -∞)) = (+∞ +𝑒
-∞)) |
120 | | xmul01 12097 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e 0) = 0) |
121 | 1, 29, 120 | 3syl 18 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → (𝐴 ·e 0) =
0) |
122 | 118, 119,
121 | 3eqtr4a 2682 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → ((𝐴 ·e +∞)
+𝑒 (𝐴
·e -∞)) = (𝐴 ·e 0)) |
123 | 122 | ad2antrr 762 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 = -∞) → ((𝐴 ·e +∞)
+𝑒 (𝐴
·e -∞)) = (𝐴 ·e 0)) |
124 | 99, 72 | oveqan12d 6669 |
. . . . 5
⊢ ((𝐵 = +∞ ∧ 𝐶 = -∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 ·e +∞)
+𝑒 (𝐴
·e -∞))) |
125 | 124 | adantll 750 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 = -∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 ·e +∞)
+𝑒 (𝐴
·e -∞))) |
126 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝐵 = +∞ ∧ 𝐶 = -∞) → (𝐵 +𝑒 𝐶) = (+∞
+𝑒 -∞)) |
127 | 126, 118 | syl6eq 2672 |
. . . . . 6
⊢ ((𝐵 = +∞ ∧ 𝐶 = -∞) → (𝐵 +𝑒 𝐶) = 0) |
128 | 127 | oveq2d 6666 |
. . . . 5
⊢ ((𝐵 = +∞ ∧ 𝐶 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e 0)) |
129 | 128 | adantll 750 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e 0)) |
130 | 123, 125,
129 | 3eqtr4rd 2667 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) ∧ 𝐶 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
131 | 78 | adantr 481 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
132 | 103, 117,
130, 131 | mpjao3dan 1395 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
133 | 56 | ad2antrr 762 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e -∞) =
-∞) |
134 | 1 | adantr 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ) |
135 | 134, 83 | sylan 488 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e 𝐶) ∈ ℝ) |
136 | | renepnf 10087 |
. . . . . . 7
⊢ ((𝐴 ·e 𝐶) ∈ ℝ → (𝐴 ·e 𝐶) ≠
+∞) |
137 | | xaddmnf2 12060 |
. . . . . . 7
⊢ (((𝐴 ·e 𝐶) ∈ ℝ*
∧ (𝐴
·e 𝐶)
≠ +∞) → (-∞ +𝑒 (𝐴 ·e 𝐶)) = -∞) |
138 | 85, 136, 137 | syl2anc 693 |
. . . . . 6
⊢ ((𝐴 ·e 𝐶) ∈ ℝ →
(-∞ +𝑒 (𝐴 ·e 𝐶)) = -∞) |
139 | 135, 138 | syl 17 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 ∈ ℝ) → (-∞
+𝑒 (𝐴
·e 𝐶)) =
-∞) |
140 | 133, 139 | eqtr4d 2659 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e -∞) = (-∞
+𝑒 (𝐴
·e 𝐶))) |
141 | | simpr 477 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) → 𝐵 = -∞) |
142 | 141 | oveq1d 6665 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) → (𝐵 +𝑒 𝐶) = (-∞ +𝑒 𝐶)) |
143 | | renepnf 10087 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ → 𝐶 ≠ +∞) |
144 | | xaddmnf2 12060 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ +∞)
→ (-∞ +𝑒 𝐶) = -∞) |
145 | 93, 143, 144 | syl2anc 693 |
. . . . . 6
⊢ (𝐶 ∈ ℝ → (-∞
+𝑒 𝐶) =
-∞) |
146 | 142, 145 | sylan9eq 2676 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = -∞) |
147 | 146 | oveq2d 6666 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e
-∞)) |
148 | | oveq2 6658 |
. . . . . . 7
⊢ (𝐵 = -∞ → (𝐴 ·e 𝐵) = (𝐴 ·e
-∞)) |
149 | 148, 56 | sylan9eqr 2678 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) → (𝐴 ·e 𝐵) = -∞) |
150 | 149 | adantr 481 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e 𝐵) = -∞) |
151 | 150 | oveq1d 6665 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 ∈ ℝ) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (-∞ +𝑒 (𝐴 ·e 𝐶))) |
152 | 140, 147,
151 | 3eqtr4d 2666 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
153 | 56, 32 | oveq12d 6668 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → ((𝐴 ·e -∞)
+𝑒 (𝐴
·e +∞)) = (-∞ +𝑒
+∞)) |
154 | | mnfaddpnf 12062 |
. . . . . . 7
⊢ (-∞
+𝑒 +∞) = 0 |
155 | 153, 154 | syl6eq 2672 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → ((𝐴 ·e -∞)
+𝑒 (𝐴
·e +∞)) = 0) |
156 | 121, 155 | eqtr4d 2659 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → (𝐴 ·e 0) = ((𝐴 ·e -∞)
+𝑒 (𝐴
·e +∞))) |
157 | 156 | ad2antrr 762 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 = +∞) → (𝐴 ·e 0) = ((𝐴 ·e -∞)
+𝑒 (𝐴
·e +∞))) |
158 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝐵 = -∞ ∧ 𝐶 = +∞) → (𝐵 +𝑒 𝐶) = (-∞
+𝑒 +∞)) |
159 | 158, 154 | syl6eq 2672 |
. . . . . 6
⊢ ((𝐵 = -∞ ∧ 𝐶 = +∞) → (𝐵 +𝑒 𝐶) = 0) |
160 | 159 | oveq2d 6666 |
. . . . 5
⊢ ((𝐵 = -∞ ∧ 𝐶 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e 0)) |
161 | 160 | adantll 750 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e 0)) |
162 | 148, 51 | oveqan12d 6669 |
. . . . 5
⊢ ((𝐵 = -∞ ∧ 𝐶 = +∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 ·e -∞)
+𝑒 (𝐴
·e +∞))) |
163 | 162 | adantll 750 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 = +∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 ·e -∞)
+𝑒 (𝐴
·e +∞))) |
164 | 157, 161,
163 | 3eqtr4d 2666 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
165 | | mnfxr 10096 |
. . . . . . 7
⊢ -∞
∈ ℝ* |
166 | | mnfnepnf 10095 |
. . . . . . 7
⊢ -∞
≠ +∞ |
167 | | xaddmnf1 12059 |
. . . . . . 7
⊢
((-∞ ∈ ℝ* ∧ -∞ ≠ +∞)
→ (-∞ +𝑒 -∞) = -∞) |
168 | 165, 166,
167 | mp2an 708 |
. . . . . 6
⊢ (-∞
+𝑒 -∞) = -∞ |
169 | 56, 56 | oveq12d 6668 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → ((𝐴 ·e -∞)
+𝑒 (𝐴
·e -∞)) = (-∞ +𝑒
-∞)) |
170 | 168, 169,
56 | 3eqtr4a 2682 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → ((𝐴 ·e -∞)
+𝑒 (𝐴
·e -∞)) = (𝐴 ·e
-∞)) |
171 | 170 | ad2antrr 762 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → ((𝐴 ·e -∞)
+𝑒 (𝐴
·e -∞)) = (𝐴 ·e
-∞)) |
172 | 148, 72 | oveqan12d 6669 |
. . . . 5
⊢ ((𝐵 = -∞ ∧ 𝐶 = -∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 ·e -∞)
+𝑒 (𝐴
·e -∞))) |
173 | 172 | adantll 750 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((𝐴 ·e -∞)
+𝑒 (𝐴
·e -∞))) |
174 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝐵 = -∞ ∧ 𝐶 = -∞) → (𝐵 +𝑒 𝐶) = (-∞
+𝑒 -∞)) |
175 | 174, 168 | syl6eq 2672 |
. . . . . 6
⊢ ((𝐵 = -∞ ∧ 𝐶 = -∞) → (𝐵 +𝑒 𝐶) = -∞) |
176 | 175 | oveq2d 6666 |
. . . . 5
⊢ ((𝐵 = -∞ ∧ 𝐶 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e
-∞)) |
177 | 176 | adantll 750 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e
-∞)) |
178 | 171, 173,
177 | 3eqtr4rd 2667 |
. . 3
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) ∧ 𝐶 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
179 | 78 | adantr 481 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
180 | 152, 164,
178, 179 | mpjao3dan 1395 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) ∧ 𝐵 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
181 | | simpl2 1065 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → 𝐵 ∈
ℝ*) |
182 | | elxr 11950 |
. . 3
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
183 | 181, 182 | sylib 208 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
184 | 80, 132, 180, 183 | mpjao3dan 1395 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |