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  11142  reim0b  11144  rereb  11145  mulreap  11146  cjreb  11148  recj  11149  reneg  11150  readd  11151  resub  11152  remullem  11153  remul2  11155  redivap  11156  imcj  11157  imneg  11158  imadd  11159  imsub  11160  immul2  11162  imdivap  11163  cjcj  11165  cjadd  11166  ipcnval  11168  cjmulval  11170  cjneg  11172  imval2  11176  cjreim2  11186  cjap  11188  cnrecnv  11192  caucvgrelemrec  11261  cvg1nlemres  11267  recvguniqlem  11276  recvguniq  11277  resqrexlemover  11292  resqrexlemcalc1  11296  resqrexlemcalc2  11297  resqrexlemcalc3  11298  resqrexlemnmsq  11299  resqrexlemnm  11300  resqrexlemgt0  11302  resqrexlemoverl  11303  resqrexlemglsq  11304  remsqsqrt  11314  sqrtmul  11317  sqrtdiv  11324  sqrtmsq  11327  abs00ap  11344  absext  11345  abs00  11346  absdivap  11352  absid  11353  absexp  11361  absexpzap  11362  absimle  11366  abslt  11370  absle  11371  abssubap0  11372  abssubne0  11373  releabs  11378  recvalap  11379  abstri  11386  abs2difabs  11390  amgm2  11400  icodiamlt  11462  maxabsle  11486  maxabslemab  11488  maxabslemlub  11489  maxabslemval  11490  maxcl  11492  maxltsup  11500  max0addsup  11501  minmax  11512  minabs  11518  minclpr  11519  bdtrilem  11521  bdtri  11522  mul0inf  11523  mingeb  11524  climabs0  11589  reccn2ap  11595  climrecl  11606  climge0  11607  climle  11616  climsqz  11617  climsqz2  11618  climlec2  11623  climrecvg1n  11630  climcvg1nlem  11631  isumrecl  11711  isumge0  11712  fsumlessfi  11742  fsumge1  11743  fsum00  11744  fsumle  11745  fsumlt  11746  fsumabs  11747  iserabs  11757  isumrpcl  11776  isumle  11777  isumlessdc  11778  trireciplem  11782  trirecip  11783  expcnvre  11785  expcnv  11786  explecnv  11787  absltap  11791  geo2sum  11796  cvgratnnlembern  11805  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  cvgratnnlemabsle  11809  cvgratnnlemsumlt  11810  cvgratnnlemfm  11811  cvgratnnlemrate  11812  cvgratz  11814  mertenslemi1  11817  mertenslem2  11818  fprodabs  11898  fprodle  11922  efcllemp  11940  ege2le3  11953  efaddlem  11956  efgt0  11966  reeftlcl  11971  eftlub  11972  effsumlt  11974  efltim  11980  eflegeo  11983  resin4p  12000  recos4p  12001  efeul  12016  ef01bndlem  12038  sin01bnd  12039  cos01bnd  12040  sin01gt0  12044  cos01gt0  12045  sin02gt0  12046  cos12dec  12050  absefi  12051  absef  12052  absefib  12053  efieq1re  12054  eirraplem  12059  dvdsaddre2b  12123  dvdslelemd  12125  odd2np1  12155  divalglemnqt  12202  bitsp1o  12235  bitsfzo  12237  bitscmp  12240  nn0seqcvgd  12334  sqnprm  12429  isprm5lem  12434  odzdvds  12539  pythagtriplem14  12571  pcid  12618  fldivp1  12642  pockthlem  12650  4sqlem5  12676  4sqlem10  12681  mul4sqlem  12687  4sqlem15  12699  4sqlem16  12700  mulgneg  13447  ghmmulg  13563  rege0subm  14317  metrtri  14820  bl2in  14846  blhalf  14851  blssps  14870  blss  14871  maxcncf  15058  mincncf  15059  dedekindeu  15066  dedekindicclemicc  15075  ivthinclemlopn  15079  ivthinclemuopn  15081  ivthinc  15086  ivthdec  15087  ivthreinc  15088  dvconstre  15139  dvidre  15140  dvcjbr  15151  dvfre  15153  dveflem  15169  plyrecj  15206  reeff1olem  15214  reeff1oleme  15215  eflt  15218  sin0pilem1  15224  sin0pilem2  15225  pilem3  15226  sincosq2sgn  15270  sincosq3sgn  15271  sincosq4sgn  15272  sinq12gt0  15273  sinq34lt0t  15274  cosq14gt0  15275  cosq23lt0  15276  coseq0q4123  15277  coseq0negpitopi  15279  tanrpcl  15280  tangtx  15281  coskpi  15291  cosordlem  15292  cosq34lt1  15293  cos11  15296  reexplog  15314  relogexp  15315  logdivlti  15324  rpcxpef  15337  rpcncxpcl  15345  cxpap0  15347  rpcxpadd  15348  rpmulcxp  15352  cxpmul  15355  abscxp  15358  cxplt  15359  cxplt3  15363  logsqrt  15366  apcxp2  15382  rpabscxpbnd  15383  rplogbid1  15390  rplogb1  15391  rpelogb  15392  rplogbchbase  15393  rplogbreexp  15396  rprelogbmul  15398  rprelogbdiv  15400  rplogbcxp  15406  rpcxplogb  15407  logbgcd1irraplemexp  15411  logbgcd1irraplemap  15412  mersenne  15440  lgsvalmod  15467  lgsdilem  15475  lgsne0  15486  gausslemma2dlem1a  15506  gausslemma2dlem6  15515  lgseisenlem1  15518  lgseisenlem2  15519  lgseisen  15522  lgsquadlem1  15525  lgsquadlem2  15526  2sqlem1  15562  mul2sq  15564  2sqlem3  15565  2sqlem8  15571  qdencn  15928  refeq  15929  cvgcmp2nlemabs  15933  cvgcmp2n  15934  trilpolemisumle  15939  trilpolemeq1  15941  trilpolemlt1  15942  trirec0  15945  apdifflemf  15947  apdifflemr  15948  apdiff  15949  redc0  15958  reap0  15959  cndcap  15960  nconstwlpolem0  15964  nconstwlpolemgt0  15965  neap0mkv  15970  ltlenmkv  15971