Theorem qden1elz

Description: A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014)

	Ref	Expression
Assertion	qden1elz	|- ( A e. QQ -> ( ( denom ` A ) = 1 <-> A e. ZZ ) )

Proof

Step	Hyp	Ref	Expression
1		qeqnumdivden	|- ( A e. QQ -> A = ( ( numer ` A ) / ( denom ` A ) ) )
2	1	adantr	|- ( ( A e. QQ /\ ( denom ` A ) = 1 ) -> A = ( ( numer ` A ) / ( denom ` A ) ) )
3		oveq2	|- ( ( denom ` A ) = 1 -> ( ( numer ` A ) / ( denom ` A ) ) = ( ( numer ` A ) / 1 ) )
4	3	adantl	|- ( ( A e. QQ /\ ( denom ` A ) = 1 ) -> ( ( numer ` A ) / ( denom ` A ) ) = ( ( numer ` A ) / 1 ) )
5		qnumcl	|- ( A e. QQ -> ( numer ` A ) e. ZZ )
6	5	adantr	|- ( ( A e. QQ /\ ( denom ` A ) = 1 ) -> ( numer ` A ) e. ZZ )
7	6	zcnd	|- ( ( A e. QQ /\ ( denom ` A ) = 1 ) -> ( numer ` A ) e. CC )
8	7	div1d	|- ( ( A e. QQ /\ ( denom ` A ) = 1 ) -> ( ( numer ` A ) / 1 ) = ( numer ` A ) )
9	2 4 8	3eqtrd	|- ( ( A e. QQ /\ ( denom ` A ) = 1 ) -> A = ( numer ` A ) )
10	9 6	eqeltrd	|- ( ( A e. QQ /\ ( denom ` A ) = 1 ) -> A e. ZZ )
11		simpr	|- ( ( A e. QQ /\ A e. ZZ ) -> A e. ZZ )
12	11	zcnd	|- ( ( A e. QQ /\ A e. ZZ ) -> A e. CC )
13	12	div1d	|- ( ( A e. QQ /\ A e. ZZ ) -> ( A / 1 ) = A )
14	13	fveq2d	|- ( ( A e. QQ /\ A e. ZZ ) -> ( denom ` ( A / 1 ) ) = ( denom ` A ) )
15		1nn	|- 1 e. NN
16		divdenle	|- ( ( A e. ZZ /\ 1 e. NN ) -> ( denom ` ( A / 1 ) ) <_ 1 )
17	11 15 16	sylancl	|- ( ( A e. QQ /\ A e. ZZ ) -> ( denom ` ( A / 1 ) ) <_ 1 )
18	14 17	eqbrtrrd	|- ( ( A e. QQ /\ A e. ZZ ) -> ( denom ` A ) <_ 1 )
19		qdencl	|- ( A e. QQ -> ( denom ` A ) e. NN )
20	19	adantr	|- ( ( A e. QQ /\ A e. ZZ ) -> ( denom ` A ) e. NN )
21		nnle1eq1	|- ( ( denom ` A ) e. NN -> ( ( denom ` A ) <_ 1 <-> ( denom ` A ) = 1 ) )
22	20 21	syl	|- ( ( A e. QQ /\ A e. ZZ ) -> ( ( denom ` A ) <_ 1 <-> ( denom ` A ) = 1 ) )
23	18 22	mpbid	|- ( ( A e. QQ /\ A e. ZZ ) -> ( denom ` A ) = 1 )
24	10 23	impbida	|- ( A e. QQ -> ( ( denom ` A ) = 1 <-> A e. ZZ ) )