Theorem recnd 8058

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

Syntax hints:   -> wi 4   e. wcel 2167   CCcc 7880   RRcr 7881

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7974

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  readdcan  8169  ltadd2  8449  ltadd1  8459  leadd2  8461  ltsubadd  8462  ltsubadd2  8463  lesubadd  8464  lesubadd2  8465  ltaddsub  8466  leaddsub  8468  lesub1  8486  lesub2  8487  ltsub1  8488  ltsub2  8489  ltnegcon1  8493  ltnegcon2  8494  add20  8504  subge0  8505  suble0  8506  lesub0  8509  eqord2  8514  possumd  8599  sublt0d  8600  rimul  8615  rereim  8616  apreap  8617  ltmul1a  8621  ltmul1  8622  reapmul1  8625  remulext2  8630  cru  8632  apreim  8633  mulreim  8634  apadd1  8638  apneg  8641  mulext1  8642  ltapd  8668  aprcl  8676  aptap  8680  rerecclap  8760  redivclap  8761  recgt0  8880  prodgt0gt0  8881  prodgt0  8882  prodge0  8884  lemul1a  8888  ltdiv1  8898  ltmuldiv  8904  ledivmul  8907  lt2mul2div  8909  ltrec  8913  lt2msq  8916  ltdiv2  8917  ltrec1  8918  lerec2  8919  ledivdiv  8920  lediv2  8921  ltdiv23  8922  lediv23  8923  lediv12a  8924  recp1lt1  8929  recreclt  8930  ledivp1  8933  mulle0r  8974  negiso  8985  avglt1  9233  avglt2  9234  div4p1lem1div2  9248  nn0cnd  9307  zcn  9334  peano2z  9365  zaddcllemneg  9368  ztri3or  9372  zeo  9434  zcnd  9452  eluzelcn  9615  infrenegsupex  9671  supinfneg  9672  infsupneg  9673  supminfex  9674  irrmulap  9725  cnref1o  9728  rpcn  9740  rpcnd  9776  ltaddrp2d  9809  mul2lt0rlt0  9837  mul2lt0rgt0  9838  mul2lt0llt0  9839  mul2lt0lgt0  9840  mul2lt0np  9841  mul2lt0pn  9842  xpncan  9949  icoshftf1o  10069  lincmb01cmp  10081  iccf1o  10082  infssuzcldc  10328  qbtwnrelemcalc  10348  flhalf  10395  intfracq  10415  flqdiv  10416  modqid  10444  modqid0  10445  mulqaddmodid  10459  seqf1oglem1  10614  ser3le  10632  expcl2lemap  10646  expnegzap  10668  expaddzaplem  10677  expaddzap  10678  expmulzap  10680  ltexp2a  10686  leexp2a  10687  leexp2r  10688  exple1  10690  expubnd  10691  sq11  10707  bernneq2  10756  expnbnd  10758  nn0ltexp2  10804  nn0opthlem2d  10816  faclbnd  10836  bcp1nk  10857  remim  11028  reim0b  11030  rereb  11031  mulreap  11032  cjreb  11034  recj  11035  reneg  11036  readd  11037  resub  11038  remullem  11039  remul2  11041  redivap  11042  imcj  11043  imneg  11044  imadd  11045  imsub  11046  immul2  11048  imdivap  11049  cjcj  11051  cjadd  11052  ipcnval  11054  cjmulval  11056  cjneg  11058  imval2  11062  cjreim2  11072  cjap  11074  cnrecnv  11078  caucvgrelemrec  11147  cvg1nlemres  11153  recvguniqlem  11162  recvguniq  11163  resqrexlemover  11178  resqrexlemcalc1  11182  resqrexlemcalc2  11183  resqrexlemcalc3  11184  resqrexlemnmsq  11185  resqrexlemnm  11186  resqrexlemgt0  11188  resqrexlemoverl  11189  resqrexlemglsq  11190  remsqsqrt  11200  sqrtmul  11203  sqrtdiv  11210  sqrtmsq  11213  abs00ap  11230  absext  11231  abs00  11232  absdivap  11238  absid  11239  absexp  11247  absexpzap  11248  absimle  11252  abslt  11256  absle  11257  abssubap0  11258  abssubne0  11259  releabs  11264  recvalap  11265  abstri  11272  abs2difabs  11276  amgm2  11286  icodiamlt  11348  maxabsle  11372  maxabslemab  11374  maxabslemlub  11375  maxabslemval  11376  maxcl  11378  maxltsup  11386  max0addsup  11387  minmax  11398  minabs  11404  minclpr  11405  bdtrilem  11407  bdtri  11408  mul0inf  11409  mingeb  11410  climabs0  11475  reccn2ap  11481  climrecl  11492  climge0  11493  climle  11502  climsqz  11503  climsqz2  11504  climlec2  11509  climrecvg1n  11516  climcvg1nlem  11517  isumrecl  11597  isumge0  11598  fsumlessfi  11628  fsumge1  11629  fsum00  11630  fsumle  11631  fsumlt  11632  fsumabs  11633  iserabs  11643  isumrpcl  11662  isumle  11663  isumlessdc  11664  trireciplem  11668  trirecip  11669  expcnvre  11671  expcnv  11672  explecnv  11673  absltap  11677  geo2sum  11682  cvgratnnlembern  11691  cvgratnnlemnexp  11692  cvgratnnlemmn  11693  cvgratnnlemabsle  11695  cvgratnnlemsumlt  11696  cvgratnnlemfm  11697  cvgratnnlemrate  11698  cvgratz  11700  mertenslemi1  11703  mertenslem2  11704  fprodabs  11784  fprodle  11808  efcllemp  11826  ege2le3  11839  efaddlem  11842  efgt0  11852  reeftlcl  11857  eftlub  11858  effsumlt  11860  efltim  11866  eflegeo  11869  resin4p  11886  recos4p  11887  efeul  11902  ef01bndlem  11924  sin01bnd  11925  cos01bnd  11926  sin01gt0  11930  cos01gt0  11931  sin02gt0  11932  cos12dec  11936  absefi  11937  absef  11938  absefib  11939  efieq1re  11940  eirraplem  11945  dvdsaddre2b  12009  dvdslelemd  12011  odd2np1  12041  divalglemnqt  12088  bitsp1o  12121  bitsfzo  12123  bitscmp  12126  nn0seqcvgd  12220  sqnprm  12315  isprm5lem  12320  odzdvds  12425  pythagtriplem14  12457  pcid  12504  fldivp1  12528  pockthlem  12536  4sqlem5  12562  4sqlem10  12567  mul4sqlem  12573  4sqlem15  12585  4sqlem16  12586  mulgneg  13296  ghmmulg  13412  rege0subm  14166  metrtri  14639  bl2in  14665  blhalf  14670  blssps  14689  blss  14690  maxcncf  14877  mincncf  14878  dedekindeu  14885  dedekindicclemicc  14894  ivthinclemlopn  14898  ivthinclemuopn  14900  ivthinc  14905  ivthdec  14906  ivthreinc  14907  dvconstre  14958  dvidre  14959  dvcjbr  14970  dvfre  14972  dveflem  14988  plyrecj  15025  reeff1olem  15033  reeff1oleme  15034  eflt  15037  sin0pilem1  15043  sin0pilem2  15044  pilem3  15045  sincosq2sgn  15089  sincosq3sgn  15090  sincosq4sgn  15091  sinq12gt0  15092  sinq34lt0t  15093  cosq14gt0  15094  cosq23lt0  15095  coseq0q4123  15096  coseq0negpitopi  15098  tanrpcl  15099  tangtx  15100  coskpi  15110  cosordlem  15111  cosq34lt1  15112  cos11  15115  reexplog  15133  relogexp  15134  logdivlti  15143  rpcxpef  15156  rpcncxpcl  15164  cxpap0  15166  rpcxpadd  15167  rpmulcxp  15171  cxpmul  15174  abscxp  15177  cxplt  15178  cxplt3  15182  logsqrt  15185  apcxp2  15201  rpabscxpbnd  15202  rplogbid1  15209  rplogb1  15210  rpelogb  15211  rplogbchbase  15212  rplogbreexp  15215  rprelogbmul  15217  rprelogbdiv  15219  rplogbcxp  15225  rpcxplogb  15226  logbgcd1irraplemexp  15230  logbgcd1irraplemap  15231  mersenne  15259  lgsvalmod  15286  lgsdilem  15294  lgsne0  15305  gausslemma2dlem1a  15325  gausslemma2dlem6  15334  lgseisenlem1  15337  lgseisenlem2  15338  lgseisen  15341  lgsquadlem1  15344  lgsquadlem2  15345  2sqlem1  15381  mul2sq  15383  2sqlem3  15384  2sqlem8  15390  qdencn  15700  refeq  15701  cvgcmp2nlemabs  15705  cvgcmp2n  15706  trilpolemisumle  15711  trilpolemeq1  15713  trilpolemlt1  15714  trirec0  15717  apdifflemf  15719  apdifflemr  15720  apdiff  15721  redc0  15730  reap0  15731  cndcap  15732  nconstwlpolem0  15736  nconstwlpolemgt0  15737  neap0mkv  15742  ltlenmkv  15743