Theorem nn0cnd 9447

Description: A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nn0red.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Assertion

Ref	Expression
nn0cnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem nn0cnd

Step	Hyp	Ref	Expression
1		nn0red.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
2	1	nn0red 9446	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 8198	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8020  ℕ₀cn0 9392

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119  ax-rnegex 8131

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-int 3927  df-inn 9134  df-n0 9393

This theorem is referenced by:  modsumfzodifsn  10648  addmodlteq  10650  uzennn  10688  expaddzaplem  10834  expaddzap  10835  expmulzap  10837  nn0le2msqd  10971  nn0opthlem1d  10972  nn0opthd  10974  nn0opth2d  10975  facdiv  10990  bcp1n  11013  bcn2m1  11021  bcn2p1  11022  omgadd  11055  fihashssdif  11072  hashdifpr  11074  hashxp  11080  zfz1isolemsplit  11092  zfz1isolem1  11094  ccatval3  11166  ccatval21sw  11172  ccatlid  11173  ccatrid  11174  ccatass  11175  ccatrn  11176  lswccatn0lsw  11178  ccatalpha  11180  ccatws1lenp1bg  11202  wrdlenccats1lenm1g  11203  ccats1val2  11207  lswccats1  11210  swrdccat2  11242  pfxfv  11255  addlenpfx  11262  pfxtrcfvl  11268  pfxpfx  11279  lenrevpfxcctswrd  11283  ccats1pfxeq  11285  ccatopth2  11288  cats1un  11292  swrdccat3b  11311  cats1fvnd  11336  fsumconst  12005  hash2iun1dif1  12031  binomlem  12034  bcxmas  12040  arisum  12049  arisum2  12050  mertensabs  12088  effsumlt  12243  dvdsexp  12412  nn0ob  12459  divalglemnn  12469  divalgmod  12478  bitsinv1lem  12512  bezoutlemnewy  12557  bezoutlema  12560  bezoutlemb  12561  mulgcd  12577  absmulgcd  12578  mulgcdr  12579  gcddiv  12580  lcmgcd  12640  lcmid  12642  lcm1  12643  3lcm2e6woprm  12648  6lcm4e12  12649  mulgcddvds  12656  qredeu  12659  divgcdcoprm0  12663  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  pw2dvdseulemle  12729  phiprmpw  12784  eulerthlema  12792  prmdiveq  12798  odzdvds  12808  powm2modprm  12815  coprimeprodsq  12820  pceulem  12857  pczpre  12860  pcqmul  12866  pcaddlem  12902  pcmpt  12906  pcmpt2  12907  sumhashdc  12910  pcfac  12913  oddprmdvds  12917  mul4sq  12957  4sqlem12  12965  mulgnn0dir  13729  mulgnn0ass  13735  plyaddlem1  15461  plymullem1  15462  dvply1  15479  dvply2g  15480  0sgm  15699  sgmppw  15706  lgslem1  15719  lgsvalmod  15738  gausslemma2dlem6  15786  gausslemma2d  15788  lgseisenlem2  15790  lgseisenlem3  15791  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem2  15801  m1lgs  15804  2lgslem1c  15809  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2sqlem8  15842  vtxdfifiun  16103  vtxdumgrfival  16104  wlklenvm1  16138  wlklenvm1g  16139  wlklenvclwlk  16170  clwwlkccatlem  16195