Theorem nncnd 8408

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 8399	. 2 |- NN C_ CC
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sseldi 3021	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1438   CCcc 7327   NNcn 8394

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-cnex 7415  ax-resscn 7416  ax-1re 7418  ax-addrcl 7421

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-v 2621  df-in 3003  df-ss 3010  df-int 3684  df-inn 8395

This theorem is referenced by:  peano5uzti  8824  qapne  9093  qtri3or  9619  exbtwnzlemstep  9624  intfracq  9692  flqdiv  9693  modqmulnn  9714  addmodid  9744  modaddmodup  9759  modsumfzodifsn  9768  addmodlteq  9770  facdiv  10111  facndiv  10112  faclbnd  10114  faclbnd6  10117  facubnd  10118  facavg  10119  bccmpl  10127  bcn0  10128  bcn1  10131  bcm1k  10133  bcp1n  10134  bcp1nk  10135  ibcval5  10136  bcpasc  10139  permnn  10144  cvg1nlemcxze  10380  cvg1nlemcau  10382  resqrexlemcalc3  10414  binom11  10842  binom1dif  10843  divcnv  10852  arisum2  10854  trireciplem  10855  trirecip  10856  expcnvap0  10857  geo2sum  10869  geo2lim  10871  cvgratnnlembern  10878  cvgratnnlemnexp  10879  cvgratnnlemmn  10880  cvgratnnlemsumlt  10883  cvgratnnlemfm  10884  cvgratnnlemrate  10885  cvgratz  10887  oexpneg  10970  divalglemnn  11011  bezoutlemnewy  11078  mulgcd  11098  rplpwr  11109  sqgcd  11111  lcmgcdlem  11152  3lcm2e6woprm  11161  cncongr1  11178  cncongr2  11179  prmind2  11195  divgcdodd  11215  prmdvdsexpr  11222  sqrt2irrlem  11233  oddpwdclemxy  11240  oddpwdclemodd  11243  oddpwdclemdc  11244  oddpwdc  11245  sqpweven  11246  2sqpwodd  11247  sqrt2irraplemnn  11250  sqrt2irrap  11251  qmuldeneqnum  11266  divnumden  11267  qnumgt0  11269  numdensq  11273  hashdvds  11290  phiprmpw  11291  oddennn  11298  evenennn  11299