Theorem prmz 12619

Description: A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.)

Assertion

Ref	Expression
prmz	|- ( P e. Prime -> P e. ZZ )

Proof of Theorem prmz

Step	Hyp	Ref	Expression
1		prmnn 12618	. 2 |- ( P e. Prime -> P e. NN )
2	1	nnzd 9556	1 |- ( P e. Prime -> P e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2200   ZZcz 9434   Primecprime 12615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4521  ax-setind 4626  ax-cnex 8078  ax-resscn 8079  ax-1cn 8080  ax-1re 8081  ax-icn 8082  ax-addcl 8083  ax-addrcl 8084  ax-mulcl 8085  ax-addcom 8087  ax-addass 8089  ax-distr 8091  ax-i2m1 8092  ax-0lt1 8093  ax-0id 8095  ax-rnegex 8096  ax-cnre 8098  ax-pre-ltirr 8099  ax-pre-ltwlin 8100  ax-pre-lttrn 8101  ax-pre-ltadd 8103

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-br 4083  df-opab 4145  df-id 4381  df-xp 4722  df-rel 4723  df-cnv 4724  df-co 4725  df-dm 4726  df-iota 5274  df-fun 5316  df-fv 5322  df-riota 5947  df-ov 5997  df-oprab 5998  df-mpo 5999  df-pnf 8171  df-mnf 8172  df-xr 8173  df-ltxr 8174  df-le 8175  df-sub 8307  df-neg 8308  df-inn 9099  df-n0 9358  df-z 9435  df-prm 12616

This theorem is referenced by:  dvdsprime  12630  prm2orodd  12634  oddprmge3  12643  exprmfct  12646  prmdvdsfz  12647  isprm5lem  12649  isprm5  12650  coprm  12652  prmrp  12653  euclemma  12654  prmdvdsexpb  12657  prmexpb  12659  prmfac1  12660  rpexp  12661  prmndvdsfaclt  12664  cncongrprm  12665  phiprmpw  12730  phiprm  12731  fermltl  12742  prmdiv  12743  prmdiveq  12744  vfermltl  12760  reumodprminv  12762  modprm0  12763  oddprm  12768  prm23lt5  12772  prm23ge5  12773  pcneg  12834  pcprmpw2  12842  pcprmpw  12843  difsqpwdvds  12847  pcmpt  12852  pcmptdvds  12854  pcprod  12855  prmpwdvds  12864  prmunb  12871  1arithlem4  12875  1arith  12876  4sqlem11  12910  4sqlem12  12911  4sqlem13m  12912  4sqlem14  12913  4sqlem17  12916  4sqlem19  12918  wilthlem1  15639  dvdsppwf1o  15648  perfect1  15657  lgslem1  15664  lgsval2lem  15674  lgsvalmod  15683  lgsmod  15690  lgsdirprm  15698  lgsdir  15699  lgsdilem2  15700  lgsdi  15701  lgsne0  15702  lgsprme0  15706  gausslemma2dlem1a  15722  gausslemma2dlem1cl  15723  gausslemma2dlem1f1o  15724  gausslemma2dlem4  15728  gausslemma2dlem5a  15729  lgseisenlem1  15734  lgseisenlem2  15735  lgseisenlem3  15736  lgseisenlem4  15737  lgseisen  15738  lgsquadlem2  15742  lgsquadlem3  15743  lgsquad2lem2  15746  m1lgs  15749  2lgslem1a  15752  2lgslem1  15755  2lgslem2  15756  2lgs  15768  2lgsoddprm  15777  2sqlem3  15781  2sqlem4  15782  2sqlem6  15784  2sqlem8  15787