Theorem nn0cnd 9298

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7872  ℕ₀cn0 9243

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 4148  ax-cnex 7965  ax-resscn 7966  ax-1re 7968  ax-addrcl 7971  ax-rnegex 7983

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 3158  df-in 3160  df-ss 3167  df-sn 3625  df-int 3872  df-inn 8985  df-n0 9244

This theorem is referenced by:  modsumfzodifsn  10470  addmodlteq  10472  uzennn  10510  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  nn0le2msqd  10793  nn0opthlem1d  10794  nn0opthd  10796  nn0opth2d  10797  facdiv  10812  bcp1n  10835  bcn2m1  10843  bcn2p1  10844  omgadd  10876  fihashssdif  10892  hashdifpr  10894  hashxp  10900  zfz1isolemsplit  10912  zfz1isolem1  10914  fsumconst  11600  hash2iun1dif1  11626  binomlem  11629  bcxmas  11635  arisum  11644  arisum2  11645  mertensabs  11683  effsumlt  11838  dvdsexp  12006  nn0ob  12052  divalglemnn  12062  divalgmod  12071  bezoutlemnewy  12136  bezoutlema  12139  bezoutlemb  12140  mulgcd  12156  absmulgcd  12157  mulgcdr  12158  gcddiv  12159  lcmgcd  12219  lcmid  12221  lcm1  12222  3lcm2e6woprm  12227  6lcm4e12  12228  mulgcddvds  12235  qredeu  12238  divgcdcoprm0  12242  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  pw2dvdseulemle  12308  phiprmpw  12363  eulerthlema  12371  prmdiveq  12377  odzdvds  12386  powm2modprm  12393  coprimeprodsq  12398  pceulem  12435  pczpre  12438  pcqmul  12444  pcaddlem  12480  pcmpt  12484  pcmpt2  12485  sumhashdc  12488  pcfac  12491  oddprmdvds  12495  mul4sq  12535  4sqlem12  12543  mulgnn0dir  13225  mulgnn0ass  13231  plyaddlem1  14926  plymullem1  14927  dvply1  14943  lgslem1  15157  lgsvalmod  15176  gausslemma2dlem6  15224  gausslemma2d  15226  lgseisenlem2  15228  lgseisenlem3  15229  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem2  15239  m1lgs  15242  2lgslem1c  15247  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2sqlem8  15280