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 e. QQ -> ( 0 < A <-> 0 < ( numer ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		0red	|- ( A e. QQ -> 0 e. RR )
2		qre	|- ( A e. QQ -> A e. RR )
3		qdencl	|- ( A e. QQ -> ( denom ` A ) e. NN )
4	3	nnred	|- ( A e. QQ -> ( denom ` A ) e. RR )
5	3	nngt0d	|- ( A e. QQ -> 0 < ( denom ` A ) )
6		ltmul1	|- ( ( 0 e. RR /\ A e. RR /\ ( ( denom ` A ) e. RR /\ 0 < ( denom ` A ) ) ) -> ( 0 < A <-> ( 0 x. ( denom ` A ) ) < ( A x. ( denom ` A ) ) ) )
7	1 2 4 5 6	syl112anc	|- ( A e. QQ -> ( 0 < A <-> ( 0 x. ( denom ` A ) ) < ( A x. ( denom ` A ) ) ) )
8	3	nncnd	|- ( A e. QQ -> ( denom ` A ) e. CC )
9	8	mul02d	|- ( A e. QQ -> ( 0 x. ( denom ` A ) ) = 0 )
10		qmuldeneqnum	|- ( A e. QQ -> ( A x. ( denom ` A ) ) = ( numer ` A ) )
11	9 10	breq12d	|- ( A e. QQ -> ( ( 0 x. ( denom ` A ) ) < ( A x. ( denom ` A ) ) <-> 0 < ( numer ` A ) ) )
12	7 11	bitrd	|- ( A e. QQ -> ( 0 < A <-> 0 < ( numer ` A ) ) )