Metamath Proof Explorer

Theorem zdend

Description: Denominator of an integer. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypothesis znumd.1 
|- ( ph -> Z e. ZZ )
Assertion zdend 
|- ( ph -> ( denom ` Z ) = 1 )

Proof

Step Hyp Ref Expression
1 znumd.1 
 |-  ( ph -> Z e. ZZ )
2 zq 
 |-  ( Z e. ZZ -> Z e. QQ )
3 1 2 syl 
 |-  ( ph -> Z e. QQ )
4 1nn 
 |-  1 e. NN
5 4 a1i 
 |-  ( ph -> 1 e. NN )
6 gcd1 
 |-  ( Z e. ZZ -> ( Z gcd 1 ) = 1 )
7 1 6 syl 
 |-  ( ph -> ( Z gcd 1 ) = 1 )
8 1 zcnd 
 |-  ( ph -> Z e. CC )
9 8 div1d 
 |-  ( ph -> ( Z / 1 ) = Z )
10 9 eqcomd 
 |-  ( ph -> Z = ( Z / 1 ) )
11 qnumdenbi 
 |-  ( ( Z e. QQ /\ Z e. ZZ /\ 1 e. NN ) -> ( ( ( Z gcd 1 ) = 1 /\ Z = ( Z / 1 ) ) <-> ( ( numer ` Z ) = Z /\ ( denom ` Z ) = 1 ) ) )
12 11 biimpa 
 |-  ( ( ( Z e. QQ /\ Z e. ZZ /\ 1 e. NN ) /\ ( ( Z gcd 1 ) = 1 /\ Z = ( Z / 1 ) ) ) -> ( ( numer ` Z ) = Z /\ ( denom ` Z ) = 1 ) )
13 3 1 5 7 10 12 syl32anc 
 |-  ( ph -> ( ( numer ` Z ) = Z /\ ( denom ` Z ) = 1 ) )
14 13 simprd 
 |-  ( ph -> ( denom ` Z ) = 1 )