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

Theorem pcmptcl 13262
 Description: Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014.)
Hypotheses
Ref Expression
pcmpt.1
pcmpt.2
Assertion
Ref Expression
pcmptcl

Proof of Theorem pcmptcl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pcmpt.2 . . . 4
2 pm2.27 38 . . . . . . . 8
3 iftrue 3747 . . . . . . . . . . 11
43adantr 453 . . . . . . . . . 10
5 prmnn 13084 . . . . . . . . . . 11
6 nnexpcl 11396 . . . . . . . . . . 11
75, 6sylan 459 . . . . . . . . . 10
84, 7eqeltrd 2512 . . . . . . . . 9
98ex 425 . . . . . . . 8
102, 9syld 43 . . . . . . 7
11 iffalse 3748 . . . . . . . . 9
12 1nn 10013 . . . . . . . . 9
1311, 12syl6eqel 2526 . . . . . . . 8
1413a1d 24 . . . . . . 7
1510, 14pm2.61i 159 . . . . . 6
1615a1d 24 . . . . 5
1716ralimi2 2780 . . . 4
181, 17syl 16 . . 3
19 pcmpt.1 . . . 4
2019fmpt 5892 . . 3
2118, 20sylib 190 . 2
22 nnuz 10523 . . 3
23 1z 10313 . . . 4
2423a1i 11 . . 3
2521ffvelrnda 5872 . . 3
26 nnmulcl 10025 . . . 4