Metamath Proof Explorer

Theorem ge0div

Description: Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005)

Ref Expression
Assertion ge0div ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B → 0 ≤ A ↔ 0 ≤ A B

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 lediv1 ⊢ 0 ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B → 0 ≤ A ↔ 0 B ≤ A B
3 1 2 mp3an1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B → 0 ≤ A ↔ 0 B ≤ A B
4 3 3impb ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B → 0 ≤ A ↔ 0 B ≤ A B
5 recn ⊢ B ∈ ℝ → B ∈ ℂ
6 gt0ne0 ⊢ B ∈ ℝ ∧ 0 < B → B ≠ 0
7 div0 ⊢ B ∈ ℂ ∧ B ≠ 0 → 0 B = 0
8 5 6 7 syl2an2r ⊢ B ∈ ℝ ∧ 0 < B → 0 B = 0
9 8 breq1d ⊢ B ∈ ℝ ∧ 0 < B → 0 B ≤ A B ↔ 0 ≤ A B
10 9 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B → 0 B ≤ A B ↔ 0 ≤ A B
11 4 10 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B → 0 ≤ A ↔ 0 ≤ A B