Theorem nn0cnd 12669

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11198  ℕ₀cn0 12606

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-nn 12336  df-n0 12607

This theorem is used by:  quoremnn0ALT  13997  expaddzlem  14248  expaddz  14249  expmulz  14251  facdiv  14431  faclbnd4lem3  14439  bcp1n  14460  bcn2m1  14468  bcn2p1  14469  hashgadd  14521  hashdom  14523  hashun3  14528  hashssdif  14557  hashdifpr  14560  hashxplem  14578  hashmap  14580  hashreshashfun  14584  hashbclem  14597  hashf1lem2  14601  hashf1  14602  ccatval3  14724  ccatval21sw  14731  ccatlid  14732  ccatrid  14733  ccatass  14734  ccatrn  14735  ccatf1  14736  lswccatn0lsw  14738  ccatalpha  14740  ccatws1lenp1b  14769  wrdlenccats1lenm1  14770  ccats1val2  14775  swrdccat2  14819  pfxfv  14832  addlenpfx  14840  pfxtrcfvl  14846  pfxpfx  14857  lenrevpfxcctswrd  14861  ccats1pfxeq  14863  ccatopth2  14866  cats1un  14870  swrdccat3b  14889  spllen  14903  splfv2a  14905  revccat  14915  revpfxsfxrev  14917  cshwlen  14950  cshwidxmod  14954  repswcshw  14963  2cshwid  14965  cshweqdif2  14970  relexpaddg  15206  rtrclreclem3  15213  isercoll2  15836  iseraltlem3  15851  fsumconst1  15957  hash2iun1dif1  15991  binomlem  15998  bcxmas  16004  incexclem  16005  incexc  16006  incexc2  16007  climcndslem1  16018  climcndslem2  16019  arisum  16029  arisum2  16030  pwdif  16037  geomulcvg  16045  mertens  16055  risefacval2  16177  fallfacval2  16178  fallfacval3  16179  risefallfac  16191  risefacp1  16195  fallfacp1  16196  fallfacfwd  16202  binomfallfaclem1  16205  binomfallfaclem2  16206  binomrisefac  16208  bpolycl  16218  bpolysum  16219  bpolydiflem  16220  fsumkthpow  16222  bpoly4  16225  effsumlt  16279  dvdsexp  16498  nn0ob  16554  divalgmod  16576  bitsinv1lem  16611  sadcp1  16625  sadcaddlem  16627  sadadd2lem  16629  sadadd3  16631  sadaddlem  16636  sadasslem  16640  smupp1  16650  smumullem  16662  mulgcd  16721  absmulgcd  16722  mulgcdr  16723  gcddiv  16724  lcmgcd  16782  lcmid  16784  lcm1  16785  3lcm2e6woprm  16790  6lcm4e12  16791  mulgcddvds  16830  qredeu  16833  divgcdcoprm0  16840  divgcdcoprmex  16841  cncongr1  16842  cncongr2  16843  odzdvds  16973  powm2modprm  16981  coprimeprodsq  16986  pceulem  17023  pczpre  17025  pcqmul  17031  pcaddlem  17066  pcmpt  17070  pcmpt2  17071  sumhash  17074  oddprmdvds  17081  mul4sq  17132  4sqlem12  17134  vdwapun  17152  vdwlem2  17160  vdwlem3  17161  vdwlem6  17164  vdwlem8  17166  vdwlem9  17167  ramub1lem2  17205  ramcl  17207  chnrev  18801  mulgnn0dir  19314  mulgnn0ass  19320  lagsubg2  19409  psgnunilem2  19709  odmodnn0  19754  odmulg  19770  odmulgeq  19771  odinv  19775  sylow1lem1  19812  sylow2a  19833  sylow2blem3  19836  sylow3lem3  19843  sylow3lem4  19844  efginvrel2  19941  efgsval2  19947  efgsp1  19951  efgredlemg  19956  efgredleme  19957  efgcpbllemb  19969  odadd2  20063  odadd  20064  torsubg  20068  frgpnabllem1  20087  pgpfaclem1  20297  fincygsubgodd  20328  omndmul2  20347  omndmul3  20348  srgbinomlem3  20454  srgbinomlem4  20455  nn0srg  21743  freshmansdream  21880  mplcoe5  22349  mhpmulcl  22470  mhppwdeg  22471  psdmplcl  22483  psdmul  22487  coe1tmmul2  22595  coe1tmmul2fv  22597  coe1pwmulfv  22599  mbfi1fseqlem3  26038  dvn2bss  26250  itgpowd  26370  tdeglem4  26378  tdeglem2  26379  mdegmullem  26396  coe1mul3  26417  ply1divex  26455  fta1glem1  26486  plyaddlem1  26532  plymullem1  26533  coeeulem  26543  coemulc  26574  dgrmulc  26590  dgrcolem2  26593  dgrco  26594  dvply1  26605  dvply2g  26606  plydivlem4  26617  fta1lem  26628  vieta1lem1  26633  aareccl  26653  aaliou3lem8  26672  taylply2  26695  dvtaylp  26697  dvntaylp  26698  dvntaylp0  26699  dvradcnv  26748  pserdvlem2  26755  advlogexp  26983  cxpeq  27085  atantayl3  27267  birthdaylem2  27280  harmonicbnd4  27338  dmgmaddnn0  27354  lgamucov  27365  wilthlem2  27396  basellem2  27409  basellem3  27410  basellem5  27412  0sgm  27471  sgmppw  27524  chtublem  27538  chpval2  27545  sumdchr2  27597  bcp1ctr  27606  lgslem1  27624  gausslemma2dlem6  27699  gausslemma2d  27701  lgseisenlem2  27703  lgseisenlem3  27704  lgsquadlem1  27707  lgsquadlem2  27708  lgsquad2lem2  27712  m1lgs  27715  2lgslem1c  27720  2lgslem3a  27723  2lgslem3b  27724  2lgslem3c  27725  2lgslem3d  27726  2sqlem8  27753  2sq2  27760  2sqmod  27763  dchrisumlem1  27816  dchrisum0flblem2  27836  rpvmasum2  27839  mulogsumlem  27858  selberg2lem  27877  pntrsumo1  27892  pntrlog2bndlem4  27907  finsumvtxdg2ssteplem4  30129  vtxdgoddnumeven  30134  wlklenvm1  30202  wlklenvclwlk  30234  revwlk  30267  crctcshlem4  30409  crctcsh  30413  wlklnwwlkln2lem  30471  wlknwwlksnbij  30477  wwlksnred  30481  wwlksnext  30482  wwlksnextbi  30483  wwlksnredwwlkn  30484  wwlksnextproplem2  30499  rusgrnumwwlks  30566  rusgrnumwwlk  30567  clwwlkccatlem  30580  clwlkclwwlk  30593  clwwlkwwlksb  30645  eupth2lem3lem3  30831  eupth2lem3lem6  30834  fusgreghash2wsp  30939  frrusgrord0lem  30940  numclwwlk1  30962  numclwwlk3  30986  ex-lcm  31059  ex-ind-dvds  31062  nnmulge  33331  elq2  33403  divnumden2  33407  pfxlsw2ccat  33513  ccatws1f1o  33514  wrdt2ind  33516  gsummptrev  33617  gsummptp1  33618  gsummulsubdishift1  33629  cycpmco2lem2  33688  cycpmco2lem3  33689  cycpmco2lem4  33690  cycpmco2lem5  33691  cycpmco2lem6  33692  cycpmco2lem7  33693  cycpmco2  33694  archiabllem1a  33752  gsumind  33906  deg1prod  34115  ply1dg3rt0irred  34116  esplyind  34207  esplyindfv  34208  esplyfvn  34209  vietadeg1  34210  vietalem  34211  vieta  34212  iconstr  34398  cos9thpiminplylem1  34414  oddpwdc  34986  eulerpartlemsv2  34990  eulerpartlems  34992  eulerpartlemsv3  34993  eulerpartlemv  34996  eulerpartlemb  35000  iwrdsplit  35019  ballotlemgun  35157  ccatmulgnn0dir  35174  ofcccat  35175  signsplypnf  35179  signslema  35191  signstfvn  35198  signstfveq0  35206  signsvtp  35212  signsvtn  35213  signlem0  35216  signshf  35217  fsum2dsub  35236  hashreprin  35249  breprexp  35262  circlemeth  35269  lpadlem2  35312  lpadlen2  35313  subfacp1lem6  35950  subfacval2  35952  subfaclim  35953  cvmliftlem7  36056  elmrsubrn  36285  bcprod  36503  bccolsum  36504  faclimlem1  36508  faclim2  36513  fwddifnp1  36930  knoppndvlem6  37383  knoppndvlem14  37391  poimirlem4  38542  poimirlem5  38543  poimirlem6  38544  poimirlem7  38545  poimirlem10  38548  poimirlem11  38549  poimirlem12  38550  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem22  38560  poimirlem24  38562  poimirlem25  38563  poimirlem29  38567  poimirlem31  38569  lcmineqlem1  43079  lcmineqlem2  43080  lcmineqlem12  43090  lcmineqlem17  43095  primrootscoprmpow  43149  aks6d1c2p2  43169  deg1gprod  43190  deg1pow  43191  2np3bcnp1  43194  2ap1caineq  43195  sticksstones7  43202  sticksstones9  43204  sticksstones10  43205  sticksstones11  43206  sticksstones12a  43207  sticksstones12  43208  sticksstones22  43218  aks6d1c6lem1  43220  aks6d1c6lem3  43222  bcled  43228  bcle2d  43229  aks6d1c7lem1  43230  unitscyglem2  43246  unitscyglem4  43248  ccatcan2d  43302  fz1sump1  43367  sumcubes  43370  zaddcomlem  43527  frlmvscadiccat  43573  fltnltalem  43673  3cubeslem3l  43696  3cubeslem3r  43697  rmxyneg  43926  rmxyadd  43927  rmyp1  43939  rmxm1  43940  rmym1  43941  rmxluc  43942  rmyluc  43943  rmxdbl  43945  rmydbl  43946  jm2.18  43994  jm2.19lem1  43995  jm2.19lem2  43996  jm2.22  44001  jm2.23  44002  jm2.25  44005  jm2.27c  44013  rmxdiophlem  44021  expdioph  44029  hbtlem4  44127  relexpmulg  44709  radcnvrat  45297  nzprmdif  45302  bcc0  45323  bccp1k  45324  bccbc  45328  binomcxplemnn0  45332  binomcxplemrat  45333  binomcxplemfrat  45334  binomcxplemnotnn0  45339  fzisoeu  46315  mccllem  46608  dvxpaek  46949  dvnxpaek  46951  dvnmul  46952  dvnprodlem1  46955  dvnprodlem2  46956  stoweidlem24  47033  stirlinglem3  47085  stirlinglem7  47089  fourierdlem36  47152  fourierdlem47  47162  etransclem23  47266  etransclem32  47275  etransclem48  47291  fz0addcom  48386  fmtnom1nn  48616  fmtnof1  48619  fmtnorec1  48621  sqrtpwpw2p  48622  fmtnorec2lem  48626  fmtnorec3  48632  fmtnofac2lem  48652  fmtnofac2  48653  fmtnofac1  48654  lighneallem3  48691  lighneallem4b  48693  altgsumbc  49463  altgsumbcALT  49464  nnpw2pmod  49694  dignn0ehalf  49728  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731  nn0sumshdiglem2  49733  nn0mullong  49736  itcovalpclem2  49782  itcovalt2lem2lem2  49785  itcovalt2lem1  49786  aacllem  50938