Theorem nn0cnd 9295

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7870  ℕ₀cn0 9240

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969  ax-rnegex 7981

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-sn 3624  df-int 3871  df-inn 8983  df-n0 9241

This theorem is referenced by:  modsumfzodifsn  10467  addmodlteq  10469  uzennn  10507  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  nn0le2msqd  10790  nn0opthlem1d  10791  nn0opthd  10793  nn0opth2d  10794  facdiv  10809  bcp1n  10832  bcn2m1  10840  bcn2p1  10841  omgadd  10873  fihashssdif  10889  hashdifpr  10891  hashxp  10897  zfz1isolemsplit  10909  zfz1isolem1  10911  fsumconst  11597  hash2iun1dif1  11623  binomlem  11626  bcxmas  11632  arisum  11641  arisum2  11642  mertensabs  11680  effsumlt  11835  dvdsexp  12003  nn0ob  12049  divalglemnn  12059  divalgmod  12068  bezoutlemnewy  12133  bezoutlema  12136  bezoutlemb  12137  mulgcd  12153  absmulgcd  12154  mulgcdr  12155  gcddiv  12156  lcmgcd  12216  lcmid  12218  lcm1  12219  3lcm2e6woprm  12224  6lcm4e12  12225  mulgcddvds  12232  qredeu  12235  divgcdcoprm0  12239  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  pw2dvdseulemle  12305  phiprmpw  12360  eulerthlema  12368  prmdiveq  12374  odzdvds  12383  powm2modprm  12390  coprimeprodsq  12395  pceulem  12432  pczpre  12435  pcqmul  12441  pcaddlem  12477  pcmpt  12481  pcmpt2  12482  sumhashdc  12485  pcfac  12488  oddprmdvds  12492  mul4sq  12532  4sqlem12  12540  mulgnn0dir  13222  mulgnn0ass  13228  plyaddlem1  14893  plymullem1  14894  lgslem1  15116  lgsvalmod  15135  gausslemma2dlem6  15183  gausslemma2d  15185  lgseisenlem2  15187  lgseisenlem3  15188  lgsquadlem1  15191  m1lgs  15192  2sqlem8  15210