Theorem recnd 8360

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 8318	. 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 8183   RRcr 8184

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 8277

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  8473  ltadd2  8754  ltadd1  8764  leadd2  8766  ltsubadd  8767  ltsubadd2  8768  lesubadd  8769  lesubadd2  8770  ltaddsub  8771  leaddsub  8773  lesub1  8791  lesub2  8792  ltsub1  8793  ltsub2  8794  ltnegcon1  8798  ltnegcon2  8799  add20  8809  subge0  8810  suble0  8811  lesub0  8814  eqord2  8819  lesub3d  8898  possumd  8905  sublt0d  8906  rimul  8921  rereim  8922  apreap  8923  ltmul1a  8927  ltmul1  8928  reapmul1  8931  remulext2  8936  cru  8938  apreim  8939  mulreim  8940  apadd1  8944  apneg  8947  mulext1  8948  ltapd  8974  aprcl  8982  aptap  8986  rerecclap  9068  redivclap  9069  recgt0  9188  prodgt0gt0  9189  prodgt0  9190  prodge0  9192  lemul1a  9196  ltdiv1  9206  ltmuldiv  9212  ledivmul  9215  lt2mul2div  9217  ltrec  9221  lt2msq  9224  ltdiv2  9225  ltrec1  9226  lerec2  9227  ledivdiv  9228  lediv2  9229  ltdiv23  9230  lediv23  9231  lediv12a  9232  recp1lt1  9237  recreclt  9238  ledivp1  9241  mulle0r  9282  negiso  9293  avglt1  9555  avglt2  9556  div4p1lem1div2  9570  nn0cnd  9633  zcn  9660  peano2z  9691  zaddcllemneg  9694  ztri3or  9698  zeo  9762  zcnd  9780  eluzmn  9944  eluzelcn  9949  infrenegsupex  10010  supinfneg  10011  infsupneg  10012  supminfex  10013  irraddap  10063  irrmulap  10065  cnref1o  10068  rpcn  10080  rpcnd  10116  ltaddrp2d  10149  mul2lt0rlt0  10177  mul2lt0rgt0  10178  mul2lt0llt0  10179  mul2lt0lgt0  10180  mul2lt0np  10181  mul2lt0pn  10182  xpncan  10290  icoshftf1o  10410  lincmb01cmp  10422  lincmble  10423  iccf1o  10424  infssuzcldc  10685  qbtwnrelemcalc  10707  flhalf  10758  intfracq  10778  flqdiv  10779  modqid  10807  modqid0  10808  mulqaddmodid  10822  seqf1oglem1  10977  ser3le  10995  expcl2lemap  11009  expnegzap  11031  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  ltexp2a  11049  leexp2a  11050  leexp2r  11051  exple1  11053  expubnd  11054  sq11  11070  resq01  11116  bernneq2  11120  expnbnd  11122  nn0ltexp2  11169  nn0opthlem2d  11181  faclbnd  11201  bcp1nk  11222  bcm1n  11229  remim  11647  reim0b  11649  rereb  11650  mulreap  11651  cjreb  11653  recj  11654  reneg  11655  readd  11656  resub  11657  remullem  11658  remul2  11660  redivap  11661  imcj  11662  imneg  11663  imadd  11664  imsub  11665  immul2  11667  imdivap  11668  cjcj  11670  cjadd  11671  ipcnval  11673  cjmulval  11675  cjneg  11677  imval2  11681  sq01  11682  cjreim2  11692  cjap  11694  cnrecnv  11698  caucvgrelemrec  11767  cvg1nlemres  11773  recvguniqlem  11782  recvguniq  11783  resqrexlemover  11798  resqrexlemcalc1  11802  resqrexlemcalc2  11803  resqrexlemcalc3  11804  resqrexlemnmsq  11805  resqrexlemnm  11806  resqrexlemgt0  11808  resqrexlemoverl  11809  resqrexlemglsq  11810  remsqsqrt  11820  sqrtmul  11823  sqrtdiv  11830  sqrtmsq  11833  abs00ap  11850  absext  11851  abs00  11852  absdivap  11858  absid  11859  absexp  11868  absexpzap  11869  absimle  11873  abslt  11877  absle  11878  abssubap0  11879  abssubne0  11880  releabs  11885  recvalap  11886  abstri  11893  abs2difabs  11897  amgm2  11907  icodiamlt  11969  maxabsle  11993  maxabslemab  11995  maxabslemlub  11996  maxabslemval  11997  maxcl  11999  maxltsup  12007  max0addsup  12008  minmax  12020  minabs  12026  minclpr  12027  bdtrilem  12030  bdtri  12031  mul0inf  12032  mingeb  12033  climabs0  12098  reccn2ap  12104  climrecl  12115  climge0  12116  climle  12125  climsqz  12126  climsqz2  12127  climlec2  12132  climrecvg1n  12139  climcvg1nlem  12140  isumrecl  12221  isumge0  12222  fsumlessfi  12252  fsumge1  12253  fsum00  12254  fsumle  12255  fsumlt  12256  fsumabs  12257  iserabs  12267  isumrpcl  12286  isumle  12287  isumlessdc  12288  trireciplem  12292  trirecip  12293  expcnvre  12295  expcnv  12296  explecnv  12297  absltap  12301  geo2sum  12306  cvgratnnlembern  12315  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemabsle  12319  cvgratnnlemsumlt  12320  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratz  12324  mertenslemi1  12327  mertenslem2  12328  fprodabs  12408  fprodle  12432  efcllemp  12450  ege2le3  12463  efaddlem  12466  efgt0  12476  reeftlcl  12481  eftlub  12482  effsumlt  12484  efltim  12490  eflegeo  12493  resin4p  12510  recos4p  12511  efeul  12526  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  cos12dec  12560  absefi  12561  absef  12562  absefib  12563  efieq1re  12564  eirraplem  12569  dvdsaddre2b  12633  dvdslelemd  12635  odd2np1  12665  divalglemnqt  12712  bitsp1o  12745  bitsfzo  12747  bitscmp  12750  nn0seqcvgd  12844  sqnprm  12940  isprm5lem  12945  nn0sqdcq  13013  odzdvds  13053  pythagtriplem14  13085  pcid  13132  fldivp1  13156  pockthlem  13164  4sqlem5  13190  4sqlem10  13195  mul4sqlem  13201  4sqlem15  13213  4sqlem16  13214  ballotfilemsi  13316  mulgneg  14002  ghmmulg  14118  rege0subm  15030  metrtri  15603  bl2in  15629  blhalf  15634  blssps  15653  blss  15654  maxcncf  15841  mincncf  15842  dedekindeu  15849  dedekindicclemicc  15858  ivthinclemlopn  15862  ivthinclemuopn  15864  ivthinc  15869  ivthdec  15870  ivthreinc  15871  dvconstre  15922  dvidre  15923  dvcjbr  15934  dvfre  15936  dveflem  15952  plyrecj  15989  reeff1olem  15997  reeff1oleme  15998  eflt  16001  efap1p  16005  sin0pilem1  16008  sin0pilem2  16009  pilem3  16010  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  sinq12gt0  16057  sinq34lt0t  16058  cosq14gt0  16059  cosq23lt0  16060  coseq0q4123  16061  coseq0negpitopi  16063  tanrpcl  16064  tangtx  16065  coskpi  16075  cosordlem  16077  cosq34lt1  16078  cos11  16081  reexplog  16101  relogexp  16102  logdivlti  16111  logdivlt  16124  logfac  16126  rpcxpef  16127  rpcncxpcl  16135  cxpap0  16137  rpcxpadd  16138  rpmulcxp  16142  cxpmul  16145  rpcxpmul2z  16148  abscxp  16150  cxplt  16151  cxplt3  16155  logsqrt  16158  apcxp2  16174  rpabscxpbnd  16175  rplogbid1  16183  rplogb1  16184  rpelogb  16185  rplogbchbase  16186  rplogbreexp  16189  rprelogbmul  16191  rprelogbdiv  16193  rplogbcxp  16199  rpcxplogb  16200  logbgcd1irraplemexp  16204  logbgcd1irraplemap  16205  zprmlogbaplem2  16216  log2tlbndlog2  16220  log2ublem2  16222  birthdaylem2  16226  birthdaylem3  16227  pellexlem2  16230  efnnfsumcl  16239  chtprm  16261  chtdif  16264  efchtqdvds  16265  prmorcht  16282  ppiqub  16293  chtqleppi  16294  chtublem  16295  chtqub  16296  mersenne  16297  bcmax  16305  bcp1ctr  16306  bposlem1  16311  bposlem9  16319  lgsvalmod  16343  lgsdilem  16351  lgsne0  16362  gausslemma2dlem1a  16382  gausslemma2dlem6  16391  lgseisenlem1  16394  lgseisenlem2  16395  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  2sqlem1  16438  mul2sq  16440  2sqlem3  16441  2sqlem8  16447  dichmul0orlem1  16958  dichmul0orlem4  16961  dichmul0orlem5  16962  dichmul0orlem6  16963  dichmul0orlem7  16964  qdencn  17278  refeq  17279  repiecele0  17281  repiecege0  17282  cvgcmp2nlemabs  17287  cvgcmp2n  17288  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  trirec0  17300  apdifflemf  17302  apdifflemr  17303  apdiff  17304  qdiff  17305  redc0  17314  reap0  17315  cndcap  17316  nconstwlpolem0  17320  nconstwlpolemgt0  17321  neap0mkv  17326  ltlenmkv  17327