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