Theorem recnd 8050

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7872  ℝcr 7873

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7966

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  readdcan  8161  ltadd2  8440  ltadd1  8450  leadd2  8452  ltsubadd  8453  ltsubadd2  8454  lesubadd  8455  lesubadd2  8456  ltaddsub  8457  leaddsub  8459  lesub1  8477  lesub2  8478  ltsub1  8479  ltsub2  8480  ltnegcon1  8484  ltnegcon2  8485  add20  8495  subge0  8496  suble0  8497  lesub0  8500  eqord2  8505  possumd  8590  sublt0d  8591  rimul  8606  rereim  8607  apreap  8608  ltmul1a  8612  ltmul1  8613  reapmul1  8616  remulext2  8621  cru  8623  apreim  8624  mulreim  8625  apadd1  8629  apneg  8632  mulext1  8633  ltapd  8659  aprcl  8667  aptap  8671  rerecclap  8751  redivclap  8752  recgt0  8871  prodgt0gt0  8872  prodgt0  8873  prodge0  8875  lemul1a  8879  ltdiv1  8889  ltmuldiv  8895  ledivmul  8898  lt2mul2div  8900  ltrec  8904  lt2msq  8907  ltdiv2  8908  ltrec1  8909  lerec2  8910  ledivdiv  8911  lediv2  8912  ltdiv23  8913  lediv23  8914  lediv12a  8915  recp1lt1  8920  recreclt  8921  ledivp1  8924  mulle0r  8965  negiso  8976  avglt1  9224  avglt2  9225  div4p1lem1div2  9239  nn0cnd  9298  zcn  9325  peano2z  9356  zaddcllemneg  9359  ztri3or  9363  zeo  9425  zcnd  9443  eluzelcn  9606  infrenegsupex  9662  supinfneg  9663  infsupneg  9664  supminfex  9665  irrmulap  9716  cnref1o  9719  rpcn  9731  rpcnd  9767  ltaddrp2d  9800  mul2lt0rlt0  9828  mul2lt0rgt0  9829  mul2lt0llt0  9830  mul2lt0lgt0  9831  mul2lt0np  9832  mul2lt0pn  9833  xpncan  9940  icoshftf1o  10060  lincmb01cmp  10072  iccf1o  10073  qbtwnrelemcalc  10327  flhalf  10374  intfracq  10394  flqdiv  10395  modqid  10423  modqid0  10424  mulqaddmodid  10438  seqf1oglem1  10593  ser3le  10611  expcl2lemap  10625  expnegzap  10647  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  ltexp2a  10665  leexp2a  10666  leexp2r  10667  exple1  10669  expubnd  10670  sq11  10686  bernneq2  10735  expnbnd  10737  nn0ltexp2  10783  nn0opthlem2d  10795  faclbnd  10815  bcp1nk  10836  remim  11007  reim0b  11009  rereb  11010  mulreap  11011  cjreb  11013  recj  11014  reneg  11015  readd  11016  resub  11017  remullem  11018  remul2  11020  redivap  11021  imcj  11022  imneg  11023  imadd  11024  imsub  11025  immul2  11027  imdivap  11028  cjcj  11030  cjadd  11031  ipcnval  11033  cjmulval  11035  cjneg  11037  imval2  11041  cjreim2  11051  cjap  11053  cnrecnv  11057  caucvgrelemrec  11126  cvg1nlemres  11132  recvguniqlem  11141  recvguniq  11142  resqrexlemover  11157  resqrexlemcalc1  11161  resqrexlemcalc2  11162  resqrexlemcalc3  11163  resqrexlemnmsq  11164  resqrexlemnm  11165  resqrexlemgt0  11167  resqrexlemoverl  11168  resqrexlemglsq  11169  remsqsqrt  11179  sqrtmul  11182  sqrtdiv  11189  sqrtmsq  11192  abs00ap  11209  absext  11210  abs00  11211  absdivap  11217  absid  11218  absexp  11226  absexpzap  11227  absimle  11231  abslt  11235  absle  11236  abssubap0  11237  abssubne0  11238  releabs  11243  recvalap  11244  abstri  11251  abs2difabs  11255  amgm2  11265  icodiamlt  11327  maxabsle  11351  maxabslemab  11353  maxabslemlub  11354  maxabslemval  11355  maxcl  11357  maxltsup  11365  max0addsup  11366  minmax  11376  minabs  11382  minclpr  11383  bdtrilem  11385  bdtri  11386  mul0inf  11387  mingeb  11388  climabs0  11453  reccn2ap  11459  climrecl  11470  climge0  11471  climle  11480  climsqz  11481  climsqz2  11482  climlec2  11487  climrecvg1n  11494  climcvg1nlem  11495  isumrecl  11575  isumge0  11576  fsumlessfi  11606  fsumge1  11607  fsum00  11608  fsumle  11609  fsumlt  11610  fsumabs  11611  iserabs  11621  isumrpcl  11640  isumle  11641  isumlessdc  11642  trireciplem  11646  trirecip  11647  expcnvre  11649  expcnv  11650  explecnv  11651  absltap  11655  geo2sum  11660  cvgratnnlembern  11669  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratnnlemabsle  11673  cvgratnnlemsumlt  11674  cvgratnnlemfm  11675  cvgratnnlemrate  11676  cvgratz  11678  mertenslemi1  11681  mertenslem2  11682  fprodabs  11762  fprodle  11786  efcllemp  11804  ege2le3  11817  efaddlem  11820  efgt0  11830  reeftlcl  11835  eftlub  11836  effsumlt  11838  efltim  11844  eflegeo  11847  resin4p  11864  recos4p  11865  efeul  11880  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  sin01gt0  11908  cos01gt0  11909  sin02gt0  11910  cos12dec  11914  absefi  11915  absef  11916  absefib  11917  efieq1re  11918  eirraplem  11923  dvdsaddre2b  11987  dvdslelemd  11988  odd2np1  12017  divalglemnqt  12064  infssuzcldc  12091  nn0seqcvgd  12182  sqnprm  12277  isprm5lem  12282  odzdvds  12386  pythagtriplem14  12418  pcid  12465  fldivp1  12489  pockthlem  12497  4sqlem5  12523  4sqlem10  12528  mul4sqlem  12534  4sqlem15  12546  4sqlem16  12547  mulgneg  13213  ghmmulg  13329  rege0subm  14083  metrtri  14556  bl2in  14582  blhalf  14587  blssps  14606  blss  14607  maxcncf  14794  mincncf  14795  dedekindeu  14802  dedekindicclemicc  14811  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthinc  14822  ivthdec  14823  ivthreinc  14824  dvconstre  14875  dvidre  14876  dvcjbr  14887  dvfre  14889  dveflem  14905  plyrecj  14941  reeff1olem  14947  reeff1oleme  14948  eflt  14951  sin0pilem1  14957  sin0pilem2  14958  pilem3  14959  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  sinq34lt0t  15007  cosq14gt0  15008  cosq23lt0  15009  coseq0q4123  15010  coseq0negpitopi  15012  tanrpcl  15013  tangtx  15014  coskpi  15024  cosordlem  15025  cosq34lt1  15026  cos11  15029  reexplog  15047  relogexp  15048  logdivlti  15057  rpcxpef  15070  rpcncxpcl  15078  cxpap0  15080  rpcxpadd  15081  rpmulcxp  15085  cxpmul  15088  abscxp  15090  cxplt  15091  cxplt3  15095  logsqrt  15098  apcxp2  15113  rpabscxpbnd  15114  rplogbid1  15120  rplogb1  15121  rpelogb  15122  rplogbchbase  15123  rplogbreexp  15126  rprelogbmul  15128  rprelogbdiv  15130  rplogbcxp  15136  rpcxplogb  15137  logbgcd1irraplemexp  15141  logbgcd1irraplemap  15142  lgsvalmod  15176  lgsdilem  15184  lgsne0  15195  gausslemma2dlem1a  15215  gausslemma2dlem6  15224  lgseisenlem1  15227  lgseisenlem2  15228  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  2sqlem1  15271  mul2sq  15273  2sqlem3  15274  2sqlem8  15280  qdencn  15587  refeq  15588  cvgcmp2nlemabs  15592  cvgcmp2n  15593  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  trirec0  15604  apdifflemf  15606  apdifflemr  15607  apdiff  15608  redc0  15617  reap0  15618  cndcap  15619  nconstwlpolem0  15623  nconstwlpolemgt0  15624  neap0mkv  15629  ltlenmkv  15630