Theorem recnd 8198

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 8155	. 2 |- ( A e. RR -> A e. CC )
3	1, 2	syl 14	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8020   RRcr 8021

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8114

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  readdcan  8309  ltadd2  8589  ltadd1  8599  leadd2  8601  ltsubadd  8602  ltsubadd2  8603  lesubadd  8604  lesubadd2  8605  ltaddsub  8606  leaddsub  8608  lesub1  8626  lesub2  8627  ltsub1  8628  ltsub2  8629  ltnegcon1  8633  ltnegcon2  8634  add20  8644  subge0  8645  suble0  8646  lesub0  8649  eqord2  8654  possumd  8739  sublt0d  8740  rimul  8755  rereim  8756  apreap  8757  ltmul1a  8761  ltmul1  8762  reapmul1  8765  remulext2  8770  cru  8772  apreim  8773  mulreim  8774  apadd1  8778  apneg  8781  mulext1  8782  ltapd  8808  aprcl  8816  aptap  8820  rerecclap  8900  redivclap  8901  recgt0  9020  prodgt0gt0  9021  prodgt0  9022  prodge0  9024  lemul1a  9028  ltdiv1  9038  ltmuldiv  9044  ledivmul  9047  lt2mul2div  9049  ltrec  9053  lt2msq  9056  ltdiv2  9057  ltrec1  9058  lerec2  9059  ledivdiv  9060  lediv2  9061  ltdiv23  9062  lediv23  9063  lediv12a  9064  recp1lt1  9069  recreclt  9070  ledivp1  9073  mulle0r  9114  negiso  9125  avglt1  9373  avglt2  9374  div4p1lem1div2  9388  nn0cnd  9447  zcn  9474  peano2z  9505  zaddcllemneg  9508  ztri3or  9512  zeo  9575  zcnd  9593  eluzmn  9752  eluzelcn  9757  infrenegsupex  9818  supinfneg  9819  infsupneg  9820  supminfex  9821  irrmulap  9872  cnref1o  9875  rpcn  9887  rpcnd  9923  ltaddrp2d  9956  mul2lt0rlt0  9984  mul2lt0rgt0  9985  mul2lt0llt0  9986  mul2lt0lgt0  9987  mul2lt0np  9988  mul2lt0pn  9989  xpncan  10096  icoshftf1o  10216  lincmb01cmp  10228  iccf1o  10229  infssuzcldc  10485  qbtwnrelemcalc  10505  flhalf  10552  intfracq  10572  flqdiv  10573  modqid  10601  modqid0  10602  mulqaddmodid  10616  seqf1oglem1  10771  ser3le  10789  expcl2lemap  10803  expnegzap  10825  expaddzaplem  10834  expaddzap  10835  expmulzap  10837  ltexp2a  10843  leexp2a  10844  leexp2r  10845  exple1  10847  expubnd  10848  sq11  10864  bernneq2  10913  expnbnd  10915  nn0ltexp2  10961  nn0opthlem2d  10973  faclbnd  10993  bcp1nk  11014  remim  11411  reim0b  11413  rereb  11414  mulreap  11415  cjreb  11417  recj  11418  reneg  11419  readd  11420  resub  11421  remullem  11422  remul2  11424  redivap  11425  imcj  11426  imneg  11427  imadd  11428  imsub  11429  immul2  11431  imdivap  11432  cjcj  11434  cjadd  11435  ipcnval  11437  cjmulval  11439  cjneg  11441  imval2  11445  cjreim2  11455  cjap  11457  cnrecnv  11461  caucvgrelemrec  11530  cvg1nlemres  11536  recvguniqlem  11545  recvguniq  11546  resqrexlemover  11561  resqrexlemcalc1  11565  resqrexlemcalc2  11566  resqrexlemcalc3  11567  resqrexlemnmsq  11568  resqrexlemnm  11569  resqrexlemgt0  11571  resqrexlemoverl  11572  resqrexlemglsq  11573  remsqsqrt  11583  sqrtmul  11586  sqrtdiv  11593  sqrtmsq  11596  abs00ap  11613  absext  11614  abs00  11615  absdivap  11621  absid  11622  absexp  11630  absexpzap  11631  absimle  11635  abslt  11639  absle  11640  abssubap0  11641  abssubne0  11642  releabs  11647  recvalap  11648  abstri  11655  abs2difabs  11659  amgm2  11669  icodiamlt  11731  maxabsle  11755  maxabslemab  11757  maxabslemlub  11758  maxabslemval  11759  maxcl  11761  maxltsup  11769  max0addsup  11770  minmax  11781  minabs  11787  minclpr  11788  bdtrilem  11790  bdtri  11791  mul0inf  11792  mingeb  11793  climabs0  11858  reccn2ap  11864  climrecl  11875  climge0  11876  climle  11885  climsqz  11886  climsqz2  11887  climlec2  11892  climrecvg1n  11899  climcvg1nlem  11900  isumrecl  11980  isumge0  11981  fsumlessfi  12011  fsumge1  12012  fsum00  12013  fsumle  12014  fsumlt  12015  fsumabs  12016  iserabs  12026  isumrpcl  12045  isumle  12046  isumlessdc  12047  trireciplem  12051  trirecip  12052  expcnvre  12054  expcnv  12055  explecnv  12056  absltap  12060  geo2sum  12065  cvgratnnlembern  12074  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemabsle  12078  cvgratnnlemsumlt  12079  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratz  12083  mertenslemi1  12086  mertenslem2  12087  fprodabs  12167  fprodle  12191  efcllemp  12209  ege2le3  12222  efaddlem  12225  efgt0  12235  reeftlcl  12240  eftlub  12241  effsumlt  12243  efltim  12249  eflegeo  12252  resin4p  12269  recos4p  12270  efeul  12285  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  sin01gt0  12313  cos01gt0  12314  sin02gt0  12315  cos12dec  12319  absefi  12320  absef  12321  absefib  12322  efieq1re  12323  eirraplem  12328  dvdsaddre2b  12392  dvdslelemd  12394  odd2np1  12424  divalglemnqt  12471  bitsp1o  12504  bitsfzo  12506  bitscmp  12509  nn0seqcvgd  12603  sqnprm  12698  isprm5lem  12703  odzdvds  12808  pythagtriplem14  12840  pcid  12887  fldivp1  12911  pockthlem  12919  4sqlem5  12945  4sqlem10  12950  mul4sqlem  12956  4sqlem15  12968  4sqlem16  12969  mulgneg  13717  ghmmulg  13833  rege0subm  14588  metrtri  15091  bl2in  15117  blhalf  15122  blssps  15141  blss  15142  maxcncf  15329  mincncf  15330  dedekindeu  15337  dedekindicclemicc  15346  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthinc  15357  ivthdec  15358  ivthreinc  15359  dvconstre  15410  dvidre  15411  dvcjbr  15422  dvfre  15424  dveflem  15440  plyrecj  15477  reeff1olem  15485  reeff1oleme  15486  eflt  15489  sin0pilem1  15495  sin0pilem2  15496  pilem3  15497  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  sinq34lt0t  15545  cosq14gt0  15546  cosq23lt0  15547  coseq0q4123  15548  coseq0negpitopi  15550  tanrpcl  15551  tangtx  15552  coskpi  15562  cosordlem  15563  cosq34lt1  15564  cos11  15567  reexplog  15585  relogexp  15586  logdivlti  15595  rpcxpef  15608  rpcncxpcl  15616  cxpap0  15618  rpcxpadd  15619  rpmulcxp  15623  cxpmul  15626  abscxp  15629  cxplt  15630  cxplt3  15634  logsqrt  15637  apcxp2  15653  rpabscxpbnd  15654  rplogbid1  15661  rplogb1  15662  rpelogb  15663  rplogbchbase  15664  rplogbreexp  15667  rprelogbmul  15669  rprelogbdiv  15671  rplogbcxp  15677  rpcxplogb  15678  logbgcd1irraplemexp  15682  logbgcd1irraplemap  15683  mersenne  15711  lgsvalmod  15738  lgsdilem  15746  lgsne0  15757  gausslemma2dlem1a  15777  gausslemma2dlem6  15786  lgseisenlem1  15789  lgseisenlem2  15790  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  2sqlem1  15833  mul2sq  15835  2sqlem3  15836  2sqlem8  15842  qdencn  16567  refeq  16568  cvgcmp2nlemabs  16572  cvgcmp2n  16573  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  trirec0  16584  apdifflemf  16586  apdifflemr  16587  apdiff  16588  redc0  16597  reap0  16598  cndcap  16599  nconstwlpolem0  16603  nconstwlpolemgt0  16604  neap0mkv  16609  ltlenmkv  16610