Theorem nn0cnd 9435

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8008  ℕ₀cn0 9380

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8101  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107  ax-rnegex 8119

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-int 3924  df-inn 9122  df-n0 9381

This theorem is referenced by:  modsumfzodifsn  10630  addmodlteq  10632  uzennn  10670  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  nn0le2msqd  10953  nn0opthlem1d  10954  nn0opthd  10956  nn0opth2d  10957  facdiv  10972  bcp1n  10995  bcn2m1  11003  bcn2p1  11004  omgadd  11036  fihashssdif  11053  hashdifpr  11055  hashxp  11061  zfz1isolemsplit  11073  zfz1isolem1  11075  ccatval3  11147  ccatval21sw  11153  ccatlid  11154  ccatrid  11155  ccatass  11156  ccatrn  11157  lswccatn0lsw  11159  ccatalpha  11161  ccatws1lenp1bg  11183  wrdlenccats1lenm1g  11184  ccats1val2  11187  lswccats1  11190  swrdccat2  11219  pfxfv  11232  addlenpfx  11239  pfxtrcfvl  11245  pfxpfx  11256  lenrevpfxcctswrd  11260  ccats1pfxeq  11262  ccatopth2  11265  cats1un  11269  swrdccat3b  11288  cats1fvnd  11313  fsumconst  11981  hash2iun1dif1  12007  binomlem  12010  bcxmas  12016  arisum  12025  arisum2  12026  mertensabs  12064  effsumlt  12219  dvdsexp  12388  nn0ob  12435  divalglemnn  12445  divalgmod  12454  bitsinv1lem  12488  bezoutlemnewy  12533  bezoutlema  12536  bezoutlemb  12537  mulgcd  12553  absmulgcd  12554  mulgcdr  12555  gcddiv  12556  lcmgcd  12616  lcmid  12618  lcm1  12619  3lcm2e6woprm  12624  6lcm4e12  12625  mulgcddvds  12632  qredeu  12635  divgcdcoprm0  12639  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  pw2dvdseulemle  12705  phiprmpw  12760  eulerthlema  12768  prmdiveq  12774  odzdvds  12784  powm2modprm  12791  coprimeprodsq  12796  pceulem  12833  pczpre  12836  pcqmul  12842  pcaddlem  12878  pcmpt  12882  pcmpt2  12883  sumhashdc  12886  pcfac  12889  oddprmdvds  12893  mul4sq  12933  4sqlem12  12941  mulgnn0dir  13705  mulgnn0ass  13711  plyaddlem1  15437  plymullem1  15438  dvply1  15455  dvply2g  15456  0sgm  15675  sgmppw  15682  lgslem1  15695  lgsvalmod  15714  gausslemma2dlem6  15762  gausslemma2d  15764  lgseisenlem2  15766  lgseisenlem3  15767  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem2  15777  m1lgs  15780  2lgslem1c  15785  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2sqlem8  15818  vtxdfifiun  16057  vtxdumgrfival  16058  wlklenvm1  16087  wlklenvm1g  16088  wlklenvclwlk  16119  clwwlkccatlem  16143