Theorem nn0cnd 12531

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11105  ℕ₀cn0 12469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-i2m1 11175  ax-1ne0 11176  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-nn 12210  df-n0 12470

This theorem is referenced by:  quoremnn0ALT  13819  expaddzlem  14068  expaddz  14069  expmulz  14071  facdiv  14244  faclbnd4lem3  14252  bcp1n  14273  bcn2m1  14281  bcn2p1  14282  hashgadd  14334  hashdom  14336  hashun3  14341  hashssdif  14369  hashdifpr  14372  hashxplem  14390  hashmap  14392  hashreshashfun  14396  hashbclem  14408  hashf1lem2  14414  hashf1  14415  ccatval3  14526  ccatval21sw  14532  ccatlid  14533  ccatrid  14534  ccatass  14535  ccatrn  14536  lswccatn0lsw  14538  ccatalpha  14540  ccatws1lenp1b  14568  wrdlenccats1lenm1  14569  ccats1val2  14574  swrdccat2  14616  pfxfv  14629  addlenpfx  14638  pfxtrcfvl  14644  pfxpfx  14655  ccats1pfxeq  14661  ccatopth2  14664  cats1un  14668  swrdccat3b  14687  spllen  14701  splfv2a  14703  revccat  14713  cshwlen  14746  cshwidxmod  14750  repswcshw  14759  2cshwid  14761  cshweqdif2  14766  relexpaddg  14997  rtrclreclem3  15004  isercoll2  15612  iseraltlem3  15627  hash2iun1dif1  15767  binomlem  15772  bcxmas  15778  incexclem  15779  incexc  15780  incexc2  15781  climcndslem1  15792  climcndslem2  15793  arisum  15803  arisum2  15804  pwdif  15811  geomulcvg  15819  mertens  15829  risefacval2  15951  fallfacval2  15952  fallfacval3  15953  risefallfac  15965  risefacp1  15970  fallfacp1  15971  fallfacfwd  15977  binomfallfaclem1  15980  binomfallfaclem2  15981  binomrisefac  15983  bpolycl  15993  bpolysum  15994  bpolydiflem  15995  fsumkthpow  15997  bpoly4  16000  effsumlt  16051  dvdsexp  16268  nn0ob  16324  divalgmod  16346  bitsinv1lem  16379  sadcp1  16393  sadcaddlem  16395  sadadd2lem  16397  sadadd3  16399  sadaddlem  16404  sadasslem  16408  smupp1  16418  smumullem  16430  mulgcd  16487  absmulgcd  16488  mulgcdr  16489  gcddiv  16490  lcmgcd  16541  lcmid  16543  lcm1  16544  3lcm2e6woprm  16549  6lcm4e12  16550  mulgcddvds  16589  qredeu  16592  divgcdcoprm0  16599  divgcdcoprmex  16600  cncongr1  16601  cncongr2  16602  odzdvds  16725  powm2modprm  16733  coprimeprodsq  16738  pceulem  16775  pczpre  16777  pcqmul  16783  pcaddlem  16818  pcmpt  16822  pcmpt2  16823  sumhash  16826  oddprmdvds  16833  mul4sq  16884  4sqlem12  16886  vdwapun  16904  vdwlem2  16912  vdwlem3  16913  vdwlem6  16916  vdwlem8  16918  vdwlem9  16919  ramub1lem2  16957  ramcl  16959  mulgnn0dir  18979  mulgnn0ass  18985  lagsubg2  19066  psgnunilem2  19358  odmodnn0  19403  odmulg  19419  odmulgeq  19420  odinv  19424  sylow1lem1  19461  sylow2a  19482  sylow2blem3  19485  sylow3lem3  19492  sylow3lem4  19493  efginvrel2  19590  efgsval2  19596  efgsp1  19600  efgredlemg  19605  efgredleme  19606  efgcpbllemb  19618  odadd2  19712  odadd  19713  torsubg  19717  frgpnabllem1  19736  pgpfaclem1  19946  fincygsubgodd  19977  srgbinomlem3  20045  srgbinomlem4  20046  nn0srg  21008  mplcoe5  21587  mhpmulcl  21684  mhppwdeg  21685  coe1tmmul2  21790  coe1tmmul2fv  21792  coe1pwmulfv  21794  mbfi1fseqlem3  25227  dvn2bss  25439  itgpowd  25559  tdeglem4  25569  tdeglem4OLD  25570  tdeglem2  25571  mdegmullem  25588  coe1mul3  25609  ply1divex  25646  fta1glem1  25675  plyaddlem1  25719  plymullem1  25720  coeeulem  25730  coemulc  25761  dgrmulc  25777  dgrcolem2  25780  dgrco  25781  dvply1  25789  dvply2g  25790  plydivlem4  25801  fta1lem  25812  vieta1lem1  25815  aareccl  25831  aaliou3lem8  25850  taylply2  25872  dvtaylp  25874  dvntaylp  25875  dvntaylp0  25876  dvradcnv  25925  pserdvlem2  25932  advlogexp  26155  cxpeq  26255  atantayl3  26434  birthdaylem2  26447  harmonicbnd4  26505  dmgmaddnn0  26521  lgamucov  26532  wilthlem2  26563  basellem2  26576  basellem3  26577  basellem5  26579  0sgm  26638  sgmppw  26690  chtublem  26704  chpval2  26711  sumdchr2  26763  bcp1ctr  26772  lgslem1  26790  gausslemma2dlem6  26865  gausslemma2d  26867  lgseisenlem2  26869  lgseisenlem3  26870  lgsquadlem1  26873  lgsquadlem2  26874  lgsquad2lem2  26878  m1lgs  26881  2lgslem1c  26886  2lgslem3a  26889  2lgslem3b  26890  2lgslem3c  26891  2lgslem3d  26892  2sqlem8  26919  2sq2  26926  2sqmod  26929  dchrisumlem1  26982  dchrisum0flblem2  27002  rpvmasum2  27005  mulogsumlem  27024  selberg2lem  27043  pntrsumo1  27058  pntrlog2bndlem4  27073  finsumvtxdg2ssteplem4  28795  vtxdgoddnumeven  28800  wlklenvm1  28869  wlklenvclwlk  28902  crctcshlem4  29064  crctcsh  29068  wlklnwwlkln2lem  29126  wlknwwlksnbij  29132  wwlksnred  29136  wwlksnext  29137  wwlksnextbi  29138  wwlksnredwwlkn  29139  wwlksnextproplem2  29154  rusgrnumwwlks  29218  rusgrnumwwlk  29219  clwwlkccatlem  29232  clwlkclwwlk  29245  clwwlkwwlksb  29297  eupth2lem3lem3  29473  eupth2lem3lem6  29476  fusgreghash2wsp  29581  frrusgrord0lem  29582  numclwwlk1  29604  numclwwlk3  29628  ex-lcm  29701  ex-ind-dvds  29704  nnmulge  31951  divnumden2  32012  ccatf1  32103  pfxlsw2ccat  32104  wrdt2ind  32105  omndmul2  32218  omndmul3  32219  cycpmco2lem2  32274  cycpmco2lem3  32275  cycpmco2lem4  32276  cycpmco2lem5  32277  cycpmco2lem6  32278  cycpmco2lem7  32279  cycpmco2  32280  archiabllem1a  32325  freshmansdream  32370  oddpwdc  33342  eulerpartlemsv2  33346  eulerpartlems  33348  eulerpartlemsv3  33349  eulerpartlemv  33352  eulerpartlemb  33356  iwrdsplit  33375  ballotlemgun  33512  ccatmulgnn0dir  33542  ofcccat  33543  signsplypnf  33550  signslema  33562  signstfvn  33569  signstfveq0  33577  signsvtp  33583  signsvtn  33584  signlem0  33587  signshf  33588  fsum2dsub  33608  hashreprin  33621  breprexp  33634  circlemeth  33641  lpadlem2  33681  lpadlen2  33682  revpfxsfxrev  34095  revwlk  34104  subfacp1lem6  34165  subfacval2  34167  subfaclim  34168  cvmliftlem7  34271  elmrsubrn  34500  bcprod  34697  bccolsum  34698  faclimlem1  34702  faclim2  34707  fwddifnp1  35126  knoppndvlem6  35382  knoppndvlem14  35390  poimirlem4  36481  poimirlem5  36482  poimirlem6  36483  poimirlem7  36484  poimirlem10  36487  poimirlem11  36488  poimirlem12  36489  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem22  36499  poimirlem24  36501  poimirlem25  36502  poimirlem29  36506  poimirlem31  36508  lcmineqlem1  40883  lcmineqlem2  40884  lcmineqlem12  40894  lcmineqlem17  40899  aks6d1c2p2  40946  2np3bcnp1  40949  2ap1caineq  40950  sticksstones7  40957  sticksstones9  40959  sticksstones10  40960  sticksstones11  40961  sticksstones12a  40962  sticksstones12  40963  sticksstones22  40973  ccatcan2d  41067  frlmvscadiccat  41078  fz1sump1  41204  sumcubes  41207  zaddcomlem  41321  fltnltalem  41401  3cubeslem3l  41410  3cubeslem3r  41411  rmxyneg  41645  rmxyadd  41646  rmyp1  41658  rmxm1  41659  rmym1  41660  rmxluc  41661  rmyluc  41662  rmxdbl  41664  rmydbl  41665  jm2.18  41713  jm2.19lem1  41714  jm2.19lem2  41715  jm2.22  41720  jm2.23  41721  jm2.25  41724  jm2.27c  41732  rmxdiophlem  41740  expdioph  41748  hbtlem4  41854  relexpmulg  42447  radcnvrat  43059  nzprmdif  43064  bcc0  43085  bccp1k  43086  bccbc  43090  binomcxplemnn0  43094  binomcxplemrat  43095  binomcxplemfrat  43096  binomcxplemnotnn0  43101  fzisoeu  43997  mccllem  44300  dvxpaek  44643  dvnxpaek  44645  dvnmul  44646  dvnprodlem1  44649  dvnprodlem2  44650  stoweidlem24  44727  stirlinglem3  44779  stirlinglem7  44783  fourierdlem36  44846  fourierdlem47  44856  etransclem23  44960  etransclem32  44969  etransclem48  44985  fz0addcom  46012  fmtnom1nn  46187  fmtnof1  46190  fmtnorec1  46192  sqrtpwpw2p  46193  fmtnorec2lem  46197  fmtnorec3  46203  fmtnofac2lem  46223  fmtnofac2  46224  fmtnofac1  46225  lighneallem3  46262  lighneallem4b  46264  altgsumbc  46982  altgsumbcALT  46983  nnpw2pmod  47223  dignn0ehalf  47257  nn0sumshdiglemA  47259  nn0sumshdiglemB  47260  nn0sumshdiglem2  47262  nn0mullong  47265  itcovalpclem2  47311  itcovalt2lem2lem2  47314  itcovalt2lem1  47315  aacllem  47802