Theorem recnd 8100

Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)

Hypothesis

Ref	Expression
recnd.1	|- ( ph -> A e. RR )

Assertion

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

Proof of Theorem recnd

Step	Hyp	Ref	Expression
1		recnd.1	. 2 |- ( ph -> A e. RR )
2		recn 8057	. 2 |- ( A e. RR -> A e. CC )
3	1, 2	syl 14	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2175   CCcc 7922   RRcr 7923

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-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-resscn 8016

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  readdcan  8211  ltadd2  8491  ltadd1  8501  leadd2  8503  ltsubadd  8504  ltsubadd2  8505  lesubadd  8506  lesubadd2  8507  ltaddsub  8508  leaddsub  8510  lesub1  8528  lesub2  8529  ltsub1  8530  ltsub2  8531  ltnegcon1  8535  ltnegcon2  8536  add20  8546  subge0  8547  suble0  8548  lesub0  8551  eqord2  8556  possumd  8641  sublt0d  8642  rimul  8657  rereim  8658  apreap  8659  ltmul1a  8663  ltmul1  8664  reapmul1  8667  remulext2  8672  cru  8674  apreim  8675  mulreim  8676  apadd1  8680  apneg  8683  mulext1  8684  ltapd  8710  aprcl  8718  aptap  8722  rerecclap  8802  redivclap  8803  recgt0  8922  prodgt0gt0  8923  prodgt0  8924  prodge0  8926  lemul1a  8930  ltdiv1  8940  ltmuldiv  8946  ledivmul  8949  lt2mul2div  8951  ltrec  8955  lt2msq  8958  ltdiv2  8959  ltrec1  8960  lerec2  8961  ledivdiv  8962  lediv2  8963  ltdiv23  8964  lediv23  8965  lediv12a  8966  recp1lt1  8971  recreclt  8972  ledivp1  8975  mulle0r  9016  negiso  9027  avglt1  9275  avglt2  9276  div4p1lem1div2  9290  nn0cnd  9349  zcn  9376  peano2z  9407  zaddcllemneg  9410  ztri3or  9414  zeo  9477  zcnd  9495  eluzelcn  9658  infrenegsupex  9714  supinfneg  9715  infsupneg  9716  supminfex  9717  irrmulap  9768  cnref1o  9771  rpcn  9783  rpcnd  9819  ltaddrp2d  9852  mul2lt0rlt0  9880  mul2lt0rgt0  9881  mul2lt0llt0  9882  mul2lt0lgt0  9883  mul2lt0np  9884  mul2lt0pn  9885  xpncan  9992  icoshftf1o  10112  lincmb01cmp  10124  iccf1o  10125  infssuzcldc  10376  qbtwnrelemcalc  10396  flhalf  10443  intfracq  10463  flqdiv  10464  modqid  10492  modqid0  10493  mulqaddmodid  10507  seqf1oglem1  10662  ser3le  10680  expcl2lemap  10694  expnegzap  10716  expaddzaplem  10725  expaddzap  10726  expmulzap  10728  ltexp2a  10734  leexp2a  10735  leexp2r  10736  exple1  10738  expubnd  10739  sq11  10755  bernneq2  10804  expnbnd  10806  nn0ltexp2  10852  nn0opthlem2d  10864  faclbnd  10884  bcp1nk  10905  remim  11113  reim0b  11115  rereb  11116  mulreap  11117  cjreb  11119  recj  11120  reneg  11121  readd  11122  resub  11123  remullem  11124  remul2  11126  redivap  11127  imcj  11128  imneg  11129  imadd  11130  imsub  11131  immul2  11133  imdivap  11134  cjcj  11136  cjadd  11137  ipcnval  11139  cjmulval  11141  cjneg  11143  imval2  11147  cjreim2  11157  cjap  11159  cnrecnv  11163  caucvgrelemrec  11232  cvg1nlemres  11238  recvguniqlem  11247  recvguniq  11248  resqrexlemover  11263  resqrexlemcalc1  11267  resqrexlemcalc2  11268  resqrexlemcalc3  11269  resqrexlemnmsq  11270  resqrexlemnm  11271  resqrexlemgt0  11273  resqrexlemoverl  11274  resqrexlemglsq  11275  remsqsqrt  11285  sqrtmul  11288  sqrtdiv  11295  sqrtmsq  11298  abs00ap  11315  absext  11316  abs00  11317  absdivap  11323  absid  11324  absexp  11332  absexpzap  11333  absimle  11337  abslt  11341  absle  11342  abssubap0  11343  abssubne0  11344  releabs  11349  recvalap  11350  abstri  11357  abs2difabs  11361  amgm2  11371  icodiamlt  11433  maxabsle  11457  maxabslemab  11459  maxabslemlub  11460  maxabslemval  11461  maxcl  11463  maxltsup  11471  max0addsup  11472  minmax  11483  minabs  11489  minclpr  11490  bdtrilem  11492  bdtri  11493  mul0inf  11494  mingeb  11495  climabs0  11560  reccn2ap  11566  climrecl  11577  climge0  11578  climle  11587  climsqz  11588  climsqz2  11589  climlec2  11594  climrecvg1n  11601  climcvg1nlem  11602  isumrecl  11682  isumge0  11683  fsumlessfi  11713  fsumge1  11714  fsum00  11715  fsumle  11716  fsumlt  11717  fsumabs  11718  iserabs  11728  isumrpcl  11747  isumle  11748  isumlessdc  11749  trireciplem  11753  trirecip  11754  expcnvre  11756  expcnv  11757  explecnv  11758  absltap  11762  geo2sum  11767  cvgratnnlembern  11776  cvgratnnlemnexp  11777  cvgratnnlemmn  11778  cvgratnnlemabsle  11780  cvgratnnlemsumlt  11781  cvgratnnlemfm  11782  cvgratnnlemrate  11783  cvgratz  11785  mertenslemi1  11788  mertenslem2  11789  fprodabs  11869  fprodle  11893  efcllemp  11911  ege2le3  11924  efaddlem  11927  efgt0  11937  reeftlcl  11942  eftlub  11943  effsumlt  11945  efltim  11951  eflegeo  11954  resin4p  11971  recos4p  11972  efeul  11987  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  sin01gt0  12015  cos01gt0  12016  sin02gt0  12017  cos12dec  12021  absefi  12022  absef  12023  absefib  12024  efieq1re  12025  eirraplem  12030  dvdsaddre2b  12094  dvdslelemd  12096  odd2np1  12126  divalglemnqt  12173  bitsp1o  12206  bitsfzo  12208  bitscmp  12211  nn0seqcvgd  12305  sqnprm  12400  isprm5lem  12405  odzdvds  12510  pythagtriplem14  12542  pcid  12589  fldivp1  12613  pockthlem  12621  4sqlem5  12647  4sqlem10  12652  mul4sqlem  12658  4sqlem15  12670  4sqlem16  12671  mulgneg  13418  ghmmulg  13534  rege0subm  14288  metrtri  14791  bl2in  14817  blhalf  14822  blssps  14841  blss  14842  maxcncf  15029  mincncf  15030  dedekindeu  15037  dedekindicclemicc  15046  ivthinclemlopn  15050  ivthinclemuopn  15052  ivthinc  15057  ivthdec  15058  ivthreinc  15059  dvconstre  15110  dvidre  15111  dvcjbr  15122  dvfre  15124  dveflem  15140  plyrecj  15177  reeff1olem  15185  reeff1oleme  15186  eflt  15189  sin0pilem1  15195  sin0pilem2  15196  pilem3  15197  sincosq2sgn  15241  sincosq3sgn  15242  sincosq4sgn  15243  sinq12gt0  15244  sinq34lt0t  15245  cosq14gt0  15246  cosq23lt0  15247  coseq0q4123  15248  coseq0negpitopi  15250  tanrpcl  15251  tangtx  15252  coskpi  15262  cosordlem  15263  cosq34lt1  15264  cos11  15267  reexplog  15285  relogexp  15286  logdivlti  15295  rpcxpef  15308  rpcncxpcl  15316  cxpap0  15318  rpcxpadd  15319  rpmulcxp  15323  cxpmul  15326  abscxp  15329  cxplt  15330  cxplt3  15334  logsqrt  15337  apcxp2  15353  rpabscxpbnd  15354  rplogbid1  15361  rplogb1  15362  rpelogb  15363  rplogbchbase  15364  rplogbreexp  15367  rprelogbmul  15369  rprelogbdiv  15371  rplogbcxp  15377  rpcxplogb  15378  logbgcd1irraplemexp  15382  logbgcd1irraplemap  15383  mersenne  15411  lgsvalmod  15438  lgsdilem  15446  lgsne0  15457  gausslemma2dlem1a  15477  gausslemma2dlem6  15486  lgseisenlem1  15489  lgseisenlem2  15490  lgseisen  15493  lgsquadlem1  15496  lgsquadlem2  15497  2sqlem1  15533  mul2sq  15535  2sqlem3  15536  2sqlem8  15542  qdencn  15899  refeq  15900  cvgcmp2nlemabs  15904  cvgcmp2n  15905  trilpolemisumle  15910  trilpolemeq1  15912  trilpolemlt1  15913  trirec0  15916  apdifflemf  15918  apdifflemr  15919  apdiff  15920  redc0  15929  reap0  15930  cndcap  15931  nconstwlpolem0  15935  nconstwlpolemgt0  15936  neap0mkv  15941  ltlenmkv  15942