Theorem nn0cnd 9622

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

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

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 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276  ax-rnegex 8288

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 9305  df-n0 9564

This theorem is used by:  modsumfzodifsn  10833  addmodlteq  10835  uzennn  10873  expaddzaplem  11019  expaddzap  11020  expmulzap  11022  nn0le2msqd  11157  nn0opthlem1d  11158  nn0opthd  11160  nn0opth2d  11161  facdiv  11176  bcp1n  11199  bcn2m1  11208  bcn2p1  11209  omgadd  11242  fihashssdif  11259  hashdifpr  11261  hashxp  11267  hashmap  11268  hashfibclem  11282  hashf1lem2  11286  hashf1  11287  zfz1isolemsplit  11290  zfz1isolem1  11292  ccatval3  11367  ccatval21sw  11373  ccatlid  11374  ccatrid  11375  ccatass  11376  ccatrn  11377  lswccatn0lsw  11379  ccatalpha  11381  ccatws1lenp1bg  11403  wrdlenccats1lenm1g  11404  ccats1val2  11408  lswccats1  11411  swrdccat2  11443  pfxfv  11456  addlenpfx  11463  pfxtrcfvl  11469  pfxpfx  11480  lenrevpfxcctswrd  11484  ccats1pfxeq  11486  ccatopth2  11489  cats1un  11493  swrdccat3b  11512  cats1fvnd  11537  fsumconst  12221  hash2iun1dif1  12247  binomlem  12250  bcxmas  12256  arisum  12265  arisum2  12266  mertensabs  12304  effsumlt  12459  dvdsexp  12628  nn0ob  12675  divalglemnn  12685  divalgmod  12694  bitsinv1lem  12728  bezoutlemnewy  12773  bezoutlema  12776  bezoutlemb  12777  mulgcd  12793  absmulgcd  12794  mulgcdr  12795  gcddiv  12796  lcmgcd  12856  lcmid  12858  lcm1  12859  3lcm2e6woprm  12864  6lcm4e12  12865  mulgcddvds  12872  qredeu  12875  divgcdcoprm0  12879  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  pw2dvdseulemle  12945  phiprmpw  13000  eulerthlema  13008  prmdiveq  13014  odzdvds  13024  powm2modprm  13031  coprimeprodsq  13036  pceulem  13073  pczpre  13076  pcqmul  13082  pcaddlem  13118  pcmpt  13122  pcmpt2  13123  sumhashdc  13126  pcfac  13129  oddprmdvds  13133  mul4sq  13173  4sqlem12  13181  ballotfilemfp1  13231  ballotfilemgun  13268  mulgnn0dir  13955  mulgnn0ass  13961  plyaddlem1  15848  plymullem1  15849  dvply1  15866  dvply2g  15867  birthdaylem2  16088  0sgm  16099  sgmppw  16106  lgslem1  16119  lgsvalmod  16138  gausslemma2dlem6  16186  gausslemma2d  16188  lgseisenlem2  16190  lgseisenlem3  16191  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem2  16201  m1lgs  16204  2lgslem1c  16209  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2sqlem8  16242  vtxdfifiun  16538  vtxdumgrfival  16539  p1evtxdeqfi  16553  wlklenvm1  16582  wlklenvm1g  16583  wlklenvclwlk  16614  clwwlkccatlem  16641  eupth2lem3lem3fi  16711  eupth2lem3lem6fi  16712  depindlem1  16747