Theorem 3z 12566

Description: 3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
3z	⊢ 3 ∈ ℤ

Proof of Theorem 3z

Step	Hyp	Ref	Expression
1		3nn 12265	. 2 ⊢ 3 ∈ ℕ
2	1	nnzi 12557	1 ⊢ 3 ∈ ℤ

Syntax hints:   ∈ wcel 2109  3c3 12242  ℤcz 12529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-neg 11408  df-nn 12187  df-2 12249  df-3 12250  df-z 12530

This theorem is referenced by:  5eluz3  12842  uzuzle34  12845  fz0to4untppr  13591  fz0to5un2tp  13592  4fvwrd4  13609  fzo13pr  13710  fzo0to3tp  13713  expnass  14173  ef01bndlem  16152  sin01bnd  16153  sin01gt0  16158  3dvds  16301  3dvdsdec  16302  3dvds2dec  16303  n2dvds3  16341  3lcm2e6woprm  16585  lcmf2a3a4e12  16617  3prm  16664  oddprmge3  16670  ge2nprmge4  16671  2logb9irr  26705  2irrexpqALT  26710  dcubic1lem  26753  dcubic2  26754  dcubic  26756  cubic2  26758  cubic  26759  quart  26771  ppiublem1  27113  ppiublem2  27114  ppiub  27115  chtub  27123  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem8  27202  lgsdir2lem5  27240  2lgsoddprmlem3  27325  dchrvmasumiflem1  27412  mulog2sumlem2  27446  pntlemo  27518  pntlem3  27520  pntleml  27522  istrkg3ld  28388  axlowdimlem7  28875  axlowdimlem16  28884  axlowdimlem17  28885  usgrexmplef  29186  wlk2v2e  30086  ex-bc  30381  ex-dvds  30385  ex-gcd  30386  ex-ind-dvds  30390  cyc3conja  33114  evl1deg3  33547  2sqr3minply  33770  2sqr3nconstr  33771  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem5  33776  cos9thpinconstrlem2  33780  prodfzo03  34594  hgt750lemd  34639  lcm3un  42003  3lexlogpow2ineq1  42046  aks4d1p1p7  42062  aks4d1p1  42064  2np3bcnp1  42132  3cubeslem4  42677  jm2.23  42985  jm2.20nn  42986  inductionexd  44144  lhe4.4ex1a  44318  wallispilem4  46066  smfmullem2  46790  smfmullem4  46792  m1modnep2mod  47353  minusmodnep2tmod  47354  fmtnoge3  47531  fmtnoprmfac2lem1  47567  31prm  47598  lighneallem4b  47610  41prothprmlem2  47619  41prothprm  47620  6even  47712  2exp340mod341  47734  4fppr1  47736  9fppr8  47738  nfermltl8rev  47743  nfermltl2rev  47744  sbgoldbalt  47782  sbgoldbo  47788  nnsum3primesle9  47795  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  gpg3kgrtriexlem3  48076  gpg3kgrtriexlem5  48078  gpg3kgrtriexlem6  48079  gpg5grlic  48084  linevalexample  48384  zlmodzxzequa  48485  zlmodzxznm  48486  zlmodzxzequap  48488  zlmodzxzldeplem3  48491  zlmodzxzldep  48493  ldepsnlinclem2  48495  ldepsnlinc  48497