Theorem nn0cnd 9245

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

Syntax hints:   -> wi 4   e. wcel 2158   CCcc 7823   NN0cn0 9190

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169  ax-sep 4133  ax-cnex 7916  ax-resscn 7917  ax-1re 7919  ax-addrcl 7922  ax-rnegex 7934

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-v 2751  df-un 3145  df-in 3147  df-ss 3154  df-sn 3610  df-int 3857  df-inn 8934  df-n0 9191

This theorem is referenced by:  modsumfzodifsn  10410  addmodlteq  10412  uzennn  10450  expaddzaplem  10577  expaddzap  10578  expmulzap  10580  nn0le2msqd  10713  nn0opthlem1d  10714  nn0opthd  10716  nn0opth2d  10717  facdiv  10732  bcp1n  10755  bcn2m1  10763  bcn2p1  10764  omgadd  10796  fihashssdif  10812  hashdifpr  10814  hashxp  10820  zfz1isolemsplit  10832  zfz1isolem1  10834  fsumconst  11476  hash2iun1dif1  11502  binomlem  11505  bcxmas  11511  arisum  11520  arisum2  11521  mertensabs  11559  effsumlt  11714  dvdsexp  11881  nn0ob  11927  divalglemnn  11937  divalgmod  11946  bezoutlemnewy  12011  bezoutlema  12014  bezoutlemb  12015  mulgcd  12031  absmulgcd  12032  mulgcdr  12033  gcddiv  12034  lcmgcd  12092  lcmid  12094  lcm1  12095  3lcm2e6woprm  12100  6lcm4e12  12101  mulgcddvds  12108  qredeu  12111  divgcdcoprm0  12115  divgcdcoprmex  12116  cncongr1  12117  cncongr2  12118  pw2dvdseulemle  12181  phiprmpw  12236  eulerthlema  12244  prmdiveq  12250  odzdvds  12259  powm2modprm  12266  coprimeprodsq  12271  pceulem  12308  pczpre  12311  pcqmul  12317  pcaddlem  12352  pcmpt  12355  pcmpt2  12356  sumhashdc  12359  pcfac  12362  oddprmdvds  12366  mul4sq  12406  mulgnn0dir  13053  mulgnn0ass  13059  lgslem1  14754  lgsvalmod  14773  lgseisenlem2  14804  m1lgs  14805  2sqlem8  14823