Theorem nn0cnd 9190

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7772  ℕ₀cn0 9135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4107  ax-cnex 7865  ax-resscn 7866  ax-1re 7868  ax-addrcl 7871  ax-rnegex 7883

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3589  df-int 3832  df-inn 8879  df-n0 9136

This theorem is referenced by:  modsumfzodifsn  10352  addmodlteq  10354  uzennn  10392  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  nn0le2msqd  10653  nn0opthlem1d  10654  nn0opthd  10656  nn0opth2d  10657  facdiv  10672  bcp1n  10695  bcn2m1  10703  bcn2p1  10704  omgadd  10737  fihashssdif  10753  hashdifpr  10755  hashxp  10761  zfz1isolemsplit  10773  zfz1isolem1  10775  fsumconst  11417  hash2iun1dif1  11443  binomlem  11446  bcxmas  11452  arisum  11461  arisum2  11462  mertensabs  11500  effsumlt  11655  dvdsexp  11821  nn0ob  11867  divalglemnn  11877  divalgmod  11886  bezoutlemnewy  11951  bezoutlema  11954  bezoutlemb  11955  mulgcd  11971  absmulgcd  11972  mulgcdr  11973  gcddiv  11974  lcmgcd  12032  lcmid  12034  lcm1  12035  3lcm2e6woprm  12040  6lcm4e12  12041  mulgcddvds  12048  qredeu  12051  divgcdcoprm0  12055  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  pw2dvdseulemle  12121  phiprmpw  12176  eulerthlema  12184  prmdiveq  12190  odzdvds  12199  powm2modprm  12206  coprimeprodsq  12211  pceulem  12248  pczpre  12251  pcqmul  12257  pcaddlem  12292  pcmpt  12295  pcmpt2  12296  sumhashdc  12299  pcfac  12302  oddprmdvds  12306  mul4sq  12346  lgslem1  13695  lgsvalmod  13714  2sqlem8  13753