Metamath Proof Explorer

Theorem qexpz

Description: If a power of a rational number is an integer, then the number is an integer. In other words, all n-th roots are irrational unless they are integers (so that the original number is an n-th power). (Contributed by Mario Carneiro, 10-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( A = 0 -> ( A e. ZZ <-> 0 e. ZZ ) )
2 simpll2 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> N e. NN )
3 2 nncnd 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> N e. CC )
4 3 mul01d 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> ( N x. 0 ) = 0 )
5 simpr 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> p e. Prime )
6 simpll3 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> ( A ^ N ) e. ZZ )
7 simpll1 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> A e. QQ )
8 qcn 
 |-  ( A e. QQ -> A e. CC )
9 7 8 syl 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> A e. CC )
10 simplr 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> A =/= 0 )
11 2 nnzd 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> N e. ZZ )
12 9 10 11 expne0d 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> ( A ^ N ) =/= 0 )
13 pczcl 
 |-  ( ( p e. Prime /\ ( ( A ^ N ) e. ZZ /\ ( A ^ N ) =/= 0 ) ) -> ( p pCnt ( A ^ N ) ) e. NN0 )
14 5 6 12 13 syl12anc 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> ( p pCnt ( A ^ N ) ) e. NN0 )
15 14 nn0ge0d 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> 0 <_ ( p pCnt ( A ^ N ) ) )
16 pcexp 
 |-  ( ( p e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ N e. ZZ ) -> ( p pCnt ( A ^ N ) ) = ( N x. ( p pCnt A ) ) )
17 5 7 10 11 16 syl121anc 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> ( p pCnt ( A ^ N ) ) = ( N x. ( p pCnt A ) ) )
18 15 17 breqtrd 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> 0 <_ ( N x. ( p pCnt A ) ) )
19 4 18 eqbrtrd 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> ( N x. 0 ) <_ ( N x. ( p pCnt A ) ) )
20 0red 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> 0 e. RR )
21 pcqcl 
 |-  ( ( p e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( p pCnt A ) e. ZZ )
22 5 7 10 21 syl12anc 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> ( p pCnt A ) e. ZZ )
23 22 zred 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> ( p pCnt A ) e. RR )
24 2 nnred 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> N e. RR )
25 2 nngt0d 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> 0 < N )
26 lemul2 
 |-  ( ( 0 e. RR /\ ( p pCnt A ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( 0 <_ ( p pCnt A ) <-> ( N x. 0 ) <_ ( N x. ( p pCnt A ) ) ) )
27 20 23 24 25 26 syl112anc 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> ( 0 <_ ( p pCnt A ) <-> ( N x. 0 ) <_ ( N x. ( p pCnt A ) ) ) )
28 19 27 mpbird 
 |-  ( ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> 0 <_ ( p pCnt A ) )
29 28 ralrimiva 
 |-  ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) -> A. p e. Prime 0 <_ ( p pCnt A ) )
30 simpl1 
 |-  ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) -> A e. QQ )
31 pcz 
 |-  ( A e. QQ -> ( A e. ZZ <-> A. p e. Prime 0 <_ ( p pCnt A ) ) )
32 30 31 syl 
 |-  ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) -> ( A e. ZZ <-> A. p e. Prime 0 <_ ( p pCnt A ) ) )
33 29 32 mpbird 
 |-  ( ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) /\ A =/= 0 ) -> A e. ZZ )
34 0zd 
 |-  ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) -> 0 e. ZZ )
35 1 33 34 pm2.61ne 
 |-  ( ( A e. QQ /\ N e. NN /\ ( A ^ N ) e. ZZ ) -> A e. ZZ )