Metamath Proof Explorer

Theorem expnprm

Description: A second or higher power of a rational number is not a prime number. Or by contraposition, the n-th root of a prime number is irrational. Suggested by Norm Megill. (Contributed by Mario Carneiro, 10-Aug-2015)

Ref Expression
Assertion expnprm 
|- ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> -. ( A ^ N ) e. Prime )

Proof

Step Hyp Ref Expression
1 eluz2b3 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ N =/= 1 ) )
2 1 simprbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> N =/= 1 )
3 2 adantl 
 |-  ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> N =/= 1 )
4 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
5 4 ad2antlr 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> N e. ZZ )
6 simpr 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( A ^ N ) e. Prime )
7 simpll 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> A e. QQ )
8 prmnn 
 |-  ( ( A ^ N ) e. Prime -> ( A ^ N ) e. NN )
9 8 adantl 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( A ^ N ) e. NN )
10 9 nnne0d 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( A ^ N ) =/= 0 )
11 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
12 11 ad2antlr 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> N e. NN )
13 12 0expd 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( 0 ^ N ) = 0 )
14 10 13 neeqtrrd 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( A ^ N ) =/= ( 0 ^ N ) )
15 oveq1 
 |-  ( A = 0 -> ( A ^ N ) = ( 0 ^ N ) )
16 15 necon3i 
 |-  ( ( A ^ N ) =/= ( 0 ^ N ) -> A =/= 0 )
17 14 16 syl 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> A =/= 0 )
18 pcqcl 
 |-  ( ( ( A ^ N ) e. Prime /\ ( A e. QQ /\ A =/= 0 ) ) -> ( ( A ^ N ) pCnt A ) e. ZZ )
19 6 7 17 18 syl12anc 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( ( A ^ N ) pCnt A ) e. ZZ )
20 dvdsmul1 
 |-  ( ( N e. ZZ /\ ( ( A ^ N ) pCnt A ) e. ZZ ) -> N || ( N x. ( ( A ^ N ) pCnt A ) ) )
21 5 19 20 syl2anc 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> N || ( N x. ( ( A ^ N ) pCnt A ) ) )
22 9 nncnd 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( A ^ N ) e. CC )
23 22 exp1d 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( ( A ^ N ) ^ 1 ) = ( A ^ N ) )
24 23 oveq2d 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( ( A ^ N ) pCnt ( ( A ^ N ) ^ 1 ) ) = ( ( A ^ N ) pCnt ( A ^ N ) ) )
25 1z 
 |-  1 e. ZZ
26 pcid 
 |-  ( ( ( A ^ N ) e. Prime /\ 1 e. ZZ ) -> ( ( A ^ N ) pCnt ( ( A ^ N ) ^ 1 ) ) = 1 )
27 6 25 26 sylancl 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( ( A ^ N ) pCnt ( ( A ^ N ) ^ 1 ) ) = 1 )
28 pcexp 
 |-  ( ( ( A ^ N ) e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ N e. ZZ ) -> ( ( A ^ N ) pCnt ( A ^ N ) ) = ( N x. ( ( A ^ N ) pCnt A ) ) )
29 6 7 17 5 28 syl121anc 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( ( A ^ N ) pCnt ( A ^ N ) ) = ( N x. ( ( A ^ N ) pCnt A ) ) )
30 24 27 29 3eqtr3rd 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> ( N x. ( ( A ^ N ) pCnt A ) ) = 1 )
31 21 30 breqtrd 
 |-  ( ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) /\ ( A ^ N ) e. Prime ) -> N || 1 )
32 31 ex 
 |-  ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( A ^ N ) e. Prime -> N || 1 ) )
33 11 adantl 
 |-  ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> N e. NN )
34 33 nnnn0d 
 |-  ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> N e. NN0 )
35 dvds1 
 |-  ( N e. NN0 -> ( N || 1 <-> N = 1 ) )
36 34 35 syl 
 |-  ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> ( N || 1 <-> N = 1 ) )
37 32 36 sylibd 
 |-  ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( A ^ N ) e. Prime -> N = 1 ) )
38 37 necon3ad 
 |-  ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> ( N =/= 1 -> -. ( A ^ N ) e. Prime ) )
39 3 38 mpd 
 |-  ( ( A e. QQ /\ N e. ( ZZ>= ` 2 ) ) -> -. ( A ^ N ) e. Prime )