Theorem 4z 12658

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 12356	. 2 ⊢ 4 ∈ ℕ
2	1	nnzi 12648	1 ⊢ 4 ∈ ℤ

Syntax hints:   ∈ wcel 2108  4c4 12330  ℤcz 12620

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5305  ax-nul 5315  ax-pr 5441  ax-un 7761  ax-1cn 11220  ax-icn 11221  ax-addcl 11222  ax-addrcl 11223  ax-mulcl 11224  ax-mulrcl 11225  ax-i2m1 11230  ax-1ne0 11231  ax-rrecex 11234  ax-cnre 11235

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3483  df-sbc 3795  df-csb 3912  df-dif 3969  df-un 3971  df-in 3973  df-ss 3983  df-pss 3986  df-nul 4343  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4916  df-iun 5001  df-br 5152  df-opab 5214  df-mpt 5235  df-tr 5269  df-id 5587  df-eprel 5593  df-po 5601  df-so 5602  df-fr 5645  df-we 5647  df-xp 5699  df-rel 5700  df-cnv 5701  df-co 5702  df-dm 5703  df-rn 5704  df-res 5705  df-ima 5706  df-pred 6329  df-ord 6395  df-on 6396  df-lim 6397  df-suc 6398  df-iota 6522  df-fun 6571  df-fn 6572  df-f 6573  df-f1 6574  df-fo 6575  df-f1o 6576  df-fv 6577  df-ov 7441  df-om 7895  df-2nd 8023  df-frecs 8314  df-wrecs 8345  df-recs 8419  df-rdg 8458  df-neg 11502  df-nn 12274  df-2 12336  df-3 12337  df-4 12338  df-z 12621

This theorem is referenced by:  fz0to4untppr  13676  fzo0to42pr  13798  fzo1to4tp  13799  iexpcyc  14252  sqoddm1div8  14288  4bc2eq6  14374  ef01bndlem  16226  sin01bnd  16227  cos01bnd  16228  4dvdseven  16416  flodddiv4lt  16460  6gcd4e2  16581  6lcm4e12  16659  lcmf2a3a4e12  16690  ge2nprmge4  16744  prm23lt5  16857  1259lem3  17176  ppiub  27274  bclbnd  27350  bposlem6  27359  bposlem9  27362  lgsdir2lem2  27396  m1lgs  27458  2lgsoddprmlem2  27479  chebbnd1lem2  27540  chebbnd1lem3  27541  pntlema  27666  pntlemb  27667  ex-ind-dvds  30506  hgt750lemd  34656  3lexlogpow5ineq5  42056  aks4d1p1p7  42070  aks4d1p1p5  42071  aks4d1p1  42072  flt4lem7  42662  inductionexd  44161  wallispi2lem1  46055  fmtno4prmfac  47525  31prm  47550  mod42tp1mod8  47555  8even  47666  341fppr2  47687  4fppr1  47688  9fppr8  47690  fpprel2  47694  sbgoldbo  47740  nnsum3primesle9  47747  nnsum4primeseven  47753  nnsum4primesevenALTV  47754  tgblthelfgott  47768  gpg5nbgr3star  48003  zlmodzxzequa  48380  zlmodzxznm  48381  zlmodzxzequap  48383  zlmodzxzldeplem3  48386  zlmodzxzldep  48388  ldepsnlinclem1  48389  ldepsnlinc  48392