Theorem nn0cnd 8619

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

Syntax hints:   → wi 4   ∈ wcel 1434  ℂcc 7250  ℕ₀cn0 8564

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-cnex 7338  ax-resscn 7339  ax-1re 7341  ax-addrcl 7344  ax-rnegex 7356

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-un 2988  df-in 2990  df-ss 2997  df-sn 3428  df-int 3663  df-inn 8316  df-n0 8565

This theorem is referenced by:  modsumfzodifsn  9691  addmodlteq  9693  expaddzaplem  9834  expaddzap  9835  expmulzap  9837  nn0le2msqd  9961  nn0opthlem1d  9962  nn0opthd  9964  nn0opth2d  9965  facdiv  9980  bcp1n  10003  bcn2m1  10011  bcn2p1  10012  omgadd  10044  fihashssdif  10060  hashdifpr  10062  hashxp  10068  dvdsexp  10641  nn0ob  10687  divalglemnn  10697  divalgmod  10706  bezoutlemnewy  10764  bezoutlema  10767  bezoutlemb  10768  mulgcd  10784  absmulgcd  10785  mulgcdr  10786  gcddiv  10787  lcmgcd  10839  lcmid  10841  lcm1  10842  3lcm2e6woprm  10847  6lcm4e12  10848  mulgcddvds  10855  qredeu  10858  divgcdcoprm0  10862  divgcdcoprmex  10863  cncongr1  10864  cncongr2  10865  pw2dvdseulemle  10924  phiprmpw  10977