Theorem 1z 8874

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 8531	. 2 ⊢ 1 ∈ ℕ
2	1	nnzi 8869	1 ⊢ 1 ∈ ℤ

Syntax hints:   ∈ wcel 1445  1c1 7448  ℤcz 8848

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381  ax-cnex 7533  ax-resscn 7534  ax-1cn 7535  ax-1re 7536  ax-icn 7537  ax-addcl 7538  ax-addrcl 7539  ax-mulcl 7540  ax-addcom 7542  ax-addass 7544  ax-distr 7546  ax-i2m1 7547  ax-0lt1 7548  ax-0id 7550  ax-rnegex 7551  ax-cnre 7553  ax-pre-ltirr 7554  ax-pre-ltwlin 7555  ax-pre-lttrn 7556  ax-pre-ltadd 7558

This theorem depends on definitions:  df-bi 116  df-3or 928  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-nel 2358  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-br 3868  df-opab 3922  df-id 4144  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-iota 5014  df-fun 5051  df-fv 5057  df-riota 5646  df-ov 5693  df-oprab 5694  df-mpt2 5695  df-pnf 7621  df-mnf 7622  df-xr 7623  df-ltxr 7624  df-le 7625  df-sub 7752  df-neg 7753  df-inn 8521  df-z 8849

This theorem is referenced by:  1zzd  8875  znnnlt1  8896  nn0n0n1ge2b  8924  nn0lt2  8926  nn0le2is012  8927  3halfnz  8942  prime  8944  nnuz  9153  eluz2nn  9156  eluzge3nn  9159  1eluzge0  9161  2eluzge1  9163  eluz2b1  9187  uz2m1nn  9191  elnn1uz2  9193  nn01to3  9201  nnrecq  9229  fz1n  9607  fz10  9609  fz01en  9616  fzpreddisj  9634  fznatpl1  9639  fzprval  9645  fztpval  9646  fseq1p1m1  9657  elfzp1b  9660  elfzm1b  9661  4fvwrd4  9700  ige2m2fzo  9758  fzo12sn  9777  fzofzp1  9787  fzostep1  9797  rebtwn2zlemstep  9813  qbtwnxr  9818  flqge1nn  9850  fldiv4p1lem1div2  9861  modqfrac  9893  modqid0  9906  q1mod  9912  mulp1mod1  9921  m1modnnsub1  9926  modqm1p1mod0  9931  modqltm1p1mod  9932  frecfzennn  9982  frecfzen2  9983  zexpcl  10101  qexpcl  10102  qexpclz  10107  m1expcl  10109  expp1zap  10135  expm1ap  10136  bcn1  10297  bcpasc  10305  bcnm1  10311  isfinite4im  10332  hashsng  10337  hashfz  10360  climuni  10852  sum0  10947  sumsnf  10968  expcnv  11063  cvgratz  11091  sin01gt0  11217  iddvds  11252  1dvds  11253  dvds1  11297  nn0o1gt2  11348  n2dvds1  11355  gcdadd  11419  gcdid  11420  gcd1  11421  1gcd  11426  bezoutlema  11431  bezoutlemb  11432  gcdmultiple  11452  lcmgcdlem  11502  lcm1  11506  3lcm2e6woprm  11511  isprm3  11543  prmgt1  11556  phicl2  11633  phibnd  11636  phi1  11638  dfphi2  11639  phimullem  11644  ex-fl  12376