Theorem recnd 8072

Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)

Hypothesis

Ref	Expression
recnd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
recnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem recnd

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		recn 8029	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7894  ℝcr 7895

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 7988

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  8183  ltadd2  8463  ltadd1  8473  leadd2  8475  ltsubadd  8476  ltsubadd2  8477  lesubadd  8478  lesubadd2  8479  ltaddsub  8480  leaddsub  8482  lesub1  8500  lesub2  8501  ltsub1  8502  ltsub2  8503  ltnegcon1  8507  ltnegcon2  8508  add20  8518  subge0  8519  suble0  8520  lesub0  8523  eqord2  8528  possumd  8613  sublt0d  8614  rimul  8629  rereim  8630  apreap  8631  ltmul1a  8635  ltmul1  8636  reapmul1  8639  remulext2  8644  cru  8646  apreim  8647  mulreim  8648  apadd1  8652  apneg  8655  mulext1  8656  ltapd  8682  aprcl  8690  aptap  8694  rerecclap  8774  redivclap  8775  recgt0  8894  prodgt0gt0  8895  prodgt0  8896  prodge0  8898  lemul1a  8902  ltdiv1  8912  ltmuldiv  8918  ledivmul  8921  lt2mul2div  8923  ltrec  8927  lt2msq  8930  ltdiv2  8931  ltrec1  8932  lerec2  8933  ledivdiv  8934  lediv2  8935  ltdiv23  8936  lediv23  8937  lediv12a  8938  recp1lt1  8943  recreclt  8944  ledivp1  8947  mulle0r  8988  negiso  8999  avglt1  9247  avglt2  9248  div4p1lem1div2  9262  nn0cnd  9321  zcn  9348  peano2z  9379  zaddcllemneg  9382  ztri3or  9386  zeo  9448  zcnd  9466  eluzelcn  9629  infrenegsupex  9685  supinfneg  9686  infsupneg  9687  supminfex  9688  irrmulap  9739  cnref1o  9742  rpcn  9754  rpcnd  9790  ltaddrp2d  9823  mul2lt0rlt0  9851  mul2lt0rgt0  9852  mul2lt0llt0  9853  mul2lt0lgt0  9854  mul2lt0np  9855  mul2lt0pn  9856  xpncan  9963  icoshftf1o  10083  lincmb01cmp  10095  iccf1o  10096  infssuzcldc  10342  qbtwnrelemcalc  10362  flhalf  10409  intfracq  10429  flqdiv  10430  modqid  10458  modqid0  10459  mulqaddmodid  10473  seqf1oglem1  10628  ser3le  10646  expcl2lemap  10660  expnegzap  10682  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  ltexp2a  10700  leexp2a  10701  leexp2r  10702  exple1  10704  expubnd  10705  sq11  10721  bernneq2  10770  expnbnd  10772  nn0ltexp2  10818  nn0opthlem2d  10830  faclbnd  10850  bcp1nk  10871  remim  11042  reim0b  11044  rereb  11045  mulreap  11046  cjreb  11048  recj  11049  reneg  11050  readd  11051  resub  11052  remullem  11053  remul2  11055  redivap  11056  imcj  11057  imneg  11058  imadd  11059  imsub  11060  immul2  11062  imdivap  11063  cjcj  11065  cjadd  11066  ipcnval  11068  cjmulval  11070  cjneg  11072  imval2  11076  cjreim2  11086  cjap  11088  cnrecnv  11092  caucvgrelemrec  11161  cvg1nlemres  11167  recvguniqlem  11176  recvguniq  11177  resqrexlemover  11192  resqrexlemcalc1  11196  resqrexlemcalc2  11197  resqrexlemcalc3  11198  resqrexlemnmsq  11199  resqrexlemnm  11200  resqrexlemgt0  11202  resqrexlemoverl  11203  resqrexlemglsq  11204  remsqsqrt  11214  sqrtmul  11217  sqrtdiv  11224  sqrtmsq  11227  abs00ap  11244  absext  11245  abs00  11246  absdivap  11252  absid  11253  absexp  11261  absexpzap  11262  absimle  11266  abslt  11270  absle  11271  abssubap0  11272  abssubne0  11273  releabs  11278  recvalap  11279  abstri  11286  abs2difabs  11290  amgm2  11300  icodiamlt  11362  maxabsle  11386  maxabslemab  11388  maxabslemlub  11389  maxabslemval  11390  maxcl  11392  maxltsup  11400  max0addsup  11401  minmax  11412  minabs  11418  minclpr  11419  bdtrilem  11421  bdtri  11422  mul0inf  11423  mingeb  11424  climabs0  11489  reccn2ap  11495  climrecl  11506  climge0  11507  climle  11516  climsqz  11517  climsqz2  11518  climlec2  11523  climrecvg1n  11530  climcvg1nlem  11531  isumrecl  11611  isumge0  11612  fsumlessfi  11642  fsumge1  11643  fsum00  11644  fsumle  11645  fsumlt  11646  fsumabs  11647  iserabs  11657  isumrpcl  11676  isumle  11677  isumlessdc  11678  trireciplem  11682  trirecip  11683  expcnvre  11685  expcnv  11686  explecnv  11687  absltap  11691  geo2sum  11696  cvgratnnlembern  11705  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemabsle  11709  cvgratnnlemsumlt  11710  cvgratnnlemfm  11711  cvgratnnlemrate  11712  cvgratz  11714  mertenslemi1  11717  mertenslem2  11718  fprodabs  11798  fprodle  11822  efcllemp  11840  ege2le3  11853  efaddlem  11856  efgt0  11866  reeftlcl  11871  eftlub  11872  effsumlt  11874  efltim  11880  eflegeo  11883  resin4p  11900  recos4p  11901  efeul  11916  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  sin01gt0  11944  cos01gt0  11945  sin02gt0  11946  cos12dec  11950  absefi  11951  absef  11952  absefib  11953  efieq1re  11954  eirraplem  11959  dvdsaddre2b  12023  dvdslelemd  12025  odd2np1  12055  divalglemnqt  12102  bitsp1o  12135  bitsfzo  12137  bitscmp  12140  nn0seqcvgd  12234  sqnprm  12329  isprm5lem  12334  odzdvds  12439  pythagtriplem14  12471  pcid  12518  fldivp1  12542  pockthlem  12550  4sqlem5  12576  4sqlem10  12581  mul4sqlem  12587  4sqlem15  12599  4sqlem16  12600  mulgneg  13346  ghmmulg  13462  rege0subm  14216  metrtri  14697  bl2in  14723  blhalf  14728  blssps  14747  blss  14748  maxcncf  14935  mincncf  14936  dedekindeu  14943  dedekindicclemicc  14952  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthinc  14963  ivthdec  14964  ivthreinc  14965  dvconstre  15016  dvidre  15017  dvcjbr  15028  dvfre  15030  dveflem  15046  plyrecj  15083  reeff1olem  15091  reeff1oleme  15092  eflt  15095  sin0pilem1  15101  sin0pilem2  15102  pilem3  15103  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  sinq12gt0  15150  sinq34lt0t  15151  cosq14gt0  15152  cosq23lt0  15153  coseq0q4123  15154  coseq0negpitopi  15156  tanrpcl  15157  tangtx  15158  coskpi  15168  cosordlem  15169  cosq34lt1  15170  cos11  15173  reexplog  15191  relogexp  15192  logdivlti  15201  rpcxpef  15214  rpcncxpcl  15222  cxpap0  15224  rpcxpadd  15225  rpmulcxp  15229  cxpmul  15232  abscxp  15235  cxplt  15236  cxplt3  15240  logsqrt  15243  apcxp2  15259  rpabscxpbnd  15260  rplogbid1  15267  rplogb1  15268  rpelogb  15269  rplogbchbase  15270  rplogbreexp  15273  rprelogbmul  15275  rprelogbdiv  15277  rplogbcxp  15283  rpcxplogb  15284  logbgcd1irraplemexp  15288  logbgcd1irraplemap  15289  mersenne  15317  lgsvalmod  15344  lgsdilem  15352  lgsne0  15363  gausslemma2dlem1a  15383  gausslemma2dlem6  15392  lgseisenlem1  15395  lgseisenlem2  15396  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  2sqlem1  15439  mul2sq  15441  2sqlem3  15442  2sqlem8  15448  qdencn  15758  refeq  15759  cvgcmp2nlemabs  15763  cvgcmp2n  15764  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  trirec0  15775  apdifflemf  15777  apdifflemr  15778  apdiff  15779  redc0  15788  reap0  15789  cndcap  15790  nconstwlpolem0  15794  nconstwlpolemgt0  15795  neap0mkv  15800  ltlenmkv  15801