Theorem nn0cnd 9456

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8029  ℕ₀cn0 9401

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8122  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128  ax-rnegex 8140

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-int 3929  df-inn 9143  df-n0 9402

This theorem is referenced by:  modsumfzodifsn  10657  addmodlteq  10659  uzennn  10697  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  nn0le2msqd  10980  nn0opthlem1d  10981  nn0opthd  10983  nn0opth2d  10984  facdiv  10999  bcp1n  11022  bcn2m1  11030  bcn2p1  11031  omgadd  11064  fihashssdif  11081  hashdifpr  11083  hashxp  11089  zfz1isolemsplit  11101  zfz1isolem1  11103  ccatval3  11175  ccatval21sw  11181  ccatlid  11182  ccatrid  11183  ccatass  11184  ccatrn  11185  lswccatn0lsw  11187  ccatalpha  11189  ccatws1lenp1bg  11211  wrdlenccats1lenm1g  11212  ccats1val2  11216  lswccats1  11219  swrdccat2  11251  pfxfv  11264  addlenpfx  11271  pfxtrcfvl  11277  pfxpfx  11288  lenrevpfxcctswrd  11292  ccats1pfxeq  11294  ccatopth2  11297  cats1un  11301  swrdccat3b  11320  cats1fvnd  11345  fsumconst  12014  hash2iun1dif1  12040  binomlem  12043  bcxmas  12049  arisum  12058  arisum2  12059  mertensabs  12097  effsumlt  12252  dvdsexp  12421  nn0ob  12468  divalglemnn  12478  divalgmod  12487  bitsinv1lem  12521  bezoutlemnewy  12566  bezoutlema  12569  bezoutlemb  12570  mulgcd  12586  absmulgcd  12587  mulgcdr  12588  gcddiv  12589  lcmgcd  12649  lcmid  12651  lcm1  12652  3lcm2e6woprm  12657  6lcm4e12  12658  mulgcddvds  12665  qredeu  12668  divgcdcoprm0  12672  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  pw2dvdseulemle  12738  phiprmpw  12793  eulerthlema  12801  prmdiveq  12807  odzdvds  12817  powm2modprm  12824  coprimeprodsq  12829  pceulem  12866  pczpre  12869  pcqmul  12875  pcaddlem  12911  pcmpt  12915  pcmpt2  12916  sumhashdc  12919  pcfac  12922  oddprmdvds  12926  mul4sq  12966  4sqlem12  12974  mulgnn0dir  13738  mulgnn0ass  13744  plyaddlem1  15470  plymullem1  15471  dvply1  15488  dvply2g  15489  0sgm  15708  sgmppw  15715  lgslem1  15728  lgsvalmod  15747  gausslemma2dlem6  15795  gausslemma2d  15797  lgseisenlem2  15799  lgseisenlem3  15800  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem2  15810  m1lgs  15813  2lgslem1c  15818  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2sqlem8  15851  vtxdfifiun  16147  vtxdumgrfival  16148  p1evtxdeqfi  16162  wlklenvm1  16191  wlklenvm1g  16192  wlklenvclwlk  16223  clwwlkccatlem  16250