Theorem nn0cnd 9321

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

Syntax hints:   -> wi 4   e. wcel 2167   CCcc 7894   NN0cn0 9266

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7987  ax-resscn 7988  ax-1re 7990  ax-addrcl 7993  ax-rnegex 8005

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-int 3876  df-inn 9008  df-n0 9267

This theorem is referenced by:  modsumfzodifsn  10505  addmodlteq  10507  uzennn  10545  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  nn0le2msqd  10828  nn0opthlem1d  10829  nn0opthd  10831  nn0opth2d  10832  facdiv  10847  bcp1n  10870  bcn2m1  10878  bcn2p1  10879  omgadd  10911  fihashssdif  10927  hashdifpr  10929  hashxp  10935  zfz1isolemsplit  10947  zfz1isolem1  10949  fsumconst  11636  hash2iun1dif1  11662  binomlem  11665  bcxmas  11671  arisum  11680  arisum2  11681  mertensabs  11719  effsumlt  11874  dvdsexp  12043  nn0ob  12090  divalglemnn  12100  divalgmod  12109  bitsinv1lem  12143  bezoutlemnewy  12188  bezoutlema  12191  bezoutlemb  12192  mulgcd  12208  absmulgcd  12209  mulgcdr  12210  gcddiv  12211  lcmgcd  12271  lcmid  12273  lcm1  12274  3lcm2e6woprm  12279  6lcm4e12  12280  mulgcddvds  12287  qredeu  12290  divgcdcoprm0  12294  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  pw2dvdseulemle  12360  phiprmpw  12415  eulerthlema  12423  prmdiveq  12429  odzdvds  12439  powm2modprm  12446  coprimeprodsq  12451  pceulem  12488  pczpre  12491  pcqmul  12497  pcaddlem  12533  pcmpt  12537  pcmpt2  12538  sumhashdc  12541  pcfac  12544  oddprmdvds  12548  mul4sq  12588  4sqlem12  12596  mulgnn0dir  13358  mulgnn0ass  13364  plyaddlem1  15067  plymullem1  15068  dvply1  15085  dvply2g  15086  0sgm  15305  sgmppw  15312  lgslem1  15325  lgsvalmod  15344  gausslemma2dlem6  15392  gausslemma2d  15394  lgseisenlem2  15396  lgseisenlem3  15397  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem2  15407  m1lgs  15410  2lgslem1c  15415  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2sqlem8  15448