Theorem recnd 7054

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

Syntax hints:   -> wi 4   e. wcel 1393   CCcc 6887   RRcr 6888

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-resscn 6976

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931

This theorem is referenced by:  readdcan  7153  ltadd2  7416  ltadd1  7424  leadd2  7426  ltsubadd  7427  ltsubadd2  7428  lesubadd  7429  lesubadd2  7430  ltaddsub  7431  leaddsub  7433  lesub1  7451  lesub2  7452  ltsub1  7453  ltsub2  7454  ltnegcon1  7458  ltnegcon2  7459  add20  7469  subge0  7470  suble0  7471  lesub0  7474  possumd  7560  sublt0d  7561  rimul  7576  rereim  7577  apreap  7578  ltmul1a  7582  ltmul1  7583  reapmul1  7586  remulext2  7591  cru  7593  apreim  7594  mulreim  7595  apadd1  7599  apneg  7602  mulext1  7603  ltapd  7627  rerecclap  7706  redivclap  7707  recgt0  7816  prodgt0gt0  7817  prodgt0  7818  prodge0  7820  lemul1a  7824  ltdiv1  7834  ltmuldiv  7840  ledivmul  7843  lt2mul2div  7845  ltrec  7849  lt2msq  7852  ltdiv2  7853  ltrec1  7854  lerec2  7855  ledivdiv  7856  lediv2  7857  ltdiv23  7858  lediv23  7859  lediv12a  7860  recp1lt1  7865  recreclt  7866  ledivp1  7869  avglt1  8163  avglt2  8164  div4p1lem1div2  8177  nn0cnd  8237  zcn  8250  peano2z  8281  zaddcllemneg  8284  ztri3or  8288  zeo  8343  zcnd  8361  eluzelcn  8484  cnref1o  8582  rpcn  8591  rpcnd  8624  ltaddrp2d  8657  icoshftf1o  8859  lincmb01cmp  8871  iccf1o  8872  qbtwnrelemcalc  9110  flhalf  9144  intfracq  9162  flqdiv  9163  serile  9253  expcl2lemap  9267  expnegzap  9289  expaddzaplem  9298  expaddzap  9299  expmulzap  9301  ltexp2a  9306  leexp2a  9307  leexp2r  9308  exple1  9310  expubnd  9311  sq11  9326  bernneq2  9370  expnbnd  9372  remim  9460  reim0b  9462  rereb  9463  mulreap  9464  cjreb  9466  recj  9467  reneg  9468  readd  9469  resub  9470  remullem  9471  remul2  9473  redivap  9474  imcj  9475  imneg  9476  imadd  9477  imsub  9478  immul2  9480  imdivap  9481  cjcj  9483  cjadd  9484  ipcnval  9486  cjmulval  9488  cjneg  9490  imval2  9494  cjreim2  9504  cjap  9506  cnrecnv  9510  caucvgrelemrec  9578  cvg1nlemres  9584  recvguniqlem  9592  recvguniq  9593  resqrexlemover  9608  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrexlemcalc3  9614  resqrexlemnmsq  9615  resqrexlemnm  9616  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  remsqsqrt  9630  sqrtmul  9633  sqrtdiv  9640  sqrtmsq  9643  abs00ap  9660  absext  9661  abs00  9662  absdivap  9668  absid  9669  absexp  9675  absexpzap  9676  absimle  9680  abslt  9684  absle  9685  abssubap0  9686  abssubne0  9687  releabs  9692  recvalap  9693  abstri  9700  abs2difabs  9704  amgm2  9714  icodiamlt  9776  climabs0  9828  climrecl  9844  climge0  9845  climle  9854  climsqz  9855  climsqz2  9856  climlec2  9861  climserile  9865  climrecvg1n  9867  climcvg1nlem  9868  nn0seqcvgd  9880  qdencn  10124