Theorem recnd 8186

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 8143	. 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 8008   RRcr 8009

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 8102

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  8297  ltadd2  8577  ltadd1  8587  leadd2  8589  ltsubadd  8590  ltsubadd2  8591  lesubadd  8592  lesubadd2  8593  ltaddsub  8594  leaddsub  8596  lesub1  8614  lesub2  8615  ltsub1  8616  ltsub2  8617  ltnegcon1  8621  ltnegcon2  8622  add20  8632  subge0  8633  suble0  8634  lesub0  8637  eqord2  8642  possumd  8727  sublt0d  8728  rimul  8743  rereim  8744  apreap  8745  ltmul1a  8749  ltmul1  8750  reapmul1  8753  remulext2  8758  cru  8760  apreim  8761  mulreim  8762  apadd1  8766  apneg  8769  mulext1  8770  ltapd  8796  aprcl  8804  aptap  8808  rerecclap  8888  redivclap  8889  recgt0  9008  prodgt0gt0  9009  prodgt0  9010  prodge0  9012  lemul1a  9016  ltdiv1  9026  ltmuldiv  9032  ledivmul  9035  lt2mul2div  9037  ltrec  9041  lt2msq  9044  ltdiv2  9045  ltrec1  9046  lerec2  9047  ledivdiv  9048  lediv2  9049  ltdiv23  9050  lediv23  9051  lediv12a  9052  recp1lt1  9057  recreclt  9058  ledivp1  9061  mulle0r  9102  negiso  9113  avglt1  9361  avglt2  9362  div4p1lem1div2  9376  nn0cnd  9435  zcn  9462  peano2z  9493  zaddcllemneg  9496  ztri3or  9500  zeo  9563  zcnd  9581  eluzmn  9740  eluzelcn  9745  infrenegsupex  9801  supinfneg  9802  infsupneg  9803  supminfex  9804  irrmulap  9855  cnref1o  9858  rpcn  9870  rpcnd  9906  ltaddrp2d  9939  mul2lt0rlt0  9967  mul2lt0rgt0  9968  mul2lt0llt0  9969  mul2lt0lgt0  9970  mul2lt0np  9971  mul2lt0pn  9972  xpncan  10079  icoshftf1o  10199  lincmb01cmp  10211  iccf1o  10212  infssuzcldc  10467  qbtwnrelemcalc  10487  flhalf  10534  intfracq  10554  flqdiv  10555  modqid  10583  modqid0  10584  mulqaddmodid  10598  seqf1oglem1  10753  ser3le  10771  expcl2lemap  10785  expnegzap  10807  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  ltexp2a  10825  leexp2a  10826  leexp2r  10827  exple1  10829  expubnd  10830  sq11  10846  bernneq2  10895  expnbnd  10897  nn0ltexp2  10943  nn0opthlem2d  10955  faclbnd  10975  bcp1nk  10996  remim  11386  reim0b  11388  rereb  11389  mulreap  11390  cjreb  11392  recj  11393  reneg  11394  readd  11395  resub  11396  remullem  11397  remul2  11399  redivap  11400  imcj  11401  imneg  11402  imadd  11403  imsub  11404  immul2  11406  imdivap  11407  cjcj  11409  cjadd  11410  ipcnval  11412  cjmulval  11414  cjneg  11416  imval2  11420  cjreim2  11430  cjap  11432  cnrecnv  11436  caucvgrelemrec  11505  cvg1nlemres  11511  recvguniqlem  11520  recvguniq  11521  resqrexlemover  11536  resqrexlemcalc1  11540  resqrexlemcalc2  11541  resqrexlemcalc3  11542  resqrexlemnmsq  11543  resqrexlemnm  11544  resqrexlemgt0  11546  resqrexlemoverl  11547  resqrexlemglsq  11548  remsqsqrt  11558  sqrtmul  11561  sqrtdiv  11568  sqrtmsq  11571  abs00ap  11588  absext  11589  abs00  11590  absdivap  11596  absid  11597  absexp  11605  absexpzap  11606  absimle  11610  abslt  11614  absle  11615  abssubap0  11616  abssubne0  11617  releabs  11622  recvalap  11623  abstri  11630  abs2difabs  11634  amgm2  11644  icodiamlt  11706  maxabsle  11730  maxabslemab  11732  maxabslemlub  11733  maxabslemval  11734  maxcl  11736  maxltsup  11744  max0addsup  11745  minmax  11756  minabs  11762  minclpr  11763  bdtrilem  11765  bdtri  11766  mul0inf  11767  mingeb  11768  climabs0  11833  reccn2ap  11839  climrecl  11850  climge0  11851  climle  11860  climsqz  11861  climsqz2  11862  climlec2  11867  climrecvg1n  11874  climcvg1nlem  11875  isumrecl  11955  isumge0  11956  fsumlessfi  11986  fsumge1  11987  fsum00  11988  fsumle  11989  fsumlt  11990  fsumabs  11991  iserabs  12001  isumrpcl  12020  isumle  12021  isumlessdc  12022  trireciplem  12026  trirecip  12027  expcnvre  12029  expcnv  12030  explecnv  12031  absltap  12035  geo2sum  12040  cvgratnnlembern  12049  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  cvgratnnlemabsle  12053  cvgratnnlemsumlt  12054  cvgratnnlemfm  12055  cvgratnnlemrate  12056  cvgratz  12058  mertenslemi1  12061  mertenslem2  12062  fprodabs  12142  fprodle  12166  efcllemp  12184  ege2le3  12197  efaddlem  12200  efgt0  12210  reeftlcl  12215  eftlub  12216  effsumlt  12218  efltim  12224  eflegeo  12227  resin4p  12244  recos4p  12245  efeul  12260  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  sin01gt0  12288  cos01gt0  12289  sin02gt0  12290  cos12dec  12294  absefi  12295  absef  12296  absefib  12297  efieq1re  12298  eirraplem  12303  dvdsaddre2b  12367  dvdslelemd  12369  odd2np1  12399  divalglemnqt  12446  bitsp1o  12479  bitsfzo  12481  bitscmp  12484  nn0seqcvgd  12578  sqnprm  12673  isprm5lem  12678  odzdvds  12783  pythagtriplem14  12815  pcid  12862  fldivp1  12886  pockthlem  12894  4sqlem5  12920  4sqlem10  12925  mul4sqlem  12931  4sqlem15  12943  4sqlem16  12944  mulgneg  13692  ghmmulg  13808  rege0subm  14563  metrtri  15066  bl2in  15092  blhalf  15097  blssps  15116  blss  15117  maxcncf  15304  mincncf  15305  dedekindeu  15312  dedekindicclemicc  15321  ivthinclemlopn  15325  ivthinclemuopn  15327  ivthinc  15332  ivthdec  15333  ivthreinc  15334  dvconstre  15385  dvidre  15386  dvcjbr  15397  dvfre  15399  dveflem  15415  plyrecj  15452  reeff1olem  15460  reeff1oleme  15461  eflt  15464  sin0pilem1  15470  sin0pilem2  15471  pilem3  15472  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  sinq12gt0  15519  sinq34lt0t  15520  cosq14gt0  15521  cosq23lt0  15522  coseq0q4123  15523  coseq0negpitopi  15525  tanrpcl  15526  tangtx  15527  coskpi  15537  cosordlem  15538  cosq34lt1  15539  cos11  15542  reexplog  15560  relogexp  15561  logdivlti  15570  rpcxpef  15583  rpcncxpcl  15591  cxpap0  15593  rpcxpadd  15594  rpmulcxp  15598  cxpmul  15601  abscxp  15604  cxplt  15605  cxplt3  15609  logsqrt  15612  apcxp2  15628  rpabscxpbnd  15629  rplogbid1  15636  rplogb1  15637  rpelogb  15638  rplogbchbase  15639  rplogbreexp  15642  rprelogbmul  15644  rprelogbdiv  15646  rplogbcxp  15652  rpcxplogb  15653  logbgcd1irraplemexp  15657  logbgcd1irraplemap  15658  mersenne  15686  lgsvalmod  15713  lgsdilem  15721  lgsne0  15732  gausslemma2dlem1a  15752  gausslemma2dlem6  15761  lgseisenlem1  15764  lgseisenlem2  15765  lgseisen  15768  lgsquadlem1  15771  lgsquadlem2  15772  2sqlem1  15808  mul2sq  15810  2sqlem3  15811  2sqlem8  15817  qdencn  16455  refeq  16456  cvgcmp2nlemabs  16460  cvgcmp2n  16461  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  trirec0  16472  apdifflemf  16474  apdifflemr  16475  apdiff  16476  redc0  16485  reap0  16486  cndcap  16487  nconstwlpolem0  16491  nconstwlpolemgt0  16492  neap0mkv  16497  ltlenmkv  16498