Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  expnprm Structured version   Unicode version

Theorem expnprm 14801
 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.)
Assertion
Ref Expression
expnprm

Proof of Theorem expnprm
StepHypRef Expression
1 eluz2b3 11232 . . . 4
21simprbi 465 . . 3
4 eluzelz 11168 . . . . . . . 8
54ad2antlr 731 . . . . . . 7
6 simpr 462 . . . . . . . 8
7 simpll 758 . . . . . . . 8
8 prmnn 14587 . . . . . . . . . . . 12
98adantl 467 . . . . . . . . . . 11
109nnne0d 10654 . . . . . . . . . 10
11 eluz2nn 11197 . . . . . . . . . . . 12
1211ad2antlr 731 . . . . . . . . . . 11
13120expd 12429 . . . . . . . . . 10
1410, 13neeqtrrd 2731 . . . . . . . . 9
15 oveq1 6312 . . . . . . . . . 10
1615necon3i 2671 . . . . . . . . 9
1714, 16syl 17 . . . . . . . 8
18 pcqcl 14760 . . . . . . . 8
196, 7, 17, 18syl12anc 1262 . . . . . . 7
20 dvdsmul1 14302 . . . . . . 7
215, 19, 20syl2anc 665 . . . . . 6
229nncnd 10625 . . . . . . . . 9
2322exp1d 12408 . . . . . . . 8
2423oveq2d 6321 . . . . . . 7
25 1z 10967 . . . . . . . 8
26 pcid 14776 . . . . . . . 8
276, 25, 26sylancl 666 . . . . . . 7
28 pcexp 14763 . . . . . . . 8
296, 7, 17, 5, 28syl121anc 1269 . . . . . . 7
3024, 27, 293eqtr3rd 2479 . . . . . 6
3121, 30breqtrd 4450 . . . . 5
3231ex 435 . . . 4
3311adantl 467 . . . . . 6
3433nnnn0d 10925 . . . . 5
35 dvds1 14331 . . . . 5
3634, 35syl 17 . . . 4
3732, 36sylibd 217 . . 3