Theorem 3z 12620

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

Syntax hints:   ∈ wcel 2099  3c3 12293  ℤcz 12583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pr 5424  ax-un 7735  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-i2m1 11201  ax-1ne0 11202  ax-rrecex 11205  ax-cnre 11206

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7418  df-om 7866  df-2nd 7989  df-frecs 8281  df-wrecs 8312  df-recs 8386  df-rdg 8425  df-neg 11472  df-nn 12238  df-2 12300  df-3 12301  df-z 12584

This theorem is referenced by:  fz0to4untppr  13631  4fvwrd4  13648  fzo13pr  13743  fzo0to3tp  13745  expnass  14198  ef01bndlem  16155  sin01bnd  16156  sin01gt0  16161  3dvds  16302  3dvdsdec  16303  3dvds2dec  16304  n2dvds3  16342  3lcm2e6woprm  16580  lcmf2a3a4e12  16612  3prm  16659  oddprmge3  16665  ge2nprmge4  16666  2logb9irr  26721  2irrexpqALT  26726  dcubic1lem  26769  dcubic2  26770  dcubic  26772  cubic2  26774  cubic  26775  quart  26787  ppiublem1  27129  ppiublem2  27130  ppiub  27131  chtub  27139  bposlem4  27214  bposlem5  27215  bposlem6  27216  bposlem8  27218  lgsdir2lem5  27256  2lgsoddprmlem3  27341  dchrvmasumiflem1  27428  mulog2sumlem2  27462  pntlemo  27534  pntlem3  27536  pntleml  27538  istrkg3ld  28259  axlowdimlem7  28753  axlowdimlem16  28762  axlowdimlem17  28763  usgrexmplef  29066  wlk2v2e  29961  ex-bc  30256  ex-dvds  30260  ex-gcd  30261  ex-ind-dvds  30265  cyc3conja  32873  prodfzo03  34230  hgt750lemd  34275  lcm3un  41481  3lexlogpow2ineq1  41524  aks4d1p1p7  41540  aks4d1p1  41542  2np3bcnp1  41611  3cubeslem4  42100  jm2.23  42408  jm2.20nn  42409  inductionexd  43576  lhe4.4ex1a  43757  wallispilem4  45447  smfmullem2  46171  smfmullem4  46173  fmtnoge3  46861  fmtnoprmfac2lem1  46897  31prm  46928  lighneallem4b  46940  41prothprmlem2  46949  41prothprm  46950  6even  47042  2exp340mod341  47064  4fppr1  47066  9fppr8  47068  nfermltl8rev  47073  nfermltl2rev  47074  sbgoldbalt  47112  sbgoldbo  47118  nnsum3primesle9  47125  nnsum4primesodd  47127  nnsum4primesoddALTV  47128  nnsum4primeseven  47131  nnsum4primesevenALTV  47132  linevalexample  47454  zlmodzxzequa  47555  zlmodzxznm  47556  zlmodzxzequap  47558  zlmodzxzldeplem3  47561  zlmodzxzldep  47563  ldepsnlinclem2  47565  ldepsnlinc  47567