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