Theorem nn0cnd 9225

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7804  ℕ₀cn0 9170

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 4119  ax-cnex 7897  ax-resscn 7898  ax-1re 7900  ax-addrcl 7903  ax-rnegex 7915

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 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-int 3844  df-inn 8914  df-n0 9171

This theorem is referenced by:  modsumfzodifsn  10389  addmodlteq  10391  uzennn  10429  expaddzaplem  10556  expaddzap  10557  expmulzap  10559  nn0le2msqd  10690  nn0opthlem1d  10691  nn0opthd  10693  nn0opth2d  10694  facdiv  10709  bcp1n  10732  bcn2m1  10740  bcn2p1  10741  omgadd  10773  fihashssdif  10789  hashdifpr  10791  hashxp  10797  zfz1isolemsplit  10809  zfz1isolem1  10811  fsumconst  11453  hash2iun1dif1  11479  binomlem  11482  bcxmas  11488  arisum  11497  arisum2  11498  mertensabs  11536  effsumlt  11691  dvdsexp  11857  nn0ob  11903  divalglemnn  11913  divalgmod  11922  bezoutlemnewy  11987  bezoutlema  11990  bezoutlemb  11991  mulgcd  12007  absmulgcd  12008  mulgcdr  12009  gcddiv  12010  lcmgcd  12068  lcmid  12070  lcm1  12071  3lcm2e6woprm  12076  6lcm4e12  12077  mulgcddvds  12084  qredeu  12087  divgcdcoprm0  12091  divgcdcoprmex  12092  cncongr1  12093  cncongr2  12094  pw2dvdseulemle  12157  phiprmpw  12212  eulerthlema  12220  prmdiveq  12226  odzdvds  12235  powm2modprm  12242  coprimeprodsq  12247  pceulem  12284  pczpre  12287  pcqmul  12293  pcaddlem  12328  pcmpt  12331  pcmpt2  12332  sumhashdc  12335  pcfac  12338  oddprmdvds  12342  mul4sq  12382  mulgnn0dir  12940  mulgnn0ass  12946  lgslem1  14183  lgsvalmod  14202  2sqlem8  14241