Theorem 4z 12655

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

This proof depends on syntax axioms:   ∈ wcel 2145  4c4 12324  ℤcz 12618

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7417  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-neg 11471  df-nn 12261  df-2 12330  df-3 12331  df-4 12332  df-z 12619

This theorem is used by:  fz0to4untppr  13688  fzo0to42pr  13812  fzo1to4tp  13813  iexpcyc  14274  sqoddm1div8  14310  4bc2eq6  14396  ef01bndlem  16275  sin01bnd  16276  cos01bnd  16277  4dvdseven  16466  flodddiv4lt  16510  6gcd4e2  16631  6lcm4e12  16709  lcmf2a3a4e12  16740  ge2nprmge4  16795  prm23lt5  16909  1259lem3  17228  ppiub  27443  bclbnd  27519  bposlem6  27528  bposlem9  27531  lgsdir2lem2  27565  m1lgs  27627  2lgsoddprmlem2  27648  chebbnd1lem2  27709  chebbnd1lem3  27710  pntlema  27835  pntlemb  27836  ex-ind-dvds  30944  hgt750lemd  35159  3lexlogpow5ineq5  42929  aks4d1p1p7  42943  aks4d1p1p5  42944  aks4d1p1  42945  flt4lem7  43508  inductionexd  44998  wallispi2lem1  46902  goldratmolem2  47754  fmtno4prmfac  48478  31prm  48503  mod42tp1mod8  48508  nprmdvdsfacm1  48530  8even  48632  341fppr2  48653  4fppr1  48654  9fppr8  48656  fpprel2  48660  sbgoldbo  48706  nnsum3primesle9  48713  nnsum4primeseven  48719  nnsum4primesevenALTV  48720  tgblthelfgott  48734  gpg5nbgr3star  49000  gpgprismgr4cycllem9  49022  zlmodzxzequa  49429  zlmodzxznm  49430  zlmodzxzequap  49432  zlmodzxzldeplem3  49435  zlmodzxzldep  49437  ldepsnlinclem1  49438  ldepsnlinc  49441  veronesev4lem  50812