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