Theorem nn0cnd 9424

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 7997   NN0cn0 9369

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8090  ax-resscn 8091  ax-1re 8093  ax-addrcl 8096  ax-rnegex 8108

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-int 3924  df-inn 9111  df-n0 9370

This theorem is referenced by:  modsumfzodifsn  10618  addmodlteq  10620  uzennn  10658  expaddzaplem  10804  expaddzap  10805  expmulzap  10807  nn0le2msqd  10941  nn0opthlem1d  10942  nn0opthd  10944  nn0opth2d  10945  facdiv  10960  bcp1n  10983  bcn2m1  10991  bcn2p1  10992  omgadd  11024  fihashssdif  11040  hashdifpr  11042  hashxp  11048  zfz1isolemsplit  11060  zfz1isolem1  11062  ccatval3  11134  ccatval21sw  11140  ccatlid  11141  ccatrid  11142  ccatass  11143  ccatrn  11144  lswccatn0lsw  11146  ccatws1lenp1bg  11168  ccats1val2  11171  lswccats1  11174  swrdccat2  11203  pfxfv  11216  addlenpfx  11223  pfxtrcfvl  11229  pfxpfx  11240  lenrevpfxcctswrd  11244  ccats1pfxeq  11246  ccatopth2  11249  cats1un  11253  swrdccat3b  11272  cats1fvnd  11297  fsumconst  11965  hash2iun1dif1  11991  binomlem  11994  bcxmas  12000  arisum  12009  arisum2  12010  mertensabs  12048  effsumlt  12203  dvdsexp  12372  nn0ob  12419  divalglemnn  12429  divalgmod  12438  bitsinv1lem  12472  bezoutlemnewy  12517  bezoutlema  12520  bezoutlemb  12521  mulgcd  12537  absmulgcd  12538  mulgcdr  12539  gcddiv  12540  lcmgcd  12600  lcmid  12602  lcm1  12603  3lcm2e6woprm  12608  6lcm4e12  12609  mulgcddvds  12616  qredeu  12619  divgcdcoprm0  12623  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  pw2dvdseulemle  12689  phiprmpw  12744  eulerthlema  12752  prmdiveq  12758  odzdvds  12768  powm2modprm  12775  coprimeprodsq  12780  pceulem  12817  pczpre  12820  pcqmul  12826  pcaddlem  12862  pcmpt  12866  pcmpt2  12867  sumhashdc  12870  pcfac  12873  oddprmdvds  12877  mul4sq  12917  4sqlem12  12925  mulgnn0dir  13689  mulgnn0ass  13695  plyaddlem1  15421  plymullem1  15422  dvply1  15439  dvply2g  15440  0sgm  15659  sgmppw  15666  lgslem1  15679  lgsvalmod  15698  gausslemma2dlem6  15746  gausslemma2d  15748  lgseisenlem2  15750  lgseisenlem3  15751  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem2  15761  m1lgs  15764  2lgslem1c  15769  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2sqlem8  15802  wlklenvm1  16052  wlklenvm1g  16053  wlklenvclwlk  16084