This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qnumgt0

Description: A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014)

Ref Expression
Assertion qnumgt0 ⊢ A ∈ ℚ → 0 < A ↔ 0 < numer ⁡ A

Proof

Step Hyp Ref Expression
1 0red ⊢ A ∈ ℚ → 0 ∈ ℝ
2 qre ⊢ A ∈ ℚ → A ∈ ℝ
3 qdencl ⊢ A ∈ ℚ → denom ⁡ A ∈ ℕ
4 3 nnred ⊢ A ∈ ℚ → denom ⁡ A ∈ ℝ
5 3 nngt0d ⊢ A ∈ ℚ → 0 < denom ⁡ A
6 ltmul1 ⊢ 0 ∈ ℝ ∧ A ∈ ℝ ∧ denom ⁡ A ∈ ℝ ∧ 0 < denom ⁡ A → 0 < A ↔ 0 ⋅ denom ⁡ A < A ⁢ denom ⁡ A
7 1 2 4 5 6 syl112anc ⊢ A ∈ ℚ → 0 < A ↔ 0 ⋅ denom ⁡ A < A ⁢ denom ⁡ A
8 3 nncnd ⊢ A ∈ ℚ → denom ⁡ A ∈ ℂ
9 8 mul02d ⊢ A ∈ ℚ → 0 ⋅ denom ⁡ A = 0
10 qmuldeneqnum ⊢ A ∈ ℚ → A ⁢ denom ⁡ A = numer ⁡ A
11 9 10 breq12d ⊢ A ∈ ℚ → 0 ⋅ denom ⁡ A < A ⁢ denom ⁡ A ↔ 0 < numer ⁡ A
12 7 11 bitrd ⊢ A ∈ ℚ → 0 < A ↔ 0 < numer ⁡ A