Theorem 3z 12638

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

This proof depends on syntax axioms:   ∈ wcel 2146  3c3 12307  ℤcz 12602

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7738  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-i2m1 11179  ax-1ne0 11180  ax-rrecex 11183  ax-cnre 11184

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-neg 11455  df-nn 12245  df-2 12314  df-3 12315  df-z 12603

This theorem is used by:  5eluz3  12919  uzuzle34  12922  fz0to4untppr  13671  fz0to5un2tp  13672  4fvwrd4  13689  fzo13pr  13791  fzo0to3tp  13794  expnass  14258  ef01bndlem  16258  sin01bnd  16259  sin01gt0  16264  3dvds  16407  3dvdsdec  16408  3dvds2dec  16409  n2dvds3  16447  3lcm2e6woprm  16691  lcmf2a3a4e12  16723  3prm  16770  oddprmge3  16777  ge2nprmge4  16778  2logb9irr  26991  2irrexpqALT  26996  dcubic1lem  27039  dcubic2  27040  dcubic  27042  cubic2  27044  cubic  27045  quart  27057  ppiublem1  27397  ppiublem2  27398  ppiub  27399  chtub  27407  bposlem4  27482  bposlem5  27483  bposlem6  27484  bposlem8  27486  lgsdir2lem5  27524  2lgsoddprmlem3  27609  dchrvmasumiflem1  27696  mulog2sumlem2  27730  pntlemo  27802  pntlem3  27804  pntleml  27806  istrkg3ld  28761  axlowdimlem7  29329  axlowdimlem16  29338  axlowdimlem17  29339  usgrexmplef  29643  wlk2v2e  30555  ex-bc  30850  ex-dvds  30854  ex-gcd  30855  ex-ind-dvds  30859  cyc3conja  33517  evl1deg3  33908  2sqr3minply  34210  2sqr3nconstr  34211  cos9thpiminplylem1  34212  cos9thpiminplylem2  34213  cos9thpiminplylem5  34216  cos9thpinconstrlem2  34220  prodfzo03  35031  hgt750lemd  35076  lcm3un  42815  3lexlogpow2ineq1  42858  aks4d1p1p7  42874  aks4d1p1  42876  2np3bcnp1  42944  3cubeslem4  43453  jm2.23  43756  jm2.20nn  43757  inductionexd  44914  lhe4.4ex1a  45072  wallispilem4  46815  smfmullem2  47539  smfmullem4  47541  goldratmolem2  47656  m1modnep2mod  48128  minusmodnep2tmod  48129  fmtnoge3  48315  fmtnoprmfac2lem1  48351  31prm  48382  lighneallem4b  48394  41prothprmlem2  48403  41prothprm  48404  nprmdvdsfacm1lem3  48407  nprmdvdsfacm1lem4  48408  6even  48509  2exp340mod341  48531  4fppr1  48533  9fppr8  48535  nfermltl8rev  48540  nfermltl2rev  48541  sbgoldbalt  48579  sbgoldbo  48585  nnsum3primesle9  48592  nnsum4primesodd  48594  nnsum4primesoddALTV  48595  nnsum4primeseven  48598  nnsum4primesevenALTV  48599  gpg3kgrtriexlem3  48883  gpg3kgrtriexlem5  48885  gpg3kgrtriexlem6  48886  gpg5grlim  48891  gpg5grlic  48892  linevalexample  49208  zlmodzxzequa  49309  zlmodzxznm  49310  zlmodzxzequap  49312  zlmodzxzldeplem3  49315  zlmodzxzldep  49317  ldepsnlinclem2  49319  ldepsnlinc  49321  1elfz13  50658  2elfz13  50659  crosspdotsumi  50679