Theorem nn0cnd 12615

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11182  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-nn 12294  df-n0 12554

This theorem is referenced by:  quoremnn0ALT  13908  expaddzlem  14156  expaddz  14157  expmulz  14159  facdiv  14336  faclbnd4lem3  14344  bcp1n  14365  bcn2m1  14373  bcn2p1  14374  hashgadd  14426  hashdom  14428  hashun3  14433  hashssdif  14461  hashdifpr  14464  hashxplem  14482  hashmap  14484  hashreshashfun  14488  hashbclem  14501  hashf1lem2  14505  hashf1  14506  ccatval3  14627  ccatval21sw  14633  ccatlid  14634  ccatrid  14635  ccatass  14636  ccatrn  14637  lswccatn0lsw  14639  ccatalpha  14641  ccatws1lenp1b  14669  wrdlenccats1lenm1  14670  ccats1val2  14675  swrdccat2  14717  pfxfv  14730  addlenpfx  14739  pfxtrcfvl  14745  pfxpfx  14756  ccats1pfxeq  14762  ccatopth2  14765  cats1un  14769  swrdccat3b  14788  spllen  14802  splfv2a  14804  revccat  14814  cshwlen  14847  cshwidxmod  14851  repswcshw  14860  2cshwid  14862  cshweqdif2  14867  relexpaddg  15102  rtrclreclem3  15109  isercoll2  15717  iseraltlem3  15732  hash2iun1dif1  15872  binomlem  15877  bcxmas  15883  incexclem  15884  incexc  15885  incexc2  15886  climcndslem1  15897  climcndslem2  15898  arisum  15908  arisum2  15909  pwdif  15916  geomulcvg  15924  mertens  15934  risefacval2  16058  fallfacval2  16059  fallfacval3  16060  risefallfac  16072  risefacp1  16077  fallfacp1  16078  fallfacfwd  16084  binomfallfaclem1  16087  binomfallfaclem2  16088  binomrisefac  16090  bpolycl  16100  bpolysum  16101  bpolydiflem  16102  fsumkthpow  16104  bpoly4  16107  effsumlt  16159  dvdsexp  16376  nn0ob  16432  divalgmod  16454  bitsinv1lem  16487  sadcp1  16501  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadaddlem  16512  sadasslem  16516  smupp1  16526  smumullem  16538  mulgcd  16595  absmulgcd  16596  mulgcdr  16597  gcddiv  16598  lcmgcd  16654  lcmid  16656  lcm1  16657  3lcm2e6woprm  16662  6lcm4e12  16663  mulgcddvds  16702  qredeu  16705  divgcdcoprm0  16712  divgcdcoprmex  16713  cncongr1  16714  cncongr2  16715  odzdvds  16842  powm2modprm  16850  coprimeprodsq  16855  pceulem  16892  pczpre  16894  pcqmul  16900  pcaddlem  16935  pcmpt  16939  pcmpt2  16940  sumhash  16943  oddprmdvds  16950  mul4sq  17001  4sqlem12  17003  vdwapun  17021  vdwlem2  17029  vdwlem3  17030  vdwlem6  17033  vdwlem8  17035  vdwlem9  17036  ramub1lem2  17074  ramcl  17076  mulgnn0dir  19144  mulgnn0ass  19150  lagsubg2  19234  psgnunilem2  19537  odmodnn0  19582  odmulg  19598  odmulgeq  19599  odinv  19603  sylow1lem1  19640  sylow2a  19661  sylow2blem3  19664  sylow3lem3  19671  sylow3lem4  19672  efginvrel2  19769  efgsval2  19775  efgsp1  19779  efgredlemg  19784  efgredleme  19785  efgcpbllemb  19797  odadd2  19891  odadd  19892  torsubg  19896  frgpnabllem1  19915  pgpfaclem1  20125  fincygsubgodd  20156  srgbinomlem3  20255  srgbinomlem4  20256  nn0srg  21478  freshmansdream  21616  mplcoe5  22081  mhpmulcl  22176  mhppwdeg  22177  psdmplcl  22189  psdmul  22193  coe1tmmul2  22300  coe1tmmul2fv  22302  coe1pwmulfv  22304  mbfi1fseqlem3  25772  dvn2bss  25986  itgpowd  26111  tdeglem4  26119  tdeglem2  26120  mdegmullem  26137  coe1mul3  26158  ply1divex  26196  fta1glem1  26227  plyaddlem1  26272  plymullem1  26273  coeeulem  26283  coemulc  26314  dgrmulc  26331  dgrcolem2  26334  dgrco  26335  dvply1  26343  dvply2g  26344  dvply2gOLD  26345  plydivlem4  26356  fta1lem  26367  vieta1lem1  26370  aareccl  26386  aaliou3lem8  26405  taylply2  26427  taylply2OLD  26428  dvtaylp  26430  dvntaylp  26431  dvntaylp0  26432  dvradcnv  26482  pserdvlem2  26490  advlogexp  26715  cxpeq  26818  atantayl3  27000  birthdaylem2  27013  harmonicbnd4  27072  dmgmaddnn0  27088  lgamucov  27099  wilthlem2  27130  basellem2  27143  basellem3  27144  basellem5  27146  0sgm  27205  sgmppw  27259  chtublem  27273  chpval2  27280  sumdchr2  27332  bcp1ctr  27341  lgslem1  27359  gausslemma2dlem6  27434  gausslemma2d  27436  lgseisenlem2  27438  lgseisenlem3  27439  lgsquadlem1  27442  lgsquadlem2  27443  lgsquad2lem2  27447  m1lgs  27450  2lgslem1c  27455  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2sqlem8  27488  2sq2  27495  2sqmod  27498  dchrisumlem1  27551  dchrisum0flblem2  27571  rpvmasum2  27574  mulogsumlem  27593  selberg2lem  27612  pntrsumo1  27627  pntrlog2bndlem4  27642  finsumvtxdg2ssteplem4  29584  vtxdgoddnumeven  29589  wlklenvm1  29658  wlklenvclwlk  29691  crctcshlem4  29853  crctcsh  29857  wlklnwwlkln2lem  29915  wlknwwlksnbij  29921  wwlksnred  29925  wwlksnext  29926  wwlksnextbi  29927  wwlksnredwwlkn  29928  wwlksnextproplem2  29943  rusgrnumwwlks  30007  rusgrnumwwlk  30008  clwwlkccatlem  30021  clwlkclwwlk  30034  clwwlkwwlksb  30086  eupth2lem3lem3  30262  eupth2lem3lem6  30265  fusgreghash2wsp  30370  frrusgrord0lem  30371  numclwwlk1  30393  numclwwlk3  30417  ex-lcm  30490  ex-ind-dvds  30493  nnmulge  32752  divnumden2  32819  ccatf1  32915  pfxlsw2ccat  32917  ccatws1f1o  32918  wrdt2ind  32920  omndmul2  33062  omndmul3  33063  cycpmco2lem2  33120  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  archiabllem1a  33171  ply1dg3rt0irred  33572  oddpwdc  34319  eulerpartlemsv2  34323  eulerpartlems  34325  eulerpartlemsv3  34326  eulerpartlemv  34329  eulerpartlemb  34333  iwrdsplit  34352  ballotlemgun  34489  ccatmulgnn0dir  34519  ofcccat  34520  signsplypnf  34527  signslema  34539  signstfvn  34546  signstfveq0  34554  signsvtp  34560  signsvtn  34561  signlem0  34564  signshf  34565  fsum2dsub  34584  hashreprin  34597  breprexp  34610  circlemeth  34617  lpadlem2  34657  lpadlen2  34658  revpfxsfxrev  35083  revwlk  35092  subfacp1lem6  35153  subfacval2  35155  subfaclim  35156  cvmliftlem7  35259  elmrsubrn  35488  bcprod  35700  bccolsum  35701  faclimlem1  35705  faclim2  35710  fwddifnp1  36129  knoppndvlem6  36483  knoppndvlem14  36491  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem24  37604  poimirlem25  37605  poimirlem29  37609  poimirlem31  37611  lcmineqlem1  41986  lcmineqlem2  41987  lcmineqlem12  41997  lcmineqlem17  42002  primrootscoprmpow  42056  aks6d1c2p2  42076  deg1gprod  42097  deg1pow  42098  2np3bcnp1  42101  2ap1caineq  42102  sticksstones7  42109  sticksstones9  42111  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  aks6d1c6lem1  42127  aks6d1c6lem3  42129  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  unitscyglem2  42153  unitscyglem4  42155  ccatcan2d  42246  fz1sump1  42298  sumcubes  42301  zaddcomlem  42427  frlmvscadiccat  42461  fltnltalem  42617  3cubeslem3l  42642  3cubeslem3r  42643  rmxyneg  42877  rmxyadd  42878  rmyp1  42890  rmxm1  42891  rmym1  42892  rmxluc  42893  rmyluc  42894  rmxdbl  42896  rmydbl  42897  jm2.18  42945  jm2.19lem1  42946  jm2.19lem2  42947  jm2.22  42952  jm2.23  42953  jm2.25  42956  jm2.27c  42964  rmxdiophlem  42972  expdioph  42980  hbtlem4  43083  relexpmulg  43672  radcnvrat  44283  nzprmdif  44288  bcc0  44309  bccp1k  44310  bccbc  44314  binomcxplemnn0  44318  binomcxplemrat  44319  binomcxplemfrat  44320  binomcxplemnotnn0  44325  fzisoeu  45215  mccllem  45518  dvxpaek  45861  dvnxpaek  45863  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  stoweidlem24  45945  stirlinglem3  45997  stirlinglem7  46001  fourierdlem36  46064  fourierdlem47  46074  etransclem23  46178  etransclem32  46187  etransclem48  46203  fz0addcom  47232  fmtnom1nn  47406  fmtnof1  47409  fmtnorec1  47411  sqrtpwpw2p  47412  fmtnorec2lem  47416  fmtnorec3  47422  fmtnofac2lem  47442  fmtnofac2  47443  fmtnofac1  47444  lighneallem3  47481  lighneallem4b  47483  altgsumbc  48077  altgsumbcALT  48078  nnpw2pmod  48317  dignn0ehalf  48351  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  nn0sumshdiglem2  48356  nn0mullong  48359  itcovalpclem2  48405  itcovalt2lem2lem2  48408  itcovalt2lem1  48409  aacllem  48895