| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 0 < 𝐴 ) |
| 2 |
|
simpr |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) → 0 < 𝐵 ) |
| 3 |
1 2
|
anim12i |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) |
| 4 |
|
mulgt0 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 · 𝐵 ) ) |
| 5 |
4
|
an4s |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 · 𝐵 ) ) |
| 6 |
5
|
ancoms |
⊢ ( ( ( 0 < 𝐴 ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → 0 < ( 𝐴 · 𝐵 ) ) |
| 7 |
|
rexmul |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ·e 𝐵 ) = ( 𝐴 · 𝐵 ) ) |
| 8 |
7
|
adantl |
⊢ ( ( ( 0 < 𝐴 ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( 𝐴 ·e 𝐵 ) = ( 𝐴 · 𝐵 ) ) |
| 9 |
6 8
|
breqtrrd |
⊢ ( ( ( 0 < 𝐴 ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 10 |
3 9
|
sylan |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 11 |
10
|
anassrs |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 12 |
|
0ltpnf |
⊢ 0 < +∞ |
| 13 |
|
oveq2 |
⊢ ( 𝐵 = +∞ → ( 𝐴 ·e 𝐵 ) = ( 𝐴 ·e +∞ ) ) |
| 14 |
|
xmulpnf1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = +∞ ) |
| 15 |
14
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → ( 𝐴 ·e +∞ ) = +∞ ) |
| 16 |
13 15
|
sylan9eqr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐵 = +∞ ) → ( 𝐴 ·e 𝐵 ) = +∞ ) |
| 17 |
12 16
|
breqtrrid |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐵 = +∞ ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 18 |
17
|
adantlr |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 = +∞ ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 19 |
|
simplrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐴 ∈ ℝ ) → 0 < 𝐵 ) |
| 20 |
|
xmulasslem2 |
⊢ ( ( 0 < 𝐵 ∧ 𝐵 = -∞ ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 21 |
19 20
|
sylan |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐴 ∈ ℝ ) ∧ 𝐵 = -∞ ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 22 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → 𝐵 ∈ ℝ* ) |
| 23 |
|
elxr |
⊢ ( 𝐵 ∈ ℝ* ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) |
| 24 |
22 23
|
sylib |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) |
| 25 |
24
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) |
| 26 |
11 18 21 25
|
mpjao3dan |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐴 ∈ ℝ ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 27 |
|
oveq1 |
⊢ ( 𝐴 = +∞ → ( 𝐴 ·e 𝐵 ) = ( +∞ ·e 𝐵 ) ) |
| 28 |
|
xmulpnf2 |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) → ( +∞ ·e 𝐵 ) = +∞ ) |
| 29 |
28
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → ( +∞ ·e 𝐵 ) = +∞ ) |
| 30 |
27 29
|
sylan9eqr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐴 = +∞ ) → ( 𝐴 ·e 𝐵 ) = +∞ ) |
| 31 |
12 30
|
breqtrrid |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐴 = +∞ ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 32 |
|
xmulasslem2 |
⊢ ( ( 0 < 𝐴 ∧ 𝐴 = -∞ ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 33 |
32
|
ad4ant24 |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) ∧ 𝐴 = -∞ ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
| 34 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → 𝐴 ∈ ℝ* ) |
| 35 |
|
elxr |
⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ) |
| 36 |
34 35
|
sylib |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ) |
| 37 |
26 31 33 36
|
mpjao3dan |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 ·e 𝐵 ) ) |