Metamath Proof Explorer

Theorem gt0div

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

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

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 ltdiv1 ⊢ 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