Metamath Proof Explorer

Theorem zrtelqelz

Description: If the N -th root of an integer A is rational, that root is must be an integer. Similar to zsqrtelqelz , generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023)

Ref Expression
Assertion zrtelqelz 
|- ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( A ^c ( 1 / N ) ) e. ZZ )

Proof

Step Hyp Ref Expression
1 qdencl 
 |-  ( ( A ^c ( 1 / N ) ) e. QQ -> ( denom ` ( A ^c ( 1 / N ) ) ) e. NN )
2 1 3ad2ant3 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( denom ` ( A ^c ( 1 / N ) ) ) e. NN )
3 2 nnrpd 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( denom ` ( A ^c ( 1 / N ) ) ) e. RR+ )
4 1rp 
 |-  1 e. RR+
5 4 a1i 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> 1 e. RR+ )
6 simp2 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> N e. NN )
7 6 nnzd 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> N e. ZZ )
8 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
9 7 8 syl 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( 1 ^ N ) = 1 )
10 zcn 
 |-  ( A e. ZZ -> A e. CC )
11 10 3ad2ant1 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> A e. CC )
12 cxproot 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A ^c ( 1 / N ) ) ^ N ) = A )
13 11 6 12 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( ( A ^c ( 1 / N ) ) ^ N ) = A )
14 13 fveq2d 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( denom ` ( ( A ^c ( 1 / N ) ) ^ N ) ) = ( denom ` A ) )
15 zq 
 |-  ( A e. ZZ -> A e. QQ )
16 qden1elz 
 |-  ( A e. QQ -> ( ( denom ` A ) = 1 <-> A e. ZZ ) )
17 15 16 syl 
 |-  ( A e. ZZ -> ( ( denom ` A ) = 1 <-> A e. ZZ ) )
18 17 ibir 
 |-  ( A e. ZZ -> ( denom ` A ) = 1 )
19 18 3ad2ant1 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( denom ` A ) = 1 )
20 14 19 eqtrd 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( denom ` ( ( A ^c ( 1 / N ) ) ^ N ) ) = 1 )
21 simp3 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( A ^c ( 1 / N ) ) e. QQ )
22 6 nnnn0d 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> N e. NN0 )
23 denexp 
 |-  ( ( ( A ^c ( 1 / N ) ) e. QQ /\ N e. NN0 ) -> ( denom ` ( ( A ^c ( 1 / N ) ) ^ N ) ) = ( ( denom ` ( A ^c ( 1 / N ) ) ) ^ N ) )
24 21 22 23 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( denom ` ( ( A ^c ( 1 / N ) ) ^ N ) ) = ( ( denom ` ( A ^c ( 1 / N ) ) ) ^ N ) )
25 9 20 24 3eqtr2rd 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( ( denom ` ( A ^c ( 1 / N ) ) ) ^ N ) = ( 1 ^ N ) )
26 3 5 6 25 exp11nnd 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( denom ` ( A ^c ( 1 / N ) ) ) = 1 )
27 qden1elz 
 |-  ( ( A ^c ( 1 / N ) ) e. QQ -> ( ( denom ` ( A ^c ( 1 / N ) ) ) = 1 <-> ( A ^c ( 1 / N ) ) e. ZZ ) )
28 27 3ad2ant3 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( ( denom ` ( A ^c ( 1 / N ) ) ) = 1 <-> ( A ^c ( 1 / N ) ) e. ZZ ) )
29 26 28 mpbid 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. QQ ) -> ( A ^c ( 1 / N ) ) e. ZZ )