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 ‘ 𝐴 ) ) )