Theorem 3z 12647

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 12342	. 2 ⊢ 3 ∈ ℕ
2	1	nnzi 12638	1 ⊢ 3 ∈ ℤ

Syntax hints:   ∈ wcel 2105  3c3 12319  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-z 12611

This theorem is referenced by:  eluz4eluz3  12923  5eluz3  12924  fz0to4untppr  13666  fz0to5un2tp  13667  4fvwrd4  13684  fzo13pr  13784  fzo0to3tp  13787  expnass  14243  ef01bndlem  16216  sin01bnd  16217  sin01gt0  16222  3dvds  16364  3dvdsdec  16365  3dvds2dec  16366  n2dvds3  16404  3lcm2e6woprm  16648  lcmf2a3a4e12  16680  3prm  16727  oddprmge3  16733  ge2nprmge4  16734  2logb9irr  26852  2irrexpqALT  26857  dcubic1lem  26900  dcubic2  26901  dcubic  26903  cubic2  26905  cubic  26906  quart  26918  ppiublem1  27260  ppiublem2  27261  ppiub  27262  chtub  27270  bposlem4  27345  bposlem5  27346  bposlem6  27347  bposlem8  27349  lgsdir2lem5  27387  2lgsoddprmlem3  27472  dchrvmasumiflem1  27559  mulog2sumlem2  27593  pntlemo  27665  pntlem3  27667  pntleml  27669  istrkg3ld  28483  axlowdimlem7  28977  axlowdimlem16  28986  axlowdimlem17  28987  usgrexmplef  29290  wlk2v2e  30185  ex-bc  30480  ex-dvds  30484  ex-gcd  30485  ex-ind-dvds  30489  cyc3conja  33159  evl1deg3  33582  2sqr3minply  33752  prodfzo03  34596  hgt750lemd  34641  lcm3un  41996  3lexlogpow2ineq1  42039  aks4d1p1p7  42055  aks4d1p1  42057  2np3bcnp1  42125  3cubeslem4  42676  jm2.23  42984  jm2.20nn  42985  inductionexd  44144  lhe4.4ex1a  44324  wallispilem4  46023  smfmullem2  46747  smfmullem4  46749  m1modnep2mod  47291  minusmodnep2tmod  47292  fmtnoge3  47454  fmtnoprmfac2lem1  47490  31prm  47521  lighneallem4b  47533  41prothprmlem2  47542  41prothprm  47543  6even  47635  2exp340mod341  47657  4fppr1  47659  9fppr8  47661  nfermltl8rev  47666  nfermltl2rev  47667  sbgoldbalt  47705  sbgoldbo  47711  nnsum3primesle9  47718  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  gpg5grlic  47974  linevalexample  48240  zlmodzxzequa  48341  zlmodzxznm  48342  zlmodzxzequap  48344  zlmodzxzldeplem3  48347  zlmodzxzldep  48349  ldepsnlinclem2  48351  ldepsnlinc  48353