Metamath Proof Explorer

Theorem xmulge0

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

Ref Expression
Assertion xmulge0 ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 ·e 𝐵 ) )

Proof

Step Hyp Ref Expression
1 xmulgt0 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 ·e 𝐵 ) )
2 1 an4s ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 ·e 𝐵 ) )
3 0xr ⊢ 0 ∈ ℝ*
4 xmulcl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e 𝐵 ) ∈ ℝ* )
5 4 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → ( 𝐴 ·e 𝐵 ) ∈ ℝ* )
6 xrltle ⊢ ( ( 0 ∈ ℝ* ∧ ( 𝐴 ·e 𝐵 ) ∈ ℝ* ) → ( 0 < ( 𝐴 ·e 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) )
7 3 5 6 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → ( 0 < ( 𝐴 ·e 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) )
8 2 7 mpd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → 0 ≤ ( 𝐴 ·e 𝐵 ) )
9 8 ex ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 0 < 𝐴 ∧ 0 < 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) )
10 9 ad2ant2r ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → ( ( 0 < 𝐴 ∧ 0 < 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) )
11 10 impl ⊢ ( ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 < 𝐴 ) ∧ 0 < 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) )
12 0le0 ⊢ 0 ≤ 0
13 oveq2 ⊢ ( 0 = 𝐵 → ( 𝐴 ·e 0 ) = ( 𝐴 ·e 𝐵 ) )
14 13 eqcomd ⊢ ( 0 = 𝐵 → ( 𝐴 ·e 𝐵 ) = ( 𝐴 ·e 0 ) )
15 xmul01 ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·e 0 ) = 0 )
16 15 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 ·e 0 ) = 0 )
17 14 16 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 = 𝐵 ) → ( 𝐴 ·e 𝐵 ) = 0 )
18 12 17 breqtrrid ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 = 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) )
19 18 adantlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 < 𝐴 ) ∧ 0 = 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) )
20 xrleloe ⊢ ( ( 0 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 ↔ ( 0 < 𝐵 ∨ 0 = 𝐵 ) ) )
21 3 20 mpan ⊢ ( 𝐵 ∈ ℝ* → ( 0 ≤ 𝐵 ↔ ( 0 < 𝐵 ∨ 0 = 𝐵 ) ) )
22 21 biimpa ⊢ ( ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) → ( 0 < 𝐵 ∨ 0 = 𝐵 ) )
23 22 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 < 𝐴 ) → ( 0 < 𝐵 ∨ 0 = 𝐵 ) )
24 11 19 23 mpjaodan ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 < 𝐴 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) )
25 oveq1 ⊢ ( 0 = 𝐴 → ( 0 ·e 𝐵 ) = ( 𝐴 ·e 𝐵 ) )
26 25 eqcomd ⊢ ( 0 = 𝐴 → ( 𝐴 ·e 𝐵 ) = ( 0 ·e 𝐵 ) )
27 xmul02 ⊢ ( 𝐵 ∈ ℝ* → ( 0 ·e 𝐵 ) = 0 )
28 27 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → ( 0 ·e 𝐵 ) = 0 )
29 26 28 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 = 𝐴 ) → ( 𝐴 ·e 𝐵 ) = 0 )
30 12 29 breqtrrid ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 = 𝐴 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) )
31 xrleloe ⊢ ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
32 3 31 mpan ⊢ ( 𝐴 ∈ ℝ* → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
33 32 biimpa ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → ( 0 < 𝐴 ∨ 0 = 𝐴 ) )
34 33 adantr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → ( 0 < 𝐴 ∨ 0 = 𝐴 ) )
35 24 30 34 mpjaodan ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 ·e 𝐵 ) )