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 ( 𝐴 ∈ ℚ → ( 0 < 𝐴 ↔ 0 < ( numer ‘ 𝐴 ) ) )

Proof

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