Theorem zcn 9350

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 9349	. 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2	1	recnd 8074	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7896  ℤcz 9345

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 7990

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 8219  df-z 9346

This theorem is referenced by:  zsscn  9353  zaddcllempos  9382  peano2zm  9383  zaddcllemneg  9384  zaddcl  9385  zsubcl  9386  zrevaddcl  9395  nzadd  9397  zlem1lt  9401  zltlem1  9402  zapne  9419  zdiv  9433  zdivadd  9434  zdivmul  9435  zextlt  9437  zneo  9446  zeo2  9451  peano5uzti  9453  zindd  9463  divfnzn  9714  qmulz  9716  zq  9719  qaddcl  9728  qnegcl  9729  qmulcl  9730  qreccl  9735  fzen  10137  uzsubsubfz  10141  fz01en  10147  fzmmmeqm  10152  fzsubel  10154  fztp  10172  fzsuc2  10173  fzrev2  10179  fzrev3  10181  elfzp1b  10191  fzrevral  10199  fzrevral2  10200  fzrevral3  10201  fzshftral  10202  fzoaddel2  10288  fzosubel2  10290  eluzgtdifelfzo  10292  fzocatel  10294  elfzom1elp1fzo  10297  fzval3  10299  zpnn0elfzo1  10303  fzosplitprm1  10329  fzoshftral  10333  flqzadd  10407  2tnp1ge0ge0  10410  ceilid  10426  intfracq  10431  zmod10  10451  modqmuladdnn0  10479  addmodlteq  10509  frecfzen2  10538  seqshft2g  10593  ser3mono  10598  m1expeven  10697  expsubap  10698  zesq  10769  sqoddm1div8  10804  bccmpl  10865  shftuz  11001  nnabscl  11284  climshftlemg  11486  climshft  11488  mptfzshft  11626  fsumrev  11627  fisum0diag2  11631  efexp  11866  efzval  11867  demoivre  11957  dvdsval2  11974  iddvds  11988  1dvds  11989  dvds0  11990  negdvdsb  11991  dvdsnegb  11992  0dvds  11995  dvdsmul1  11997  iddvdsexp  11999  muldvds1  12000  muldvds2  12001  dvdscmul  12002  dvdsmulc  12003  summodnegmod  12006  modmulconst  12007  dvds2ln  12008  dvds2add  12009  dvds2sub  12010  dvdstr  12012  dvdssub2  12019  dvdsadd  12020  dvdsaddr  12021  dvdssub  12022  dvdssubr  12023  dvdsadd2b  12024  dvdsabseq  12031  divconjdvds  12033  alzdvds  12038  addmodlteqALT  12043  zeo3  12052  odd2np1lem  12056  odd2np1  12057  even2n  12058  oddp1even  12060  mulsucdiv2z  12069  zob  12075  ltoddhalfle  12077  halfleoddlt  12078  opoe  12079  omoe  12080  opeo  12081  omeo  12082  m1exp1  12085  divalgb  12109  divalgmod  12111  modremain  12113  ndvdssub  12114  ndvdsadd  12115  flodddiv4  12120  flodddiv4t2lthalf  12123  bits0  12132  bitsp1e  12136  bitsp1o  12137  gcdneg  12176  gcdadd  12179  gcdid  12180  modgcd  12185  dvdsgcd  12206  mulgcd  12210  absmulgcd  12211  mulgcdr  12212  gcddiv  12213  gcdmultiplez  12215  dvdssqim  12218  dvdssq  12225  bezoutr1  12227  lcmneg  12269  lcmgcdlem  12272  lcmgcd  12273  lcmid  12275  lcm1  12276  coprmdvds  12287  coprmdvds2  12288  qredeq  12291  qredeu  12292  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  prmdvdsexp  12343  rpexp1i  12349  sqrt2irr  12357  divnumden  12391  phiprmpw  12417  nnnn0modprm0  12451  modprmn0modprm0  12452  coprimeprodsq2  12454  pclemub  12483  pcprendvds2  12487  pcmul  12497  pcneg  12521  fldivp1  12544  prmpwdvds  12551  zgz  12569  4sqexercise1  12594  4sqexercise2  12595  modxai  12612  mulgz  13358  mulgassr  13368  mulgmodid  13369  gsumfzconst  13549  zsubrg  14215  zsssubrg  14219  zringmulg  14232  zringinvg  14238  mulgrhm2  14244  znunit  14293  ef2kpi  15150  efper  15151  sinperlem  15152  sin2kpi  15155  cos2kpi  15156  abssinper  15190  sinkpi  15191  coskpi  15192  cxpexprp  15239  sgmval2  15328  lgslem3  15351  lgsneg  15373  lgsdir2lem2  15378  lgsdir2lem4  15380  lgsdir2  15382  lgssq  15389  lgsmulsqcoprm  15395  lgsdirnn0  15396  gausslemma2dlem3  15412  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2  15432  2lgslem1a2  15436  2lgsoddprmlem1  15454  2lgsoddprmlem2  15455  2sqlem2  15464  2sqlem7  15470