Theorem nn0cnd 9627

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

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

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 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277  ax-rnegex 8289

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 9308  df-n0 9569

This theorem is used by:  modsumfzodifsn  10848  addmodlteq  10850  uzennn  10888  expaddzaplem  11034  expaddzap  11035  expmulzap  11037  nn0le2msqd  11173  nn0opthlem1d  11174  nn0opthd  11176  nn0opth2d  11177  facdiv  11192  bcp1n  11215  bcn2m1  11224  bcn2p1  11225  omgadd  11258  fihashssdif  11275  hashdifpr  11277  hashxp  11283  hashmap  11284  hashfibclem  11298  hashf1lem2  11302  hashf1  11303  zfz1isolemsplit  11306  zfz1isolem1  11308  ccatval3  11383  ccatval21sw  11389  ccatlid  11390  ccatrid  11391  ccatass  11392  ccatrn  11393  lswccatn0lsw  11395  ccatalpha  11397  ccatws1lenp1bg  11419  wrdlenccats1lenm1g  11420  ccats1val2  11424  lswccats1  11427  swrdccat2  11459  pfxfv  11472  addlenpfx  11479  pfxtrcfvl  11485  pfxpfx  11496  lenrevpfxcctswrd  11500  ccats1pfxeq  11502  ccatopth2  11505  cats1un  11509  swrdccat3b  11528  cats1fvnd  11553  fsumconst  12240  hash2iun1dif1  12266  binomlem  12269  bcxmas  12275  arisum  12284  arisum2  12285  mertensabs  12323  effsumlt  12478  dvdsexp  12647  nn0ob  12694  divalglemnn  12704  divalgmod  12713  bitsinv1lem  12747  bezoutlemnewy  12792  bezoutlema  12795  bezoutlemb  12796  mulgcd  12812  absmulgcd  12813  mulgcdr  12814  gcddiv  12815  lcmgcd  12875  lcmid  12877  lcm1  12878  3lcm2e6woprm  12883  6lcm4e12  12884  mulgcddvds  12891  qredeu  12894  divgcdcoprm0  12898  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  pwbdvdseulemle  12965  phiprmpw  13023  eulerthlema  13031  prmdiveq  13037  odzdvds  13047  powm2modprm  13054  coprimeprodsq  13059  pceulem  13096  pczpre  13099  pcqmul  13105  pcaddlem  13141  pcmpt  13145  pcmpt2  13146  sumhashdc  13149  pcfac  13152  oddprmdvds  13156  mul4sq  13196  4sqlem12  13204  ballotfilemfp1  13283  ballotfilemgun  13320  mulgnn0dir  14008  mulgnn0ass  14014  plyaddlem1  15939  plymullem1  15940  dvply1  15957  dvply2g  15958  zprmlogbaplem2  16177  birthdaylem2  16187  0sgm  16215  ppidif  16230  sgmppw  16247  chtublem  16256  bcp1ctr  16267  lgslem1  16285  lgsvalmod  16304  gausslemma2dlem6  16352  gausslemma2d  16354  lgseisenlem2  16356  lgseisenlem3  16357  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem2  16367  m1lgs  16370  2lgslem1c  16375  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2sqlem8  16408  vtxdfifiun  16704  vtxdumgrfival  16705  p1evtxdeqfi  16719  wlklenvm1  16748  wlklenvm1g  16749  wlklenvclwlk  16780  clwwlkccatlem  16807  eupth2lem3lem3fi  16877  eupth2lem3lem6fi  16878  depindlem1  16913