Theorem nn0cnd 9518

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8090  ℕ₀cn0 9461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8183  ax-resscn 8184  ax-1re 8186  ax-addrcl 8189  ax-rnegex 8201

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-int 3934  df-inn 9203  df-n0 9462

This theorem is referenced by:  modsumfzodifsn  10721  addmodlteq  10723  uzennn  10761  expaddzaplem  10907  expaddzap  10908  expmulzap  10910  nn0le2msqd  11044  nn0opthlem1d  11045  nn0opthd  11047  nn0opth2d  11048  facdiv  11063  bcp1n  11086  bcn2m1  11094  bcn2p1  11095  omgadd  11128  fihashssdif  11145  hashdifpr  11147  hashxp  11153  zfz1isolemsplit  11165  zfz1isolem1  11167  ccatval3  11242  ccatval21sw  11248  ccatlid  11249  ccatrid  11250  ccatass  11251  ccatrn  11252  lswccatn0lsw  11254  ccatalpha  11256  ccatws1lenp1bg  11278  wrdlenccats1lenm1g  11279  ccats1val2  11283  lswccats1  11286  swrdccat2  11318  pfxfv  11331  addlenpfx  11338  pfxtrcfvl  11344  pfxpfx  11355  lenrevpfxcctswrd  11359  ccats1pfxeq  11361  ccatopth2  11364  cats1un  11368  swrdccat3b  11387  cats1fvnd  11412  fsumconst  12095  hash2iun1dif1  12121  binomlem  12124  bcxmas  12130  arisum  12139  arisum2  12140  mertensabs  12178  effsumlt  12333  dvdsexp  12502  nn0ob  12549  divalglemnn  12559  divalgmod  12568  bitsinv1lem  12602  bezoutlemnewy  12647  bezoutlema  12650  bezoutlemb  12651  mulgcd  12667  absmulgcd  12668  mulgcdr  12669  gcddiv  12670  lcmgcd  12730  lcmid  12732  lcm1  12733  3lcm2e6woprm  12738  6lcm4e12  12739  mulgcddvds  12746  qredeu  12749  divgcdcoprm0  12753  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  pw2dvdseulemle  12819  phiprmpw  12874  eulerthlema  12882  prmdiveq  12888  odzdvds  12898  powm2modprm  12905  coprimeprodsq  12910  pceulem  12947  pczpre  12950  pcqmul  12956  pcaddlem  12992  pcmpt  12996  pcmpt2  12997  sumhashdc  13000  pcfac  13003  oddprmdvds  13007  mul4sq  13047  4sqlem12  13055  mulgnn0dir  13819  mulgnn0ass  13825  plyaddlem1  15558  plymullem1  15559  dvply1  15576  dvply2g  15577  0sgm  15799  sgmppw  15806  lgslem1  15819  lgsvalmod  15838  gausslemma2dlem6  15886  gausslemma2d  15888  lgseisenlem2  15890  lgseisenlem3  15891  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem2  15901  m1lgs  15904  2lgslem1c  15909  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2sqlem8  15942  vtxdfifiun  16238  vtxdumgrfival  16239  p1evtxdeqfi  16253  wlklenvm1  16282  wlklenvm1g  16283  wlklenvclwlk  16314  clwwlkccatlem  16341  eupth2lem3lem3fi  16411  eupth2lem3lem6fi  16412  depindlem1  16447