Theorem prmz 12676

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℤcz 9472  ℙcprime 12672

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8116  ax-resscn 8117  ax-1cn 8118  ax-1re 8119  ax-icn 8120  ax-addcl 8121  ax-addrcl 8122  ax-mulcl 8123  ax-addcom 8125  ax-addass 8127  ax-distr 8129  ax-i2m1 8130  ax-0lt1 8131  ax-0id 8133  ax-rnegex 8134  ax-cnre 8136  ax-pre-ltirr 8137  ax-pre-ltwlin 8138  ax-pre-lttrn 8139  ax-pre-ltadd 8141

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-pnf 8209  df-mnf 8210  df-xr 8211  df-ltxr 8212  df-le 8213  df-sub 8345  df-neg 8346  df-inn 9137  df-n0 9396  df-z 9473  df-prm 12673

This theorem is referenced by:  dvdsprime  12687  prm2orodd  12691  oddprmge3  12700  exprmfct  12703  prmdvdsfz  12704  isprm5lem  12706  isprm5  12707  coprm  12709  prmrp  12710  euclemma  12711  prmdvdsexpb  12714  prmexpb  12716  prmfac1  12717  rpexp  12718  prmndvdsfaclt  12721  cncongrprm  12722  phiprmpw  12787  phiprm  12788  fermltl  12799  prmdiv  12800  prmdiveq  12801  vfermltl  12817  reumodprminv  12819  modprm0  12820  oddprm  12825  prm23lt5  12829  prm23ge5  12830  pcneg  12891  pcprmpw2  12899  pcprmpw  12900  difsqpwdvds  12904  pcmpt  12909  pcmptdvds  12911  pcprod  12912  prmpwdvds  12921  prmunb  12928  1arithlem4  12932  1arith  12933  4sqlem11  12967  4sqlem12  12968  4sqlem13m  12969  4sqlem14  12970  4sqlem17  12973  4sqlem19  12975  wilthlem1  15697  dvdsppwf1o  15706  perfect1  15715  lgslem1  15722  lgsval2lem  15732  lgsvalmod  15741  lgsmod  15748  lgsdirprm  15756  lgsdir  15757  lgsdilem2  15758  lgsdi  15759  lgsne0  15760  lgsprme0  15764  gausslemma2dlem1a  15780  gausslemma2dlem1cl  15781  gausslemma2dlem1f1o  15782  gausslemma2dlem4  15786  gausslemma2dlem5a  15787  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem3  15794  lgseisenlem4  15795  lgseisen  15796  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad2lem2  15804  m1lgs  15807  2lgslem1a  15810  2lgslem1  15813  2lgslem2  15814  2lgs  15826  2lgsoddprm  15835  2sqlem3  15839  2sqlem4  15840  2sqlem6  15842  2sqlem8  15845