Theorem zcn 9376

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

Syntax hints:   → wi 4   ∈ wcel 2175  ℂcc 7922  ℤcz 9371

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-resscn 8016

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-rab 2492  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278  df-ov 5946  df-neg 8245  df-z 9372

This theorem is referenced by:  zsscn  9379  zaddcllempos  9408  peano2zm  9409  zaddcllemneg  9410  zaddcl  9411  zsubcl  9412  zrevaddcl  9422  nzadd  9424  zlem1lt  9428  zltlem1  9429  zapne  9446  zdiv  9460  zdivadd  9461  zdivmul  9462  zextlt  9464  zneo  9473  zeo2  9478  peano5uzti  9480  zindd  9490  divfnzn  9741  qmulz  9743  zq  9746  qaddcl  9755  qnegcl  9756  qmulcl  9757  qreccl  9762  fzen  10164  uzsubsubfz  10168  fz01en  10174  fzmmmeqm  10179  fzsubel  10181  fztp  10199  fzsuc2  10200  fzrev2  10206  fzrev3  10208  elfzp1b  10218  fzrevral  10226  fzrevral2  10227  fzrevral3  10228  fzshftral  10229  fzo0addel  10315  fzo0addelr  10316  fzoaddel2  10317  fzosubel2  10322  eluzgtdifelfzo  10324  fzocatel  10326  elfzom1elp1fzo  10329  fzval3  10331  zpnn0elfzo1  10335  fzosplitprm1  10361  fzoshftral  10365  flqzadd  10439  2tnp1ge0ge0  10442  ceilid  10458  intfracq  10463  zmod10  10483  modqmuladdnn0  10511  addmodlteq  10541  frecfzen2  10570  seqshft2g  10625  ser3mono  10630  m1expeven  10729  expsubap  10730  zesq  10801  sqoddm1div8  10836  bccmpl  10897  shftuz  11099  nnabscl  11382  climshftlemg  11584  climshft  11586  mptfzshft  11724  fsumrev  11725  fisum0diag2  11729  efexp  11964  efzval  11965  demoivre  12055  dvdsval2  12072  iddvds  12086  1dvds  12087  dvds0  12088  negdvdsb  12089  dvdsnegb  12090  0dvds  12093  dvdsmul1  12095  iddvdsexp  12097  muldvds1  12098  muldvds2  12099  dvdscmul  12100  dvdsmulc  12101  summodnegmod  12104  modmulconst  12105  dvds2ln  12106  dvds2add  12107  dvds2sub  12108  dvdstr  12110  dvdssub2  12117  dvdsadd  12118  dvdsaddr  12119  dvdssub  12120  dvdssubr  12121  dvdsadd2b  12122  dvdsabseq  12129  divconjdvds  12131  alzdvds  12136  addmodlteqALT  12141  zeo3  12150  odd2np1lem  12154  odd2np1  12155  even2n  12156  oddp1even  12158  mulsucdiv2z  12167  zob  12173  ltoddhalfle  12175  halfleoddlt  12176  opoe  12177  omoe  12178  opeo  12179  omeo  12180  m1exp1  12183  divalgb  12207  divalgmod  12209  modremain  12211  ndvdssub  12212  ndvdsadd  12213  flodddiv4  12218  flodddiv4t2lthalf  12221  bits0  12230  bitsp1e  12234  bitsp1o  12235  gcdneg  12274  gcdadd  12277  gcdid  12278  modgcd  12283  dvdsgcd  12304  mulgcd  12308  absmulgcd  12309  mulgcdr  12310  gcddiv  12311  gcdmultiplez  12313  dvdssqim  12316  dvdssq  12323  bezoutr1  12325  lcmneg  12367  lcmgcdlem  12370  lcmgcd  12371  lcmid  12373  lcm1  12374  coprmdvds  12385  coprmdvds2  12386  qredeq  12389  qredeu  12390  divgcdcoprmex  12395  cncongr1  12396  cncongr2  12397  prmdvdsexp  12441  rpexp1i  12447  sqrt2irr  12455  divnumden  12489  phiprmpw  12515  nnnn0modprm0  12549  modprmn0modprm0  12550  coprimeprodsq2  12552  pclemub  12581  pcprendvds2  12585  pcmul  12595  pcneg  12619  fldivp1  12642  prmpwdvds  12649  zgz  12667  4sqexercise1  12692  4sqexercise2  12693  modxai  12710  mulgz  13457  mulgassr  13467  mulgmodid  13468  gsumfzconst  13648  zsubrg  14314  zsssubrg  14318  zringmulg  14331  zringinvg  14337  mulgrhm2  14343  znunit  14392  ef2kpi  15249  efper  15250  sinperlem  15251  sin2kpi  15254  cos2kpi  15255  abssinper  15289  sinkpi  15290  coskpi  15291  cxpexprp  15338  sgmval2  15427  lgslem3  15450  lgsneg  15472  lgsdir2lem2  15477  lgsdir2lem4  15479  lgsdir2  15481  lgssq  15488  lgsmulsqcoprm  15494  lgsdirnn0  15495  gausslemma2dlem3  15511  lgsquadlem1  15525  lgsquadlem2  15526  lgsquad2  15531  2lgslem1a2  15535  2lgsoddprmlem1  15553  2lgsoddprmlem2  15554  2sqlem2  15563  2sqlem7  15569