Theorem nn0cnd 9601

Description: A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nn0red.1	|- ( ph -> A e. NN0 )

Assertion

Ref	Expression
nn0cnd	|- ( ph -> A e. CC )

Proof of Theorem nn0cnd

Step	Hyp	Ref	Expression
1		nn0red.1	. . 3 |- ( ph -> A e. NN0 )
2	1	nn0red 9600	. 2 |- ( ph -> A e. RR )
3	2	recnd 8344	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2209   CCcc 8167   NN0cn0 9542

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4244  ax-cnex 8260  ax-resscn 8261  ax-1re 8263  ax-addrcl 8266  ax-rnegex 8278

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3711  df-int 3966  df-inn 9284  df-n0 9543

This theorem is referenced by:  modsumfzodifsn  10811  addmodlteq  10813  uzennn  10851  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  nn0le2msqd  11135  nn0opthlem1d  11136  nn0opthd  11138  nn0opth2d  11139  facdiv  11154  bcp1n  11177  bcn2m1  11186  bcn2p1  11187  omgadd  11220  fihashssdif  11237  hashdifpr  11239  hashxp  11245  hashmap  11246  hashfibclem  11260  hashf1lem2  11264  hashf1  11265  zfz1isolemsplit  11268  zfz1isolem1  11270  ccatval3  11345  ccatval21sw  11351  ccatlid  11352  ccatrid  11353  ccatass  11354  ccatrn  11355  lswccatn0lsw  11357  ccatalpha  11359  ccatws1lenp1bg  11381  wrdlenccats1lenm1g  11382  ccats1val2  11386  lswccats1  11389  swrdccat2  11421  pfxfv  11434  addlenpfx  11441  pfxtrcfvl  11447  pfxpfx  11458  lenrevpfxcctswrd  11462  ccats1pfxeq  11464  ccatopth2  11467  cats1un  11471  swrdccat3b  11490  cats1fvnd  11515  fsumconst  12199  hash2iun1dif1  12225  binomlem  12228  bcxmas  12234  arisum  12243  arisum2  12244  mertensabs  12282  effsumlt  12437  dvdsexp  12606  nn0ob  12653  divalglemnn  12663  divalgmod  12672  bitsinv1lem  12706  bezoutlemnewy  12751  bezoutlema  12754  bezoutlemb  12755  mulgcd  12771  absmulgcd  12772  mulgcdr  12773  gcddiv  12774  lcmgcd  12834  lcmid  12836  lcm1  12837  3lcm2e6woprm  12842  6lcm4e12  12843  mulgcddvds  12850  qredeu  12853  divgcdcoprm0  12857  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  pw2dvdseulemle  12923  phiprmpw  12978  eulerthlema  12986  prmdiveq  12992  odzdvds  13002  powm2modprm  13009  coprimeprodsq  13014  pceulem  13051  pczpre  13054  pcqmul  13060  pcaddlem  13096  pcmpt  13100  pcmpt2  13101  sumhashdc  13104  pcfac  13107  oddprmdvds  13111  mul4sq  13151  4sqlem12  13159  ballotfilemfp1  13209  ballotfilemgun  13246  mulgnn0dir  13932  mulgnn0ass  13938  plyaddlem1  15771  plymullem1  15772  dvply1  15789  dvply2g  15790  0sgm  16013  sgmppw  16020  lgslem1  16033  lgsvalmod  16052  gausslemma2dlem6  16100  gausslemma2d  16102  lgseisenlem2  16104  lgseisenlem3  16105  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem2  16115  m1lgs  16118  2lgslem1c  16123  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2sqlem8  16156  vtxdfifiun  16452  vtxdumgrfival  16453  p1evtxdeqfi  16467  wlklenvm1  16496  wlklenvm1g  16497  wlklenvclwlk  16528  clwwlkccatlem  16555  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626  depindlem1  16661