Theorem nn0cnd 9457

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 9456	. 2 |- ( ph -> A e. RR )
3	2	recnd 8208	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8030   NN0cn0 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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-int 3929  df-inn 9144  df-n0 9403

This theorem is referenced by:  modsumfzodifsn  10659  addmodlteq  10661  uzennn  10699  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  nn0le2msqd  10982  nn0opthlem1d  10983  nn0opthd  10985  nn0opth2d  10986  facdiv  11001  bcp1n  11024  bcn2m1  11032  bcn2p1  11033  omgadd  11066  fihashssdif  11083  hashdifpr  11085  hashxp  11091  zfz1isolemsplit  11103  zfz1isolem1  11105  ccatval3  11180  ccatval21sw  11186  ccatlid  11187  ccatrid  11188  ccatass  11189  ccatrn  11190  lswccatn0lsw  11192  ccatalpha  11194  ccatws1lenp1bg  11216  wrdlenccats1lenm1g  11217  ccats1val2  11221  lswccats1  11224  swrdccat2  11256  pfxfv  11269  addlenpfx  11276  pfxtrcfvl  11282  pfxpfx  11293  lenrevpfxcctswrd  11297  ccats1pfxeq  11299  ccatopth2  11302  cats1un  11306  swrdccat3b  11325  cats1fvnd  11350  fsumconst  12033  hash2iun1dif1  12059  binomlem  12062  bcxmas  12068  arisum  12077  arisum2  12078  mertensabs  12116  effsumlt  12271  dvdsexp  12440  nn0ob  12487  divalglemnn  12497  divalgmod  12506  bitsinv1lem  12540  bezoutlemnewy  12585  bezoutlema  12588  bezoutlemb  12589  mulgcd  12605  absmulgcd  12606  mulgcdr  12607  gcddiv  12608  lcmgcd  12668  lcmid  12670  lcm1  12671  3lcm2e6woprm  12676  6lcm4e12  12677  mulgcddvds  12684  qredeu  12687  divgcdcoprm0  12691  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  pw2dvdseulemle  12757  phiprmpw  12812  eulerthlema  12820  prmdiveq  12826  odzdvds  12836  powm2modprm  12843  coprimeprodsq  12848  pceulem  12885  pczpre  12888  pcqmul  12894  pcaddlem  12930  pcmpt  12934  pcmpt2  12935  sumhashdc  12938  pcfac  12941  oddprmdvds  12945  mul4sq  12985  4sqlem12  12993  mulgnn0dir  13757  mulgnn0ass  13763  plyaddlem1  15490  plymullem1  15491  dvply1  15508  dvply2g  15509  0sgm  15728  sgmppw  15735  lgslem1  15748  lgsvalmod  15767  gausslemma2dlem6  15815  gausslemma2d  15817  lgseisenlem2  15819  lgseisenlem3  15820  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem2  15830  m1lgs  15833  2lgslem1c  15838  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2sqlem8  15871  vtxdfifiun  16167  vtxdumgrfival  16168  p1evtxdeqfi  16182  wlklenvm1  16211  wlklenvm1g  16212  wlklenvclwlk  16243  clwwlkccatlem  16270  eupth2lem3lem3fi  16340  eupth2lem3lem6fi  16341  depindlem1  16376