Theorem nn0cnd 9557

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 9556	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 8304	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8127  ℕ₀cn0 9498

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4230  ax-cnex 8220  ax-resscn 8221  ax-1re 8223  ax-addrcl 8226  ax-rnegex 8238

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-sn 3697  df-int 3952  df-inn 9240  df-n0 9499

This theorem is referenced by:  modsumfzodifsn  10762  addmodlteq  10764  uzennn  10802  expaddzaplem  10948  expaddzap  10949  expmulzap  10951  nn0le2msqd  11085  nn0opthlem1d  11086  nn0opthd  11088  nn0opth2d  11089  facdiv  11104  bcp1n  11127  bcn2m1  11136  bcn2p1  11137  omgadd  11170  fihashssdif  11187  hashdifpr  11189  hashxp  11195  hashmap  11196  hashfibclem  11210  zfz1isolemsplit  11214  zfz1isolem1  11216  ccatval3  11291  ccatval21sw  11297  ccatlid  11298  ccatrid  11299  ccatass  11300  ccatrn  11301  lswccatn0lsw  11303  ccatalpha  11305  ccatws1lenp1bg  11327  wrdlenccats1lenm1g  11328  ccats1val2  11332  lswccats1  11335  swrdccat2  11367  pfxfv  11380  addlenpfx  11387  pfxtrcfvl  11393  pfxpfx  11404  lenrevpfxcctswrd  11408  ccats1pfxeq  11410  ccatopth2  11413  cats1un  11417  swrdccat3b  11436  cats1fvnd  11461  fsumconst  12144  hash2iun1dif1  12170  binomlem  12173  bcxmas  12179  arisum  12188  arisum2  12189  mertensabs  12227  effsumlt  12382  dvdsexp  12551  nn0ob  12598  divalglemnn  12608  divalgmod  12617  bitsinv1lem  12651  bezoutlemnewy  12696  bezoutlema  12699  bezoutlemb  12700  mulgcd  12716  absmulgcd  12717  mulgcdr  12718  gcddiv  12719  lcmgcd  12779  lcmid  12781  lcm1  12782  3lcm2e6woprm  12787  6lcm4e12  12788  mulgcddvds  12795  qredeu  12798  divgcdcoprm0  12802  divgcdcoprmex  12803  cncongr1  12804  cncongr2  12805  pw2dvdseulemle  12868  phiprmpw  12923  eulerthlema  12931  prmdiveq  12937  odzdvds  12947  powm2modprm  12954  coprimeprodsq  12959  pceulem  12996  pczpre  12999  pcqmul  13005  pcaddlem  13041  pcmpt  13045  pcmpt2  13046  sumhashdc  13049  pcfac  13052  oddprmdvds  13056  mul4sq  13096  4sqlem12  13104  ballotfilemfp1  13152  mulgnn0dir  13886  mulgnn0ass  13892  plyaddlem1  15629  plymullem1  15630  dvply1  15647  dvply2g  15648  0sgm  15870  sgmppw  15877  lgslem1  15890  lgsvalmod  15909  gausslemma2dlem6  15957  gausslemma2d  15959  lgseisenlem2  15961  lgseisenlem3  15962  lgsquadlem1  15967  lgsquadlem2  15968  lgsquad2lem2  15972  m1lgs  15975  2lgslem1c  15980  2lgslem3a  15983  2lgslem3b  15984  2lgslem3c  15985  2lgslem3d  15986  2sqlem8  16013  vtxdfifiun  16309  vtxdumgrfival  16310  p1evtxdeqfi  16324  wlklenvm1  16353  wlklenvm1g  16354  wlklenvclwlk  16385  clwwlkccatlem  16412  eupth2lem3lem3fi  16482  eupth2lem3lem6fi  16483  depindlem1  16518