Theorem nn0cnd 9165

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

Syntax hints:   -> wi 4   e. wcel 2136   CCcc 7747   NN0cn0 9110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4099  ax-cnex 7840  ax-resscn 7841  ax-1re 7843  ax-addrcl 7846  ax-rnegex 7858

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-rex 2449  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-sn 3581  df-int 3824  df-inn 8854  df-n0 9111

This theorem is referenced by:  modsumfzodifsn  10327  addmodlteq  10329  uzennn  10367  expaddzaplem  10494  expaddzap  10495  expmulzap  10497  nn0le2msqd  10628  nn0opthlem1d  10629  nn0opthd  10631  nn0opth2d  10632  facdiv  10647  bcp1n  10670  bcn2m1  10678  bcn2p1  10679  omgadd  10711  fihashssdif  10727  hashdifpr  10729  hashxp  10735  zfz1isolemsplit  10747  zfz1isolem1  10749  fsumconst  11391  hash2iun1dif1  11417  binomlem  11420  bcxmas  11426  arisum  11435  arisum2  11436  mertensabs  11474  effsumlt  11629  dvdsexp  11795  nn0ob  11841  divalglemnn  11851  divalgmod  11860  bezoutlemnewy  11925  bezoutlema  11928  bezoutlemb  11929  mulgcd  11945  absmulgcd  11946  mulgcdr  11947  gcddiv  11948  lcmgcd  12006  lcmid  12008  lcm1  12009  3lcm2e6woprm  12014  6lcm4e12  12015  mulgcddvds  12022  qredeu  12025  divgcdcoprm0  12029  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  pw2dvdseulemle  12095  phiprmpw  12150  eulerthlema  12158  prmdiveq  12164  odzdvds  12173  powm2modprm  12180  coprimeprodsq  12185  pceulem  12222  pczpre  12225  pcqmul  12231  pcaddlem  12266  pcmpt  12269  pcmpt2  12270  sumhashdc  12273  pcfac  12276  oddprmdvds  12280  mul4sq  12320  lgslem1  13501  lgsvalmod  13520  2sqlem8  13559