Theorem nn0cnd 9231

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7809   NN0cn0 9176

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4122  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908  ax-rnegex 7920

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-int 3846  df-inn 8920  df-n0 9177

This theorem is referenced by:  modsumfzodifsn  10396  addmodlteq  10398  uzennn  10436  expaddzaplem  10563  expaddzap  10564  expmulzap  10566  nn0le2msqd  10699  nn0opthlem1d  10700  nn0opthd  10702  nn0opth2d  10703  facdiv  10718  bcp1n  10741  bcn2m1  10749  bcn2p1  10750  omgadd  10782  fihashssdif  10798  hashdifpr  10800  hashxp  10806  zfz1isolemsplit  10818  zfz1isolem1  10820  fsumconst  11462  hash2iun1dif1  11488  binomlem  11491  bcxmas  11497  arisum  11506  arisum2  11507  mertensabs  11545  effsumlt  11700  dvdsexp  11867  nn0ob  11913  divalglemnn  11923  divalgmod  11932  bezoutlemnewy  11997  bezoutlema  12000  bezoutlemb  12001  mulgcd  12017  absmulgcd  12018  mulgcdr  12019  gcddiv  12020  lcmgcd  12078  lcmid  12080  lcm1  12081  3lcm2e6woprm  12086  6lcm4e12  12087  mulgcddvds  12094  qredeu  12097  divgcdcoprm0  12101  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  pw2dvdseulemle  12167  phiprmpw  12222  eulerthlema  12230  prmdiveq  12236  odzdvds  12245  powm2modprm  12252  coprimeprodsq  12257  pceulem  12294  pczpre  12297  pcqmul  12303  pcaddlem  12338  pcmpt  12341  pcmpt2  12342  sumhashdc  12345  pcfac  12348  oddprmdvds  12352  mul4sq  12392  mulgnn0dir  13013  mulgnn0ass  13019  lgslem1  14404  lgsvalmod  14423  lgseisenlem2  14454  m1lgs  14455  2sqlem8  14473