This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xmulgt0

Description: Extended real version of mulgt0 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulgt0 ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 ·e 𝐵 ) )

Proof

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 𝐵 ) )