Theorem nn0cnd 11353

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

Syntax hints:   → wi 4   ∈ wcel 1990  ℂcc 9934  ℕ₀cn0 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-nn 11021  df-n0 11293

This theorem is referenced by:  quoremnn0ALT  12656  expaddzlem  12903  expaddz  12904  expmulz  12906  facdiv  13074  faclbnd4lem3  13082  bcp1n  13103  bcn2m1  13111  bcn2p1  13112  hashgadd  13166  hashdom  13168  hashun3  13173  hashssdif  13200  hashdifpr  13203  hashxplem  13220  hashmap  13222  hashreshashfun  13226  hashbclem  13236  hashf1lem2  13240  hashf1  13241  ccatval3  13363  ccatlid  13369  ccatrid  13370  ccatass  13371  ccatrn  13372  lswccatn0lsw  13373  ccatalpha  13375  wrdlenccats1lenm1  13399  ccats1val2  13404  ccatws1lenrevOLD  13408  swrd0f  13427  swrdid  13428  addlenswrd  13438  swrdtrcfvl  13450  swrdccat2  13458  ccatopth2  13471  cats1un  13475  swrdccat3b  13496  spllen  13505  splfv2a  13507  revccat  13515  cshwlen  13545  cshwidxmod  13549  repswcshw  13558  2cshwid  13560  cshweqdif2  13565  relexpaddg  13793  rtrclreclem3  13800  isercoll2  14399  iseraltlem3  14414  hash2iun1dif1  14556  binomlem  14561  bcxmas  14567  incexclem  14568  incexc  14569  incexc2  14570  climcndslem1  14581  climcndslem2  14582  arisum  14592  arisum2  14593  geomulcvg  14607  mertens  14618  risefacval2  14741  fallfacval2  14742  fallfacval3  14743  risefallfac  14755  risefacp1  14760  fallfacp1  14761  fallfacfwd  14767  binomfallfaclem1  14770  binomfallfaclem2  14771  binomrisefac  14773  bpolycl  14783  bpolysum  14784  bpolydiflem  14785  fsumkthpow  14787  bpoly4  14790  effsumlt  14841  dvdsexp  15049  nn0ob  15100  divalgmod  15129  divalgmodOLD  15130  bitsinv1lem  15163  sadcp1  15177  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  sadaddlem  15188  sadasslem  15192  smupp1  15202  smumullem  15214  mulgcd  15265  absmulgcd  15266  mulgcdr  15267  gcddiv  15268  lcmgcd  15320  lcmid  15322  lcm1  15323  3lcm2e6woprm  15328  6lcm4e12  15329  mulgcddvds  15369  qredeu  15372  divgcdcoprm0  15379  divgcdcoprmex  15380  cncongr1  15381  cncongr2  15382  odzdvds  15500  powm2modprm  15508  coprimeprodsq  15513  pceulem  15550  pczpre  15552  pcqmul  15558  pcaddlem  15592  pcmpt  15596  pcmpt2  15597  sumhash  15600  oddprmdvds  15607  mul4sq  15658  4sqlem12  15660  vdwapun  15678  vdwlem2  15686  vdwlem3  15687  vdwlem6  15690  vdwlem8  15692  vdwlem9  15693  ramub1lem2  15731  ramcl  15733  mulgnn0dir  17571  mulgnn0ass  17578  lagsubg2  17655  psgnunilem2  17915  odmodnn0  17959  odmulg  17973  odmulgeq  17974  odinv  17978  sylow1lem1  18013  sylow2a  18034  sylow2blem3  18037  sylow3lem3  18044  sylow3lem4  18045  efginvrel2  18140  efgsval2  18146  efgsp1  18150  efgredlemg  18155  efgredleme  18156  efgcpbllemb  18168  odadd2  18252  odadd  18253  torsubg  18257  frgpnabllem1  18276  pgpfaclem1  18480  srgbinomlem3  18542  srgbinomlem4  18543  mplcoe5  19468  coe1tmmul2  19646  coe1tmmul2fv  19648  coe1pwmulfv  19650  nn0srg  19816  mbfi1fseqlem3  23484  dvn2bss  23693  tdeglem4  23820  tdeglem2  23821  mdegmullem  23838  coe1mul3  23859  ply1divex  23896  fta1glem1  23925  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  coemulc  24011  dgrmulc  24027  dgrcolem2  24030  dgrco  24031  dvply1  24039  dvply2g  24040  plydivlem4  24051  fta1lem  24062  vieta1lem1  24065  aareccl  24081  aaliou3lem8  24100  taylply2  24122  dvtaylp  24124  dvntaylp  24125  dvntaylp0  24126  dvradcnv  24175  pserdvlem2  24182  advlogexp  24401  cxpeq  24498  atantayl3  24666  birthdaylem2  24679  harmonicbnd4  24737  dmgmaddnn0  24753  lgamucov  24764  wilthlem2  24795  basellem2  24808  basellem3  24809  basellem5  24811  0sgm  24870  sgmppw  24922  chtublem  24936  chpval2  24943  sumdchr2  24995  bcp1ctr  25004  lgslem1  25022  gausslemma2dlem6  25097  gausslemma2d  25099  lgseisenlem2  25101  lgseisenlem3  25102  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad2lem2  25110  m1lgs  25113  2lgslem1c  25118  2lgslem3a  25121  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2sqlem8  25151  dchrisumlem1  25178  dchrisum0flblem2  25198  rpvmasum2  25201  mulogsumlem  25220  selberg2lem  25239  pntrsumo1  25254  pntrlog2bndlem4  25269  finsumvtxdg2ssteplem4  26444  vtxdgoddnumeven  26449  wlklenvm1  26517  crctcshlem4  26712  crctcsh  26716  wlklnwwlkln2lem  26768  wwlksnred  26787  wwlksnext  26788  wwlksnextbi  26789  wwlksnredwwlkn  26790  wwlksnextproplem2  26805  rusgrnumwwlks  26869  rusgrnumwwlk  26870  clwlkclwwlk  26903  eupth2lem3lem3  27090  eupth2lem3lem6  27093  fusgreghash2wsp  27202  frrusgrord0lem  27203  numclwwlk1  27231  numclwwlk3OLD  27242  numclwwlk3  27243  ex-lcm  27315  ex-ind-dvds  27318  nnmulge  29515  divnumden2  29564  2sqmod  29648  omndmul2  29712  omndmul3  29713  archiabllem1a  29745  oddpwdc  30416  eulerpartlemsv2  30420  eulerpartlems  30422  eulerpartlemsv3  30423  eulerpartlemv  30426  eulerpartlemb  30430  iwrdsplit  30449  ballotlemgun  30586  ccatmulgnn0dir  30619  ofcccat  30620  signsplypnf  30627  signslema  30639  signstfvn  30646  signstfveq0  30654  signsvtp  30660  signsvtn  30661  signlem0  30664  signshf  30665  fsum2dsub  30685  hashreprin  30698  breprexp  30711  circlemeth  30718  subfacp1lem6  31167  subfacval2  31169  subfaclim  31170  cvmliftlem7  31273  elmrsubrn  31417  bcprod  31624  bccolsum  31625  faclimlem1  31629  faclim2  31634  fwddifnp1  32272  knoppndvlem6  32508  knoppndvlem14  32516  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem24  33433  poimirlem25  33434  poimirlem29  33438  poimirlem31  33440  rmxyneg  37485  rmxyadd  37486  rmyp1  37498  rmxm1  37499  rmym1  37500  rmxluc  37501  rmyluc  37502  rmxdbl  37504  rmydbl  37505  jm2.18  37555  jm2.19lem1  37556  jm2.19lem2  37557  jm2.22  37562  jm2.23  37563  jm2.25  37566  jm2.27c  37574  rmxdiophlem  37582  expdioph  37590  hbtlem4  37696  itgpowd  37800  relexpmulg  38002  radcnvrat  38513  nzprmdif  38518  bcc0  38539  bccp1k  38540  bccbc  38544  binomcxplemnn0  38548  binomcxplemrat  38549  binomcxplemfrat  38550  binomcxplemnotnn0  38555  fzisoeu  39514  mccllem  39829  dvxpaek  40155  dvnxpaek  40157  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  stoweidlem24  40241  stirlinglem3  40293  stirlinglem7  40297  fourierdlem36  40360  fourierdlem47  40370  etransclem23  40474  etransclem32  40483  etransclem48  40499  fz0addcom  41327  addlenpfx  41398  pfxfv  41399  pfxtrcfvl  41405  pfxpfx  41415  ccats1pfxeq  41421  fmtnom1nn  41444  fmtnof1  41447  fmtnorec1  41449  sqrtpwpw2p  41450  fmtnorec2lem  41454  fmtnorec3  41460  fmtnofac2lem  41480  fmtnofac2  41481  fmtnofac1  41482  pwdif  41501  lighneallem3  41524  lighneallem4b  41526  altgsumbc  42130  altgsumbcALT  42131  nnpw2pmod  42377  dignn0ehalf  42411  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdiglem2  42416  nn0mullong  42419  aacllem  42547