Theorem nn0cnd 8343

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

Syntax hints:   → wi 4   ∈ wcel 1433  ℂcc 6979  ℕ₀cn0 8288

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-cnex 7067  ax-resscn 7068  ax-1re 7070  ax-addrcl 7073  ax-rnegex 7085

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-sn 3404  df-int 3637  df-inn 8040  df-n0 8289

This theorem is referenced by:  modsumfzodifsn  9398  addmodlteq  9400  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  nn0le2msqd  9646  nn0opthlem1d  9647  nn0opthd  9649  nn0opth2d  9650  facdiv  9665  bcp1n  9688  bcn2m1  9696  bcn2p1  9697  dvdsexp  10261  nn0ob  10308  divalglemnn  10318  divalgmod  10327  bezoutlemnewy  10385  bezoutlema  10388  bezoutlemb  10389  mulgcd  10405  absmulgcd  10406  mulgcdr  10407  gcddiv  10408  lcmgcd  10460  lcmid  10462  lcm1  10463  3lcm2e6woprm  10468  6lcm4e12  10469  mulgcddvds  10476  qredeu  10479  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  pw2dvdseulemle  10545