Theorem 3z 12651

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

This proof depends on syntax axioms:   ∈ wcel 2145  3c3 12320  ℤcz 12615

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-i2m1 11192  ax-1ne0 11193  ax-rrecex 11196  ax-cnre 11197

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-neg 11468  df-nn 12258  df-2 12327  df-3 12328  df-z 12616

This theorem is used by:  5eluz3  12932  uzuzle34  12935  fz0to4untppr  13685  fz0to5un2tp  13686  4fvwrd4  13703  fzo13pr  13805  fzo0to3tp  13808  expnass  14272  ef01bndlem  16272  sin01bnd  16273  sin01gt0  16278  3dvds  16421  3dvdsdec  16422  3dvds2dec  16423  n2dvds3  16461  3lcm2e6woprm  16705  lcmf2a3a4e12  16737  3prm  16784  oddprmge3  16791  ge2nprmge4  16792  2logb9irr  27032  2irrexpqALT  27037  dcubic1lem  27080  dcubic2  27081  dcubic  27083  cubic2  27085  cubic  27086  quart  27098  ppiublem1  27438  ppiublem2  27439  ppiub  27440  chtub  27448  bposlem4  27523  bposlem5  27524  bposlem6  27525  bposlem8  27527  lgsdir2lem5  27565  2lgsoddprmlem3  27650  dchrvmasumiflem1  27737  mulog2sumlem2  27771  pntlemo  27843  pntlem3  27845  pntleml  27847  istrkg3ld  28802  axlowdimlem7  29405  axlowdimlem16  29414  axlowdimlem17  29415  usgrexmplef  29719  wlk2v2e  30637  ex-bc  30932  ex-dvds  30936  ex-gcd  30937  ex-ind-dvds  30941  cyc3conja  33597  evl1deg3  33988  2sqr3minply  34290  2sqr3nconstr  34291  cos9thpiminplylem1  34292  cos9thpiminplylem2  34293  cos9thpiminplylem5  34296  cos9thpinconstrlem2  34300  prodfzo03  35111  hgt750lemd  35156  lcm3un  42881  3lexlogpow2ineq1  42924  aks4d1p1p7  42940  aks4d1p1  42942  2np3bcnp1  43010  3cubeslem4  43534  jm2.23  43837  jm2.20nn  43838  inductionexd  44995  lhe4.4ex1a  45153  wallispilem4  46896  smfmullem2  47620  smfmullem4  47622  goldratmolem2  47751  m1modnep2mod  48246  minusmodnep2tmod  48247  fmtnoge3  48433  fmtnoprmfac2lem1  48469  31prm  48500  lighneallem4b  48512  41prothprmlem2  48521  41prothprm  48522  nprmdvdsfacm1lem3  48525  nprmdvdsfacm1lem4  48526  6even  48627  2exp340mod341  48649  4fppr1  48651  9fppr8  48653  nfermltl8rev  48658  nfermltl2rev  48659  sbgoldbalt  48697  sbgoldbo  48703  nnsum3primesle9  48710  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  gpg3kgrtriexlem3  49001  gpg3kgrtriexlem5  49003  gpg3kgrtriexlem6  49004  gpg5grlim  49009  gpg5grlic  49010  linevalexample  49325  zlmodzxzequa  49426  zlmodzxznm  49427  zlmodzxzequap  49429  zlmodzxzldeplem3  49432  zlmodzxzldep  49434  ldepsnlinclem2  49436  ldepsnlinc  49438  crosspdotsumlem  50797  veronesev3lem  50808