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

Metamath Proof Explorer

Theorem qnumcl

Description: The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion qnumcl 
|- ( A e. QQ -> ( numer ` A ) e. ZZ )

Proof

Step Hyp Ref Expression
1 qnumdencl 
 |-  ( A e. QQ -> ( ( numer ` A ) e. ZZ /\ ( denom ` A ) e. NN ) )
2 1 simpld 
 |-  ( A e. QQ -> ( numer ` A ) e. ZZ )