Theorem zcn 9412

Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
zcn	|- ( N e. ZZ -> N e. CC )

Proof of Theorem zcn

Step	Hyp	Ref	Expression
1		zre 9411	. 2 |- ( N e. ZZ -> N e. RR )
2	1	recnd 8136	1 |- ( N e. ZZ -> N e. CC )

Syntax hints:   -> wi 4   e. wcel 2178   CCcc 7958   ZZcz 9407

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-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-resscn 8052

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-rab 2495  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970  df-neg 8281  df-z 9408

This theorem is referenced by:  zsscn  9415  zaddcllempos  9444  peano2zm  9445  zaddcllemneg  9446  zaddcl  9447  zsubcl  9448  zrevaddcl  9458  nzadd  9460  zlem1lt  9464  zltlem1  9465  zapne  9482  zdiv  9496  zdivadd  9497  zdivmul  9498  zextlt  9500  zneo  9509  zeo2  9514  peano5uzti  9516  zindd  9526  divfnzn  9777  qmulz  9779  zq  9782  qaddcl  9791  qnegcl  9792  qmulcl  9793  qreccl  9798  fzen  10200  uzsubsubfz  10204  fz01en  10210  fzmmmeqm  10215  fzsubel  10217  fztp  10235  fzsuc2  10236  fzrev2  10242  fzrev3  10244  elfzp1b  10254  fzrevral  10262  fzrevral2  10263  fzrevral3  10264  fzshftral  10265  fzo0addel  10354  fzo0addelr  10355  fzoaddel2  10356  fzosubel2  10361  eluzgtdifelfzo  10363  fzocatel  10365  elfzom1elp1fzo  10368  fzval3  10370  zpnn0elfzo1  10374  fzosplitprm1  10400  fzoshftral  10404  flqzadd  10478  2tnp1ge0ge0  10481  ceilid  10497  intfracq  10502  zmod10  10522  modqmuladdnn0  10550  addmodlteq  10580  frecfzen2  10609  seqshft2g  10664  ser3mono  10669  m1expeven  10768  expsubap  10769  zesq  10840  sqoddm1div8  10875  bccmpl  10936  swrd00g  11140  swrdswrd  11196  swrdpfx  11198  pfxccatin12lem4  11217  pfxccatin12lem1  11219  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12  11224  shftuz  11243  nnabscl  11526  climshftlemg  11728  climshft  11730  mptfzshft  11868  fsumrev  11869  fisum0diag2  11873  efexp  12108  efzval  12109  demoivre  12199  dvdsval2  12216  iddvds  12230  1dvds  12231  dvds0  12232  negdvdsb  12233  dvdsnegb  12234  0dvds  12237  dvdsmul1  12239  iddvdsexp  12241  muldvds1  12242  muldvds2  12243  dvdscmul  12244  dvdsmulc  12245  summodnegmod  12248  modmulconst  12249  dvds2ln  12250  dvds2add  12251  dvds2sub  12252  dvdstr  12254  dvdssub2  12261  dvdsadd  12262  dvdsaddr  12263  dvdssub  12264  dvdssubr  12265  dvdsadd2b  12266  dvdsabseq  12273  divconjdvds  12275  alzdvds  12280  addmodlteqALT  12285  zeo3  12294  odd2np1lem  12298  odd2np1  12299  even2n  12300  oddp1even  12302  mulsucdiv2z  12311  zob  12317  ltoddhalfle  12319  halfleoddlt  12320  opoe  12321  omoe  12322  opeo  12323  omeo  12324  m1exp1  12327  divalgb  12351  divalgmod  12353  modremain  12355  ndvdssub  12356  ndvdsadd  12357  flodddiv4  12362  flodddiv4t2lthalf  12365  bits0  12374  bitsp1e  12378  bitsp1o  12379  gcdneg  12418  gcdadd  12421  gcdid  12422  modgcd  12427  dvdsgcd  12448  mulgcd  12452  absmulgcd  12453  mulgcdr  12454  gcddiv  12455  gcdmultiplez  12457  dvdssqim  12460  dvdssq  12467  bezoutr1  12469  lcmneg  12511  lcmgcdlem  12514  lcmgcd  12515  lcmid  12517  lcm1  12518  coprmdvds  12529  coprmdvds2  12530  qredeq  12533  qredeu  12534  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  prmdvdsexp  12585  rpexp1i  12591  sqrt2irr  12599  divnumden  12633  phiprmpw  12659  nnnn0modprm0  12693  modprmn0modprm0  12694  coprimeprodsq2  12696  pclemub  12725  pcprendvds2  12729  pcmul  12739  pcneg  12763  fldivp1  12786  prmpwdvds  12793  zgz  12811  4sqexercise1  12836  4sqexercise2  12837  modxai  12854  mulgz  13601  mulgassr  13611  mulgmodid  13612  gsumfzconst  13792  zsubrg  14458  zsssubrg  14462  zringmulg  14475  zringinvg  14481  mulgrhm2  14487  znunit  14536  ef2kpi  15393  efper  15394  sinperlem  15395  sin2kpi  15398  cos2kpi  15399  abssinper  15433  sinkpi  15434  coskpi  15435  cxpexprp  15482  sgmval2  15571  lgslem3  15594  lgsneg  15616  lgsdir2lem2  15621  lgsdir2lem4  15623  lgsdir2  15625  lgssq  15632  lgsmulsqcoprm  15638  lgsdirnn0  15639  gausslemma2dlem3  15655  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2  15675  2lgslem1a2  15679  2lgsoddprmlem1  15697  2lgsoddprmlem2  15698  2sqlem2  15707  2sqlem7  15713