Theorem nn0cnd 8930

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

Syntax hints:   -> wi 4   e. wcel 1461   CCcc 7539   NN0cn0 8875

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-cnex 7630  ax-resscn 7631  ax-1re 7633  ax-addrcl 7636  ax-rnegex 7648

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-sn 3497  df-int 3736  df-inn 8625  df-n0 8876

This theorem is referenced by:  modsumfzodifsn  10056  addmodlteq  10058  uzennn  10096  expaddzaplem  10223  expaddzap  10224  expmulzap  10226  nn0le2msqd  10352  nn0opthlem1d  10353  nn0opthd  10355  nn0opth2d  10356  facdiv  10371  bcp1n  10394  bcn2m1  10402  bcn2p1  10403  omgadd  10435  fihashssdif  10451  hashdifpr  10453  hashxp  10459  zfz1isolemsplit  10468  zfz1isolem1  10470  fsumconst  11109  hash2iun1dif1  11135  binomlem  11138  bcxmas  11144  arisum  11153  arisum2  11154  mertensabs  11192  effsumlt  11243  dvdsexp  11401  nn0ob  11447  divalglemnn  11457  divalgmod  11466  bezoutlemnewy  11524  bezoutlema  11527  bezoutlemb  11528  mulgcd  11544  absmulgcd  11545  mulgcdr  11546  gcddiv  11547  lcmgcd  11599  lcmid  11601  lcm1  11602  3lcm2e6woprm  11607  6lcm4e12  11608  mulgcddvds  11615  qredeu  11618  divgcdcoprm0  11622  divgcdcoprmex  11623  cncongr1  11624  cncongr2  11625  pw2dvdseulemle  11684  phiprmpw  11737