Theorem nn0cnd 12566

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℂcc 11097  ℕ₀cn0 12503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-i2m1 11167  ax-1ne0 11168  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-nn 12233  df-n0 12504

This theorem is referenced by:  quoremnn0ALT  13889  expaddzlem  14140  expaddz  14141  expmulz  14143  facdiv  14322  faclbnd4lem3  14330  bcp1n  14351  bcn2m1  14359  bcn2p1  14360  hashgadd  14412  hashdom  14414  hashun3  14419  hashssdif  14448  hashdifpr  14451  hashxplem  14469  hashmap  14471  hashreshashfun  14475  hashbclem  14488  hashf1lem2  14492  hashf1  14493  ccatval3  14615  ccatval21sw  14622  ccatlid  14623  ccatrid  14624  ccatass  14625  ccatrn  14626  lswccatn0lsw  14628  ccatalpha  14630  ccatws1lenp1b  14658  wrdlenccats1lenm1  14659  ccats1val2  14664  swrdccat2  14706  pfxfv  14719  addlenpfx  14727  pfxtrcfvl  14733  pfxpfx  14744  lenrevpfxcctswrd  14748  ccats1pfxeq  14750  ccatopth2  14753  cats1un  14757  swrdccat3b  14776  spllen  14790  splfv2a  14792  revccat  14802  cshwlen  14835  cshwidxmod  14839  repswcshw  14848  2cshwid  14850  cshweqdif2  14855  relexpaddg  15089  rtrclreclem3  15096  isercoll2  15719  iseraltlem3  15734  fsumconst1  15841  hash2iun1dif1  15875  binomlem  15882  bcxmas  15888  incexclem  15889  incexc  15890  incexc2  15891  climcndslem1  15902  climcndslem2  15903  arisum  15913  arisum2  15914  pwdif  15921  geomulcvg  15929  mertens  15939  risefacval2  16063  fallfacval2  16064  fallfacval3  16065  risefallfac  16077  risefacp1  16082  fallfacp1  16083  fallfacfwd  16089  binomfallfaclem1  16092  binomfallfaclem2  16093  binomrisefac  16095  bpolycl  16105  bpolysum  16106  bpolydiflem  16107  fsumkthpow  16109  bpoly4  16112  effsumlt  16166  dvdsexp  16385  nn0ob  16441  divalgmod  16463  bitsinv1lem  16498  sadcp1  16512  sadcaddlem  16514  sadadd2lem  16516  sadadd3  16518  sadaddlem  16523  sadasslem  16527  smupp1  16537  smumullem  16549  mulgcd  16605  absmulgcd  16606  mulgcdr  16607  gcddiv  16608  lcmgcd  16664  lcmid  16666  lcm1  16667  3lcm2e6woprm  16672  6lcm4e12  16673  mulgcddvds  16712  qredeu  16715  divgcdcoprm0  16722  divgcdcoprmex  16723  cncongr1  16724  cncongr2  16725  odzdvds  16854  powm2modprm  16862  coprimeprodsq  16867  pceulem  16904  pczpre  16906  pcqmul  16912  pcaddlem  16947  pcmpt  16951  pcmpt2  16952  sumhash  16955  oddprmdvds  16962  mul4sq  17013  4sqlem12  17015  vdwapun  17033  vdwlem2  17041  vdwlem3  17042  vdwlem6  17045  vdwlem8  17047  vdwlem9  17048  ramub1lem2  17086  ramcl  17088  chnrev  18682  mulgnn0dir  19169  mulgnn0ass  19175  lagsubg2  19264  psgnunilem2  19564  odmodnn0  19609  odmulg  19625  odmulgeq  19626  odinv  19630  sylow1lem1  19667  sylow2a  19688  sylow2blem3  19691  sylow3lem3  19698  sylow3lem4  19699  efginvrel2  19796  efgsval2  19802  efgsp1  19806  efgredlemg  19811  efgredleme  19812  efgcpbllemb  19824  odadd2  19918  odadd  19919  torsubg  19923  frgpnabllem1  19942  pgpfaclem1  20152  fincygsubgodd  20183  omndmul2  20202  omndmul3  20203  srgbinomlem3  20309  srgbinomlem4  20310  nn0srg  21555  freshmansdream  21692  mplcoe5  22159  mhpmulcl  22280  mhppwdeg  22281  psdmplcl  22293  psdmul  22297  coe1tmmul2  22405  coe1tmmul2fv  22407  coe1pwmulfv  22409  mbfi1fseqlem3  25844  dvn2bss  26057  itgpowd  26177  tdeglem4  26185  tdeglem2  26186  mdegmullem  26203  coe1mul3  26224  ply1divex  26262  fta1glem1  26293  plyaddlem1  26338  plymullem1  26339  coeeulem  26349  coemulc  26380  dgrmulc  26396  dgrcolem2  26399  dgrco  26400  dvply1  26413  dvply2g  26414  plydivlem4  26425  fta1lem  26436  vieta1lem1  26439  aareccl  26455  aaliou3lem8  26474  taylply2  26496  dvtaylp  26498  dvntaylp  26499  dvntaylp0  26500  dvradcnv  26549  pserdvlem2  26556  advlogexp  26785  cxpeq  26887  atantayl3  27069  birthdaylem2  27082  harmonicbnd4  27140  dmgmaddnn0  27156  lgamucov  27167  wilthlem2  27198  basellem2  27211  basellem3  27212  basellem5  27214  0sgm  27273  sgmppw  27326  chtublem  27340  chpval2  27347  sumdchr2  27399  bcp1ctr  27408  lgslem1  27426  gausslemma2dlem6  27501  gausslemma2d  27503  lgseisenlem2  27505  lgseisenlem3  27506  lgsquadlem1  27509  lgsquadlem2  27510  lgsquad2lem2  27514  m1lgs  27517  2lgslem1c  27522  2lgslem3a  27525  2lgslem3b  27526  2lgslem3c  27527  2lgslem3d  27528  2sqlem8  27555  2sq2  27562  2sqmod  27565  dchrisumlem1  27618  dchrisum0flblem2  27638  rpvmasum2  27641  mulogsumlem  27660  selberg2lem  27679  pntrsumo1  27694  pntrlog2bndlem4  27709  finsumvtxdg2ssteplem4  29838  vtxdgoddnumeven  29843  wlklenvm1  29911  wlklenvclwlk  29943  crctcshlem4  30109  crctcsh  30113  wlklnwwlkln2lem  30171  wlknwwlksnbij  30177  wwlksnred  30181  wwlksnext  30182  wwlksnextbi  30183  wwlksnredwwlkn  30184  wwlksnextproplem2  30199  rusgrnumwwlks  30266  rusgrnumwwlk  30267  clwwlkccatlem  30280  clwlkclwwlk  30293  clwwlkwwlksb  30345  eupth2lem3lem3  30521  eupth2lem3lem6  30524  fusgreghash2wsp  30629  frrusgrord0lem  30630  numclwwlk1  30652  numclwwlk3  30676  ex-lcm  30749  ex-ind-dvds  30752  nnmulge  33024  elq2  33096  divnumden2  33100  ccatf1  33209  pfxlsw2ccat  33210  ccatws1f1o  33211  wrdt2ind  33213  gsummptrev  33316  gsummptp1  33317  gsummulsubdishift1  33328  cycpmco2lem2  33387  cycpmco2lem3  33388  cycpmco2lem4  33389  cycpmco2lem5  33390  cycpmco2lem6  33391  cycpmco2lem7  33392  cycpmco2  33393  archiabllem1a  33451  gsumind  33607  deg1prod  33817  ply1dg3rt0irred  33818  esplyind  33909  esplyindfv  33910  esplyfvn  33911  vietadeg1  33912  vietalem  33913  vieta  33914  iconstr  34100  cos9thpiminplylem1  34116  oddpwdc  34688  eulerpartlemsv2  34692  eulerpartlems  34694  eulerpartlemsv3  34695  eulerpartlemv  34698  eulerpartlemb  34702  iwrdsplit  34721  ballotlemgun  34859  ccatmulgnn0dir  34876  ofcccat  34877  signsplypnf  34881  signslema  34893  signstfvn  34900  signstfveq0  34908  signsvtp  34914  signsvtn  34915  signlem0  34918  signshf  34919  fsum2dsub  34938  hashreprin  34951  breprexp  34964  circlemeth  34971  lpadlem2  35014  lpadlen2  35015  revpfxsfxrev  35505  revwlk  35515  subfacp1lem6  35575  subfacval2  35577  subfaclim  35578  cvmliftlem7  35681  elmrsubrn  35910  bcprod  36128  bccolsum  36129  faclimlem1  36133  faclim2  36138  fwddifnp1  36555  knoppndvlem6  36994  knoppndvlem14  37002  poimirlem4  38162  poimirlem5  38163  poimirlem6  38164  poimirlem7  38165  poimirlem10  38168  poimirlem11  38169  poimirlem12  38170  poimirlem16  38174  poimirlem17  38175  poimirlem19  38177  poimirlem20  38178  poimirlem22  38180  poimirlem24  38182  poimirlem25  38183  poimirlem29  38187  poimirlem31  38189  lcmineqlem1  42685  lcmineqlem2  42686  lcmineqlem12  42696  lcmineqlem17  42701  primrootscoprmpow  42755  aks6d1c2p2  42775  deg1gprod  42796  deg1pow  42797  2np3bcnp1  42800  2ap1caineq  42801  sticksstones7  42808  sticksstones9  42810  sticksstones10  42811  sticksstones11  42812  sticksstones12a  42813  sticksstones12  42814  sticksstones22  42824  aks6d1c6lem1  42826  aks6d1c6lem3  42828  bcled  42834  bcle2d  42835  aks6d1c7lem1  42836  unitscyglem2  42852  unitscyglem4  42854  ccatcan2d  42908  fz1sump1  42960  sumcubes  42963  zaddcomlem  43126  frlmvscadiccat  43169  fltnltalem  43285  3cubeslem3l  43308  3cubeslem3r  43309  rmxyneg  43538  rmxyadd  43539  rmyp1  43551  rmxm1  43552  rmym1  43553  rmxluc  43554  rmyluc  43555  rmxdbl  43557  rmydbl  43558  jm2.18  43606  jm2.19lem1  43607  jm2.19lem2  43608  jm2.22  43613  jm2.23  43614  jm2.25  43617  jm2.27c  43625  rmxdiophlem  43633  expdioph  43641  hbtlem4  43744  relexpmulg  44327  radcnvrat  44915  nzprmdif  44920  bcc0  44941  bccp1k  44942  bccbc  44946  binomcxplemnn0  44950  binomcxplemrat  44951  binomcxplemfrat  44952  binomcxplemnotnn0  44957  fzisoeu  45910  mccllem  46204  dvxpaek  46545  dvnxpaek  46547  dvnmul  46548  dvnprodlem1  46551  dvnprodlem2  46552  stoweidlem24  46629  stirlinglem3  46681  stirlinglem7  46685  fourierdlem36  46748  fourierdlem47  46758  etransclem23  46862  etransclem32  46871  etransclem48  46887  fz0addcom  47942  fmtnom1nn  48172  fmtnof1  48175  fmtnorec1  48177  sqrtpwpw2p  48178  fmtnorec2lem  48182  fmtnorec3  48188  fmtnofac2lem  48208  fmtnofac2  48209  fmtnofac1  48210  lighneallem3  48247  lighneallem4b  48249  altgsumbc  49016  altgsumbcALT  49017  nnpw2pmod  49247  dignn0ehalf  49281  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284  nn0sumshdiglem2  49286  nn0mullong  49289  itcovalpclem2  49335  itcovalt2lem2lem2  49338  itcovalt2lem1  49339  aacllem  50474