Theorem recnd 8298

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8121  ℝcr 8122

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-resscn 8215

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  readdcan  8409  ltadd2  8689  ltadd1  8699  leadd2  8701  ltsubadd  8702  ltsubadd2  8703  lesubadd  8704  lesubadd2  8705  ltaddsub  8706  leaddsub  8708  lesub1  8726  lesub2  8727  ltsub1  8728  ltsub2  8729  ltnegcon1  8733  ltnegcon2  8734  add20  8744  subge0  8745  suble0  8746  lesub0  8749  eqord2  8754  possumd  8839  sublt0d  8840  rimul  8855  rereim  8856  apreap  8857  ltmul1a  8861  ltmul1  8862  reapmul1  8865  remulext2  8870  cru  8872  apreim  8873  mulreim  8874  apadd1  8878  apneg  8881  mulext1  8882  ltapd  8908  aprcl  8916  aptap  8920  rerecclap  9000  redivclap  9001  recgt0  9120  prodgt0gt0  9121  prodgt0  9122  prodge0  9124  lemul1a  9128  ltdiv1  9138  ltmuldiv  9144  ledivmul  9147  lt2mul2div  9149  ltrec  9153  lt2msq  9156  ltdiv2  9157  ltrec1  9158  lerec2  9159  ledivdiv  9160  lediv2  9161  ltdiv23  9162  lediv23  9163  lediv12a  9164  recp1lt1  9169  recreclt  9170  ledivp1  9173  mulle0r  9214  negiso  9225  avglt1  9473  avglt2  9474  div4p1lem1div2  9488  nn0cnd  9551  zcn  9578  peano2z  9609  zaddcllemneg  9612  ztri3or  9616  zeo  9679  zcnd  9697  eluzmn  9856  eluzelcn  9861  infrenegsupex  9922  supinfneg  9923  infsupneg  9924  supminfex  9925  irrmulap  9976  cnref1o  9979  rpcn  9991  rpcnd  10027  ltaddrp2d  10060  mul2lt0rlt0  10088  mul2lt0rgt0  10089  mul2lt0llt0  10090  mul2lt0lgt0  10091  mul2lt0np  10092  mul2lt0pn  10093  xpncan  10200  icoshftf1o  10320  lincmb01cmp  10332  lincmble  10333  iccf1o  10334  infssuzcldc  10591  qbtwnrelemcalc  10611  flhalf  10658  intfracq  10678  flqdiv  10679  modqid  10707  modqid0  10708  mulqaddmodid  10722  seqf1oglem1  10877  ser3le  10895  expcl2lemap  10909  expnegzap  10931  expaddzaplem  10940  expaddzap  10941  expmulzap  10943  ltexp2a  10949  leexp2a  10950  leexp2r  10951  exple1  10953  expubnd  10954  sq11  10970  bernneq2  11019  expnbnd  11021  nn0ltexp2  11067  nn0opthlem2d  11079  faclbnd  11099  bcp1nk  11120  remim  11538  reim0b  11540  rereb  11541  mulreap  11542  cjreb  11544  recj  11545  reneg  11546  readd  11547  resub  11548  remullem  11549  remul2  11551  redivap  11552  imcj  11553  imneg  11554  imadd  11555  imsub  11556  immul2  11558  imdivap  11559  cjcj  11561  cjadd  11562  ipcnval  11564  cjmulval  11566  cjneg  11568  imval2  11572  cjreim2  11582  cjap  11584  cnrecnv  11588  caucvgrelemrec  11657  cvg1nlemres  11663  recvguniqlem  11672  recvguniq  11673  resqrexlemover  11688  resqrexlemcalc1  11692  resqrexlemcalc2  11693  resqrexlemcalc3  11694  resqrexlemnmsq  11695  resqrexlemnm  11696  resqrexlemgt0  11698  resqrexlemoverl  11699  resqrexlemglsq  11700  remsqsqrt  11710  sqrtmul  11713  sqrtdiv  11720  sqrtmsq  11723  abs00ap  11740  absext  11741  abs00  11742  absdivap  11748  absid  11749  absexp  11757  absexpzap  11758  absimle  11762  abslt  11766  absle  11767  abssubap0  11768  abssubne0  11769  releabs  11774  recvalap  11775  abstri  11782  abs2difabs  11786  amgm2  11796  icodiamlt  11858  maxabsle  11882  maxabslemab  11884  maxabslemlub  11885  maxabslemval  11886  maxcl  11888  maxltsup  11896  max0addsup  11897  minmax  11908  minabs  11914  minclpr  11915  bdtrilem  11917  bdtri  11918  mul0inf  11919  mingeb  11920  climabs0  11985  reccn2ap  11991  climrecl  12002  climge0  12003  climle  12012  climsqz  12013  climsqz2  12014  climlec2  12019  climrecvg1n  12026  climcvg1nlem  12027  isumrecl  12108  isumge0  12109  fsumlessfi  12139  fsumge1  12140  fsum00  12141  fsumle  12142  fsumlt  12143  fsumabs  12144  iserabs  12154  isumrpcl  12173  isumle  12174  isumlessdc  12175  trireciplem  12179  trirecip  12180  expcnvre  12182  expcnv  12183  explecnv  12184  absltap  12188  geo2sum  12193  cvgratnnlembern  12202  cvgratnnlemnexp  12203  cvgratnnlemmn  12204  cvgratnnlemabsle  12206  cvgratnnlemsumlt  12207  cvgratnnlemfm  12208  cvgratnnlemrate  12209  cvgratz  12211  mertenslemi1  12214  mertenslem2  12215  fprodabs  12295  fprodle  12319  efcllemp  12337  ege2le3  12350  efaddlem  12353  efgt0  12363  reeftlcl  12368  eftlub  12369  effsumlt  12371  efltim  12377  eflegeo  12380  resin4p  12397  recos4p  12398  efeul  12413  ef01bndlem  12435  sin01bnd  12436  cos01bnd  12437  sin01gt0  12441  cos01gt0  12442  sin02gt0  12443  cos12dec  12447  absefi  12448  absef  12449  absefib  12450  efieq1re  12451  eirraplem  12456  dvdsaddre2b  12520  dvdslelemd  12522  odd2np1  12552  divalglemnqt  12599  bitsp1o  12632  bitsfzo  12634  bitscmp  12637  nn0seqcvgd  12731  sqnprm  12826  isprm5lem  12831  odzdvds  12936  pythagtriplem14  12968  pcid  13015  fldivp1  13039  pockthlem  13047  4sqlem5  13073  4sqlem10  13078  mul4sqlem  13084  4sqlem15  13096  4sqlem16  13097  mulgneg  13846  ghmmulg  13962  rege0subm  14719  metrtri  15229  bl2in  15255  blhalf  15260  blssps  15279  blss  15280  maxcncf  15467  mincncf  15468  dedekindeu  15475  dedekindicclemicc  15484  ivthinclemlopn  15488  ivthinclemuopn  15490  ivthinc  15495  ivthdec  15496  ivthreinc  15497  dvconstre  15548  dvidre  15549  dvcjbr  15560  dvfre  15562  dveflem  15578  plyrecj  15615  reeff1olem  15623  reeff1oleme  15624  eflt  15627  sin0pilem1  15633  sin0pilem2  15634  pilem3  15635  sincosq2sgn  15679  sincosq3sgn  15680  sincosq4sgn  15681  sinq12gt0  15682  sinq34lt0t  15683  cosq14gt0  15684  cosq23lt0  15685  coseq0q4123  15686  coseq0negpitopi  15688  tanrpcl  15689  tangtx  15690  coskpi  15700  cosordlem  15701  cosq34lt1  15702  cos11  15705  reexplog  15723  relogexp  15724  logdivlti  15733  rpcxpef  15746  rpcncxpcl  15754  cxpap0  15756  rpcxpadd  15757  rpmulcxp  15761  cxpmul  15764  abscxp  15767  cxplt  15768  cxplt3  15772  logsqrt  15775  apcxp2  15791  rpabscxpbnd  15792  rplogbid1  15799  rplogb1  15800  rpelogb  15801  rplogbchbase  15802  rplogbreexp  15805  rprelogbmul  15807  rprelogbdiv  15809  rplogbcxp  15815  rpcxplogb  15816  logbgcd1irraplemexp  15820  logbgcd1irraplemap  15821  pellexlem2  15833  mersenne  15852  lgsvalmod  15879  lgsdilem  15887  lgsne0  15898  gausslemma2dlem1a  15918  gausslemma2dlem6  15927  lgseisenlem1  15930  lgseisenlem2  15931  lgseisen  15934  lgsquadlem1  15937  lgsquadlem2  15938  2sqlem1  15974  mul2sq  15976  2sqlem3  15977  2sqlem8  15983  qdencn  16794  refeq  16795  repiecele0  16797  repiecege0  16798  cvgcmp2nlemabs  16803  cvgcmp2n  16804  trilpolemisumle  16809  trilpolemeq1  16811  trilpolemlt1  16812  trirec0  16815  apdifflemf  16817  apdifflemr  16818  apdiff  16819  qdiff  16820  redc0  16829  reap0  16830  cndcap  16831  nconstwlpolem0  16835  nconstwlpolemgt0  16836  neap0mkv  16841  ltlenmkv  16842