Theorem nn0cnd 9350

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

Syntax hints:   → wi 4   ∈ wcel 2176  ℂcc 7923  ℕ₀cn0 9295

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4162  ax-cnex 8016  ax-resscn 8017  ax-1re 8019  ax-addrcl 8022  ax-rnegex 8034

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-int 3886  df-inn 9037  df-n0 9296

This theorem is referenced by:  modsumfzodifsn  10541  addmodlteq  10543  uzennn  10581  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  nn0le2msqd  10864  nn0opthlem1d  10865  nn0opthd  10867  nn0opth2d  10868  facdiv  10883  bcp1n  10906  bcn2m1  10914  bcn2p1  10915  omgadd  10947  fihashssdif  10963  hashdifpr  10965  hashxp  10971  zfz1isolemsplit  10983  zfz1isolem1  10985  ccatval3  11055  ccatval21sw  11061  ccatlid  11062  ccatrid  11063  ccatass  11064  ccatrn  11065  lswccatn0lsw  11067  ccatws1lenp1bg  11089  ccats1val2  11092  lswccats1  11095  swrdccat2  11124  fsumconst  11765  hash2iun1dif1  11791  binomlem  11794  bcxmas  11800  arisum  11809  arisum2  11810  mertensabs  11848  effsumlt  12003  dvdsexp  12172  nn0ob  12219  divalglemnn  12229  divalgmod  12238  bitsinv1lem  12272  bezoutlemnewy  12317  bezoutlema  12320  bezoutlemb  12321  mulgcd  12337  absmulgcd  12338  mulgcdr  12339  gcddiv  12340  lcmgcd  12400  lcmid  12402  lcm1  12403  3lcm2e6woprm  12408  6lcm4e12  12409  mulgcddvds  12416  qredeu  12419  divgcdcoprm0  12423  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  pw2dvdseulemle  12489  phiprmpw  12544  eulerthlema  12552  prmdiveq  12558  odzdvds  12568  powm2modprm  12575  coprimeprodsq  12580  pceulem  12617  pczpre  12620  pcqmul  12626  pcaddlem  12662  pcmpt  12666  pcmpt2  12667  sumhashdc  12670  pcfac  12673  oddprmdvds  12677  mul4sq  12717  4sqlem12  12725  mulgnn0dir  13488  mulgnn0ass  13494  plyaddlem1  15219  plymullem1  15220  dvply1  15237  dvply2g  15238  0sgm  15457  sgmppw  15464  lgslem1  15477  lgsvalmod  15496  gausslemma2dlem6  15544  gausslemma2d  15546  lgseisenlem2  15548  lgseisenlem3  15549  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem2  15559  m1lgs  15562  2lgslem1c  15567  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2sqlem8  15600