Theorem prmz 12599

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	⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)

Proof of Theorem prmz

Step	Hyp	Ref	Expression
1		prmnn 12598	. 2 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2	1	nnzd 9536	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2180  ℤcz 9414  ℙcprime 12595

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-setind 4606  ax-cnex 8058  ax-resscn 8059  ax-1cn 8060  ax-1re 8061  ax-icn 8062  ax-addcl 8063  ax-addrcl 8064  ax-mulcl 8065  ax-addcom 8067  ax-addass 8069  ax-distr 8071  ax-i2m1 8072  ax-0lt1 8073  ax-0id 8075  ax-rnegex 8076  ax-cnre 8078  ax-pre-ltirr 8079  ax-pre-ltwlin 8080  ax-pre-lttrn 8081  ax-pre-ltadd 8083

This theorem depends on definitions:  df-bi 117  df-3or 984  df-3an 985  df-tru 1378  df-fal 1381  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-nel 2476  df-ral 2493  df-rex 2494  df-reu 2495  df-rab 2497  df-v 2781  df-sbc 3009  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-int 3903  df-br 4063  df-opab 4125  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-iota 5254  df-fun 5296  df-fv 5302  df-riota 5927  df-ov 5977  df-oprab 5978  df-mpo 5979  df-pnf 8151  df-mnf 8152  df-xr 8153  df-ltxr 8154  df-le 8155  df-sub 8287  df-neg 8288  df-inn 9079  df-n0 9338  df-z 9415  df-prm 12596

This theorem is referenced by:  dvdsprime  12610  prm2orodd  12614  oddprmge3  12623  exprmfct  12626  prmdvdsfz  12627  isprm5lem  12629  isprm5  12630  coprm  12632  prmrp  12633  euclemma  12634  prmdvdsexpb  12637  prmexpb  12639  prmfac1  12640  rpexp  12641  prmndvdsfaclt  12644  cncongrprm  12645  phiprmpw  12710  phiprm  12711  fermltl  12722  prmdiv  12723  prmdiveq  12724  vfermltl  12740  reumodprminv  12742  modprm0  12743  oddprm  12748  prm23lt5  12752  prm23ge5  12753  pcneg  12814  pcprmpw2  12822  pcprmpw  12823  difsqpwdvds  12827  pcmpt  12832  pcmptdvds  12834  pcprod  12835  prmpwdvds  12844  prmunb  12851  1arithlem4  12855  1arith  12856  4sqlem11  12890  4sqlem12  12891  4sqlem13m  12892  4sqlem14  12893  4sqlem17  12896  4sqlem19  12898  wilthlem1  15619  dvdsppwf1o  15628  perfect1  15637  lgslem1  15644  lgsval2lem  15654  lgsvalmod  15663  lgsmod  15670  lgsdirprm  15678  lgsdir  15679  lgsdilem2  15680  lgsdi  15681  lgsne0  15682  lgsprme0  15686  gausslemma2dlem1a  15702  gausslemma2dlem1cl  15703  gausslemma2dlem1f1o  15704  gausslemma2dlem4  15708  gausslemma2dlem5a  15709  lgseisenlem1  15714  lgseisenlem2  15715  lgseisenlem3  15716  lgseisenlem4  15717  lgseisen  15718  lgsquadlem2  15722  lgsquadlem3  15723  lgsquad2lem2  15726  m1lgs  15729  2lgslem1a  15732  2lgslem1  15735  2lgslem2  15736  2lgs  15748  2lgsoddprm  15757  2sqlem3  15761  2sqlem4  15762  2sqlem6  15764  2sqlem8  15767