Theorem 1z 9504

Description: One is an integer. (Contributed by NM, 10-May-2004.)

Assertion

Ref	Expression
1z	⊢ 1 ∈ ℤ

Proof of Theorem 1z

Step	Hyp	Ref	Expression
1		1nn 9153	. 2 ⊢ 1 ∈ ℕ
2	1	nnzi 9499	1 ⊢ 1 ∈ ℤ

Syntax hints:   ∈ wcel 2202  1c1 8032  ℤcz 9478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8122  ax-resscn 8123  ax-1cn 8124  ax-1re 8125  ax-icn 8126  ax-addcl 8127  ax-addrcl 8128  ax-mulcl 8129  ax-addcom 8131  ax-addass 8133  ax-distr 8135  ax-i2m1 8136  ax-0lt1 8137  ax-0id 8139  ax-rnegex 8140  ax-cnre 8142  ax-pre-ltirr 8143  ax-pre-ltwlin 8144  ax-pre-lttrn 8145  ax-pre-ltadd 8147

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5970  df-ov 6020  df-oprab 6021  df-mpo 6022  df-pnf 8215  df-mnf 8216  df-xr 8217  df-ltxr 8218  df-le 8219  df-sub 8351  df-neg 8352  df-inn 9143  df-z 9479

This theorem is referenced by:  1zzd  9505  znnnlt1  9526  nn0n0n1ge2b  9558  nn0lt2  9560  nn0le2is012  9561  3halfnz  9576  prime  9578  nnuz  9791  eluz2nn  9799  eluzge3nn  9805  1eluzge0  9807  2eluzge1  9809  eluz2b1  9834  uz2m1nn  9838  elnn1uz2  9840  elnndc  9845  nn01to3  9850  nnrecq  9878  fz1n  10278  fz10  10280  fz01en  10287  fzpreddisj  10305  fznatpl1  10310  fzprval  10316  fztpval  10317  fseq1p1m1  10328  elfzp1b  10331  elfzm1b  10332  4fvwrd4  10374  ige2m2fzo  10442  fzo12sn  10461  fzofzp1  10471  fzostep1  10482  rebtwn2zlemstep  10511  qbtwnxr  10516  flqge1nn  10553  fldiv4p1lem1div2  10564  fldiv4lem1div2  10566  modqfrac  10598  modqid0  10611  q1mod  10617  mulp1mod1  10626  m1modnnsub1  10631  modqm1p1mod0  10636  modqltm1p1mod  10637  frecfzennn  10687  frecfzen2  10688  zexpcl  10815  qexpcl  10816  qexpclz  10821  m1expcl  10823  expp1zap  10849  expm1ap  10850  bcn1  11019  bcpasc  11027  bcnm1  11033  isfinite4im  11053  hashsng  11059  hashfz  11084  climuni  11853  sum0  11948  sumsnf  11969  expcnv  12064  cvgratz  12092  prod0  12145  prodsnf  12152  sinltxirr  12321  sin01gt0  12322  p1modz1  12354  iddvds  12364  1dvds  12365  dvds1  12413  3dvds  12424  nn0o1gt2  12465  n2dvds1  12472  bitsp1o  12513  bitsfzo  12515  gcdadd  12555  gcdid  12556  gcd1  12557  1gcd  12562  bezoutlema  12569  bezoutlemb  12570  gcdmultiple  12590  lcmgcdlem  12648  lcm1  12652  3lcm2e6woprm  12657  isprm3  12689  prmgt1  12703  phicl2  12785  phibnd  12788  phi1  12790  dfphi2  12791  phimullem  12796  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemth  12803  fermltl  12805  prmdiv  12806  prmdiveq  12807  odzcllem  12814  odzdvds  12817  oddprm  12831  pythagtriplem4  12840  pcpre1  12864  pc1  12877  pcrec  12880  pcmpt  12915  fldivp1  12920  expnprm  12925  pockthlem  12928  igz  12946  4sqlem12  12974  4sqlem13m  12975  4sqlem19  12981  ssnnctlemct  13066  mulgm1  13728  mulgp1  13741  mulgneg2  13742  zsubrg  14594  gzsubrg  14595  zringmulg  14611  mulgrhm2  14623  sin2pim  15536  cos2pim  15537  rpcxp1  15622  logbleb  15684  logblt  15685  lgslem2  15729  lgsfcl2  15734  lgsval2lem  15738  lgsmod  15754  lgsdir2lem1  15756  lgsdir2lem5  15760  lgsdir  15763  lgsne0  15766  1lgs  15771  lgsdinn0  15776  gausslemma2dlem0i  15785  gausslemma2d  15797  lgseisen  15802  lgsquad2lem2  15810  m1lgs  15813  2lgs  15832  2sqlem9  15852  2sqlem10  15853  usgrexmpldifpr  16099  upgr2wlkdc  16227  umgrclwwlkge2  16252  ex-fl  16321  apdiff  16652  iswomni0  16655  nconstwlpolem0  16667