Theorem recnd 8348

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℂcc 8171  ℝcr 8172

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 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 8265

This theorem 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 referenced by:  readdcan  8460  ltadd2  8741  ltadd1  8751  leadd2  8753  ltsubadd  8754  ltsubadd2  8755  lesubadd  8756  lesubadd2  8757  ltaddsub  8758  leaddsub  8760  lesub1  8778  lesub2  8779  ltsub1  8780  ltsub2  8781  ltnegcon1  8785  ltnegcon2  8786  add20  8796  subge0  8797  suble0  8798  lesub0  8801  eqord2  8806  possumd  8891  sublt0d  8892  rimul  8907  rereim  8908  apreap  8909  ltmul1a  8913  ltmul1  8914  reapmul1  8917  remulext2  8922  cru  8924  apreim  8925  mulreim  8926  apadd1  8930  apneg  8933  mulext1  8934  ltapd  8960  aprcl  8968  aptap  8972  rerecclap  9054  redivclap  9055  recgt0  9174  prodgt0gt0  9175  prodgt0  9176  prodge0  9178  lemul1a  9182  ltdiv1  9192  ltmuldiv  9198  ledivmul  9201  lt2mul2div  9203  ltrec  9207  lt2msq  9210  ltdiv2  9211  ltrec1  9212  lerec2  9213  ledivdiv  9214  lediv2  9215  ltdiv23  9216  lediv23  9217  lediv12a  9218  recp1lt1  9223  recreclt  9224  ledivp1  9227  mulle0r  9268  negiso  9279  avglt1  9527  avglt2  9528  div4p1lem1div2  9542  nn0cnd  9605  zcn  9632  peano2z  9663  zaddcllemneg  9666  ztri3or  9670  zeo  9734  zcnd  9752  eluzmn  9911  eluzelcn  9916  infrenegsupex  9977  supinfneg  9978  infsupneg  9979  supminfex  9980  irrmulap  10031  cnref1o  10034  rpcn  10046  rpcnd  10082  ltaddrp2d  10115  mul2lt0rlt0  10143  mul2lt0rgt0  10144  mul2lt0llt0  10145  mul2lt0lgt0  10146  mul2lt0np  10147  mul2lt0pn  10148  xpncan  10256  icoshftf1o  10376  lincmb01cmp  10388  lincmble  10389  iccf1o  10390  infssuzcldc  10651  qbtwnrelemcalc  10673  flhalf  10720  intfracq  10740  flqdiv  10741  modqid  10769  modqid0  10770  mulqaddmodid  10784  seqf1oglem1  10939  ser3le  10957  expcl2lemap  10971  expnegzap  10993  expaddzaplem  11002  expaddzap  11003  expmulzap  11005  ltexp2a  11011  leexp2a  11012  leexp2r  11013  exple1  11015  expubnd  11016  sq11  11032  resq01  11078  bernneq2  11082  expnbnd  11084  nn0ltexp2  11130  nn0opthlem2d  11142  faclbnd  11162  bcp1nk  11183  bcm1n  11190  remim  11608  reim0b  11610  rereb  11611  mulreap  11612  cjreb  11614  recj  11615  reneg  11616  readd  11617  resub  11618  remullem  11619  remul2  11621  redivap  11622  imcj  11623  imneg  11624  imadd  11625  imsub  11626  immul2  11628  imdivap  11629  cjcj  11631  cjadd  11632  ipcnval  11634  cjmulval  11636  cjneg  11638  imval2  11642  sq01  11643  cjreim2  11653  cjap  11655  cnrecnv  11659  caucvgrelemrec  11728  cvg1nlemres  11734  recvguniqlem  11743  recvguniq  11744  resqrexlemover  11759  resqrexlemcalc1  11763  resqrexlemcalc2  11764  resqrexlemcalc3  11765  resqrexlemnmsq  11766  resqrexlemnm  11767  resqrexlemgt0  11769  resqrexlemoverl  11770  resqrexlemglsq  11771  remsqsqrt  11781  sqrtmul  11784  sqrtdiv  11791  sqrtmsq  11794  abs00ap  11811  absext  11812  abs00  11813  absdivap  11819  absid  11820  absexp  11828  absexpzap  11829  absimle  11833  abslt  11837  absle  11838  abssubap0  11839  abssubne0  11840  releabs  11845  recvalap  11846  abstri  11853  abs2difabs  11857  amgm2  11867  icodiamlt  11929  maxabsle  11953  maxabslemab  11955  maxabslemlub  11956  maxabslemval  11957  maxcl  11959  maxltsup  11967  max0addsup  11968  minmax  11979  minabs  11985  minclpr  11986  bdtrilem  11988  bdtri  11989  mul0inf  11990  mingeb  11991  climabs0  12056  reccn2ap  12062  climrecl  12073  climge0  12074  climle  12083  climsqz  12084  climsqz2  12085  climlec2  12090  climrecvg1n  12097  climcvg1nlem  12098  isumrecl  12179  isumge0  12180  fsumlessfi  12210  fsumge1  12211  fsum00  12212  fsumle  12213  fsumlt  12214  fsumabs  12215  iserabs  12225  isumrpcl  12244  isumle  12245  isumlessdc  12246  trireciplem  12250  trirecip  12251  expcnvre  12253  expcnv  12254  explecnv  12255  absltap  12259  geo2sum  12264  cvgratnnlembern  12273  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  cvgratnnlemabsle  12277  cvgratnnlemsumlt  12278  cvgratnnlemfm  12279  cvgratnnlemrate  12280  cvgratz  12282  mertenslemi1  12285  mertenslem2  12286  fprodabs  12366  fprodle  12390  efcllemp  12408  ege2le3  12421  efaddlem  12424  efgt0  12434  reeftlcl  12439  eftlub  12440  effsumlt  12442  efltim  12448  eflegeo  12451  resin4p  12468  recos4p  12469  efeul  12484  ef01bndlem  12506  sin01bnd  12507  cos01bnd  12508  sin01gt0  12512  cos01gt0  12513  sin02gt0  12514  cos12dec  12518  absefi  12519  absef  12520  absefib  12521  efieq1re  12522  eirraplem  12527  dvdsaddre2b  12591  dvdslelemd  12593  odd2np1  12623  divalglemnqt  12670  bitsp1o  12703  bitsfzo  12705  bitscmp  12708  nn0seqcvgd  12802  sqnprm  12897  isprm5lem  12902  odzdvds  13007  pythagtriplem14  13039  pcid  13086  fldivp1  13110  pockthlem  13118  4sqlem5  13144  4sqlem10  13149  mul4sqlem  13155  4sqlem15  13167  4sqlem16  13168  ballotfilemsi  13241  mulgneg  13926  ghmmulg  14042  rege0subm  14904  metrtri  15461  bl2in  15487  blhalf  15492  blssps  15511  blss  15512  maxcncf  15699  mincncf  15700  dedekindeu  15707  dedekindicclemicc  15716  ivthinclemlopn  15720  ivthinclemuopn  15722  ivthinc  15727  ivthdec  15728  ivthreinc  15729  dvconstre  15780  dvidre  15781  dvcjbr  15792  dvfre  15794  dveflem  15810  plyrecj  15847  reeff1olem  15855  reeff1oleme  15856  eflt  15859  sin0pilem1  15865  sin0pilem2  15866  pilem3  15867  sincosq2sgn  15911  sincosq3sgn  15912  sincosq4sgn  15913  sinq12gt0  15914  sinq34lt0t  15915  cosq14gt0  15916  cosq23lt0  15917  coseq0q4123  15918  coseq0negpitopi  15920  tanrpcl  15921  tangtx  15922  coskpi  15932  cosordlem  15933  cosq34lt1  15934  cos11  15937  reexplog  15955  relogexp  15956  logdivlti  15965  logfac  15978  rpcxpef  15979  rpcncxpcl  15987  cxpap0  15989  rpcxpadd  15990  rpmulcxp  15994  cxpmul  15997  abscxp  16000  cxplt  16001  cxplt3  16005  logsqrt  16008  apcxp2  16024  rpabscxpbnd  16025  rplogbid1  16032  rplogb1  16033  rpelogb  16034  rplogbchbase  16035  rplogbreexp  16038  rprelogbmul  16040  rprelogbdiv  16042  rplogbcxp  16048  rpcxplogb  16049  logbgcd1irraplemexp  16053  logbgcd1irraplemap  16054  log2tlbndlog2  16065  log2ublem2  16067  birthdaylem2  16071  birthdaylem3  16072  pellexlem2  16075  mersenne  16094  lgsvalmod  16121  lgsdilem  16129  lgsne0  16140  gausslemma2dlem1a  16160  gausslemma2dlem6  16169  lgseisenlem1  16172  lgseisenlem2  16173  lgseisen  16176  lgsquadlem1  16179  lgsquadlem2  16180  2sqlem1  16216  mul2sq  16218  2sqlem3  16219  2sqlem8  16225  dichmul0orlem1  16736  dichmul0orlem4  16739  dichmul0orlem5  16740  dichmul0orlem6  16741  dichmul0orlem7  16742  qdencn  17046  refeq  17047  repiecele0  17049  repiecege0  17050  cvgcmp2nlemabs  17055  cvgcmp2n  17056  trilpolemisumle  17061  trilpolemeq1  17063  trilpolemlt1  17064  trirec0  17067  apdifflemf  17069  apdifflemr  17070  apdiff  17071  qdiff  17072  redc0  17081  reap0  17082  cndcap  17083  nconstwlpolem0  17087  nconstwlpolemgt0  17088  neap0mkv  17093  ltlenmkv  17094