Theorem 4z 12634

Description: 4 is an integer. (Contributed by BJ, 26-Mar-2020.)

Assertion

Ref	Expression
4z	⊢ 4 ∈ ℤ

Proof of Theorem 4z

Step	Hyp	Ref	Expression
1		4nn 12331	. 2 ⊢ 4 ∈ ℕ
2	1	nnzi 12624	1 ⊢ 4 ∈ ℤ

Syntax hints:   ∈ wcel 2107  4c4 12305  ℤcz 12596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-i2m1 11205  ax-1ne0 11206  ax-rrecex 11209  ax-cnre 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-neg 11477  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-z 12597

This theorem is referenced by:  fz0to4untppr  13652  fzo0to42pr  13774  fzo1to4tp  13775  iexpcyc  14228  sqoddm1div8  14264  4bc2eq6  14350  ef01bndlem  16202  sin01bnd  16203  cos01bnd  16204  4dvdseven  16392  flodddiv4lt  16436  6gcd4e2  16557  6lcm4e12  16635  lcmf2a3a4e12  16666  ge2nprmge4  16720  prm23lt5  16834  1259lem3  17152  ppiub  27184  bclbnd  27260  bposlem6  27269  bposlem9  27272  lgsdir2lem2  27306  m1lgs  27368  2lgsoddprmlem2  27389  chebbnd1lem2  27450  chebbnd1lem3  27451  pntlema  27576  pntlemb  27577  ex-ind-dvds  30408  hgt750lemd  34622  3lexlogpow5ineq5  42020  aks4d1p1p7  42034  aks4d1p1p5  42035  aks4d1p1  42036  flt4lem7  42632  inductionexd  44130  wallispi2lem1  46043  fmtno4prmfac  47517  31prm  47542  mod42tp1mod8  47547  8even  47658  341fppr2  47679  4fppr1  47680  9fppr8  47682  fpprel2  47686  sbgoldbo  47732  nnsum3primesle9  47739  nnsum4primeseven  47745  nnsum4primesevenALTV  47746  tgblthelfgott  47760  gpg5nbgr3star  47995  zlmodzxzequa  48371  zlmodzxznm  48372  zlmodzxzequap  48374  zlmodzxzldeplem3  48377  zlmodzxzldep  48379  ldepsnlinclem1  48380  ldepsnlinc  48383