Theorem nn0cnd 9233

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7811  ℕ₀cn0 9178

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4123  ax-cnex 7904  ax-resscn 7905  ax-1re 7907  ax-addrcl 7910  ax-rnegex 7922

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-sn 3600  df-int 3847  df-inn 8922  df-n0 9179

This theorem is referenced by:  modsumfzodifsn  10398  addmodlteq  10400  uzennn  10438  expaddzaplem  10565  expaddzap  10566  expmulzap  10568  nn0le2msqd  10701  nn0opthlem1d  10702  nn0opthd  10704  nn0opth2d  10705  facdiv  10720  bcp1n  10743  bcn2m1  10751  bcn2p1  10752  omgadd  10784  fihashssdif  10800  hashdifpr  10802  hashxp  10808  zfz1isolemsplit  10820  zfz1isolem1  10822  fsumconst  11464  hash2iun1dif1  11490  binomlem  11493  bcxmas  11499  arisum  11508  arisum2  11509  mertensabs  11547  effsumlt  11702  dvdsexp  11869  nn0ob  11915  divalglemnn  11925  divalgmod  11934  bezoutlemnewy  11999  bezoutlema  12002  bezoutlemb  12003  mulgcd  12019  absmulgcd  12020  mulgcdr  12021  gcddiv  12022  lcmgcd  12080  lcmid  12082  lcm1  12083  3lcm2e6woprm  12088  6lcm4e12  12089  mulgcddvds  12096  qredeu  12099  divgcdcoprm0  12103  divgcdcoprmex  12104  cncongr1  12105  cncongr2  12106  pw2dvdseulemle  12169  phiprmpw  12224  eulerthlema  12232  prmdiveq  12238  odzdvds  12247  powm2modprm  12254  coprimeprodsq  12259  pceulem  12296  pczpre  12299  pcqmul  12305  pcaddlem  12340  pcmpt  12343  pcmpt2  12344  sumhashdc  12347  pcfac  12350  oddprmdvds  12354  mul4sq  12394  mulgnn0dir  13018  mulgnn0ass  13024  lgslem1  14440  lgsvalmod  14459  lgseisenlem2  14490  m1lgs  14491  2sqlem8  14509