Theorem recnd 8354

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   RRcr 8178

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8271

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  readdcan  8466  ltadd2  8747  ltadd1  8757  leadd2  8759  ltsubadd  8760  ltsubadd2  8761  lesubadd  8762  lesubadd2  8763  ltaddsub  8764  leaddsub  8766  lesub1  8784  lesub2  8785  ltsub1  8786  ltsub2  8787  ltnegcon1  8791  ltnegcon2  8792  add20  8802  subge0  8803  suble0  8804  lesub0  8807  eqord2  8812  possumd  8897  sublt0d  8898  rimul  8913  rereim  8914  apreap  8915  ltmul1a  8919  ltmul1  8920  reapmul1  8923  remulext2  8928  cru  8930  apreim  8931  mulreim  8932  apadd1  8936  apneg  8939  mulext1  8940  ltapd  8966  aprcl  8974  aptap  8978  rerecclap  9060  redivclap  9061  recgt0  9180  prodgt0gt0  9181  prodgt0  9182  prodge0  9184  lemul1a  9188  ltdiv1  9198  ltmuldiv  9204  ledivmul  9207  lt2mul2div  9209  ltrec  9213  lt2msq  9216  ltdiv2  9217  ltrec1  9218  lerec2  9219  ledivdiv  9220  lediv2  9221  ltdiv23  9222  lediv23  9223  lediv12a  9224  recp1lt1  9229  recreclt  9230  ledivp1  9233  mulle0r  9274  negiso  9285  avglt1  9544  avglt2  9545  div4p1lem1div2  9559  nn0cnd  9622  zcn  9649  peano2z  9680  zaddcllemneg  9683  ztri3or  9687  zeo  9751  zcnd  9769  eluzmn  9928  eluzelcn  9933  infrenegsupex  9994  supinfneg  9995  infsupneg  9996  supminfex  9997  irrmulap  10048  cnref1o  10051  rpcn  10063  rpcnd  10099  ltaddrp2d  10132  mul2lt0rlt0  10160  mul2lt0rgt0  10161  mul2lt0llt0  10162  mul2lt0lgt0  10163  mul2lt0np  10164  mul2lt0pn  10165  xpncan  10273  icoshftf1o  10393  lincmb01cmp  10405  lincmble  10406  iccf1o  10407  infssuzcldc  10668  qbtwnrelemcalc  10690  flhalf  10737  intfracq  10757  flqdiv  10758  modqid  10786  modqid0  10787  mulqaddmodid  10801  seqf1oglem1  10956  ser3le  10974  expcl2lemap  10988  expnegzap  11010  expaddzaplem  11019  expaddzap  11020  expmulzap  11022  ltexp2a  11028  leexp2a  11029  leexp2r  11030  exple1  11032  expubnd  11033  sq11  11049  resq01  11095  bernneq2  11099  expnbnd  11101  nn0ltexp2  11147  nn0opthlem2d  11159  faclbnd  11179  bcp1nk  11200  bcm1n  11207  remim  11625  reim0b  11627  rereb  11628  mulreap  11629  cjreb  11631  recj  11632  reneg  11633  readd  11634  resub  11635  remullem  11636  remul2  11638  redivap  11639  imcj  11640  imneg  11641  imadd  11642  imsub  11643  immul2  11645  imdivap  11646  cjcj  11648  cjadd  11649  ipcnval  11651  cjmulval  11653  cjneg  11655  imval2  11659  sq01  11660  cjreim2  11670  cjap  11672  cnrecnv  11676  caucvgrelemrec  11745  cvg1nlemres  11751  recvguniqlem  11760  recvguniq  11761  resqrexlemover  11776  resqrexlemcalc1  11780  resqrexlemcalc2  11781  resqrexlemcalc3  11782  resqrexlemnmsq  11783  resqrexlemnm  11784  resqrexlemgt0  11786  resqrexlemoverl  11787  resqrexlemglsq  11788  remsqsqrt  11798  sqrtmul  11801  sqrtdiv  11808  sqrtmsq  11811  abs00ap  11828  absext  11829  abs00  11830  absdivap  11836  absid  11837  absexp  11845  absexpzap  11846  absimle  11850  abslt  11854  absle  11855  abssubap0  11856  abssubne0  11857  releabs  11862  recvalap  11863  abstri  11870  abs2difabs  11874  amgm2  11884  icodiamlt  11946  maxabsle  11970  maxabslemab  11972  maxabslemlub  11973  maxabslemval  11974  maxcl  11976  maxltsup  11984  max0addsup  11985  minmax  11996  minabs  12002  minclpr  12003  bdtrilem  12005  bdtri  12006  mul0inf  12007  mingeb  12008  climabs0  12073  reccn2ap  12079  climrecl  12090  climge0  12091  climle  12100  climsqz  12101  climsqz2  12102  climlec2  12107  climrecvg1n  12114  climcvg1nlem  12115  isumrecl  12196  isumge0  12197  fsumlessfi  12227  fsumge1  12228  fsum00  12229  fsumle  12230  fsumlt  12231  fsumabs  12232  iserabs  12242  isumrpcl  12261  isumle  12262  isumlessdc  12263  trireciplem  12267  trirecip  12268  expcnvre  12270  expcnv  12271  explecnv  12272  absltap  12276  geo2sum  12281  cvgratnnlembern  12290  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratnnlemabsle  12294  cvgratnnlemsumlt  12295  cvgratnnlemfm  12296  cvgratnnlemrate  12297  cvgratz  12299  mertenslemi1  12302  mertenslem2  12303  fprodabs  12383  fprodle  12407  efcllemp  12425  ege2le3  12438  efaddlem  12441  efgt0  12451  reeftlcl  12456  eftlub  12457  effsumlt  12459  efltim  12465  eflegeo  12468  resin4p  12485  recos4p  12486  efeul  12501  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  sin01gt0  12529  cos01gt0  12530  sin02gt0  12531  cos12dec  12535  absefi  12536  absef  12537  absefib  12538  efieq1re  12539  eirraplem  12544  dvdsaddre2b  12608  dvdslelemd  12610  odd2np1  12640  divalglemnqt  12687  bitsp1o  12720  bitsfzo  12722  bitscmp  12725  nn0seqcvgd  12819  sqnprm  12914  isprm5lem  12919  odzdvds  13024  pythagtriplem14  13056  pcid  13103  fldivp1  13127  pockthlem  13135  4sqlem5  13161  4sqlem10  13166  mul4sqlem  13172  4sqlem15  13184  4sqlem16  13185  ballotfilemsi  13258  mulgneg  13943  ghmmulg  14059  rege0subm  14921  metrtri  15478  bl2in  15504  blhalf  15509  blssps  15528  blss  15529  maxcncf  15716  mincncf  15717  dedekindeu  15724  dedekindicclemicc  15733  ivthinclemlopn  15737  ivthinclemuopn  15739  ivthinc  15744  ivthdec  15745  ivthreinc  15746  dvconstre  15797  dvidre  15798  dvcjbr  15809  dvfre  15811  dveflem  15827  plyrecj  15864  reeff1olem  15872  reeff1oleme  15873  eflt  15876  sin0pilem1  15882  sin0pilem2  15883  pilem3  15884  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  sinq12gt0  15931  sinq34lt0t  15932  cosq14gt0  15933  cosq23lt0  15934  coseq0q4123  15935  coseq0negpitopi  15937  tanrpcl  15938  tangtx  15939  coskpi  15949  cosordlem  15950  cosq34lt1  15951  cos11  15954  reexplog  15972  relogexp  15973  logdivlti  15982  logfac  15995  rpcxpef  15996  rpcncxpcl  16004  cxpap0  16006  rpcxpadd  16007  rpmulcxp  16011  cxpmul  16014  abscxp  16017  cxplt  16018  cxplt3  16022  logsqrt  16025  apcxp2  16041  rpabscxpbnd  16042  rplogbid1  16049  rplogb1  16050  rpelogb  16051  rplogbchbase  16052  rplogbreexp  16055  rprelogbmul  16057  rprelogbdiv  16059  rplogbcxp  16065  rpcxplogb  16066  logbgcd1irraplemexp  16070  logbgcd1irraplemap  16071  log2tlbndlog2  16082  log2ublem2  16084  birthdaylem2  16088  birthdaylem3  16089  pellexlem2  16092  mersenne  16111  lgsvalmod  16138  lgsdilem  16146  lgsne0  16157  gausslemma2dlem1a  16177  gausslemma2dlem6  16186  lgseisenlem1  16189  lgseisenlem2  16190  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  2sqlem1  16233  mul2sq  16235  2sqlem3  16236  2sqlem8  16242  dichmul0orlem1  16753  dichmul0orlem4  16756  dichmul0orlem5  16757  dichmul0orlem6  16758  dichmul0orlem7  16759  qdencn  17072  refeq  17073  repiecele0  17075  repiecege0  17076  cvgcmp2nlemabs  17081  cvgcmp2n  17082  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  trirec0  17093  apdifflemf  17095  apdifflemr  17096  apdiff  17097  qdiff  17098  redc0  17107  reap0  17108  cndcap  17109  nconstwlpolem0  17113  nconstwlpolemgt0  17114  neap0mkv  17119  ltlenmkv  17120