Theorem nn0cnd 12462

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11022  ℕ₀cn0 12399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-i2m1 11092  ax-1ne0 11093  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12144  df-n0 12400

This theorem is referenced by:  quoremnn0ALT  13775  expaddzlem  14026  expaddz  14027  expmulz  14029  facdiv  14208  faclbnd4lem3  14216  bcp1n  14237  bcn2m1  14245  bcn2p1  14246  hashgadd  14298  hashdom  14300  hashun3  14305  hashssdif  14333  hashdifpr  14336  hashxplem  14354  hashmap  14356  hashreshashfun  14360  hashbclem  14373  hashf1lem2  14377  hashf1  14378  ccatval3  14500  ccatval21sw  14507  ccatlid  14508  ccatrid  14509  ccatass  14510  ccatrn  14511  lswccatn0lsw  14513  ccatalpha  14515  ccatws1lenp1b  14543  wrdlenccats1lenm1  14544  ccats1val2  14549  swrdccat2  14591  pfxfv  14604  addlenpfx  14612  pfxtrcfvl  14618  pfxpfx  14629  lenrevpfxcctswrd  14633  ccats1pfxeq  14635  ccatopth2  14638  cats1un  14642  swrdccat3b  14661  spllen  14675  splfv2a  14677  revccat  14687  cshwlen  14720  cshwidxmod  14724  repswcshw  14733  2cshwid  14735  cshweqdif2  14740  relexpaddg  14974  rtrclreclem3  14981  isercoll2  15590  iseraltlem3  15605  hash2iun1dif1  15745  binomlem  15750  bcxmas  15756  incexclem  15757  incexc  15758  incexc2  15759  climcndslem1  15770  climcndslem2  15771  arisum  15781  arisum2  15782  pwdif  15789  geomulcvg  15797  mertens  15807  risefacval2  15931  fallfacval2  15932  fallfacval3  15933  risefallfac  15945  risefacp1  15950  fallfacp1  15951  fallfacfwd  15957  binomfallfaclem1  15960  binomfallfaclem2  15961  binomrisefac  15963  bpolycl  15973  bpolysum  15974  bpolydiflem  15975  fsumkthpow  15977  bpoly4  15980  effsumlt  16034  dvdsexp  16253  nn0ob  16309  divalgmod  16331  bitsinv1lem  16366  sadcp1  16380  sadcaddlem  16382  sadadd2lem  16384  sadadd3  16386  sadaddlem  16391  sadasslem  16395  smupp1  16405  smumullem  16417  mulgcd  16473  absmulgcd  16474  mulgcdr  16475  gcddiv  16476  lcmgcd  16532  lcmid  16534  lcm1  16535  3lcm2e6woprm  16540  6lcm4e12  16541  mulgcddvds  16580  qredeu  16583  divgcdcoprm0  16590  divgcdcoprmex  16591  cncongr1  16592  cncongr2  16593  odzdvds  16721  powm2modprm  16729  coprimeprodsq  16734  pceulem  16771  pczpre  16773  pcqmul  16779  pcaddlem  16814  pcmpt  16818  pcmpt2  16819  sumhash  16822  oddprmdvds  16829  mul4sq  16880  4sqlem12  16882  vdwapun  16900  vdwlem2  16908  vdwlem3  16909  vdwlem6  16912  vdwlem8  16914  vdwlem9  16915  ramub1lem2  16953  ramcl  16955  chnrev  18548  mulgnn0dir  19032  mulgnn0ass  19038  lagsubg2  19121  psgnunilem2  19422  odmodnn0  19467  odmulg  19483  odmulgeq  19484  odinv  19488  sylow1lem1  19525  sylow2a  19546  sylow2blem3  19549  sylow3lem3  19556  sylow3lem4  19557  efginvrel2  19654  efgsval2  19660  efgsp1  19664  efgredlemg  19669  efgredleme  19670  efgcpbllemb  19682  odadd2  19776  odadd  19777  torsubg  19781  frgpnabllem1  19800  pgpfaclem1  20010  fincygsubgodd  20041  omndmul2  20060  omndmul3  20061  srgbinomlem3  20161  srgbinomlem4  20162  nn0srg  21390  freshmansdream  21527  mplcoe5  21993  mhpmulcl  22090  mhppwdeg  22091  psdmplcl  22103  psdmul  22107  coe1tmmul2  22216  coe1tmmul2fv  22218  coe1pwmulfv  22220  mbfi1fseqlem3  25672  dvn2bss  25886  itgpowd  26011  tdeglem4  26019  tdeglem2  26020  mdegmullem  26037  coe1mul3  26058  ply1divex  26096  fta1glem1  26127  plyaddlem1  26172  plymullem1  26173  coeeulem  26183  coemulc  26214  dgrmulc  26231  dgrcolem2  26234  dgrco  26235  dvply1  26245  dvply2g  26246  dvply2gOLD  26247  plydivlem4  26258  fta1lem  26269  vieta1lem1  26272  aareccl  26288  aaliou3lem8  26307  taylply2  26329  taylply2OLD  26330  dvtaylp  26332  dvntaylp  26333  dvntaylp0  26334  dvradcnv  26384  pserdvlem2  26392  advlogexp  26618  cxpeq  26721  atantayl3  26903  birthdaylem2  26916  harmonicbnd4  26975  dmgmaddnn0  26991  lgamucov  27002  wilthlem2  27033  basellem2  27046  basellem3  27047  basellem5  27049  0sgm  27108  sgmppw  27162  chtublem  27176  chpval2  27183  sumdchr2  27235  bcp1ctr  27244  lgslem1  27262  gausslemma2dlem6  27337  gausslemma2d  27339  lgseisenlem2  27341  lgseisenlem3  27342  lgsquadlem1  27345  lgsquadlem2  27346  lgsquad2lem2  27350  m1lgs  27353  2lgslem1c  27358  2lgslem3a  27361  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  2sqlem8  27391  2sq2  27398  2sqmod  27401  dchrisumlem1  27454  dchrisum0flblem2  27474  rpvmasum2  27477  mulogsumlem  27496  selberg2lem  27515  pntrsumo1  27530  pntrlog2bndlem4  27545  finsumvtxdg2ssteplem4  29571  vtxdgoddnumeven  29576  wlklenvm1  29644  wlklenvclwlk  29676  crctcshlem4  29842  crctcsh  29846  wlklnwwlkln2lem  29904  wlknwwlksnbij  29910  wwlksnred  29914  wwlksnext  29915  wwlksnextbi  29916  wwlksnredwwlkn  29917  wwlksnextproplem2  29932  rusgrnumwwlks  29999  rusgrnumwwlk  30000  clwwlkccatlem  30013  clwlkclwwlk  30026  clwwlkwwlksb  30078  eupth2lem3lem3  30254  eupth2lem3lem6  30257  fusgreghash2wsp  30362  frrusgrord0lem  30363  numclwwlk1  30385  numclwwlk3  30409  ex-lcm  30482  ex-ind-dvds  30485  nnmulge  32767  elq2  32841  divnumden2  32845  ccatf1  32980  pfxlsw2ccat  32981  ccatws1f1o  32982  wrdt2ind  32984  gsummptrev  33088  gsummptp1  33089  gsummulsubdishift1  33100  cycpmco2lem2  33158  cycpmco2lem3  33159  cycpmco2lem4  33160  cycpmco2lem5  33161  cycpmco2lem6  33162  cycpmco2lem7  33163  cycpmco2  33164  archiabllem1a  33222  gsumind  33375  deg1prod  33613  ply1dg3rt0irred  33614  esplyind  33680  esplyindfv  33681  esplyfvn  33682  vietadeg1  33683  vietalem  33684  vieta  33685  iconstr  33872  cos9thpiminplylem1  33888  oddpwdc  34460  eulerpartlemsv2  34464  eulerpartlems  34466  eulerpartlemsv3  34467  eulerpartlemv  34470  eulerpartlemb  34474  iwrdsplit  34493  ballotlemgun  34631  ccatmulgnn0dir  34648  ofcccat  34649  signsplypnf  34656  signslema  34668  signstfvn  34675  signstfveq0  34683  signsvtp  34689  signsvtn  34690  signlem0  34693  signshf  34694  fsum2dsub  34713  hashreprin  34726  breprexp  34739  circlemeth  34746  lpadlem2  34786  lpadlen2  34787  revpfxsfxrev  35259  revwlk  35268  subfacp1lem6  35328  subfacval2  35330  subfaclim  35331  cvmliftlem7  35434  elmrsubrn  35663  bcprod  35881  bccolsum  35882  faclimlem1  35886  faclim2  35891  fwddifnp1  36308  knoppndvlem6  36660  knoppndvlem14  36668  poimirlem4  37764  poimirlem5  37765  poimirlem6  37766  poimirlem7  37767  poimirlem10  37770  poimirlem11  37771  poimirlem12  37772  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem22  37782  poimirlem24  37784  poimirlem25  37785  poimirlem29  37789  poimirlem31  37791  lcmineqlem1  42222  lcmineqlem2  42223  lcmineqlem12  42233  lcmineqlem17  42238  primrootscoprmpow  42292  aks6d1c2p2  42312  deg1gprod  42333  deg1pow  42334  2np3bcnp1  42337  2ap1caineq  42338  sticksstones7  42345  sticksstones9  42347  sticksstones10  42348  sticksstones11  42349  sticksstones12a  42350  sticksstones12  42351  sticksstones22  42361  aks6d1c6lem1  42363  aks6d1c6lem3  42365  bcled  42371  bcle2d  42372  aks6d1c7lem1  42373  unitscyglem2  42389  unitscyglem4  42391  ccatcan2d  42448  fz1sump1  42507  sumcubes  42510  zaddcomlem  42660  frlmvscadiccat  42703  fltnltalem  42847  3cubeslem3l  42870  3cubeslem3r  42871  rmxyneg  43104  rmxyadd  43105  rmyp1  43117  rmxm1  43118  rmym1  43119  rmxluc  43120  rmyluc  43121  rmxdbl  43123  rmydbl  43124  jm2.18  43172  jm2.19lem1  43173  jm2.19lem2  43174  jm2.22  43179  jm2.23  43180  jm2.25  43183  jm2.27c  43191  rmxdiophlem  43199  expdioph  43207  hbtlem4  43310  relexpmulg  43893  radcnvrat  44497  nzprmdif  44502  bcc0  44523  bccp1k  44524  bccbc  44528  binomcxplemnn0  44532  binomcxplemrat  44533  binomcxplemfrat  44534  binomcxplemnotnn0  44539  fzisoeu  45490  mccllem  45785  dvxpaek  46126  dvnxpaek  46128  dvnmul  46129  dvnprodlem1  46132  dvnprodlem2  46133  stoweidlem24  46210  stirlinglem3  46262  stirlinglem7  46266  fourierdlem36  46329  fourierdlem47  46339  etransclem23  46443  etransclem32  46452  etransclem48  46468  fz0addcom  47505  fmtnom1nn  47720  fmtnof1  47723  fmtnorec1  47725  sqrtpwpw2p  47726  fmtnorec2lem  47730  fmtnorec3  47736  fmtnofac2lem  47756  fmtnofac2  47757  fmtnofac1  47758  lighneallem3  47795  lighneallem4b  47797  altgsumbc  48540  altgsumbcALT  48541  nnpw2pmod  48771  dignn0ehalf  48805  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808  nn0sumshdiglem2  48810  nn0mullong  48813  itcovalpclem2  48859  itcovalt2lem2lem2  48862  itcovalt2lem1  48863  aacllem  49988