Theorem recnd 7147

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

Syntax hints:   → wi 4   ∈ wcel 1433  ℂcc 6979  ℝcr 6980

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-resscn 7068

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986

This theorem is referenced by:  readdcan  7248  ltadd2  7523  ltadd1  7533  leadd2  7535  ltsubadd  7536  ltsubadd2  7537  lesubadd  7538  lesubadd2  7539  ltaddsub  7540  leaddsub  7542  lesub1  7560  lesub2  7561  ltsub1  7562  ltsub2  7563  ltnegcon1  7567  ltnegcon2  7568  add20  7578  subge0  7579  suble0  7580  lesub0  7583  possumd  7669  sublt0d  7670  rimul  7685  rereim  7686  apreap  7687  ltmul1a  7691  ltmul1  7692  reapmul1  7695  remulext2  7700  cru  7702  apreim  7703  mulreim  7704  apadd1  7708  apneg  7711  mulext1  7712  ltapd  7736  rerecclap  7818  redivclap  7819  recgt0  7928  prodgt0gt0  7929  prodgt0  7930  prodge0  7932  lemul1a  7936  ltdiv1  7946  ltmuldiv  7952  ledivmul  7955  lt2mul2div  7957  ltrec  7961  lt2msq  7964  ltdiv2  7965  ltrec1  7966  lerec2  7967  ledivdiv  7968  lediv2  7969  ltdiv23  7970  lediv23  7971  lediv12a  7972  recp1lt1  7977  recreclt  7978  ledivp1  7981  mulle0r  8022  negiso  8033  avglt1  8269  avglt2  8270  div4p1lem1div2  8284  nn0cnd  8343  zcn  8356  peano2z  8387  zaddcllemneg  8390  ztri3or  8394  zeo  8452  zcnd  8470  eluzelcn  8630  infrenegsupex  8682  supinfneg  8683  infsupneg  8684  supminfex  8685  cnref1o  8733  rpcn  8742  rpcnd  8775  ltaddrp2d  8808  icoshftf1o  9013  lincmb01cmp  9025  iccf1o  9026  qbtwnrelemcalc  9264  flhalf  9304  intfracq  9322  flqdiv  9323  modqid  9351  modqid0  9352  mulqaddmodid  9366  serile  9474  expcl2lemap  9488  expnegzap  9510  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  ltexp2a  9528  leexp2a  9529  leexp2r  9530  exple1  9532  expubnd  9533  sq11  9548  bernneq2  9594  expnbnd  9596  nn0opthlem2d  9648  faclbnd  9668  bcp1nk  9689  remim  9747  reim0b  9749  rereb  9750  mulreap  9751  cjreb  9753  recj  9754  reneg  9755  readd  9756  resub  9757  remullem  9758  remul2  9760  redivap  9761  imcj  9762  imneg  9763  imadd  9764  imsub  9765  immul2  9767  imdivap  9768  cjcj  9770  cjadd  9771  ipcnval  9773  cjmulval  9775  cjneg  9777  imval2  9781  cjreim2  9791  cjap  9793  cnrecnv  9797  caucvgrelemrec  9865  cvg1nlemres  9871  recvguniqlem  9880  recvguniq  9881  resqrexlemover  9896  resqrexlemcalc1  9900  resqrexlemcalc2  9901  resqrexlemcalc3  9902  resqrexlemnmsq  9903  resqrexlemnm  9904  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  remsqsqrt  9918  sqrtmul  9921  sqrtdiv  9928  sqrtmsq  9931  abs00ap  9948  absext  9949  abs00  9950  absdivap  9956  absid  9957  absexp  9965  absexpzap  9966  absimle  9970  abslt  9974  absle  9975  abssubap0  9976  abssubne0  9977  releabs  9982  recvalap  9983  abstri  9990  abs2difabs  9994  amgm2  10004  icodiamlt  10066  maxabsle  10090  maxabslemab  10092  maxabslemlub  10093  maxabslemval  10094  maxcl  10096  maxltsup  10104  max0addsup  10105  minmax  10112  climabs0  10146  climrecl  10162  climge0  10163  climle  10172  climsqz  10173  climsqz2  10174  climlec2  10179  climserile  10183  climrecvg1n  10185  climcvg1nlem  10186  dvdslelemd  10243  odd2np1  10272  divalglemnqt  10320  infssuzcldc  10347  nn0seqcvgd  10423  sqnprm  10517  qdencn  10785