Theorem prmz 12685

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℤcz 9479  ℙcprime 12681

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 12682

This theorem is referenced by:  dvdsprime  12696  prm2orodd  12700  oddprmge3  12709  exprmfct  12712  prmdvdsfz  12713  isprm5lem  12715  isprm5  12716  coprm  12718  prmrp  12719  euclemma  12720  prmdvdsexpb  12723  prmexpb  12725  prmfac1  12726  rpexp  12727  prmndvdsfaclt  12730  cncongrprm  12731  phiprmpw  12796  phiprm  12797  fermltl  12808  prmdiv  12809  prmdiveq  12810  vfermltl  12826  reumodprminv  12828  modprm0  12829  oddprm  12834  prm23lt5  12838  prm23ge5  12839  pcneg  12900  pcprmpw2  12908  pcprmpw  12909  difsqpwdvds  12913  pcmpt  12918  pcmptdvds  12920  pcprod  12921  prmpwdvds  12930  prmunb  12937  1arithlem4  12941  1arith  12942  4sqlem11  12976  4sqlem12  12977  4sqlem13m  12978  4sqlem14  12979  4sqlem17  12982  4sqlem19  12984  wilthlem1  15707  dvdsppwf1o  15716  perfect1  15725  lgslem1  15732  lgsval2lem  15742  lgsvalmod  15751  lgsmod  15758  lgsdirprm  15766  lgsdir  15767  lgsdilem2  15768  lgsdi  15769  lgsne0  15770  lgsprme0  15774  gausslemma2dlem1a  15790  gausslemma2dlem1cl  15791  gausslemma2dlem1f1o  15792  gausslemma2dlem4  15796  gausslemma2dlem5a  15797  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem3  15804  lgseisenlem4  15805  lgseisen  15806  lgsquadlem2  15810  lgsquadlem3  15811  lgsquad2lem2  15814  m1lgs  15817  2lgslem1a  15820  2lgslem1  15823  2lgslem2  15824  2lgs  15836  2lgsoddprm  15845  2sqlem3  15849  2sqlem4  15850  2sqlem6  15852  2sqlem8  15855