Theorem nn0cnd 9262

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

Syntax hints:   → wi 4   ∈ wcel 2160  ℂcc 7840  ℕ₀cn0 9207

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 2171  ax-sep 4136  ax-cnex 7933  ax-resscn 7934  ax-1re 7936  ax-addrcl 7939  ax-rnegex 7951

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3613  df-int 3860  df-inn 8951  df-n0 9208

This theorem is referenced by:  modsumfzodifsn  10429  addmodlteq  10431  uzennn  10469  expaddzaplem  10597  expaddzap  10598  expmulzap  10600  nn0le2msqd  10734  nn0opthlem1d  10735  nn0opthd  10737  nn0opth2d  10738  facdiv  10753  bcp1n  10776  bcn2m1  10784  bcn2p1  10785  omgadd  10817  fihashssdif  10833  hashdifpr  10835  hashxp  10841  zfz1isolemsplit  10853  zfz1isolem1  10855  fsumconst  11497  hash2iun1dif1  11523  binomlem  11526  bcxmas  11532  arisum  11541  arisum2  11542  mertensabs  11580  effsumlt  11735  dvdsexp  11902  nn0ob  11948  divalglemnn  11958  divalgmod  11967  bezoutlemnewy  12032  bezoutlema  12035  bezoutlemb  12036  mulgcd  12052  absmulgcd  12053  mulgcdr  12054  gcddiv  12055  lcmgcd  12113  lcmid  12115  lcm1  12116  3lcm2e6woprm  12121  6lcm4e12  12122  mulgcddvds  12129  qredeu  12132  divgcdcoprm0  12136  divgcdcoprmex  12137  cncongr1  12138  cncongr2  12139  pw2dvdseulemle  12202  phiprmpw  12257  eulerthlema  12265  prmdiveq  12271  odzdvds  12280  powm2modprm  12287  coprimeprodsq  12292  pceulem  12329  pczpre  12332  pcqmul  12338  pcaddlem  12374  pcmpt  12378  pcmpt2  12379  sumhashdc  12382  pcfac  12385  oddprmdvds  12389  mul4sq  12429  4sqlem12  12437  mulgnn0dir  13109  mulgnn0ass  13115  lgslem1  14879  lgsvalmod  14898  lgseisenlem2  14929  m1lgs  14930  2sqlem8  14948