Theorem nn0cnd 9631

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 9630	. 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  10853  addmodlteq  10855  uzennn  10893  expaddzaplem  11039  expaddzap  11040  expmulzap  11042  nn0le2msqd  11178  nn0opthlem1d  11179  nn0opthd  11181  nn0opth2d  11182  facdiv  11197  bcp1n  11220  bcn2m1  11229  bcn2p1  11230  omgadd  11263  fihashssdif  11280  hashdifpr  11282  hashxp  11288  hashmap  11289  hashfibclem  11303  hashf1lem2  11307  hashf1  11308  zfz1isolemsplit  11311  zfz1isolem1  11313  ccatval3  11388  ccatval21sw  11394  ccatlid  11395  ccatrid  11396  ccatass  11397  ccatrn  11398  lswccatn0lsw  11400  ccatalpha  11402  ccatws1lenp1bg  11424  wrdlenccats1lenm1g  11425  ccats1val2  11429  lswccats1  11432  swrdccat2  11464  pfxfv  11477  addlenpfx  11484  pfxtrcfvl  11490  pfxpfx  11501  lenrevpfxcctswrd  11505  ccats1pfxeq  11507  ccatopth2  11510  cats1un  11514  swrdccat3b  11533  cats1fvnd  11558  fsumconst  12245  hash2iun1dif1  12271  binomlem  12274  bcxmas  12280  arisum  12289  arisum2  12290  mertensabs  12328  effsumlt  12483  dvdsexp  12652  nn0ob  12699  divalglemnn  12709  divalgmod  12718  bitsinv1lem  12752  bezoutlemnewy  12797  bezoutlema  12800  bezoutlemb  12801  mulgcd  12817  absmulgcd  12818  mulgcdr  12819  gcddiv  12820  lcmgcd  12880  lcmid  12882  lcm1  12883  3lcm2e6woprm  12888  6lcm4e12  12889  mulgcddvds  12896  qredeu  12899  divgcdcoprm0  12903  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  pwbdvdseulemle  12970  phiprmpw  13028  eulerthlema  13036  prmdiveq  13042  odzdvds  13052  powm2modprm  13059  coprimeprodsq  13064  pceulem  13101  pczpre  13104  pcqmul  13110  pcaddlem  13146  pcmpt  13150  pcmpt2  13151  sumhashdc  13154  pcfac  13157  oddprmdvds  13161  mul4sq  13201  4sqlem12  13209  ballotfilemfp1  13288  ballotfilemgun  13325  mulgnn0dir  14013  mulgnn0ass  14019  plyaddlem1  15990  plymullem1  15991  dvply1  16008  dvply2g  16009  efnthr  16193  zprmlogbaplem2  16233  birthdaylem2  16243  0sgm  16271  ppidif  16286  sgmppw  16303  chtublem  16312  bcp1ctr  16323  lgslem1  16341  lgsvalmod  16360  gausslemma2dlem6  16408  gausslemma2d  16410  lgseisenlem2  16412  lgseisenlem3  16413  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem2  16423  m1lgs  16426  2lgslem1c  16431  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2sqlem8  16464  vtxdfifiun  16760  vtxdumgrfival  16761  p1evtxdeqfi  16775  wlklenvm1  16804  wlklenvm1g  16805  wlklenvclwlk  16836  clwwlkccatlem  16863  eupth2lem3lem3fi  16933  eupth2lem3lem6fi  16934  depindlem1  16969