Theorem 4z 12606

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

Syntax hints:   ∈ wcel 2143  4c4 12275  ℤcz 12569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7719  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-i2m1 11142  ax-1ne0 11143  ax-rrecex 11146  ax-cnre 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6289  df-ord 6350  df-on 6351  df-lim 6352  df-suc 6353  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-ov 7400  df-om 7848  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8382  df-neg 11418  df-nn 12212  df-2 12281  df-3 12282  df-4 12283  df-z 12570

This theorem is referenced by:  fz0to4untppr  13636  fzo0to42pr  13760  fzo1to4tp  13761  iexpcyc  14221  sqoddm1div8  14257  4bc2eq6  14343  ef01bndlem  16217  sin01bnd  16218  cos01bnd  16219  4dvdseven  16408  flodddiv4lt  16452  6gcd4e2  16573  6lcm4e12  16651  lcmf2a3a4e12  16682  ge2nprmge4  16737  prm23lt5  16851  1259lem3  17170  ppiub  27269  bclbnd  27345  bposlem6  27354  bposlem9  27357  lgsdir2lem2  27391  m1lgs  27453  2lgsoddprmlem2  27474  chebbnd1lem2  27535  chebbnd1lem3  27536  pntlema  27661  pntlemb  27662  ex-ind-dvds  30664  hgt750lemd  34943  3lexlogpow5ineq5  42678  aks4d1p1p7  42692  aks4d1p1p5  42693  aks4d1p1  42694  flt4lem7  43242  inductionexd  44732  wallispi2lem1  46646  goldratmolem2  47481  fmtno4prmfac  48182  31prm  48207  mod42tp1mod8  48212  nprmdvdsfacm1  48234  8even  48336  341fppr2  48357  4fppr1  48358  9fppr8  48360  fpprel2  48364  sbgoldbo  48410  nnsum3primesle9  48417  nnsum4primeseven  48423  nnsum4primesevenALTV  48424  tgblthelfgott  48438  gpg5nbgr3star  48704  gpgprismgr4cycllem9  48726  zlmodzxzequa  49119  zlmodzxznm  49120  zlmodzxzequap  49122  zlmodzxzldeplem3  49125  zlmodzxzldep  49127  ldepsnlinclem1  49128  ldepsnlinc  49131