Theorem recnd 8355

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 8313	. 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 8178   RRcr 8179

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 8272

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  8468  ltadd2  8749  ltadd1  8759  leadd2  8761  ltsubadd  8762  ltsubadd2  8763  lesubadd  8764  lesubadd2  8765  ltaddsub  8766  leaddsub  8768  lesub1  8786  lesub2  8787  ltsub1  8788  ltsub2  8789  ltnegcon1  8793  ltnegcon2  8794  add20  8804  subge0  8805  suble0  8806  lesub0  8809  eqord2  8814  lesub3d  8893  possumd  8900  sublt0d  8901  rimul  8916  rereim  8917  apreap  8918  ltmul1a  8922  ltmul1  8923  reapmul1  8926  remulext2  8931  cru  8933  apreim  8934  mulreim  8935  apadd1  8939  apneg  8942  mulext1  8943  ltapd  8969  aprcl  8977  aptap  8981  rerecclap  9063  redivclap  9064  recgt0  9183  prodgt0gt0  9184  prodgt0  9185  prodge0  9187  lemul1a  9191  ltdiv1  9201  ltmuldiv  9207  ledivmul  9210  lt2mul2div  9212  ltrec  9216  lt2msq  9219  ltdiv2  9220  ltrec1  9221  lerec2  9222  ledivdiv  9223  lediv2  9224  ltdiv23  9225  lediv23  9226  lediv12a  9227  recp1lt1  9232  recreclt  9233  ledivp1  9236  mulle0r  9277  negiso  9288  avglt1  9549  avglt2  9550  div4p1lem1div2  9564  nn0cnd  9627  zcn  9654  peano2z  9685  zaddcllemneg  9688  ztri3or  9692  zeo  9756  zcnd  9774  eluzmn  9938  eluzelcn  9943  infrenegsupex  10004  supinfneg  10005  infsupneg  10006  supminfex  10007  irraddap  10057  irrmulap  10059  cnref1o  10062  rpcn  10074  rpcnd  10110  ltaddrp2d  10143  mul2lt0rlt0  10171  mul2lt0rgt0  10172  mul2lt0llt0  10173  mul2lt0lgt0  10174  mul2lt0np  10175  mul2lt0pn  10176  xpncan  10284  icoshftf1o  10404  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  infssuzcldc  10679  qbtwnrelemcalc  10701  flhalf  10752  intfracq  10772  flqdiv  10773  modqid  10801  modqid0  10802  mulqaddmodid  10816  seqf1oglem1  10971  ser3le  10989  expcl2lemap  11003  expnegzap  11025  expaddzaplem  11034  expaddzap  11035  expmulzap  11037  ltexp2a  11043  leexp2a  11044  leexp2r  11045  exple1  11047  expubnd  11048  sq11  11064  resq01  11110  bernneq2  11114  expnbnd  11116  nn0ltexp2  11163  nn0opthlem2d  11175  faclbnd  11195  bcp1nk  11216  bcm1n  11223  remim  11641  reim0b  11643  rereb  11644  mulreap  11645  cjreb  11647  recj  11648  reneg  11649  readd  11650  resub  11651  remullem  11652  remul2  11654  redivap  11655  imcj  11656  imneg  11657  imadd  11658  imsub  11659  immul2  11661  imdivap  11662  cjcj  11664  cjadd  11665  ipcnval  11667  cjmulval  11669  cjneg  11671  imval2  11675  sq01  11676  cjreim2  11686  cjap  11688  cnrecnv  11692  caucvgrelemrec  11761  cvg1nlemres  11767  recvguniqlem  11776  recvguniq  11777  resqrexlemover  11792  resqrexlemcalc1  11796  resqrexlemcalc2  11797  resqrexlemcalc3  11798  resqrexlemnmsq  11799  resqrexlemnm  11800  resqrexlemgt0  11802  resqrexlemoverl  11803  resqrexlemglsq  11804  remsqsqrt  11814  sqrtmul  11817  sqrtdiv  11824  sqrtmsq  11827  abs00ap  11844  absext  11845  abs00  11846  absdivap  11852  absid  11853  absexp  11862  absexpzap  11863  absimle  11867  abslt  11871  absle  11872  abssubap0  11873  abssubne0  11874  releabs  11879  recvalap  11880  abstri  11887  abs2difabs  11891  amgm2  11901  icodiamlt  11963  maxabsle  11987  maxabslemab  11989  maxabslemlub  11990  maxabslemval  11991  maxcl  11993  maxltsup  12001  max0addsup  12002  minmax  12014  minabs  12020  minclpr  12021  bdtrilem  12024  bdtri  12025  mul0inf  12026  mingeb  12027  climabs0  12092  reccn2ap  12098  climrecl  12109  climge0  12110  climle  12119  climsqz  12120  climsqz2  12121  climlec2  12126  climrecvg1n  12133  climcvg1nlem  12134  isumrecl  12215  isumge0  12216  fsumlessfi  12246  fsumge1  12247  fsum00  12248  fsumle  12249  fsumlt  12250  fsumabs  12251  iserabs  12261  isumrpcl  12280  isumle  12281  isumlessdc  12282  trireciplem  12286  trirecip  12287  expcnvre  12289  expcnv  12290  explecnv  12291  absltap  12295  geo2sum  12300  cvgratnnlembern  12309  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemabsle  12313  cvgratnnlemsumlt  12314  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratz  12318  mertenslemi1  12321  mertenslem2  12322  fprodabs  12402  fprodle  12426  efcllemp  12444  ege2le3  12457  efaddlem  12460  efgt0  12470  reeftlcl  12475  eftlub  12476  effsumlt  12478  efltim  12484  eflegeo  12487  resin4p  12504  recos4p  12505  efeul  12520  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  cos12dec  12554  absefi  12555  absef  12556  absefib  12557  efieq1re  12558  eirraplem  12563  dvdsaddre2b  12627  dvdslelemd  12629  odd2np1  12659  divalglemnqt  12706  bitsp1o  12739  bitsfzo  12741  bitscmp  12744  nn0seqcvgd  12838  sqnprm  12934  isprm5lem  12939  nn0sqdcq  13007  odzdvds  13047  pythagtriplem14  13079  pcid  13126  fldivp1  13150  pockthlem  13158  4sqlem5  13184  4sqlem10  13189  mul4sqlem  13195  4sqlem15  13207  4sqlem16  13208  ballotfilemsi  13310  mulgneg  13996  ghmmulg  14112  rege0subm  15005  metrtri  15569  bl2in  15595  blhalf  15600  blssps  15619  blss  15620  maxcncf  15807  mincncf  15808  dedekindeu  15815  dedekindicclemicc  15824  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthinc  15835  ivthdec  15836  ivthreinc  15837  dvconstre  15888  dvidre  15889  dvcjbr  15900  dvfre  15902  dveflem  15918  plyrecj  15955  reeff1olem  15963  reeff1oleme  15964  eflt  15967  efap1p  15971  sin0pilem1  15974  sin0pilem2  15975  pilem3  15976  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  sinq34lt0t  16024  cosq14gt0  16025  cosq23lt0  16026  coseq0q4123  16027  coseq0negpitopi  16029  tanrpcl  16030  tangtx  16031  coskpi  16041  cosordlem  16042  cosq34lt1  16043  cos11  16046  reexplog  16065  relogexp  16066  logdivlti  16075  logdivlt  16088  logfac  16090  rpcxpef  16091  rpcncxpcl  16099  cxpap0  16101  rpcxpadd  16102  rpmulcxp  16106  cxpmul  16109  abscxp  16112  cxplt  16113  cxplt3  16117  logsqrt  16120  apcxp2  16136  rpabscxpbnd  16137  rplogbid1  16144  rplogb1  16145  rpelogb  16146  rplogbchbase  16147  rplogbreexp  16150  rprelogbmul  16152  rprelogbdiv  16154  rplogbcxp  16160  rpcxplogb  16161  logbgcd1irraplemexp  16165  logbgcd1irraplemap  16166  zprmlogbaplem2  16177  log2tlbndlog2  16181  log2ublem2  16183  birthdaylem2  16187  birthdaylem3  16188  pellexlem2  16191  efnnfsumcl  16200  chtprm  16222  chtdif  16225  efchtqdvds  16226  prmorcht  16243  ppiqub  16254  chtqleppi  16255  chtublem  16256  chtqub  16257  mersenne  16258  bcmax  16266  bcp1ctr  16267  bposlem1  16272  bposlem9  16280  lgsvalmod  16304  lgsdilem  16312  lgsne0  16323  gausslemma2dlem1a  16343  gausslemma2dlem6  16352  lgseisenlem1  16355  lgseisenlem2  16356  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  2sqlem1  16399  mul2sq  16401  2sqlem3  16402  2sqlem8  16408  dichmul0orlem1  16919  dichmul0orlem4  16922  dichmul0orlem5  16923  dichmul0orlem6  16924  dichmul0orlem7  16925  qdencn  17238  refeq  17239  repiecele0  17241  repiecege0  17242  cvgcmp2nlemabs  17247  cvgcmp2n  17248  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  trirec0  17260  apdifflemf  17262  apdifflemr  17263  apdiff  17264  qdiff  17265  redc0  17274  reap0  17275  cndcap  17276  nconstwlpolem0  17280  nconstwlpolemgt0  17281  neap0mkv  17286  ltlenmkv  17287