Theorem zcn 9407

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℂcc 7953  ℤcz 9402

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8047

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-rab 2494  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-br 4055  df-iota 5246  df-fv 5293  df-ov 5965  df-neg 8276  df-z 9403

This theorem is referenced by:  zsscn  9410  zaddcllempos  9439  peano2zm  9440  zaddcllemneg  9441  zaddcl  9442  zsubcl  9443  zrevaddcl  9453  nzadd  9455  zlem1lt  9459  zltlem1  9460  zapne  9477  zdiv  9491  zdivadd  9492  zdivmul  9493  zextlt  9495  zneo  9504  zeo2  9509  peano5uzti  9511  zindd  9521  divfnzn  9772  qmulz  9774  zq  9777  qaddcl  9786  qnegcl  9787  qmulcl  9788  qreccl  9793  fzen  10195  uzsubsubfz  10199  fz01en  10205  fzmmmeqm  10210  fzsubel  10212  fztp  10230  fzsuc2  10231  fzrev2  10237  fzrev3  10239  elfzp1b  10249  fzrevral  10257  fzrevral2  10258  fzrevral3  10259  fzshftral  10260  fzo0addel  10349  fzo0addelr  10350  fzoaddel2  10351  fzosubel2  10356  eluzgtdifelfzo  10358  fzocatel  10360  elfzom1elp1fzo  10363  fzval3  10365  zpnn0elfzo1  10369  fzosplitprm1  10395  fzoshftral  10399  flqzadd  10473  2tnp1ge0ge0  10476  ceilid  10492  intfracq  10497  zmod10  10517  modqmuladdnn0  10545  addmodlteq  10575  frecfzen2  10604  seqshft2g  10659  ser3mono  10664  m1expeven  10763  expsubap  10764  zesq  10835  sqoddm1div8  10870  bccmpl  10931  swrd00g  11135  swrdswrd  11191  swrdpfx  11193  shftuz  11213  nnabscl  11496  climshftlemg  11698  climshft  11700  mptfzshft  11838  fsumrev  11839  fisum0diag2  11843  efexp  12078  efzval  12079  demoivre  12169  dvdsval2  12186  iddvds  12200  1dvds  12201  dvds0  12202  negdvdsb  12203  dvdsnegb  12204  0dvds  12207  dvdsmul1  12209  iddvdsexp  12211  muldvds1  12212  muldvds2  12213  dvdscmul  12214  dvdsmulc  12215  summodnegmod  12218  modmulconst  12219  dvds2ln  12220  dvds2add  12221  dvds2sub  12222  dvdstr  12224  dvdssub2  12231  dvdsadd  12232  dvdsaddr  12233  dvdssub  12234  dvdssubr  12235  dvdsadd2b  12236  dvdsabseq  12243  divconjdvds  12245  alzdvds  12250  addmodlteqALT  12255  zeo3  12264  odd2np1lem  12268  odd2np1  12269  even2n  12270  oddp1even  12272  mulsucdiv2z  12281  zob  12287  ltoddhalfle  12289  halfleoddlt  12290  opoe  12291  omoe  12292  opeo  12293  omeo  12294  m1exp1  12297  divalgb  12321  divalgmod  12323  modremain  12325  ndvdssub  12326  ndvdsadd  12327  flodddiv4  12332  flodddiv4t2lthalf  12335  bits0  12344  bitsp1e  12348  bitsp1o  12349  gcdneg  12388  gcdadd  12391  gcdid  12392  modgcd  12397  dvdsgcd  12418  mulgcd  12422  absmulgcd  12423  mulgcdr  12424  gcddiv  12425  gcdmultiplez  12427  dvdssqim  12430  dvdssq  12437  bezoutr1  12439  lcmneg  12481  lcmgcdlem  12484  lcmgcd  12485  lcmid  12487  lcm1  12488  coprmdvds  12499  coprmdvds2  12500  qredeq  12503  qredeu  12504  divgcdcoprmex  12509  cncongr1  12510  cncongr2  12511  prmdvdsexp  12555  rpexp1i  12561  sqrt2irr  12569  divnumden  12603  phiprmpw  12629  nnnn0modprm0  12663  modprmn0modprm0  12664  coprimeprodsq2  12666  pclemub  12695  pcprendvds2  12699  pcmul  12709  pcneg  12733  fldivp1  12756  prmpwdvds  12763  zgz  12781  4sqexercise1  12806  4sqexercise2  12807  modxai  12824  mulgz  13571  mulgassr  13581  mulgmodid  13582  gsumfzconst  13762  zsubrg  14428  zsssubrg  14432  zringmulg  14445  zringinvg  14451  mulgrhm2  14457  znunit  14506  ef2kpi  15363  efper  15364  sinperlem  15365  sin2kpi  15368  cos2kpi  15369  abssinper  15403  sinkpi  15404  coskpi  15405  cxpexprp  15452  sgmval2  15541  lgslem3  15564  lgsneg  15586  lgsdir2lem2  15591  lgsdir2lem4  15593  lgsdir2  15595  lgssq  15602  lgsmulsqcoprm  15608  lgsdirnn0  15609  gausslemma2dlem3  15625  lgsquadlem1  15639  lgsquadlem2  15640  lgsquad2  15645  2lgslem1a2  15649  2lgsoddprmlem1  15667  2lgsoddprmlem2  15668  2sqlem2  15677  2sqlem7  15683