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

Theorem expnprm 13264
 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 10542 . . . 4
21simprbi 451 . . 3
4 eluzelz 10489 . . . . . . . 8
54ad2antlr 708 . . . . . . 7
6 simpr 448 . . . . . . . 8
7 simpll 731 . . . . . . . 8
8 prmnn 13075 . . . . . . . . . . . 12
98adantl 453 . . . . . . . . . . 11
109nnne0d 10037 . . . . . . . . . 10
111simplbi 447 . . . . . . . . . . . 12
1211ad2antlr 708 . . . . . . . . . . 11
13120expd 11532 . . . . . . . . . 10
1410, 13neeqtrrd 2623 . . . . . . . . 9
15 oveq1 6081 . . . . . . . . . 10
1615necon3i 2638 . . . . . . . . 9
1714, 16syl 16 . . . . . . . 8
18 pcqcl 13223 . . . . . . . 8
196, 7, 17, 18syl12anc 1182 . . . . . . 7
20 dvdsmul1 12864 . . . . . . 7
215, 19, 20syl2anc 643 . . . . . 6
229nncnd 10009 . . . . . . . . 9
2322exp1d 11511 . . . . . . . 8
2423oveq2d 6090 . . . . . . 7
25 1z 10304 . . . . . . . 8
26 pcid 13239 . . . . . . . 8
276, 25, 26sylancl 644 . . . . . . 7
28 pcexp 13226 . . . . . . . 8
296, 7, 17, 5, 28syl121anc 1189 . . . . . . 7
3024, 27, 293eqtr3rd 2477 . . . . . 6
3121, 30breqtrd 4229 . . . . 5
3231ex 424 . . . 4
3311adantl 453 . . . . . 6
3433nnnn0d 10267 . . . . 5
35 dvds1 12891 . . . . 5
3634, 35syl 16 . . . 4
3732, 36sylibd 206 . . 3