Theorem nn0cnd 8936

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

Syntax hints:   → wi 4   ∈ wcel 1463  ℂcc 7545  ℕ₀cn0 8881

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4006  ax-cnex 7636  ax-resscn 7637  ax-1re 7639  ax-addrcl 7642  ax-rnegex 7654

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ral 2395  df-rex 2396  df-v 2659  df-un 3041  df-in 3043  df-ss 3050  df-sn 3499  df-int 3738  df-inn 8631  df-n0 8882

This theorem is referenced by:  modsumfzodifsn  10062  addmodlteq  10064  uzennn  10102  expaddzaplem  10229  expaddzap  10230  expmulzap  10232  nn0le2msqd  10358  nn0opthlem1d  10359  nn0opthd  10361  nn0opth2d  10362  facdiv  10377  bcp1n  10400  bcn2m1  10408  bcn2p1  10409  omgadd  10441  fihashssdif  10457  hashdifpr  10459  hashxp  10465  zfz1isolemsplit  10474  zfz1isolem1  10476  fsumconst  11115  hash2iun1dif1  11141  binomlem  11144  bcxmas  11150  arisum  11159  arisum2  11160  mertensabs  11198  effsumlt  11249  dvdsexp  11407  nn0ob  11453  divalglemnn  11463  divalgmod  11472  bezoutlemnewy  11530  bezoutlema  11533  bezoutlemb  11534  mulgcd  11550  absmulgcd  11551  mulgcdr  11552  gcddiv  11553  lcmgcd  11605  lcmid  11607  lcm1  11608  3lcm2e6woprm  11613  6lcm4e12  11614  mulgcddvds  11621  qredeu  11624  divgcdcoprm0  11628  divgcdcoprmex  11629  cncongr1  11630  cncongr2  11631  pw2dvdseulemle  11690  phiprmpw  11743