Theorem nncnd 8638

Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nncnd	|- ( ph -> A e. CC )

Proof of Theorem nncnd

Step	Hyp	Ref	Expression
1		nnsscn 8629	. 2 |- NN C_ CC
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sseldi 3059	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1461   CCcc 7539   NNcn 8624

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-cnex 7630  ax-resscn 7631  ax-1re 7633  ax-addrcl 7636

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-v 2657  df-in 3041  df-ss 3048  df-int 3736  df-inn 8625

This theorem is referenced by:  peano5uzti  9057  qapne  9327  qtri3or  9907  exbtwnzlemstep  9912  intfracq  9980  flqdiv  9981  modqmulnn  10002  addmodid  10032  modaddmodup  10047  modsumfzodifsn  10056  addmodlteq  10058  facdiv  10371  facndiv  10372  faclbnd  10374  faclbnd6  10377  facubnd  10378  facavg  10379  bccmpl  10387  bcn0  10388  bcn1  10391  bcm1k  10393  bcp1n  10394  bcp1nk  10395  bcval5  10396  bcpasc  10399  permnn  10404  cvg1nlemcxze  10640  cvg1nlemcau  10642  resqrexlemcalc3  10674  binom11  11141  binom1dif  11142  divcnv  11152  arisum2  11154  trireciplem  11155  trirecip  11156  expcnvap0  11157  geo2sum  11169  geo2lim  11171  cvgratnnlembern  11178  cvgratnnlemnexp  11179  cvgratnnlemmn  11180  cvgratnnlemsumlt  11183  cvgratnnlemfm  11184  cvgratnnlemrate  11185  cvgratz  11187  eftcl  11205  eftabs  11207  efcllemp  11209  ege2le3  11222  efcj  11224  efaddlem  11225  eftlub  11241  eirraplem  11325  oexpneg  11416  divalglemnn  11457  bezoutlemnewy  11524  mulgcd  11544  rplpwr  11555  sqgcd  11557  lcmgcdlem  11598  3lcm2e6woprm  11607  cncongr1  11624  cncongr2  11625  prmind2  11641  divgcdodd  11661  prmdvdsexpr  11668  sqrt2irrlem  11679  oddpwdclemxy  11686  oddpwdclemodd  11689  oddpwdclemdc  11690  oddpwdc  11691  sqpweven  11692  2sqpwodd  11693  sqrt2irraplemnn  11696  sqrt2irrap  11697  qmuldeneqnum  11712  divnumden  11713  qnumgt0  11715  numdensq  11719  hashdvds  11736  phiprmpw  11737  oddennn  11744  evenennn  11745  trilpolemeq1  12914  trilpolemlt1  12915