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

Proof

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