Theorem nn0cnd 12682

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11211  ℕ₀cn0 12619

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7761  ax-resscn 11270  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-addrcl 11274  ax-mulcl 11275  ax-mulrcl 11276  ax-i2m1 11281  ax-1ne0 11282  ax-rnegex 11284  ax-rrecex 11285  ax-cnre 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6311  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-ov 7433  df-om 7888  df-2nd 8012  df-frecs 8313  df-wrecs 8344  df-recs 8393  df-rdg 8432  df-nn 12349  df-n0 12620

This theorem is used by:  quoremnn0ALT  14010  expaddzlem  14261  expaddz  14262  expmulz  14264  facdiv  14444  faclbnd4lem3  14452  bcp1n  14473  bcn2m1  14481  bcn2p1  14482  hashgadd  14534  hashdom  14536  hashun3  14541  hashssdif  14570  hashdifpr  14573  hashxplem  14591  hashmap  14593  hashreshashfun  14597  hashbclem  14610  hashf1lem2  14614  hashf1  14615  ccatval3  14737  ccatval21sw  14744  ccatlid  14745  ccatrid  14746  ccatass  14747  ccatrn  14748  ccatf1  14749  lswccatn0lsw  14751  ccatalpha  14753  ccatws1lenp1b  14783  wrdlenccats1lenm1  14784  ccats1val2  14789  swrdccat2  14833  pfxfv  14846  addlenpfx  14854  pfxtrcfvl  14860  pfxpfx  14871  lenrevpfxcctswrd  14875  ccats1pfxeq  14877  ccatopth2  14880  cats1un  14884  swrdccat3b  14903  spllen  14917  splfv2a  14919  revccat  14929  revpfxsfxrev  14931  cshwlen  14964  cshwidxmod  14968  repswcshw  14977  2cshwid  14979  cshweqdif2  14984  relexpaddg  15221  rtrclreclem3  15228  isercoll2  15851  iseraltlem3  15866  fsumconst1  15972  hash2iun1dif1  16006  binomlem  16013  bcxmas  16019  incexclem  16020  incexc  16021  incexc2  16022  climcndslem1  16033  climcndslem2  16034  arisum  16044  arisum2  16045  pwdif  16052  geomulcvg  16060  mertens  16070  risefacval2  16192  fallfacval2  16193  fallfacval3  16194  risefallfac  16206  risefacp1  16210  fallfacp1  16211  fallfacfwd  16217  binomfallfaclem1  16220  binomfallfaclem2  16221  binomrisefac  16223  bpolycl  16233  bpolysum  16234  bpolydiflem  16235  fsumkthpow  16237  bpoly4  16240  effsumlt  16294  dvdsexp  16513  nn0ob  16569  divalgmod  16591  bitsinv1lem  16626  sadcp1  16640  sadcaddlem  16642  sadadd2lem  16644  sadadd3  16646  sadaddlem  16651  sadasslem  16655  smupp1  16665  smumullem  16677  mulgcd  16736  absmulgcd  16737  mulgcdr  16738  gcddiv  16739  lcmgcd  16797  lcmid  16799  lcm1  16800  3lcm2e6woprm  16805  6lcm4e12  16806  mulgcddvds  16845  qredeu  16848  divgcdcoprm0  16855  divgcdcoprmex  16856  cncongr1  16857  cncongr2  16858  odzdvds  16988  powm2modprm  16996  coprimeprodsq  17001  pceulem  17038  pczpre  17040  pcqmul  17046  pcaddlem  17081  pcmpt  17085  pcmpt2  17086  sumhash  17089  oddprmdvds  17096  mul4sq  17147  4sqlem12  17149  vdwapun  17167  vdwlem2  17175  vdwlem3  17176  vdwlem6  17179  vdwlem8  17181  vdwlem9  17182  ramub1lem2  17220  ramcl  17222  chnrev  18816  mulgnn0dir  19329  mulgnn0ass  19335  lagsubg2  19424  psgnunilem2  19724  odmodnn0  19769  odmulg  19785  odmulgeq  19786  odinv  19790  sylow1lem1  19827  sylow2a  19848  sylow2blem3  19851  sylow3lem3  19858  sylow3lem4  19859  efginvrel2  19956  efgsval2  19962  efgsp1  19966  efgredlemg  19971  efgredleme  19972  efgcpbllemb  19984  odadd2  20078  odadd  20079  torsubg  20083  frgpnabllem1  20102  pgpfaclem1  20312  fincygsubgodd  20343  omndmul2  20362  omndmul3  20363  srgbinomlem3  20469  srgbinomlem4  20470  nn0srg  21758  freshmansdream  21895  mplcoe5  22364  mhpmulcl  22485  mhppwdeg  22486  psdmplcl  22498  psdmul  22502  coe1tmmul2  22610  coe1tmmul2fv  22612  coe1pwmulfv  22614  mbfi1fseqlem3  26053  dvn2bss  26265  itgpowd  26385  tdeglem4  26393  tdeglem2  26394  mdegmullem  26411  coe1mul3  26432  ply1divex  26470  fta1glem1  26501  plyaddlem1  26547  plymullem1  26548  coeeulem  26558  coemulc  26589  dgrmulc  26605  dgrcolem2  26608  dgrco  26609  dvply1  26620  dvply2g  26621  plydivlem4  26632  fta1lem  26643  vieta1lem1  26648  aareccl  26668  aaliou3lem8  26687  taylply2  26710  dvtaylp  26712  dvntaylp  26713  dvntaylp0  26714  dvradcnv  26763  pserdvlem2  26770  advlogexp  26998  cxpeq  27100  atantayl3  27282  birthdaylem2  27295  harmonicbnd4  27353  dmgmaddnn0  27369  lgamucov  27380  wilthlem2  27411  basellem2  27424  basellem3  27425  basellem5  27427  0sgm  27486  sgmppw  27539  chtublem  27553  chpval2  27560  sumdchr2  27612  bcp1ctr  27621  lgslem1  27639  gausslemma2dlem6  27714  gausslemma2d  27716  lgseisenlem2  27718  lgseisenlem3  27719  lgsquadlem1  27722  lgsquadlem2  27723  lgsquad2lem2  27727  m1lgs  27730  2lgslem1c  27735  2lgslem3a  27738  2lgslem3b  27739  2lgslem3c  27740  2lgslem3d  27741  2sqlem8  27768  2sq2  27775  2sqmod  27778  dchrisumlem1  27831  dchrisum0flblem2  27851  rpvmasum2  27854  mulogsumlem  27873  selberg2lem  27892  pntrsumo1  27907  pntrlog2bndlem4  27922  finsumvtxdg2ssteplem4  30144  vtxdgoddnumeven  30149  wlklenvm1  30217  wlklenvclwlk  30249  revwlk  30282  crctcshlem4  30424  crctcsh  30428  wlklnwwlkln2lem  30486  wlknwwlksnbij  30492  wwlksnred  30496  wwlksnext  30497  wwlksnextbi  30498  wwlksnredwwlkn  30499  wwlksnextproplem2  30514  rusgrnumwwlks  30581  rusgrnumwwlk  30582  clwwlkccatlem  30595  clwlkclwwlk  30608  clwwlkwwlksb  30660  eupth2lem3lem3  30846  eupth2lem3lem6  30849  fusgreghash2wsp  30954  frrusgrord0lem  30955  numclwwlk1  30977  numclwwlk3  31001  ex-lcm  31074  ex-ind-dvds  31077  nnmulge  33387  elq2  33459  divnumden2  33463  pfxlsw2ccat  33569  ccatws1f1o  33570  wrdt2ind  33572  gsummptrev  33673  gsummptp1  33674  gsummulsubdishift1  33685  cycpmco2lem2  33744  cycpmco2lem3  33745  cycpmco2lem4  33746  cycpmco2lem5  33747  cycpmco2lem6  33748  cycpmco2lem7  33749  cycpmco2  33750  archiabllem1a  33808  gsumind  33962  deg1prod  34171  ply1dg3rt0irred  34172  esplyind  34263  esplyindfv  34264  esplyfvn  34265  vietadeg1  34266  vietalem  34267  vieta  34268  iconstr  34454  cos9thpiminplylem1  34470  oddpwdc  35042  eulerpartlemsv2  35046  eulerpartlems  35048  eulerpartlemsv3  35049  eulerpartlemv  35052  eulerpartlemb  35056  iwrdsplit  35075  ballotlemgun  35213  ccatmulgnn0dir  35230  ofcccat  35231  signsplypnf  35235  signslema  35247  signstfvn  35254  signstfveq0  35262  signsvtp  35268  signsvtn  35269  signlem0  35272  signshf  35273  fsum2dsub  35292  hashreprin  35305  breprexp  35318  circlemeth  35325  lpadlem2  35368  lpadlen2  35369  subfacp1lem6  36074  subfacval2  36076  subfaclim  36077  cvmliftlem7  36180  elmrsubrn  36409  bcprod  36633  bccolsum  36634  faclimlem1  36638  faclim2  36643  fwddifnp1  37060  knoppndvlem6  37513  knoppndvlem14  37521  poimirlem4  38685  poimirlem5  38686  poimirlem6  38687  poimirlem7  38688  poimirlem10  38691  poimirlem11  38692  poimirlem12  38693  poimirlem16  38697  poimirlem17  38698  poimirlem19  38700  poimirlem20  38701  poimirlem22  38703  poimirlem24  38705  poimirlem25  38706  poimirlem29  38710  poimirlem31  38712  lcmineqlem1  43222  lcmineqlem2  43223  lcmineqlem12  43233  lcmineqlem17  43238  primrootscoprmpow  43292  aks6d1c2p2  43312  deg1gprod  43333  deg1pow  43334  2np3bcnp1  43337  2ap1caineq  43338  sticksstones7  43345  sticksstones9  43347  sticksstones10  43348  sticksstones11  43349  sticksstones12a  43350  sticksstones12  43351  sticksstones22  43361  aks6d1c6lem1  43363  aks6d1c6lem3  43365  bcled  43371  bcle2d  43372  aks6d1c7lem1  43373  unitscyglem2  43389  unitscyglem4  43391  ccatcan2d  43445  fz1sump1  43510  sumcubes  43513  zaddcomlem  43670  frlmvscadiccat  43716  fltnltalem  43816  3cubeslem3l  43839  3cubeslem3r  43840  rmxyneg  44070  rmxyadd  44071  rmyp1  44083  rmxm1  44084  rmym1  44085  rmxluc  44086  rmyluc  44087  rmxdbl  44089  rmydbl  44090  jm2.18  44138  jm2.19lem1  44139  jm2.19lem2  44140  jm2.22  44145  jm2.23  44146  jm2.25  44149  jm2.27c  44157  rmxdiophlem  44165  expdioph  44173  hbtlem4  44271  relexpmulg  44853  radcnvrat  45441  nzprmdif  45446  bcc0  45467  bccp1k  45468  bccbc  45472  binomcxplemnn0  45476  binomcxplemrat  45477  binomcxplemfrat  45478  binomcxplemnotnn0  45483  fzisoeu  46458  mccllem  46751  dvxpaek  47092  dvnxpaek  47094  dvnmul  47095  dvnprodlem1  47098  dvnprodlem2  47099  stoweidlem24  47176  stirlinglem3  47228  stirlinglem7  47232  fourierdlem36  47295  fourierdlem47  47305  etransclem23  47409  etransclem32  47418  etransclem48  47434  fz0addcom  48529  fmtnom1nn  48759  fmtnof1  48762  fmtnorec1  48764  sqrtpwpw2p  48765  fmtnorec2lem  48769  fmtnorec3  48775  fmtnofac2lem  48795  fmtnofac2  48796  fmtnofac1  48797  lighneallem3  48834  lighneallem4b  48836  altgsumbc  49606  altgsumbcALT  49607  nnpw2pmod  49837  dignn0ehalf  49871  nn0sumshdiglemA  49873  nn0sumshdiglemB  49874  nn0sumshdiglem2  49876  nn0mullong  49879  itcovalpclem2  49925  itcovalt2lem2lem2  49928  itcovalt2lem1  49929  aacllem  51156