Theorem znq

Description: The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002)

	Ref	Expression
Assertion	znq	|- ( ( A e. ZZ /\ B e. NN ) -> ( A / B ) e. QQ )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( A / B ) = ( A / B )
2		rspceov	|- ( ( A e. ZZ /\ B e. NN /\ ( A / B ) = ( A / B ) ) -> E. x e. ZZ E. y e. NN ( A / B ) = ( x / y ) )
3	1 2	mp3an3	|- ( ( A e. ZZ /\ B e. NN ) -> E. x e. ZZ E. y e. NN ( A / B ) = ( x / y ) )
4		elq	|- ( ( A / B ) e. QQ <-> E. x e. ZZ E. y e. NN ( A / B ) = ( x / y ) )
5	3 4	sylibr	|- ( ( A e. ZZ /\ B e. NN ) -> ( A / B ) e. QQ )