Theorem nn0cnd 12304

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 10878  ℕ₀cn0 12242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-i2m1 10948  ax-1ne0 10949  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-nn 11983  df-n0 12243

This theorem is referenced by:  quoremnn0ALT  13586  expaddzlem  13835  expaddz  13836  expmulz  13838  facdiv  14010  faclbnd4lem3  14018  bcp1n  14039  bcn2m1  14047  bcn2p1  14048  hashgadd  14101  hashdom  14103  hashun3  14108  hashssdif  14136  hashdifpr  14139  hashxplem  14157  hashmap  14159  hashreshashfun  14163  hashbclem  14173  hashf1lem2  14179  hashf1  14180  ccatval3  14293  ccatval21sw  14299  ccatlid  14300  ccatrid  14301  ccatass  14302  ccatrn  14303  lswccatn0lsw  14305  ccatalpha  14307  ccatws1lenp1b  14335  wrdlenccats1lenm1  14336  ccats1val2  14343  swrdccat2  14391  pfxfv  14404  addlenpfx  14413  pfxtrcfvl  14419  pfxpfx  14430  ccats1pfxeq  14436  ccatopth2  14439  cats1un  14443  swrdccat3b  14462  spllen  14476  splfv2a  14478  revccat  14488  cshwlen  14521  cshwidxmod  14525  repswcshw  14534  2cshwid  14536  cshweqdif2  14541  relexpaddg  14773  rtrclreclem3  14780  isercoll2  15389  iseraltlem3  15404  hash2iun1dif1  15545  binomlem  15550  bcxmas  15556  incexclem  15557  incexc  15558  incexc2  15559  climcndslem1  15570  climcndslem2  15571  arisum  15581  arisum2  15582  pwdif  15589  geomulcvg  15597  mertens  15607  risefacval2  15729  fallfacval2  15730  fallfacval3  15731  risefallfac  15743  risefacp1  15748  fallfacp1  15749  fallfacfwd  15755  binomfallfaclem1  15758  binomfallfaclem2  15759  binomrisefac  15761  bpolycl  15771  bpolysum  15772  bpolydiflem  15773  fsumkthpow  15775  bpoly4  15778  effsumlt  15829  dvdsexp  16046  nn0ob  16102  divalgmod  16124  bitsinv1lem  16157  sadcp1  16171  sadcaddlem  16173  sadadd2lem  16175  sadadd3  16177  sadaddlem  16182  sadasslem  16186  smupp1  16196  smumullem  16208  mulgcd  16265  absmulgcd  16266  mulgcdr  16267  gcddiv  16268  lcmgcd  16321  lcmid  16323  lcm1  16324  3lcm2e6woprm  16329  6lcm4e12  16330  mulgcddvds  16369  qredeu  16372  divgcdcoprm0  16379  divgcdcoprmex  16380  cncongr1  16381  cncongr2  16382  odzdvds  16505  powm2modprm  16513  coprimeprodsq  16518  pceulem  16555  pczpre  16557  pcqmul  16563  pcaddlem  16598  pcmpt  16602  pcmpt2  16603  sumhash  16606  oddprmdvds  16613  mul4sq  16664  4sqlem12  16666  vdwapun  16684  vdwlem2  16692  vdwlem3  16693  vdwlem6  16696  vdwlem8  16698  vdwlem9  16699  ramub1lem2  16737  ramcl  16739  mulgnn0dir  18742  mulgnn0ass  18748  lagsubg2  18826  psgnunilem2  19112  odmodnn0  19157  odmulg  19172  odmulgeq  19173  odinv  19177  sylow1lem1  19212  sylow2a  19233  sylow2blem3  19236  sylow3lem3  19243  sylow3lem4  19244  efginvrel2  19342  efgsval2  19348  efgsp1  19352  efgredlemg  19357  efgredleme  19358  efgcpbllemb  19370  odadd2  19459  odadd  19460  torsubg  19464  frgpnabllem1  19483  pgpfaclem1  19693  fincygsubgodd  19724  srgbinomlem3  19787  srgbinomlem4  19788  nn0srg  20677  mplcoe5  21250  mhpmulcl  21348  mhppwdeg  21349  coe1tmmul2  21456  coe1tmmul2fv  21458  coe1pwmulfv  21460  mbfi1fseqlem3  24891  dvn2bss  25103  itgpowd  25223  tdeglem4  25233  tdeglem4OLD  25234  tdeglem2  25235  mdegmullem  25252  coe1mul3  25273  ply1divex  25310  fta1glem1  25339  plyaddlem1  25383  plymullem1  25384  coeeulem  25394  coemulc  25425  dgrmulc  25441  dgrcolem2  25444  dgrco  25445  dvply1  25453  dvply2g  25454  plydivlem4  25465  fta1lem  25476  vieta1lem1  25479  aareccl  25495  aaliou3lem8  25514  taylply2  25536  dvtaylp  25538  dvntaylp  25539  dvntaylp0  25540  dvradcnv  25589  pserdvlem2  25596  advlogexp  25819  cxpeq  25919  atantayl3  26098  birthdaylem2  26111  harmonicbnd4  26169  dmgmaddnn0  26185  lgamucov  26196  wilthlem2  26227  basellem2  26240  basellem3  26241  basellem5  26243  0sgm  26302  sgmppw  26354  chtublem  26368  chpval2  26375  sumdchr2  26427  bcp1ctr  26436  lgslem1  26454  gausslemma2dlem6  26529  gausslemma2d  26531  lgseisenlem2  26533  lgseisenlem3  26534  lgsquadlem1  26537  lgsquadlem2  26538  lgsquad2lem2  26542  m1lgs  26545  2lgslem1c  26550  2lgslem3a  26553  2lgslem3b  26554  2lgslem3c  26555  2lgslem3d  26556  2sqlem8  26583  2sq2  26590  2sqmod  26593  dchrisumlem1  26646  dchrisum0flblem2  26666  rpvmasum2  26669  mulogsumlem  26688  selberg2lem  26707  pntrsumo1  26722  pntrlog2bndlem4  26737  finsumvtxdg2ssteplem4  27924  vtxdgoddnumeven  27929  wlklenvm1  27998  wlklenvclwlk  28031  crctcshlem4  28194  crctcsh  28198  wlklnwwlkln2lem  28256  wlknwwlksnbij  28262  wwlksnred  28266  wwlksnext  28267  wwlksnextbi  28268  wwlksnredwwlkn  28269  wwlksnextproplem2  28284  rusgrnumwwlks  28348  rusgrnumwwlk  28349  clwwlkccatlem  28362  clwlkclwwlk  28375  clwwlkwwlksb  28427  eupth2lem3lem3  28603  eupth2lem3lem6  28606  fusgreghash2wsp  28711  frrusgrord0lem  28712  numclwwlk1  28734  numclwwlk3  28758  ex-lcm  28831  ex-ind-dvds  28834  nnmulge  31082  divnumden2  31141  ccatf1  31232  pfxlsw2ccat  31233  wrdt2ind  31234  omndmul2  31347  omndmul3  31348  cycpmco2lem2  31403  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmco2  31409  archiabllem1a  31454  freshmansdream  31493  oddpwdc  32330  eulerpartlemsv2  32334  eulerpartlems  32336  eulerpartlemsv3  32337  eulerpartlemv  32340  eulerpartlemb  32344  iwrdsplit  32363  ballotlemgun  32500  ccatmulgnn0dir  32530  ofcccat  32531  signsplypnf  32538  signslema  32550  signstfvn  32557  signstfveq0  32565  signsvtp  32571  signsvtn  32572  signlem0  32575  signshf  32576  fsum2dsub  32596  hashreprin  32609  breprexp  32622  circlemeth  32629  lpadlem2  32669  lpadlen2  32670  revpfxsfxrev  33086  revwlk  33095  subfacp1lem6  33156  subfacval2  33158  subfaclim  33159  cvmliftlem7  33262  elmrsubrn  33491  bcprod  33713  bccolsum  33714  faclimlem1  33718  faclim2  33723  fwddifnp1  34476  knoppndvlem6  34706  knoppndvlem14  34714  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem24  35810  poimirlem25  35811  poimirlem29  35815  poimirlem31  35817  lcmineqlem1  40044  lcmineqlem2  40045  lcmineqlem12  40055  lcmineqlem17  40060  2np3bcnp1  40107  2ap1caineq  40108  sticksstones7  40115  sticksstones9  40117  sticksstones10  40118  sticksstones11  40119  sticksstones12a  40120  sticksstones12  40121  sticksstones22  40131  ccatcan2d  40226  frlmvscadiccat  40244  fltnltalem  40506  3cubeslem3l  40515  3cubeslem3r  40516  rmxyneg  40749  rmxyadd  40750  rmyp1  40762  rmxm1  40763  rmym1  40764  rmxluc  40765  rmyluc  40766  rmxdbl  40768  rmydbl  40769  jm2.18  40817  jm2.19lem1  40818  jm2.19lem2  40819  jm2.22  40824  jm2.23  40825  jm2.25  40828  jm2.27c  40836  rmxdiophlem  40844  expdioph  40852  hbtlem4  40958  relexpmulg  41325  radcnvrat  41939  nzprmdif  41944  bcc0  41965  bccp1k  41966  bccbc  41970  binomcxplemnn0  41974  binomcxplemrat  41975  binomcxplemfrat  41976  binomcxplemnotnn0  41981  fzisoeu  42846  mccllem  43145  dvxpaek  43488  dvnxpaek  43490  dvnmul  43491  dvnprodlem1  43494  dvnprodlem2  43495  stoweidlem24  43572  stirlinglem3  43624  stirlinglem7  43628  fourierdlem36  43691  fourierdlem47  43701  etransclem23  43805  etransclem32  43814  etransclem48  43830  fz0addcom  44820  fmtnom1nn  44995  fmtnof1  44998  fmtnorec1  45000  sqrtpwpw2p  45001  fmtnorec2lem  45005  fmtnorec3  45011  fmtnofac2lem  45031  fmtnofac2  45032  fmtnofac1  45033  lighneallem3  45070  lighneallem4b  45072  altgsumbc  45699  altgsumbcALT  45700  nnpw2pmod  45940  dignn0ehalf  45974  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  nn0sumshdiglem2  45979  nn0mullong  45982  itcovalpclem2  46028  itcovalt2lem2lem2  46031  itcovalt2lem1  46032  aacllem  46516