Theorem recnd 8074

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 8031	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7896  ℝcr 7897

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 7990

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  8185  ltadd2  8465  ltadd1  8475  leadd2  8477  ltsubadd  8478  ltsubadd2  8479  lesubadd  8480  lesubadd2  8481  ltaddsub  8482  leaddsub  8484  lesub1  8502  lesub2  8503  ltsub1  8504  ltsub2  8505  ltnegcon1  8509  ltnegcon2  8510  add20  8520  subge0  8521  suble0  8522  lesub0  8525  eqord2  8530  possumd  8615  sublt0d  8616  rimul  8631  rereim  8632  apreap  8633  ltmul1a  8637  ltmul1  8638  reapmul1  8641  remulext2  8646  cru  8648  apreim  8649  mulreim  8650  apadd1  8654  apneg  8657  mulext1  8658  ltapd  8684  aprcl  8692  aptap  8696  rerecclap  8776  redivclap  8777  recgt0  8896  prodgt0gt0  8897  prodgt0  8898  prodge0  8900  lemul1a  8904  ltdiv1  8914  ltmuldiv  8920  ledivmul  8923  lt2mul2div  8925  ltrec  8929  lt2msq  8932  ltdiv2  8933  ltrec1  8934  lerec2  8935  ledivdiv  8936  lediv2  8937  ltdiv23  8938  lediv23  8939  lediv12a  8940  recp1lt1  8945  recreclt  8946  ledivp1  8949  mulle0r  8990  negiso  9001  avglt1  9249  avglt2  9250  div4p1lem1div2  9264  nn0cnd  9323  zcn  9350  peano2z  9381  zaddcllemneg  9384  ztri3or  9388  zeo  9450  zcnd  9468  eluzelcn  9631  infrenegsupex  9687  supinfneg  9688  infsupneg  9689  supminfex  9690  irrmulap  9741  cnref1o  9744  rpcn  9756  rpcnd  9792  ltaddrp2d  9825  mul2lt0rlt0  9853  mul2lt0rgt0  9854  mul2lt0llt0  9855  mul2lt0lgt0  9856  mul2lt0np  9857  mul2lt0pn  9858  xpncan  9965  icoshftf1o  10085  lincmb01cmp  10097  iccf1o  10098  infssuzcldc  10344  qbtwnrelemcalc  10364  flhalf  10411  intfracq  10431  flqdiv  10432  modqid  10460  modqid0  10461  mulqaddmodid  10475  seqf1oglem1  10630  ser3le  10648  expcl2lemap  10662  expnegzap  10684  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  ltexp2a  10702  leexp2a  10703  leexp2r  10704  exple1  10706  expubnd  10707  sq11  10723  bernneq2  10772  expnbnd  10774  nn0ltexp2  10820  nn0opthlem2d  10832  faclbnd  10852  bcp1nk  10873  remim  11044  reim0b  11046  rereb  11047  mulreap  11048  cjreb  11050  recj  11051  reneg  11052  readd  11053  resub  11054  remullem  11055  remul2  11057  redivap  11058  imcj  11059  imneg  11060  imadd  11061  imsub  11062  immul2  11064  imdivap  11065  cjcj  11067  cjadd  11068  ipcnval  11070  cjmulval  11072  cjneg  11074  imval2  11078  cjreim2  11088  cjap  11090  cnrecnv  11094  caucvgrelemrec  11163  cvg1nlemres  11169  recvguniqlem  11178  recvguniq  11179  resqrexlemover  11194  resqrexlemcalc1  11198  resqrexlemcalc2  11199  resqrexlemcalc3  11200  resqrexlemnmsq  11201  resqrexlemnm  11202  resqrexlemgt0  11204  resqrexlemoverl  11205  resqrexlemglsq  11206  remsqsqrt  11216  sqrtmul  11219  sqrtdiv  11226  sqrtmsq  11229  abs00ap  11246  absext  11247  abs00  11248  absdivap  11254  absid  11255  absexp  11263  absexpzap  11264  absimle  11268  abslt  11272  absle  11273  abssubap0  11274  abssubne0  11275  releabs  11280  recvalap  11281  abstri  11288  abs2difabs  11292  amgm2  11302  icodiamlt  11364  maxabsle  11388  maxabslemab  11390  maxabslemlub  11391  maxabslemval  11392  maxcl  11394  maxltsup  11402  max0addsup  11403  minmax  11414  minabs  11420  minclpr  11421  bdtrilem  11423  bdtri  11424  mul0inf  11425  mingeb  11426  climabs0  11491  reccn2ap  11497  climrecl  11508  climge0  11509  climle  11518  climsqz  11519  climsqz2  11520  climlec2  11525  climrecvg1n  11532  climcvg1nlem  11533  isumrecl  11613  isumge0  11614  fsumlessfi  11644  fsumge1  11645  fsum00  11646  fsumle  11647  fsumlt  11648  fsumabs  11649  iserabs  11659  isumrpcl  11678  isumle  11679  isumlessdc  11680  trireciplem  11684  trirecip  11685  expcnvre  11687  expcnv  11688  explecnv  11689  absltap  11693  geo2sum  11698  cvgratnnlembern  11707  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratnnlemabsle  11711  cvgratnnlemsumlt  11712  cvgratnnlemfm  11713  cvgratnnlemrate  11714  cvgratz  11716  mertenslemi1  11719  mertenslem2  11720  fprodabs  11800  fprodle  11824  efcllemp  11842  ege2le3  11855  efaddlem  11858  efgt0  11868  reeftlcl  11873  eftlub  11874  effsumlt  11876  efltim  11882  eflegeo  11885  resin4p  11902  recos4p  11903  efeul  11918  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  sin01gt0  11946  cos01gt0  11947  sin02gt0  11948  cos12dec  11952  absefi  11953  absef  11954  absefib  11955  efieq1re  11956  eirraplem  11961  dvdsaddre2b  12025  dvdslelemd  12027  odd2np1  12057  divalglemnqt  12104  bitsp1o  12137  bitsfzo  12139  bitscmp  12142  nn0seqcvgd  12236  sqnprm  12331  isprm5lem  12336  odzdvds  12441  pythagtriplem14  12473  pcid  12520  fldivp1  12544  pockthlem  12552  4sqlem5  12578  4sqlem10  12583  mul4sqlem  12589  4sqlem15  12601  4sqlem16  12602  mulgneg  13348  ghmmulg  13464  rege0subm  14218  metrtri  14699  bl2in  14725  blhalf  14730  blssps  14749  blss  14750  maxcncf  14937  mincncf  14938  dedekindeu  14945  dedekindicclemicc  14954  ivthinclemlopn  14958  ivthinclemuopn  14960  ivthinc  14965  ivthdec  14966  ivthreinc  14967  dvconstre  15018  dvidre  15019  dvcjbr  15030  dvfre  15032  dveflem  15048  plyrecj  15085  reeff1olem  15093  reeff1oleme  15094  eflt  15097  sin0pilem1  15103  sin0pilem2  15104  pilem3  15105  sincosq2sgn  15149  sincosq3sgn  15150  sincosq4sgn  15151  sinq12gt0  15152  sinq34lt0t  15153  cosq14gt0  15154  cosq23lt0  15155  coseq0q4123  15156  coseq0negpitopi  15158  tanrpcl  15159  tangtx  15160  coskpi  15170  cosordlem  15171  cosq34lt1  15172  cos11  15175  reexplog  15193  relogexp  15194  logdivlti  15203  rpcxpef  15216  rpcncxpcl  15224  cxpap0  15226  rpcxpadd  15227  rpmulcxp  15231  cxpmul  15234  abscxp  15237  cxplt  15238  cxplt3  15242  logsqrt  15245  apcxp2  15261  rpabscxpbnd  15262  rplogbid1  15269  rplogb1  15270  rpelogb  15271  rplogbchbase  15272  rplogbreexp  15275  rprelogbmul  15277  rprelogbdiv  15279  rplogbcxp  15285  rpcxplogb  15286  logbgcd1irraplemexp  15290  logbgcd1irraplemap  15291  mersenne  15319  lgsvalmod  15346  lgsdilem  15354  lgsne0  15365  gausslemma2dlem1a  15385  gausslemma2dlem6  15394  lgseisenlem1  15397  lgseisenlem2  15398  lgseisen  15401  lgsquadlem1  15404  lgsquadlem2  15405  2sqlem1  15441  mul2sq  15443  2sqlem3  15444  2sqlem8  15450  qdencn  15762  refeq  15763  cvgcmp2nlemabs  15767  cvgcmp2n  15768  trilpolemisumle  15773  trilpolemeq1  15775  trilpolemlt1  15776  trirec0  15779  apdifflemf  15781  apdifflemr  15782  apdiff  15783  redc0  15792  reap0  15793  cndcap  15794  nconstwlpolem0  15798  nconstwlpolemgt0  15799  neap0mkv  15804  ltlenmkv  15805