Theorem prmz 12252

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 12251	. 2 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2	1	nnzd 9441	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2164  ℤcz 9320  ℙcprime 12248

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-addcom 7974  ax-addass 7976  ax-distr 7978  ax-i2m1 7979  ax-0lt1 7980  ax-0id 7982  ax-rnegex 7983  ax-cnre 7985  ax-pre-ltirr 7986  ax-pre-ltwlin 7987  ax-pre-lttrn 7988  ax-pre-ltadd 7990

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-int 3872  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263  df-riota 5874  df-ov 5922  df-oprab 5923  df-mpo 5924  df-pnf 8058  df-mnf 8059  df-xr 8060  df-ltxr 8061  df-le 8062  df-sub 8194  df-neg 8195  df-inn 8985  df-n0 9244  df-z 9321  df-prm 12249

This theorem is referenced by:  dvdsprime  12263  prm2orodd  12267  oddprmge3  12276  exprmfct  12279  prmdvdsfz  12280  isprm5lem  12282  isprm5  12283  coprm  12285  prmrp  12286  euclemma  12287  prmdvdsexpb  12290  prmexpb  12292  prmfac1  12293  rpexp  12294  prmndvdsfaclt  12297  cncongrprm  12298  phiprmpw  12363  phiprm  12364  fermltl  12375  prmdiv  12376  prmdiveq  12377  vfermltl  12392  reumodprminv  12394  modprm0  12395  oddprm  12400  prm23lt5  12404  prm23ge5  12405  pcneg  12466  pcprmpw2  12474  pcprmpw  12475  difsqpwdvds  12479  pcmpt  12484  pcmptdvds  12486  pcprod  12487  prmpwdvds  12496  prmunb  12503  1arithlem4  12507  1arith  12508  4sqlem11  12542  4sqlem12  12543  4sqlem13m  12544  4sqlem14  12545  4sqlem17  12548  4sqlem19  12550  wilthlem1  15153  lgslem1  15157  lgsval2lem  15167  lgsvalmod  15176  lgsmod  15183  lgsdirprm  15191  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  lgsprme0  15199  gausslemma2dlem1a  15215  gausslemma2dlem1cl  15216  gausslemma2dlem1f1o  15217  gausslemma2dlem4  15221  gausslemma2dlem5a  15222  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem2  15239  m1lgs  15242  2lgslem1a  15245  2lgslem1  15248  2lgslem2  15249  2lgs  15261  2lgsoddprm  15270  2sqlem3  15274  2sqlem4  15275  2sqlem6  15277  2sqlem8  15280