Theorem nn0cnd 9575

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

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8141   NN0cn0 9516

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-int 3955  df-inn 9258  df-n0 9517

This theorem is referenced by:  modsumfzodifsn  10785  addmodlteq  10787  uzennn  10825  expaddzaplem  10971  expaddzap  10972  expmulzap  10974  nn0le2msqd  11109  nn0opthlem1d  11110  nn0opthd  11112  nn0opth2d  11113  facdiv  11128  bcp1n  11151  bcn2m1  11160  bcn2p1  11161  omgadd  11194  fihashssdif  11211  hashdifpr  11213  hashxp  11219  hashmap  11220  hashfibclem  11234  zfz1isolemsplit  11238  zfz1isolem1  11240  ccatval3  11315  ccatval21sw  11321  ccatlid  11322  ccatrid  11323  ccatass  11324  ccatrn  11325  lswccatn0lsw  11327  ccatalpha  11329  ccatws1lenp1bg  11351  wrdlenccats1lenm1g  11352  ccats1val2  11356  lswccats1  11359  swrdccat2  11391  pfxfv  11404  addlenpfx  11411  pfxtrcfvl  11417  pfxpfx  11428  lenrevpfxcctswrd  11432  ccats1pfxeq  11434  ccatopth2  11437  cats1un  11441  swrdccat3b  11460  cats1fvnd  11485  fsumconst  12169  hash2iun1dif1  12195  binomlem  12198  bcxmas  12204  arisum  12213  arisum2  12214  mertensabs  12252  effsumlt  12407  dvdsexp  12576  nn0ob  12623  divalglemnn  12633  divalgmod  12642  bitsinv1lem  12676  bezoutlemnewy  12721  bezoutlema  12724  bezoutlemb  12725  mulgcd  12741  absmulgcd  12742  mulgcdr  12743  gcddiv  12744  lcmgcd  12804  lcmid  12806  lcm1  12807  3lcm2e6woprm  12812  6lcm4e12  12813  mulgcddvds  12820  qredeu  12823  divgcdcoprm0  12827  divgcdcoprmex  12828  cncongr1  12829  cncongr2  12830  pw2dvdseulemle  12893  phiprmpw  12948  eulerthlema  12956  prmdiveq  12962  odzdvds  12972  powm2modprm  12979  coprimeprodsq  12984  pceulem  13021  pczpre  13024  pcqmul  13030  pcaddlem  13066  pcmpt  13070  pcmpt2  13071  sumhashdc  13074  pcfac  13077  oddprmdvds  13081  mul4sq  13121  4sqlem12  13129  ballotfilemfp1  13179  ballotfilemgun  13216  mulgnn0dir  13909  mulgnn0ass  13915  plyaddlem1  15742  plymullem1  15743  dvply1  15760  dvply2g  15761  0sgm  15983  sgmppw  15990  lgslem1  16003  lgsvalmod  16022  gausslemma2dlem6  16070  gausslemma2d  16072  lgseisenlem2  16074  lgseisenlem3  16075  lgsquadlem1  16080  lgsquadlem2  16081  lgsquad2lem2  16085  m1lgs  16088  2lgslem1c  16093  2lgslem3a  16096  2lgslem3b  16097  2lgslem3c  16098  2lgslem3d  16099  2sqlem8  16126  vtxdfifiun  16422  vtxdumgrfival  16423  p1evtxdeqfi  16437  wlklenvm1  16466  wlklenvm1g  16467  wlklenvclwlk  16498  clwwlkccatlem  16525  eupth2lem3lem3fi  16595  eupth2lem3lem6fi  16596  depindlem1  16631