Theorem 3z 12362

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

Syntax hints:   ∈ wcel 2107  3c3 12038  ℤcz 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-i2m1 10948  ax-1ne0 10949  ax-rrecex 10952  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-neg 11217  df-nn 11983  df-2 12045  df-3 12046  df-z 12329

This theorem is referenced by:  fz0to4untppr  13368  4fvwrd4  13385  fzo13pr  13480  fzo0to3tp  13482  expnass  13933  ef01bndlem  15902  sin01bnd  15903  sin01gt0  15908  3dvds  16049  3dvdsdec  16050  3dvds2dec  16051  n2dvds3  16089  3lcm2e6woprm  16329  lcmf2a3a4e12  16361  3prm  16408  oddprmge3  16414  ge2nprmge4  16415  2logb9irr  25954  2irrexpqALT  25959  dcubic1lem  26002  dcubic2  26003  dcubic  26005  cubic2  26007  cubic  26008  quart  26020  ppiublem1  26359  ppiublem2  26360  ppiub  26361  chtub  26369  bposlem4  26444  bposlem5  26445  bposlem6  26446  bposlem8  26448  lgsdir2lem5  26486  2lgsoddprmlem3  26571  dchrvmasumiflem1  26658  mulog2sumlem2  26692  pntlemo  26764  pntlem3  26766  pntleml  26768  istrkg3ld  26831  axlowdimlem7  27325  axlowdimlem16  27334  axlowdimlem17  27335  usgrexmplef  27635  wlk2v2e  28530  ex-bc  28825  ex-dvds  28829  ex-gcd  28830  ex-ind-dvds  28834  cyc3conja  31433  prodfzo03  32592  hgt750lemd  32637  lcm3un  40030  3lexlogpow2ineq1  40073  aks4d1p1p7  40089  aks4d1p1  40091  2np3bcnp1  40107  3cubeslem4  40518  jm2.23  40825  jm2.20nn  40826  inductionexd  41772  lhe4.4ex1a  41954  wallispilem4  43616  smfmullem2  44337  smfmullem4  44339  fmtnoge3  44993  fmtnoprmfac2lem1  45029  31prm  45060  lighneallem4b  45072  41prothprmlem2  45081  41prothprm  45082  6even  45174  2exp340mod341  45196  4fppr1  45198  9fppr8  45200  nfermltl8rev  45205  nfermltl2rev  45206  sbgoldbalt  45244  sbgoldbo  45250  nnsum3primesle9  45257  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  linevalexample  45747  zlmodzxzequa  45848  zlmodzxznm  45849  zlmodzxzequap  45851  zlmodzxzldeplem3  45854  zlmodzxzldep  45856  ldepsnlinclem2  45858  ldepsnlinc  45860