Theorem nn0cnd 9626

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   NN0cn0 9567

This proof depends on 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 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276  ax-rnegex 8288

This proof 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 3715  df-int 3971  df-inn 9307  df-n0 9568

This theorem is used by:  modsumfzodifsn  10846  addmodlteq  10848  uzennn  10886  expaddzaplem  11032  expaddzap  11033  expmulzap  11035  nn0le2msqd  11171  nn0opthlem1d  11172  nn0opthd  11174  nn0opth2d  11175  facdiv  11190  bcp1n  11213  bcn2m1  11222  bcn2p1  11223  omgadd  11256  fihashssdif  11273  hashdifpr  11275  hashxp  11281  hashmap  11282  hashfibclem  11296  hashf1lem2  11300  hashf1  11301  zfz1isolemsplit  11304  zfz1isolem1  11306  ccatval3  11381  ccatval21sw  11387  ccatlid  11388  ccatrid  11389  ccatass  11390  ccatrn  11391  lswccatn0lsw  11393  ccatalpha  11395  ccatws1lenp1bg  11417  wrdlenccats1lenm1g  11418  ccats1val2  11422  lswccats1  11425  swrdccat2  11457  pfxfv  11470  addlenpfx  11477  pfxtrcfvl  11483  pfxpfx  11494  lenrevpfxcctswrd  11498  ccats1pfxeq  11500  ccatopth2  11503  cats1un  11507  swrdccat3b  11526  cats1fvnd  11551  fsumconst  12237  hash2iun1dif1  12263  binomlem  12266  bcxmas  12272  arisum  12281  arisum2  12282  mertensabs  12320  effsumlt  12475  dvdsexp  12644  nn0ob  12691  divalglemnn  12701  divalgmod  12710  bitsinv1lem  12744  bezoutlemnewy  12789  bezoutlema  12792  bezoutlemb  12793  mulgcd  12809  absmulgcd  12810  mulgcdr  12811  gcddiv  12812  lcmgcd  12872  lcmid  12874  lcm1  12875  3lcm2e6woprm  12880  6lcm4e12  12881  mulgcddvds  12888  qredeu  12891  divgcdcoprm0  12895  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  pwbdvdseulemle  12962  phiprmpw  13020  eulerthlema  13028  prmdiveq  13034  odzdvds  13044  powm2modprm  13051  coprimeprodsq  13056  pceulem  13093  pczpre  13096  pcqmul  13102  pcaddlem  13138  pcmpt  13142  pcmpt2  13143  sumhashdc  13146  pcfac  13149  oddprmdvds  13153  mul4sq  13193  4sqlem12  13201  ballotfilemfp1  13280  ballotfilemgun  13317  mulgnn0dir  14004  mulgnn0ass  14010  plyaddlem1  15897  plymullem1  15898  dvply1  15915  dvply2g  15916  zprmlogbaplem2  16135  birthdaylem2  16145  0sgm  16166  ppidif  16175  sgmppw  16187  bcp1ctr  16204  lgslem1  16217  lgsvalmod  16236  gausslemma2dlem6  16284  gausslemma2d  16286  lgseisenlem2  16288  lgseisenlem3  16289  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem2  16299  m1lgs  16302  2lgslem1c  16307  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2sqlem8  16340  vtxdfifiun  16636  vtxdumgrfival  16637  p1evtxdeqfi  16651  wlklenvm1  16680  wlklenvm1g  16681  wlklenvclwlk  16712  clwwlkccatlem  16739  eupth2lem3lem3fi  16809  eupth2lem3lem6fi  16810  depindlem1  16845