Metamath Proof Explorer

Theorem mulge0

Description: The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion mulge0 ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→0≤A⁢B

Proof

Step Hyp Ref Expression
1 0red ⊢A∈ℝ∧B∈ℝ→0∈ℝ
2 simpl ⊢A∈ℝ∧B∈ℝ→A∈ℝ
3 1 2 leloed ⊢A∈ℝ∧B∈ℝ→0≤A↔0<A∨0=A
4 simpr ⊢A∈ℝ∧B∈ℝ→B∈ℝ
5 1 4 leloed ⊢A∈ℝ∧B∈ℝ→0≤B↔0<B∨0=B
6 3 5 anbi12d ⊢A∈ℝ∧B∈ℝ→0≤A∧0≤B↔0<A∨0=A∧0<B∨0=B
7 0red ⊢A∈ℝ∧B∈ℝ∧0<A∧0<B→0∈ℝ
8 simpll ⊢A∈ℝ∧B∈ℝ∧0<A∧0<B→A∈ℝ
9 simplr ⊢A∈ℝ∧B∈ℝ∧0<A∧0<B→B∈ℝ
10 8 9 remulcld ⊢A∈ℝ∧B∈ℝ∧0<A∧0<B→A⁢B∈ℝ
11 mulgt0 ⊢A∈ℝ∧0<A∧B∈ℝ∧0<B→0<A⁢B
12 11 an4s ⊢A∈ℝ∧B∈ℝ∧0<A∧0<B→0<A⁢B
13 7 10 12 ltled ⊢A∈ℝ∧B∈ℝ∧0<A∧0<B→0≤A⁢B
14 13 ex ⊢A∈ℝ∧B∈ℝ→0<A∧0<B→0≤A⁢B
15 0re ⊢0∈ℝ
16 leid ⊢0∈ℝ→0≤0
17 15 16 ax-mp ⊢0≤0
18 4 recnd ⊢A∈ℝ∧B∈ℝ→B∈ℂ
19 18 mul02d ⊢A∈ℝ∧B∈ℝ→0⋅B=0
20 17 19 breqtrrid ⊢A∈ℝ∧B∈ℝ→0≤0⋅B
21 oveq1 ⊢0=A→0⋅B=A⁢B
22 21 breq2d ⊢0=A→0≤0⋅B↔0≤A⁢B
23 20 22 syl5ibcom ⊢A∈ℝ∧B∈ℝ→0=A→0≤A⁢B
24 23 adantrd ⊢A∈ℝ∧B∈ℝ→0=A∧0<B→0≤A⁢B
25 2 recnd ⊢A∈ℝ∧B∈ℝ→A∈ℂ
26 25 mul01d ⊢A∈ℝ∧B∈ℝ→A⋅0=0
27 17 26 breqtrrid ⊢A∈ℝ∧B∈ℝ→0≤A⋅0
28 oveq2 ⊢0=B→A⋅0=A⁢B
29 28 breq2d ⊢0=B→0≤A⋅0↔0≤A⁢B
30 27 29 syl5ibcom ⊢A∈ℝ∧B∈ℝ→0=B→0≤A⁢B
31 30 adantld ⊢A∈ℝ∧B∈ℝ→0<A∧0=B→0≤A⁢B
32 30 adantld ⊢A∈ℝ∧B∈ℝ→0=A∧0=B→0≤A⁢B
33 14 24 31 32 ccased ⊢A∈ℝ∧B∈ℝ→0<A∨0=A∧0<B∨0=B→0≤A⁢B
34 6 33 sylbid ⊢A∈ℝ∧B∈ℝ→0≤A∧0≤B→0≤A⁢B
35 34 imp ⊢A∈ℝ∧B∈ℝ∧0≤A∧0≤B→0≤A⁢B
36 35 an4s ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→0≤A⁢B