Theorem recnd 7712

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

Syntax hints:   → wi 4   ∈ wcel 1461  ℂcc 7539  ℝcr 7540

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-resscn 7631

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-in 3041  df-ss 3048

This theorem is referenced by:  readdcan  7819  ltadd2  8094  ltadd1  8104  leadd2  8106  ltsubadd  8107  ltsubadd2  8108  lesubadd  8109  lesubadd2  8110  ltaddsub  8111  leaddsub  8113  lesub1  8131  lesub2  8132  ltsub1  8133  ltsub2  8134  ltnegcon1  8138  ltnegcon2  8139  add20  8149  subge0  8150  suble0  8151  lesub0  8154  eqord2  8159  possumd  8243  sublt0d  8244  rimul  8259  rereim  8260  apreap  8261  ltmul1a  8265  ltmul1  8266  reapmul1  8269  remulext2  8274  cru  8276  apreim  8277  mulreim  8278  apadd1  8282  apneg  8285  mulext1  8286  ltapd  8311  rerecclap  8397  redivclap  8398  recgt0  8512  prodgt0gt0  8513  prodgt0  8514  prodge0  8516  lemul1a  8520  ltdiv1  8530  ltmuldiv  8536  ledivmul  8539  lt2mul2div  8541  ltrec  8545  lt2msq  8548  ltdiv2  8549  ltrec1  8550  lerec2  8551  ledivdiv  8552  lediv2  8553  ltdiv23  8554  lediv23  8555  lediv12a  8556  recp1lt1  8561  recreclt  8562  ledivp1  8565  mulle0r  8606  negiso  8617  avglt1  8856  avglt2  8857  div4p1lem1div2  8871  nn0cnd  8930  zcn  8957  peano2z  8988  zaddcllemneg  8991  ztri3or  8995  zeo  9054  zcnd  9072  eluzelcn  9233  infrenegsupex  9285  supinfneg  9286  infsupneg  9287  supminfex  9288  cnref1o  9336  rpcn  9345  rpcnd  9378  ltaddrp2d  9411  xpncan  9541  icoshftf1o  9661  lincmb01cmp  9673  iccf1o  9674  qbtwnrelemcalc  9920  flhalf  9962  intfracq  9980  flqdiv  9981  modqid  10009  modqid0  10010  mulqaddmodid  10024  ser3le  10178  expcl2lemap  10192  expnegzap  10214  expaddzaplem  10223  expaddzap  10224  expmulzap  10226  ltexp2a  10232  leexp2a  10233  leexp2r  10234  exple1  10236  expubnd  10237  sq11  10252  bernneq2  10300  expnbnd  10302  nn0opthlem2d  10354  faclbnd  10374  bcp1nk  10395  remim  10519  reim0b  10521  rereb  10522  mulreap  10523  cjreb  10525  recj  10526  reneg  10527  readd  10528  resub  10529  remullem  10530  remul2  10532  redivap  10533  imcj  10534  imneg  10535  imadd  10536  imsub  10537  immul2  10539  imdivap  10540  cjcj  10542  cjadd  10543  ipcnval  10545  cjmulval  10547  cjneg  10549  imval2  10553  cjreim2  10563  cjap  10565  cnrecnv  10569  caucvgrelemrec  10637  cvg1nlemres  10643  recvguniqlem  10652  recvguniq  10653  resqrexlemover  10668  resqrexlemcalc1  10672  resqrexlemcalc2  10673  resqrexlemcalc3  10674  resqrexlemnmsq  10675  resqrexlemnm  10676  resqrexlemgt0  10678  resqrexlemoverl  10679  resqrexlemglsq  10680  remsqsqrt  10690  sqrtmul  10693  sqrtdiv  10700  sqrtmsq  10703  abs00ap  10720  absext  10721  abs00  10722  absdivap  10728  absid  10729  absexp  10737  absexpzap  10738  absimle  10742  abslt  10746  absle  10747  abssubap0  10748  abssubne0  10749  releabs  10754  recvalap  10755  abstri  10762  abs2difabs  10766  amgm2  10776  icodiamlt  10838  maxabsle  10862  maxabslemab  10864  maxabslemlub  10865  maxabslemval  10866  maxcl  10868  maxltsup  10876  max0addsup  10877  minmax  10887  minabs  10893  minclpr  10894  bdtrilem  10896  bdtri  10897  mul0inf  10898  climabs0  10962  reccn2ap  10968  climrecl  10979  climge0  10980  climle  10989  climsqz  10990  climsqz2  10991  climlec2  10996  climrecvg1n  11003  climcvg1nlem  11004  isumrecl  11084  isumge0  11085  fsumlessfi  11115  fsumge1  11116  fsum00  11117  fsumle  11118  fsumlt  11119  fsumabs  11120  iserabs  11130  isumrpcl  11149  isumle  11150  isumlessdc  11151  trireciplem  11155  trirecip  11156  expcnvre  11158  expcnv  11159  explecnv  11160  absltap  11164  geo2sum  11169  cvgratnnlembern  11178  cvgratnnlemnexp  11179  cvgratnnlemmn  11180  cvgratnnlemabsle  11182  cvgratnnlemsumlt  11183  cvgratnnlemfm  11184  cvgratnnlemrate  11185  cvgratz  11187  mertenslemi1  11190  mertenslem2  11191  efcllemp  11209  ege2le3  11222  efaddlem  11225  efgt0  11235  reeftlcl  11240  eftlub  11241  effsumlt  11243  efltim  11249  eflegeo  11253  resin4p  11270  recos4p  11271  efeul  11286  ef01bndlem  11308  sin01bnd  11309  cos01bnd  11310  sin01gt0  11313  cos01gt0  11314  sin02gt0  11315  absefi  11319  absef  11320  absefib  11321  efieq1re  11322  eirraplem  11325  dvdslelemd  11383  odd2np1  11412  divalglemnqt  11459  infssuzcldc  11486  nn0seqcvgd  11562  sqnprm  11656  metrtri  12360  bl2in  12386  blhalf  12391  blssps  12410  blss  12411  qdencn  12903  refeq  12904  cvgcmp2nlemabs  12908  cvgcmp2n  12909  trilpolemisumle  12912  trilpolemeq1  12914  trilpolemlt1  12915