Theorem nn0cnd 11615

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

Syntax hints:   → wi 4   ∈ wcel 2156  ℂcc 10215  ℕ₀cn0 11555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-i2m1 10285  ax-1ne0 10286  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-om 7292  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-nn 11302  df-n0 11556

This theorem is referenced by:  quoremnn0ALT  12876  expaddzlem  13122  expaddz  13123  expmulz  13125  facdiv  13290  faclbnd4lem3  13298  bcp1n  13319  bcn2m1  13327  bcn2p1  13328  hashgadd  13380  hashdom  13382  hashun3  13387  hashssdif  13413  hashdifpr  13416  hashxplem  13433  hashmap  13435  hashreshashfun  13439  hashbclem  13449  hashf1lem2  13453  hashf1  13454  ccatval3  13572  ccatval21sw  13578  ccatlid  13579  ccatrid  13580  ccatass  13581  ccatrn  13582  lswccatn0lsw  13584  ccatalpha  13586  ccatws1lenp1b  13613  wrdlenccats1lenm1  13614  wrdlenccats1lenm1OLD  13615  ccats1val2  13621  ccatws1lenrevOLD  13626  swrd0f  13647  swrdid  13648  addlenswrd  13658  swrdtrcfvl  13670  swrdccat2  13678  ccatopth2  13691  cats1un  13695  swrdccat3b  13716  spllen  13725  splfv2a  13727  revccat  13735  cshwlen  13765  cshwidxmod  13769  repswcshw  13778  2cshwid  13780  cshweqdif2  13785  relexpaddg  14012  rtrclreclem3  14019  isercoll2  14618  iseraltlem3  14633  hash2iun1dif1  14774  binomlem  14779  bcxmas  14785  incexclem  14786  incexc  14787  incexc2  14788  climcndslem1  14799  climcndslem2  14800  arisum  14810  arisum2  14811  geomulcvg  14825  mertens  14835  risefacval2  14957  fallfacval2  14958  fallfacval3  14959  risefallfac  14971  risefacp1  14976  fallfacp1  14977  fallfacfwd  14983  binomfallfaclem1  14986  binomfallfaclem2  14987  binomrisefac  14989  bpolycl  14999  bpolysum  15000  bpolydiflem  15001  fsumkthpow  15003  bpoly4  15006  effsumlt  15057  dvdsexp  15268  nn0ob  15316  divalgmod  15345  bitsinv1lem  15378  sadcp1  15392  sadcaddlem  15394  sadadd2lem  15396  sadadd3  15398  sadaddlem  15403  sadasslem  15407  smupp1  15417  smumullem  15429  mulgcd  15480  absmulgcd  15481  mulgcdr  15482  gcddiv  15483  lcmgcd  15535  lcmid  15537  lcm1  15538  3lcm2e6woprm  15543  6lcm4e12  15544  mulgcddvds  15583  qredeu  15586  divgcdcoprm0  15593  divgcdcoprmex  15594  cncongr1  15595  cncongr2  15596  odzdvds  15713  powm2modprm  15721  coprimeprodsq  15726  pceulem  15763  pczpre  15765  pcqmul  15771  pcaddlem  15805  pcmpt  15809  pcmpt2  15810  sumhash  15813  oddprmdvds  15820  mul4sq  15871  4sqlem12  15873  vdwapun  15891  vdwlem2  15899  vdwlem3  15900  vdwlem6  15903  vdwlem8  15905  vdwlem9  15906  ramub1lem2  15944  ramcl  15946  mulgnn0dir  17770  mulgnn0ass  17776  lagsubg2  17853  psgnunilem2  18112  odmodnn0  18156  odmulg  18170  odmulgeq  18171  odinv  18175  sylow1lem1  18210  sylow2a  18231  sylow2blem3  18234  sylow3lem3  18241  sylow3lem4  18242  efginvrel2  18337  efgsval2  18343  efgsp1  18347  efgredlemg  18352  efgredleme  18353  efgcpbllemb  18365  odadd2  18449  odadd  18450  torsubg  18454  frgpnabllem1  18473  pgpfaclem1  18678  srgbinomlem3  18740  srgbinomlem4  18741  mplcoe5  19673  coe1tmmul2  19850  coe1tmmul2fv  19852  coe1pwmulfv  19854  nn0srg  20020  mbfi1fseqlem3  23697  dvn2bss  23906  tdeglem4  24033  tdeglem2  24034  mdegmullem  24051  coe1mul3  24072  ply1divex  24109  fta1glem1  24138  plyaddlem1  24182  plymullem1  24183  coeeulem  24193  coemulc  24224  dgrmulc  24240  dgrcolem2  24243  dgrco  24244  dvply1  24252  dvply2g  24253  plydivlem4  24264  fta1lem  24275  vieta1lem1  24278  aareccl  24294  aaliou3lem8  24313  taylply2  24335  dvtaylp  24337  dvntaylp  24338  dvntaylp0  24339  dvradcnv  24388  pserdvlem2  24395  advlogexp  24614  cxpeq  24711  atantayl3  24879  birthdaylem2  24892  harmonicbnd4  24950  dmgmaddnn0  24966  lgamucov  24977  wilthlem2  25008  basellem2  25021  basellem3  25022  basellem5  25024  0sgm  25083  sgmppw  25135  chtublem  25149  chpval2  25156  sumdchr2  25208  bcp1ctr  25217  lgslem1  25235  gausslemma2dlem6  25310  gausslemma2d  25312  lgseisenlem2  25314  lgseisenlem3  25315  lgsquadlem1  25318  lgsquadlem2  25319  lgsquad2lem2  25323  m1lgs  25326  2lgslem1c  25331  2lgslem3a  25334  2lgslem3b  25335  2lgslem3c  25336  2lgslem3d  25337  2sqlem8  25364  dchrisumlem1  25391  dchrisum0flblem2  25411  rpvmasum2  25414  mulogsumlem  25433  selberg2lem  25452  pntrsumo1  25467  pntrlog2bndlem4  25482  finsumvtxdg2ssteplem4  26671  vtxdgoddnumeven  26676  wlklenvm1  26744  crctcshlem4  26940  crctcsh  26944  wlklnwwlkln2lem  27008  wlknwwlksnbij  27018  wwlksnred  27028  wwlksnext  27029  wwlksnextbi  27030  wwlksnredwwlkn  27031  wwlksnextproplem2  27047  rusgrnumwwlks  27115  rusgrnumwwlk  27116  clwwlkccatlem  27131  clwlkclwwlk  27144  clwwlkwwlksb  27203  eupth2lem3lem3  27402  eupth2lem3lem6  27405  fusgreghash2wsp  27512  frrusgrord0lem  27513  numclwwlk1  27540  numclwwlk3  27572  ex-lcm  27645  ex-ind-dvds  27648  nnmulge  29841  divnumden2  29890  2sqmod  29972  omndmul2  30036  omndmul3  30037  archiabllem1a  30069  oddpwdc  30740  eulerpartlemsv2  30744  eulerpartlems  30746  eulerpartlemsv3  30747  eulerpartlemv  30750  eulerpartlemb  30754  iwrdsplit  30773  ballotlemgun  30910  ccatmulgnn0dir  30943  ofcccat  30944  signsplypnf  30951  signslema  30963  signstfvn  30970  signstfveq0  30978  signsvtp  30984  signsvtn  30985  signlem0  30988  signshf  30989  fsum2dsub  31009  hashreprin  31022  breprexp  31035  circlemeth  31042  subfacp1lem6  31488  subfacval2  31490  subfaclim  31491  cvmliftlem7  31594  elmrsubrn  31738  bcprod  31944  bccolsum  31945  faclimlem1  31949  faclim2  31954  fwddifnp1  32591  knoppndvlem6  32823  knoppndvlem14  32831  poimirlem4  33724  poimirlem5  33725  poimirlem6  33726  poimirlem7  33727  poimirlem10  33730  poimirlem11  33731  poimirlem12  33732  poimirlem16  33736  poimirlem17  33737  poimirlem19  33739  poimirlem20  33740  poimirlem22  33742  poimirlem24  33744  poimirlem25  33745  poimirlem29  33749  poimirlem31  33751  rmxyneg  37983  rmxyadd  37984  rmyp1  37996  rmxm1  37997  rmym1  37998  rmxluc  37999  rmyluc  38000  rmxdbl  38002  rmydbl  38003  jm2.18  38053  jm2.19lem1  38054  jm2.19lem2  38055  jm2.22  38060  jm2.23  38061  jm2.25  38064  jm2.27c  38072  rmxdiophlem  38080  expdioph  38088  hbtlem4  38194  itgpowd  38297  relexpmulg  38499  radcnvrat  39010  nzprmdif  39015  bcc0  39036  bccp1k  39037  bccbc  39041  binomcxplemnn0  39045  binomcxplemrat  39046  binomcxplemfrat  39047  binomcxplemnotnn0  39052  fzisoeu  39992  mccllem  40306  dvxpaek  40632  dvnxpaek  40634  dvnmul  40635  dvnprodlem1  40638  dvnprodlem2  40639  stoweidlem24  40717  stirlinglem3  40769  stirlinglem7  40773  fourierdlem36  40836  fourierdlem47  40846  etransclem23  40950  etransclem32  40959  etransclem48  40975  fz0addcom  41899  addlenpfx  41970  pfxfv  41971  pfxtrcfvl  41977  pfxpfx  41987  ccats1pfxeq  41993  fmtnom1nn  42016  fmtnof1  42019  fmtnorec1  42021  sqrtpwpw2p  42022  fmtnorec2lem  42026  fmtnorec3  42032  fmtnofac2lem  42052  fmtnofac2  42053  fmtnofac1  42054  pwdif  42073  lighneallem3  42096  lighneallem4b  42098  altgsumbc  42695  altgsumbcALT  42696  nnpw2pmod  42942  dignn0ehalf  42976  nn0sumshdiglemA  42978  nn0sumshdiglemB  42979  nn0sumshdiglem2  42981  nn0mullong  42984  aacllem  43115