Theorem prmz 12688

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 12687	. 2 |- ( P e. Prime -> P e. NN )
2	1	nnzd 9601	1 |- ( P e. Prime -> P e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2202   ZZcz 9479   Primecprime 12684

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-n0 9403  df-z 9480  df-prm 12685

This theorem is referenced by:  dvdsprime  12699  prm2orodd  12703  oddprmge3  12712  exprmfct  12715  prmdvdsfz  12716  isprm5lem  12718  isprm5  12719  coprm  12721  prmrp  12722  euclemma  12723  prmdvdsexpb  12726  prmexpb  12728  prmfac1  12729  rpexp  12730  prmndvdsfaclt  12733  cncongrprm  12734  phiprmpw  12799  phiprm  12800  fermltl  12811  prmdiv  12812  prmdiveq  12813  vfermltl  12829  reumodprminv  12831  modprm0  12832  oddprm  12837  prm23lt5  12841  prm23ge5  12842  pcneg  12903  pcprmpw2  12911  pcprmpw  12912  difsqpwdvds  12916  pcmpt  12921  pcmptdvds  12923  pcprod  12924  prmpwdvds  12933  prmunb  12940  1arithlem4  12944  1arith  12945  4sqlem11  12979  4sqlem12  12980  4sqlem13m  12981  4sqlem14  12982  4sqlem17  12985  4sqlem19  12987  wilthlem1  15710  dvdsppwf1o  15719  perfect1  15728  lgslem1  15735  lgsval2lem  15745  lgsvalmod  15754  lgsmod  15761  lgsdirprm  15769  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  lgsprme0  15777  gausslemma2dlem1a  15793  gausslemma2dlem1cl  15794  gausslemma2dlem1f1o  15795  gausslemma2dlem4  15799  gausslemma2dlem5a  15800  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgseisenlem4  15808  lgseisen  15809  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2lem2  15817  m1lgs  15820  2lgslem1a  15823  2lgslem1  15826  2lgslem2  15827  2lgs  15839  2lgsoddprm  15848  2sqlem3  15852  2sqlem4  15853  2sqlem6  15855  2sqlem8  15858