Theorem nn0cnd 9555

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8125  ℕ₀cn0 9496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4228  ax-cnex 8218  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224  ax-rnegex 8236

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-int 3950  df-inn 9238  df-n0 9497

This theorem is referenced by:  modsumfzodifsn  10758  addmodlteq  10760  uzennn  10798  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  nn0le2msqd  11081  nn0opthlem1d  11082  nn0opthd  11084  nn0opth2d  11085  facdiv  11100  bcp1n  11123  bcn2m1  11132  bcn2p1  11133  omgadd  11166  fihashssdif  11183  hashdifpr  11185  hashxp  11191  hashmap  11192  hashfibclem  11206  zfz1isolemsplit  11210  zfz1isolem1  11212  ccatval3  11287  ccatval21sw  11293  ccatlid  11294  ccatrid  11295  ccatass  11296  ccatrn  11297  lswccatn0lsw  11299  ccatalpha  11301  ccatws1lenp1bg  11323  wrdlenccats1lenm1g  11324  ccats1val2  11328  lswccats1  11331  swrdccat2  11363  pfxfv  11376  addlenpfx  11383  pfxtrcfvl  11389  pfxpfx  11400  lenrevpfxcctswrd  11404  ccats1pfxeq  11406  ccatopth2  11409  cats1un  11413  swrdccat3b  11432  cats1fvnd  11457  fsumconst  12140  hash2iun1dif1  12166  binomlem  12169  bcxmas  12175  arisum  12184  arisum2  12185  mertensabs  12223  effsumlt  12378  dvdsexp  12547  nn0ob  12594  divalglemnn  12604  divalgmod  12613  bitsinv1lem  12647  bezoutlemnewy  12692  bezoutlema  12695  bezoutlemb  12696  mulgcd  12712  absmulgcd  12713  mulgcdr  12714  gcddiv  12715  lcmgcd  12775  lcmid  12777  lcm1  12778  3lcm2e6woprm  12783  6lcm4e12  12784  mulgcddvds  12791  qredeu  12794  divgcdcoprm0  12798  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  pw2dvdseulemle  12864  phiprmpw  12919  eulerthlema  12927  prmdiveq  12933  odzdvds  12943  powm2modprm  12950  coprimeprodsq  12955  pceulem  12992  pczpre  12995  pcqmul  13001  pcaddlem  13037  pcmpt  13041  pcmpt2  13042  sumhashdc  13045  pcfac  13048  oddprmdvds  13052  mul4sq  13092  4sqlem12  13100  mulgnn0dir  13869  mulgnn0ass  13875  plyaddlem1  15612  plymullem1  15613  dvply1  15630  dvply2g  15631  0sgm  15853  sgmppw  15860  lgslem1  15873  lgsvalmod  15892  gausslemma2dlem6  15940  gausslemma2d  15942  lgseisenlem2  15944  lgseisenlem3  15945  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem2  15955  m1lgs  15958  2lgslem1c  15963  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2sqlem8  15996  vtxdfifiun  16292  vtxdumgrfival  16293  p1evtxdeqfi  16307  wlklenvm1  16336  wlklenvm1g  16337  wlklenvclwlk  16368  clwwlkccatlem  16395  eupth2lem3lem3fi  16465  eupth2lem3lem6fi  16466  depindlem1  16501