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

Metamath Proof Explorer

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