Theorem nn0cnd 9352

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

Syntax hints:   -> wi 4   e. wcel 2176   CCcc 7925   NN0cn0 9297

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163  ax-cnex 8018  ax-resscn 8019  ax-1re 8021  ax-addrcl 8024  ax-rnegex 8036

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-int 3886  df-inn 9039  df-n0 9298

This theorem is referenced by:  modsumfzodifsn  10543  addmodlteq  10545  uzennn  10583  expaddzaplem  10729  expaddzap  10730  expmulzap  10732  nn0le2msqd  10866  nn0opthlem1d  10867  nn0opthd  10869  nn0opth2d  10870  facdiv  10885  bcp1n  10908  bcn2m1  10916  bcn2p1  10917  omgadd  10949  fihashssdif  10965  hashdifpr  10967  hashxp  10973  zfz1isolemsplit  10985  zfz1isolem1  10987  ccatval3  11058  ccatval21sw  11064  ccatlid  11065  ccatrid  11066  ccatass  11067  ccatrn  11068  lswccatn0lsw  11070  ccatws1lenp1bg  11092  ccats1val2  11095  lswccats1  11098  swrdccat2  11127  pfxfv  11138  addlenpfx  11145  pfxtrcfvl  11151  fsumconst  11798  hash2iun1dif1  11824  binomlem  11827  bcxmas  11833  arisum  11842  arisum2  11843  mertensabs  11881  effsumlt  12036  dvdsexp  12205  nn0ob  12252  divalglemnn  12262  divalgmod  12271  bitsinv1lem  12305  bezoutlemnewy  12350  bezoutlema  12353  bezoutlemb  12354  mulgcd  12370  absmulgcd  12371  mulgcdr  12372  gcddiv  12373  lcmgcd  12433  lcmid  12435  lcm1  12436  3lcm2e6woprm  12441  6lcm4e12  12442  mulgcddvds  12449  qredeu  12452  divgcdcoprm0  12456  divgcdcoprmex  12457  cncongr1  12458  cncongr2  12459  pw2dvdseulemle  12522  phiprmpw  12577  eulerthlema  12585  prmdiveq  12591  odzdvds  12601  powm2modprm  12608  coprimeprodsq  12613  pceulem  12650  pczpre  12653  pcqmul  12659  pcaddlem  12695  pcmpt  12699  pcmpt2  12700  sumhashdc  12703  pcfac  12706  oddprmdvds  12710  mul4sq  12750  4sqlem12  12758  mulgnn0dir  13521  mulgnn0ass  13527  plyaddlem1  15252  plymullem1  15253  dvply1  15270  dvply2g  15271  0sgm  15490  sgmppw  15497  lgslem1  15510  lgsvalmod  15529  gausslemma2dlem6  15577  gausslemma2d  15579  lgseisenlem2  15581  lgseisenlem3  15582  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem2  15592  m1lgs  15595  2lgslem1c  15600  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2sqlem8  15633