Theorem recnd 7927

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

Syntax hints:   → wi 4   ∈ wcel 2136  ℂcc 7751  ℝcr 7752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7845

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129

This theorem is referenced by:  readdcan  8038  ltadd2  8317  ltadd1  8327  leadd2  8329  ltsubadd  8330  ltsubadd2  8331  lesubadd  8332  lesubadd2  8333  ltaddsub  8334  leaddsub  8336  lesub1  8354  lesub2  8355  ltsub1  8356  ltsub2  8357  ltnegcon1  8361  ltnegcon2  8362  add20  8372  subge0  8373  suble0  8374  lesub0  8377  eqord2  8382  possumd  8467  sublt0d  8468  rimul  8483  rereim  8484  apreap  8485  ltmul1a  8489  ltmul1  8490  reapmul1  8493  remulext2  8498  cru  8500  apreim  8501  mulreim  8502  apadd1  8506  apneg  8509  mulext1  8510  ltapd  8536  aprcl  8544  rerecclap  8626  redivclap  8627  recgt0  8745  prodgt0gt0  8746  prodgt0  8747  prodge0  8749  lemul1a  8753  ltdiv1  8763  ltmuldiv  8769  ledivmul  8772  lt2mul2div  8774  ltrec  8778  lt2msq  8781  ltdiv2  8782  ltrec1  8783  lerec2  8784  ledivdiv  8785  lediv2  8786  ltdiv23  8787  lediv23  8788  lediv12a  8789  recp1lt1  8794  recreclt  8795  ledivp1  8798  mulle0r  8839  negiso  8850  avglt1  9095  avglt2  9096  div4p1lem1div2  9110  nn0cnd  9169  zcn  9196  peano2z  9227  zaddcllemneg  9230  ztri3or  9234  zeo  9296  zcnd  9314  eluzelcn  9477  infrenegsupex  9532  supinfneg  9533  infsupneg  9534  supminfex  9535  cnref1o  9588  rpcn  9598  rpcnd  9634  ltaddrp2d  9667  mul2lt0rlt0  9695  mul2lt0rgt0  9696  mul2lt0llt0  9697  mul2lt0lgt0  9698  mul2lt0np  9699  mul2lt0pn  9700  xpncan  9807  icoshftf1o  9927  lincmb01cmp  9939  iccf1o  9940  qbtwnrelemcalc  10191  flhalf  10237  intfracq  10255  flqdiv  10256  modqid  10284  modqid0  10285  mulqaddmodid  10299  ser3le  10453  expcl2lemap  10467  expnegzap  10489  expaddzaplem  10498  expaddzap  10499  expmulzap  10501  ltexp2a  10507  leexp2a  10508  leexp2r  10509  exple1  10511  expubnd  10512  sq11  10527  bernneq2  10576  expnbnd  10578  nn0ltexp2  10623  nn0opthlem2d  10634  faclbnd  10654  bcp1nk  10675  remim  10802  reim0b  10804  rereb  10805  mulreap  10806  cjreb  10808  recj  10809  reneg  10810  readd  10811  resub  10812  remullem  10813  remul2  10815  redivap  10816  imcj  10817  imneg  10818  imadd  10819  imsub  10820  immul2  10822  imdivap  10823  cjcj  10825  cjadd  10826  ipcnval  10828  cjmulval  10830  cjneg  10832  imval2  10836  cjreim2  10846  cjap  10848  cnrecnv  10852  caucvgrelemrec  10921  cvg1nlemres  10927  recvguniqlem  10936  recvguniq  10937  resqrexlemover  10952  resqrexlemcalc1  10956  resqrexlemcalc2  10957  resqrexlemcalc3  10958  resqrexlemnmsq  10959  resqrexlemnm  10960  resqrexlemgt0  10962  resqrexlemoverl  10963  resqrexlemglsq  10964  remsqsqrt  10974  sqrtmul  10977  sqrtdiv  10984  sqrtmsq  10987  abs00ap  11004  absext  11005  abs00  11006  absdivap  11012  absid  11013  absexp  11021  absexpzap  11022  absimle  11026  abslt  11030  absle  11031  abssubap0  11032  abssubne0  11033  releabs  11038  recvalap  11039  abstri  11046  abs2difabs  11050  amgm2  11060  icodiamlt  11122  maxabsle  11146  maxabslemab  11148  maxabslemlub  11149  maxabslemval  11150  maxcl  11152  maxltsup  11160  max0addsup  11161  minmax  11171  minabs  11177  minclpr  11178  bdtrilem  11180  bdtri  11181  mul0inf  11182  mingeb  11183  climabs0  11248  reccn2ap  11254  climrecl  11265  climge0  11266  climle  11275  climsqz  11276  climsqz2  11277  climlec2  11282  climrecvg1n  11289  climcvg1nlem  11290  isumrecl  11370  isumge0  11371  fsumlessfi  11401  fsumge1  11402  fsum00  11403  fsumle  11404  fsumlt  11405  fsumabs  11406  iserabs  11416  isumrpcl  11435  isumle  11436  isumlessdc  11437  trireciplem  11441  trirecip  11442  expcnvre  11444  expcnv  11445  explecnv  11446  absltap  11450  geo2sum  11455  cvgratnnlembern  11464  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratnnlemabsle  11468  cvgratnnlemsumlt  11469  cvgratnnlemfm  11470  cvgratnnlemrate  11471  cvgratz  11473  mertenslemi1  11476  mertenslem2  11477  fprodabs  11557  fprodle  11581  efcllemp  11599  ege2le3  11612  efaddlem  11615  efgt0  11625  reeftlcl  11630  eftlub  11631  effsumlt  11633  efltim  11639  eflegeo  11642  resin4p  11659  recos4p  11660  efeul  11675  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  sin01gt0  11702  cos01gt0  11703  sin02gt0  11704  cos12dec  11708  absefi  11709  absef  11710  absefib  11711  efieq1re  11712  eirraplem  11717  dvdslelemd  11781  odd2np1  11810  divalglemnqt  11857  infssuzcldc  11884  nn0seqcvgd  11973  sqnprm  12068  isprm5lem  12073  odzdvds  12177  pythagtriplem14  12209  pcid  12255  fldivp1  12278  pockthlem  12286  4sqlem5  12312  4sqlem10  12317  mul4sqlem  12323  metrtri  13027  bl2in  13053  blhalf  13058  blssps  13077  blss  13078  dedekindeu  13251  dedekindicclemicc  13260  ivthinclemlopn  13264  ivthinclemuopn  13266  ivthinc  13271  ivthdec  13272  dvcjbr  13322  dvfre  13324  dveflem  13337  reeff1olem  13342  reeff1oleme  13343  eflt  13346  sin0pilem1  13352  sin0pilem2  13353  pilem3  13354  sincosq2sgn  13398  sincosq3sgn  13399  sincosq4sgn  13400  sinq12gt0  13401  sinq34lt0t  13402  cosq14gt0  13403  cosq23lt0  13404  coseq0q4123  13405  coseq0negpitopi  13407  tanrpcl  13408  tangtx  13409  coskpi  13419  cosordlem  13420  cosq34lt1  13421  cos11  13424  reexplog  13442  relogexp  13443  logdivlti  13452  rpcxpef  13465  rpcncxpcl  13473  cxpap0  13475  rpcxpadd  13476  rpmulcxp  13480  cxpmul  13483  abscxp  13485  cxplt  13486  cxplt3  13490  logsqrt  13493  apcxp2  13508  rpabscxpbnd  13509  rplogbid1  13515  rplogb1  13516  rpelogb  13517  rplogbchbase  13518  rplogbreexp  13521  rprelogbmul  13523  rprelogbdiv  13525  rplogbcxp  13531  rpcxplogb  13532  logbgcd1irraplemexp  13536  logbgcd1irraplemap  13537  lgsvalmod  13570  lgsdilem  13578  lgsne0  13589  2sqlem1  13600  mul2sq  13602  2sqlem3  13603  2sqlem8  13609  qdencn  13916  refeq  13917  cvgcmp2nlemabs  13921  cvgcmp2n  13922  trilpolemisumle  13927  trilpolemeq1  13929  trilpolemlt1  13930  trirec0  13933  apdifflemf  13935  apdifflemr  13936  apdiff  13937  redc0  13946  reap0  13947  nconstwlpolem0  13951  nconstwlpolemgt0  13952