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 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 · 𝐵 ) )

Proof

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