Theorem zcn 9331

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

Syntax hints:   -> wi 4   e. wcel 2167   CCcc 7877   ZZcz 9326

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7971

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-rab 2484  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925  df-neg 8200  df-z 9327

This theorem is referenced by:  zsscn  9334  zaddcllempos  9363  peano2zm  9364  zaddcllemneg  9365  zaddcl  9366  zsubcl  9367  zrevaddcl  9376  nzadd  9378  zlem1lt  9382  zltlem1  9383  zapne  9400  zdiv  9414  zdivadd  9415  zdivmul  9416  zextlt  9418  zneo  9427  zeo2  9432  peano5uzti  9434  zindd  9444  divfnzn  9695  qmulz  9697  zq  9700  qaddcl  9709  qnegcl  9710  qmulcl  9711  qreccl  9716  fzen  10118  uzsubsubfz  10122  fz01en  10128  fzmmmeqm  10133  fzsubel  10135  fztp  10153  fzsuc2  10154  fzrev2  10160  fzrev3  10162  elfzp1b  10172  fzrevral  10180  fzrevral2  10181  fzrevral3  10182  fzshftral  10183  fzoaddel2  10269  fzosubel2  10271  eluzgtdifelfzo  10273  fzocatel  10275  elfzom1elp1fzo  10278  fzval3  10280  zpnn0elfzo1  10284  fzosplitprm1  10310  fzoshftral  10314  flqzadd  10388  2tnp1ge0ge0  10391  ceilid  10407  intfracq  10412  zmod10  10432  modqmuladdnn0  10460  addmodlteq  10490  frecfzen2  10519  seqshft2g  10574  ser3mono  10579  m1expeven  10678  expsubap  10679  zesq  10750  sqoddm1div8  10785  bccmpl  10846  shftuz  10982  nnabscl  11265  climshftlemg  11467  climshft  11469  mptfzshft  11607  fsumrev  11608  fisum0diag2  11612  efexp  11847  efzval  11848  demoivre  11938  dvdsval2  11955  iddvds  11969  1dvds  11970  dvds0  11971  negdvdsb  11972  dvdsnegb  11973  0dvds  11976  dvdsmul1  11978  iddvdsexp  11980  muldvds1  11981  muldvds2  11982  dvdscmul  11983  dvdsmulc  11984  summodnegmod  11987  modmulconst  11988  dvds2ln  11989  dvds2add  11990  dvds2sub  11991  dvdstr  11993  dvdssub2  12000  dvdsadd  12001  dvdsaddr  12002  dvdssub  12003  dvdssubr  12004  dvdsadd2b  12005  dvdsabseq  12012  divconjdvds  12014  alzdvds  12019  addmodlteqALT  12024  zeo3  12033  odd2np1lem  12037  odd2np1  12038  even2n  12039  oddp1even  12041  mulsucdiv2z  12050  zob  12056  ltoddhalfle  12058  halfleoddlt  12059  opoe  12060  omoe  12061  opeo  12062  omeo  12063  m1exp1  12066  divalgb  12090  divalgmod  12092  modremain  12094  ndvdssub  12095  ndvdsadd  12096  flodddiv4  12101  flodddiv4t2lthalf  12104  bits0  12112  bitsp1e  12116  bitsp1o  12117  gcdneg  12149  gcdadd  12152  gcdid  12153  modgcd  12158  dvdsgcd  12179  mulgcd  12183  absmulgcd  12184  mulgcdr  12185  gcddiv  12186  gcdmultiplez  12188  dvdssqim  12191  dvdssq  12198  bezoutr1  12200  lcmneg  12242  lcmgcdlem  12245  lcmgcd  12246  lcmid  12248  lcm1  12249  coprmdvds  12260  coprmdvds2  12261  qredeq  12264  qredeu  12265  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  prmdvdsexp  12316  rpexp1i  12322  sqrt2irr  12330  divnumden  12364  phiprmpw  12390  nnnn0modprm0  12424  modprmn0modprm0  12425  coprimeprodsq2  12427  pclemub  12456  pcprendvds2  12460  pcmul  12470  pcneg  12494  fldivp1  12517  prmpwdvds  12524  zgz  12542  4sqexercise1  12567  4sqexercise2  12568  modxai  12585  mulgz  13280  mulgassr  13290  mulgmodid  13291  gsumfzconst  13471  zsubrg  14137  zsssubrg  14141  zringmulg  14154  zringinvg  14160  mulgrhm2  14166  znunit  14215  ef2kpi  15042  efper  15043  sinperlem  15044  sin2kpi  15047  cos2kpi  15048  abssinper  15082  sinkpi  15083  coskpi  15084  cxpexprp  15131  sgmval2  15220  lgslem3  15243  lgsneg  15265  lgsdir2lem2  15270  lgsdir2lem4  15272  lgsdir2  15274  lgssq  15281  lgsmulsqcoprm  15287  lgsdirnn0  15288  gausslemma2dlem3  15304  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2  15324  2lgslem1a2  15328  2lgsoddprmlem1  15346  2lgsoddprmlem2  15347  2sqlem2  15356  2sqlem7  15362