Theorem recnd 8171

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 8128	. 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 7993   RRcr 7994

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 8087

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 3203  df-ss 3210

This theorem is referenced by:  readdcan  8282  ltadd2  8562  ltadd1  8572  leadd2  8574  ltsubadd  8575  ltsubadd2  8576  lesubadd  8577  lesubadd2  8578  ltaddsub  8579  leaddsub  8581  lesub1  8599  lesub2  8600  ltsub1  8601  ltsub2  8602  ltnegcon1  8606  ltnegcon2  8607  add20  8617  subge0  8618  suble0  8619  lesub0  8622  eqord2  8627  possumd  8712  sublt0d  8713  rimul  8728  rereim  8729  apreap  8730  ltmul1a  8734  ltmul1  8735  reapmul1  8738  remulext2  8743  cru  8745  apreim  8746  mulreim  8747  apadd1  8751  apneg  8754  mulext1  8755  ltapd  8781  aprcl  8789  aptap  8793  rerecclap  8873  redivclap  8874  recgt0  8993  prodgt0gt0  8994  prodgt0  8995  prodge0  8997  lemul1a  9001  ltdiv1  9011  ltmuldiv  9017  ledivmul  9020  lt2mul2div  9022  ltrec  9026  lt2msq  9029  ltdiv2  9030  ltrec1  9031  lerec2  9032  ledivdiv  9033  lediv2  9034  ltdiv23  9035  lediv23  9036  lediv12a  9037  recp1lt1  9042  recreclt  9043  ledivp1  9046  mulle0r  9087  negiso  9098  avglt1  9346  avglt2  9347  div4p1lem1div2  9361  nn0cnd  9420  zcn  9447  peano2z  9478  zaddcllemneg  9481  ztri3or  9485  zeo  9548  zcnd  9566  eluzelcn  9729  infrenegsupex  9785  supinfneg  9786  infsupneg  9787  supminfex  9788  irrmulap  9839  cnref1o  9842  rpcn  9854  rpcnd  9890  ltaddrp2d  9923  mul2lt0rlt0  9951  mul2lt0rgt0  9952  mul2lt0llt0  9953  mul2lt0lgt0  9954  mul2lt0np  9955  mul2lt0pn  9956  xpncan  10063  icoshftf1o  10183  lincmb01cmp  10195  iccf1o  10196  infssuzcldc  10450  qbtwnrelemcalc  10470  flhalf  10517  intfracq  10537  flqdiv  10538  modqid  10566  modqid0  10567  mulqaddmodid  10581  seqf1oglem1  10736  ser3le  10754  expcl2lemap  10768  expnegzap  10790  expaddzaplem  10799  expaddzap  10800  expmulzap  10802  ltexp2a  10808  leexp2a  10809  leexp2r  10810  exple1  10812  expubnd  10813  sq11  10829  bernneq2  10878  expnbnd  10880  nn0ltexp2  10926  nn0opthlem2d  10938  faclbnd  10958  bcp1nk  10979  remim  11366  reim0b  11368  rereb  11369  mulreap  11370  cjreb  11372  recj  11373  reneg  11374  readd  11375  resub  11376  remullem  11377  remul2  11379  redivap  11380  imcj  11381  imneg  11382  imadd  11383  imsub  11384  immul2  11386  imdivap  11387  cjcj  11389  cjadd  11390  ipcnval  11392  cjmulval  11394  cjneg  11396  imval2  11400  cjreim2  11410  cjap  11412  cnrecnv  11416  caucvgrelemrec  11485  cvg1nlemres  11491  recvguniqlem  11500  recvguniq  11501  resqrexlemover  11516  resqrexlemcalc1  11520  resqrexlemcalc2  11521  resqrexlemcalc3  11522  resqrexlemnmsq  11523  resqrexlemnm  11524  resqrexlemgt0  11526  resqrexlemoverl  11527  resqrexlemglsq  11528  remsqsqrt  11538  sqrtmul  11541  sqrtdiv  11548  sqrtmsq  11551  abs00ap  11568  absext  11569  abs00  11570  absdivap  11576  absid  11577  absexp  11585  absexpzap  11586  absimle  11590  abslt  11594  absle  11595  abssubap0  11596  abssubne0  11597  releabs  11602  recvalap  11603  abstri  11610  abs2difabs  11614  amgm2  11624  icodiamlt  11686  maxabsle  11710  maxabslemab  11712  maxabslemlub  11713  maxabslemval  11714  maxcl  11716  maxltsup  11724  max0addsup  11725  minmax  11736  minabs  11742  minclpr  11743  bdtrilem  11745  bdtri  11746  mul0inf  11747  mingeb  11748  climabs0  11813  reccn2ap  11819  climrecl  11830  climge0  11831  climle  11840  climsqz  11841  climsqz2  11842  climlec2  11847  climrecvg1n  11854  climcvg1nlem  11855  isumrecl  11935  isumge0  11936  fsumlessfi  11966  fsumge1  11967  fsum00  11968  fsumle  11969  fsumlt  11970  fsumabs  11971  iserabs  11981  isumrpcl  12000  isumle  12001  isumlessdc  12002  trireciplem  12006  trirecip  12007  expcnvre  12009  expcnv  12010  explecnv  12011  absltap  12015  geo2sum  12020  cvgratnnlembern  12029  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  cvgratnnlemabsle  12033  cvgratnnlemsumlt  12034  cvgratnnlemfm  12035  cvgratnnlemrate  12036  cvgratz  12038  mertenslemi1  12041  mertenslem2  12042  fprodabs  12122  fprodle  12146  efcllemp  12164  ege2le3  12177  efaddlem  12180  efgt0  12190  reeftlcl  12195  eftlub  12196  effsumlt  12198  efltim  12204  eflegeo  12207  resin4p  12224  recos4p  12225  efeul  12240  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  sin01gt0  12268  cos01gt0  12269  sin02gt0  12270  cos12dec  12274  absefi  12275  absef  12276  absefib  12277  efieq1re  12278  eirraplem  12283  dvdsaddre2b  12347  dvdslelemd  12349  odd2np1  12379  divalglemnqt  12426  bitsp1o  12459  bitsfzo  12461  bitscmp  12464  nn0seqcvgd  12558  sqnprm  12653  isprm5lem  12658  odzdvds  12763  pythagtriplem14  12795  pcid  12842  fldivp1  12866  pockthlem  12874  4sqlem5  12900  4sqlem10  12905  mul4sqlem  12911  4sqlem15  12923  4sqlem16  12924  mulgneg  13672  ghmmulg  13788  rege0subm  14542  metrtri  15045  bl2in  15071  blhalf  15076  blssps  15095  blss  15096  maxcncf  15283  mincncf  15284  dedekindeu  15291  dedekindicclemicc  15300  ivthinclemlopn  15304  ivthinclemuopn  15306  ivthinc  15311  ivthdec  15312  ivthreinc  15313  dvconstre  15364  dvidre  15365  dvcjbr  15376  dvfre  15378  dveflem  15394  plyrecj  15431  reeff1olem  15439  reeff1oleme  15440  eflt  15443  sin0pilem1  15449  sin0pilem2  15450  pilem3  15451  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  sinq12gt0  15498  sinq34lt0t  15499  cosq14gt0  15500  cosq23lt0  15501  coseq0q4123  15502  coseq0negpitopi  15504  tanrpcl  15505  tangtx  15506  coskpi  15516  cosordlem  15517  cosq34lt1  15518  cos11  15521  reexplog  15539  relogexp  15540  logdivlti  15549  rpcxpef  15562  rpcncxpcl  15570  cxpap0  15572  rpcxpadd  15573  rpmulcxp  15577  cxpmul  15580  abscxp  15583  cxplt  15584  cxplt3  15588  logsqrt  15591  apcxp2  15607  rpabscxpbnd  15608  rplogbid1  15615  rplogb1  15616  rpelogb  15617  rplogbchbase  15618  rplogbreexp  15621  rprelogbmul  15623  rprelogbdiv  15625  rplogbcxp  15631  rpcxplogb  15632  logbgcd1irraplemexp  15636  logbgcd1irraplemap  15637  mersenne  15665  lgsvalmod  15692  lgsdilem  15700  lgsne0  15711  gausslemma2dlem1a  15731  gausslemma2dlem6  15740  lgseisenlem1  15743  lgseisenlem2  15744  lgseisen  15747  lgsquadlem1  15750  lgsquadlem2  15751  2sqlem1  15787  mul2sq  15789  2sqlem3  15790  2sqlem8  15796  qdencn  16354  refeq  16355  cvgcmp2nlemabs  16359  cvgcmp2n  16360  trilpolemisumle  16365  trilpolemeq1  16367  trilpolemlt1  16368  trirec0  16371  apdifflemf  16373  apdifflemr  16374  apdiff  16375  redc0  16384  reap0  16385  cndcap  16386  nconstwlpolem0  16390  nconstwlpolemgt0  16391  neap0mkv  16396  ltlenmkv  16397