Theorem zcn 9322

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 9321	. 2 |- ( N e. ZZ -> N e. RR )
2	1	recnd 8048	1 |- ( N e. ZZ -> N e. CC )

Syntax hints:   -> wi 4   e. wcel 2164   CCcc 7870   ZZcz 9317

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7964

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-rab 2481  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921  df-neg 8193  df-z 9318

This theorem is referenced by:  zsscn  9325  zaddcllempos  9354  peano2zm  9355  zaddcllemneg  9356  zaddcl  9357  zsubcl  9358  zrevaddcl  9367  nzadd  9369  zlem1lt  9373  zltlem1  9374  zapne  9391  zdiv  9405  zdivadd  9406  zdivmul  9407  zextlt  9409  zneo  9418  zeo2  9423  peano5uzti  9425  zindd  9435  divfnzn  9686  qmulz  9688  zq  9691  qaddcl  9700  qnegcl  9701  qmulcl  9702  qreccl  9707  fzen  10109  uzsubsubfz  10113  fz01en  10119  fzmmmeqm  10124  fzsubel  10126  fztp  10144  fzsuc2  10145  fzrev2  10151  fzrev3  10153  elfzp1b  10163  fzrevral  10171  fzrevral2  10172  fzrevral3  10173  fzshftral  10174  fzoaddel2  10260  fzosubel2  10262  eluzgtdifelfzo  10264  fzocatel  10266  elfzom1elp1fzo  10269  fzval3  10271  zpnn0elfzo1  10275  fzosplitprm1  10301  fzoshftral  10305  flqzadd  10367  2tnp1ge0ge0  10370  ceilid  10386  intfracq  10391  zmod10  10411  modqmuladdnn0  10439  addmodlteq  10469  frecfzen2  10498  seqshft2g  10553  ser3mono  10558  m1expeven  10657  expsubap  10658  zesq  10729  sqoddm1div8  10764  bccmpl  10825  shftuz  10961  nnabscl  11244  climshftlemg  11445  climshft  11447  mptfzshft  11585  fsumrev  11586  fisum0diag2  11590  efexp  11825  efzval  11826  demoivre  11916  dvdsval2  11933  iddvds  11947  1dvds  11948  dvds0  11949  negdvdsb  11950  dvdsnegb  11951  0dvds  11954  dvdsmul1  11956  iddvdsexp  11958  muldvds1  11959  muldvds2  11960  dvdscmul  11961  dvdsmulc  11962  summodnegmod  11965  modmulconst  11966  dvds2ln  11967  dvds2add  11968  dvds2sub  11969  dvdstr  11971  dvdssub2  11978  dvdsadd  11979  dvdsaddr  11980  dvdssub  11981  dvdssubr  11982  dvdsadd2b  11983  dvdsabseq  11989  divconjdvds  11991  alzdvds  11996  addmodlteqALT  12001  zeo3  12009  odd2np1lem  12013  odd2np1  12014  even2n  12015  oddp1even  12017  mulsucdiv2z  12026  zob  12032  ltoddhalfle  12034  halfleoddlt  12035  opoe  12036  omoe  12037  opeo  12038  omeo  12039  m1exp1  12042  divalgb  12066  divalgmod  12068  modremain  12070  ndvdssub  12071  ndvdsadd  12072  flodddiv4  12075  flodddiv4t2lthalf  12078  gcdneg  12119  gcdadd  12122  gcdid  12123  modgcd  12128  dvdsgcd  12149  mulgcd  12153  absmulgcd  12154  mulgcdr  12155  gcddiv  12156  gcdmultiplez  12158  dvdssqim  12161  dvdssq  12168  bezoutr1  12170  lcmneg  12212  lcmgcdlem  12215  lcmgcd  12216  lcmid  12218  lcm1  12219  coprmdvds  12230  coprmdvds2  12231  qredeq  12234  qredeu  12235  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  prmdvdsexp  12286  rpexp1i  12292  sqrt2irr  12300  divnumden  12334  phiprmpw  12360  nnnn0modprm0  12393  modprmn0modprm0  12394  coprimeprodsq2  12396  pclemub  12425  pcprendvds2  12429  pcmul  12439  pcneg  12463  fldivp1  12486  prmpwdvds  12493  zgz  12511  4sqexercise1  12536  4sqexercise2  12537  mulgz  13220  mulgassr  13230  mulgmodid  13231  gsumfzconst  13411  zsubrg  14069  zsssubrg  14073  zringmulg  14086  zringinvg  14092  mulgrhm2  14098  znunit  14147  ef2kpi  14941  efper  14942  sinperlem  14943  sin2kpi  14946  cos2kpi  14947  abssinper  14981  sinkpi  14982  coskpi  14983  cxpexprp  15030  lgslem3  15118  lgsneg  15140  lgsdir2lem2  15145  lgsdir2lem4  15147  lgsdir2  15149  lgssq  15156  lgsmulsqcoprm  15162  lgsdirnn0  15163  gausslemma2dlem3  15179  lgsquadlem1  15191  2lgsoddprmlem1  15193  2lgsoddprmlem2  15194  2sqlem2  15202  2sqlem7  15208