Theorem prmz 12816

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℤcz 9582  ℙcprime 12812

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-setind 4661  ax-cnex 8223  ax-resscn 8224  ax-1cn 8225  ax-1re 8226  ax-icn 8227  ax-addcl 8228  ax-addrcl 8229  ax-mulcl 8230  ax-addcom 8232  ax-addass 8234  ax-distr 8236  ax-i2m1 8237  ax-0lt1 8238  ax-0id 8240  ax-rnegex 8241  ax-cnre 8243  ax-pre-ltirr 8244  ax-pre-ltwlin 8245  ax-pre-lttrn 8246  ax-pre-ltadd 8248

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3045  df-dif 3215  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-int 3952  df-br 4112  df-opab 4174  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-iota 5314  df-fun 5356  df-fv 5362  df-riota 6005  df-ov 6055  df-oprab 6056  df-mpo 6057  df-pnf 8315  df-mnf 8316  df-xr 8317  df-ltxr 8318  df-le 8319  df-sub 8451  df-neg 8452  df-inn 9243  df-n0 9502  df-z 9583  df-prm 12813

This theorem is referenced by:  dvdsprime  12827  prm2orodd  12831  oddprmge3  12840  exprmfct  12843  prmdvdsfz  12844  isprm5lem  12846  isprm5  12847  coprm  12849  prmrp  12850  euclemma  12851  prmdvdsexpb  12854  prmexpb  12856  prmfac1  12857  rpexp  12858  prmndvdsfaclt  12861  cncongrprm  12862  phiprmpw  12927  phiprm  12928  fermltl  12939  prmdiv  12940  prmdiveq  12941  vfermltl  12957  reumodprminv  12959  modprm0  12960  oddprm  12965  prm23lt5  12969  prm23ge5  12970  pcneg  13031  pcprmpw2  13039  pcprmpw  13040  difsqpwdvds  13044  pcmpt  13049  pcmptdvds  13051  pcprod  13052  prmpwdvds  13061  prmunb  13068  1arithlem4  13072  1arith  13073  4sqlem11  13107  4sqlem12  13108  4sqlem13m  13109  4sqlem14  13110  4sqlem17  13113  4sqlem19  13115  wilthlem1  15897  dvdsppwf1o  15906  perfect1  15915  lgslem1  15922  lgsval2lem  15932  lgsvalmod  15941  lgsmod  15948  lgsdirprm  15956  lgsdir  15957  lgsdilem2  15958  lgsdi  15959  lgsne0  15960  lgsprme0  15964  gausslemma2dlem1a  15980  gausslemma2dlem1cl  15981  gausslemma2dlem1f1o  15982  gausslemma2dlem4  15986  gausslemma2dlem5a  15987  lgseisenlem1  15992  lgseisenlem2  15993  lgseisenlem3  15994  lgseisenlem4  15995  lgseisen  15996  lgsquadlem2  16000  lgsquadlem3  16001  lgsquad2lem2  16004  m1lgs  16007  2lgslem1a  16010  2lgslem1  16013  2lgslem2  16014  2lgs  16026  2lgsoddprm  16035  2sqlem3  16039  2sqlem4  16040  2sqlem6  16042  2sqlem8  16045