Theorem zcn 9348

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

Assertion

Ref	Expression
zcn	⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Proof of Theorem zcn

Step	Hyp	Ref	Expression
1		zre 9347	. 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2	1	recnd 8072	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7894  ℤcz 9343

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 7988

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 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928  df-neg 8217  df-z 9344

This theorem is referenced by:  zsscn  9351  zaddcllempos  9380  peano2zm  9381  zaddcllemneg  9382  zaddcl  9383  zsubcl  9384  zrevaddcl  9393  nzadd  9395  zlem1lt  9399  zltlem1  9400  zapne  9417  zdiv  9431  zdivadd  9432  zdivmul  9433  zextlt  9435  zneo  9444  zeo2  9449  peano5uzti  9451  zindd  9461  divfnzn  9712  qmulz  9714  zq  9717  qaddcl  9726  qnegcl  9727  qmulcl  9728  qreccl  9733  fzen  10135  uzsubsubfz  10139  fz01en  10145  fzmmmeqm  10150  fzsubel  10152  fztp  10170  fzsuc2  10171  fzrev2  10177  fzrev3  10179  elfzp1b  10189  fzrevral  10197  fzrevral2  10198  fzrevral3  10199  fzshftral  10200  fzoaddel2  10286  fzosubel2  10288  eluzgtdifelfzo  10290  fzocatel  10292  elfzom1elp1fzo  10295  fzval3  10297  zpnn0elfzo1  10301  fzosplitprm1  10327  fzoshftral  10331  flqzadd  10405  2tnp1ge0ge0  10408  ceilid  10424  intfracq  10429  zmod10  10449  modqmuladdnn0  10477  addmodlteq  10507  frecfzen2  10536  seqshft2g  10591  ser3mono  10596  m1expeven  10695  expsubap  10696  zesq  10767  sqoddm1div8  10802  bccmpl  10863  shftuz  10999  nnabscl  11282  climshftlemg  11484  climshft  11486  mptfzshft  11624  fsumrev  11625  fisum0diag2  11629  efexp  11864  efzval  11865  demoivre  11955  dvdsval2  11972  iddvds  11986  1dvds  11987  dvds0  11988  negdvdsb  11989  dvdsnegb  11990  0dvds  11993  dvdsmul1  11995  iddvdsexp  11997  muldvds1  11998  muldvds2  11999  dvdscmul  12000  dvdsmulc  12001  summodnegmod  12004  modmulconst  12005  dvds2ln  12006  dvds2add  12007  dvds2sub  12008  dvdstr  12010  dvdssub2  12017  dvdsadd  12018  dvdsaddr  12019  dvdssub  12020  dvdssubr  12021  dvdsadd2b  12022  dvdsabseq  12029  divconjdvds  12031  alzdvds  12036  addmodlteqALT  12041  zeo3  12050  odd2np1lem  12054  odd2np1  12055  even2n  12056  oddp1even  12058  mulsucdiv2z  12067  zob  12073  ltoddhalfle  12075  halfleoddlt  12076  opoe  12077  omoe  12078  opeo  12079  omeo  12080  m1exp1  12083  divalgb  12107  divalgmod  12109  modremain  12111  ndvdssub  12112  ndvdsadd  12113  flodddiv4  12118  flodddiv4t2lthalf  12121  bits0  12130  bitsp1e  12134  bitsp1o  12135  gcdneg  12174  gcdadd  12177  gcdid  12178  modgcd  12183  dvdsgcd  12204  mulgcd  12208  absmulgcd  12209  mulgcdr  12210  gcddiv  12211  gcdmultiplez  12213  dvdssqim  12216  dvdssq  12223  bezoutr1  12225  lcmneg  12267  lcmgcdlem  12270  lcmgcd  12271  lcmid  12273  lcm1  12274  coprmdvds  12285  coprmdvds2  12286  qredeq  12289  qredeu  12290  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  prmdvdsexp  12341  rpexp1i  12347  sqrt2irr  12355  divnumden  12389  phiprmpw  12415  nnnn0modprm0  12449  modprmn0modprm0  12450  coprimeprodsq2  12452  pclemub  12481  pcprendvds2  12485  pcmul  12495  pcneg  12519  fldivp1  12542  prmpwdvds  12549  zgz  12567  4sqexercise1  12592  4sqexercise2  12593  modxai  12610  mulgz  13356  mulgassr  13366  mulgmodid  13367  gsumfzconst  13547  zsubrg  14213  zsssubrg  14217  zringmulg  14230  zringinvg  14236  mulgrhm2  14242  znunit  14291  ef2kpi  15126  efper  15127  sinperlem  15128  sin2kpi  15131  cos2kpi  15132  abssinper  15166  sinkpi  15167  coskpi  15168  cxpexprp  15215  sgmval2  15304  lgslem3  15327  lgsneg  15349  lgsdir2lem2  15354  lgsdir2lem4  15356  lgsdir2  15358  lgssq  15365  lgsmulsqcoprm  15371  lgsdirnn0  15372  gausslemma2dlem3  15388  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2  15408  2lgslem1a2  15412  2lgsoddprmlem1  15430  2lgsoddprmlem2  15431  2sqlem2  15440  2sqlem7  15446