Theorem nn0cnd 9633

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8183  ℕ₀cn0 9574

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282  ax-rnegex 8294

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-int 3971  df-inn 9314  df-n0 9575

This theorem is used by:  modsumfzodifsn  10854  addmodlteq  10856  uzennn  10894  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  nn0le2msqd  11179  nn0opthlem1d  11180  nn0opthd  11182  nn0opth2d  11183  facdiv  11198  bcp1n  11221  bcn2m1  11230  bcn2p1  11231  omgadd  11264  fihashssdif  11281  hashdifpr  11283  hashxp  11289  hashmap  11290  hashfibclem  11304  hashf1lem2  11308  hashf1  11309  zfz1isolemsplit  11312  zfz1isolem1  11314  ccatval3  11389  ccatval21sw  11395  ccatlid  11396  ccatrid  11397  ccatass  11398  ccatrn  11399  lswccatn0lsw  11401  ccatalpha  11403  ccatws1lenp1bg  11425  wrdlenccats1lenm1g  11426  ccats1val2  11430  lswccats1  11433  swrdccat2  11465  pfxfv  11478  addlenpfx  11485  pfxtrcfvl  11491  pfxpfx  11502  lenrevpfxcctswrd  11506  ccats1pfxeq  11508  ccatopth2  11511  cats1un  11515  swrdccat3b  11534  cats1fvnd  11559  fsumconst  12246  hash2iun1dif1  12272  binomlem  12275  bcxmas  12281  arisum  12290  arisum2  12291  mertensabs  12329  effsumlt  12484  dvdsexp  12653  nn0ob  12700  divalglemnn  12710  divalgmod  12719  bitsinv1lem  12753  bezoutlemnewy  12798  bezoutlema  12801  bezoutlemb  12802  mulgcd  12818  absmulgcd  12819  mulgcdr  12820  gcddiv  12821  lcmgcd  12881  lcmid  12883  lcm1  12884  3lcm2e6woprm  12889  6lcm4e12  12890  mulgcddvds  12897  qredeu  12900  divgcdcoprm0  12904  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  pwbdvdseulemle  12971  phiprmpw  13029  eulerthlema  13037  prmdiveq  13043  odzdvds  13053  powm2modprm  13060  coprimeprodsq  13065  pceulem  13102  pczpre  13105  pcqmul  13111  pcaddlem  13147  pcmpt  13151  pcmpt2  13152  sumhashdc  13155  pcfac  13158  oddprmdvds  13162  mul4sq  13202  4sqlem12  13210  ballotfilemfp1  13289  ballotfilemgun  13326  mulgnn0dir  14014  mulgnn0ass  14020  plyaddlem1  15973  plymullem1  15974  dvply1  15991  dvply2g  15992  efnthr  16176  zprmlogbaplem2  16216  birthdaylem2  16226  0sgm  16254  ppidif  16269  sgmppw  16286  chtublem  16295  bcp1ctr  16306  lgslem1  16324  lgsvalmod  16343  gausslemma2dlem6  16391  gausslemma2d  16393  lgseisenlem2  16395  lgseisenlem3  16396  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem2  16406  m1lgs  16409  2lgslem1c  16414  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2sqlem8  16447  vtxdfifiun  16743  vtxdumgrfival  16744  p1evtxdeqfi  16758  wlklenvm1  16787  wlklenvm1g  16788  wlklenvclwlk  16819  clwwlkccatlem  16846  eupth2lem3lem3fi  16916  eupth2lem3lem6fi  16917  depindlem1  16952