Theorem nn0cnd 9230

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7808   NN0cn0 9175

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 4121  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907  ax-rnegex 7919

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 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-int 3845  df-inn 8919  df-n0 9176

This theorem is referenced by:  modsumfzodifsn  10395  addmodlteq  10397  uzennn  10435  expaddzaplem  10562  expaddzap  10563  expmulzap  10565  nn0le2msqd  10698  nn0opthlem1d  10699  nn0opthd  10701  nn0opth2d  10702  facdiv  10717  bcp1n  10740  bcn2m1  10748  bcn2p1  10749  omgadd  10781  fihashssdif  10797  hashdifpr  10799  hashxp  10805  zfz1isolemsplit  10817  zfz1isolem1  10819  fsumconst  11461  hash2iun1dif1  11487  binomlem  11490  bcxmas  11496  arisum  11505  arisum2  11506  mertensabs  11544  effsumlt  11699  dvdsexp  11866  nn0ob  11912  divalglemnn  11922  divalgmod  11931  bezoutlemnewy  11996  bezoutlema  11999  bezoutlemb  12000  mulgcd  12016  absmulgcd  12017  mulgcdr  12018  gcddiv  12019  lcmgcd  12077  lcmid  12079  lcm1  12080  3lcm2e6woprm  12085  6lcm4e12  12086  mulgcddvds  12093  qredeu  12096  divgcdcoprm0  12100  divgcdcoprmex  12101  cncongr1  12102  cncongr2  12103  pw2dvdseulemle  12166  phiprmpw  12221  eulerthlema  12229  prmdiveq  12235  odzdvds  12244  powm2modprm  12251  coprimeprodsq  12256  pceulem  12293  pczpre  12296  pcqmul  12302  pcaddlem  12337  pcmpt  12340  pcmpt2  12341  sumhashdc  12344  pcfac  12347  oddprmdvds  12351  mul4sq  12391  mulgnn0dir  13011  mulgnn0ass  13017  lgslem1  14371  lgsvalmod  14390  lgseisenlem2  14421  m1lgs  14422  2sqlem8  14440