Theorem recnd 8017

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

Syntax hints:   → wi 4   ∈ wcel 2160  ℂcc 7840  ℝcr 7841

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 2171  ax-resscn 7934

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  readdcan  8128  ltadd2  8407  ltadd1  8417  leadd2  8419  ltsubadd  8420  ltsubadd2  8421  lesubadd  8422  lesubadd2  8423  ltaddsub  8424  leaddsub  8426  lesub1  8444  lesub2  8445  ltsub1  8446  ltsub2  8447  ltnegcon1  8451  ltnegcon2  8452  add20  8462  subge0  8463  suble0  8464  lesub0  8467  eqord2  8472  possumd  8557  sublt0d  8558  rimul  8573  rereim  8574  apreap  8575  ltmul1a  8579  ltmul1  8580  reapmul1  8583  remulext2  8588  cru  8590  apreim  8591  mulreim  8592  apadd1  8596  apneg  8599  mulext1  8600  ltapd  8626  aprcl  8634  aptap  8638  rerecclap  8718  redivclap  8719  recgt0  8838  prodgt0gt0  8839  prodgt0  8840  prodge0  8842  lemul1a  8846  ltdiv1  8856  ltmuldiv  8862  ledivmul  8865  lt2mul2div  8867  ltrec  8871  lt2msq  8874  ltdiv2  8875  ltrec1  8876  lerec2  8877  ledivdiv  8878  lediv2  8879  ltdiv23  8880  lediv23  8881  lediv12a  8882  recp1lt1  8887  recreclt  8888  ledivp1  8891  mulle0r  8932  negiso  8943  avglt1  9188  avglt2  9189  div4p1lem1div2  9203  nn0cnd  9262  zcn  9289  peano2z  9320  zaddcllemneg  9323  ztri3or  9327  zeo  9389  zcnd  9407  eluzelcn  9570  infrenegsupex  9626  supinfneg  9627  infsupneg  9628  supminfex  9629  cnref1o  9682  rpcn  9694  rpcnd  9730  ltaddrp2d  9763  mul2lt0rlt0  9791  mul2lt0rgt0  9792  mul2lt0llt0  9793  mul2lt0lgt0  9794  mul2lt0np  9795  mul2lt0pn  9796  xpncan  9903  icoshftf1o  10023  lincmb01cmp  10035  iccf1o  10036  qbtwnrelemcalc  10288  flhalf  10335  intfracq  10353  flqdiv  10354  modqid  10382  modqid0  10383  mulqaddmodid  10397  ser3le  10552  expcl2lemap  10566  expnegzap  10588  expaddzaplem  10597  expaddzap  10598  expmulzap  10600  ltexp2a  10606  leexp2a  10607  leexp2r  10608  exple1  10610  expubnd  10611  sq11  10627  bernneq2  10676  expnbnd  10678  nn0ltexp2  10724  nn0opthlem2d  10736  faclbnd  10756  bcp1nk  10777  remim  10904  reim0b  10906  rereb  10907  mulreap  10908  cjreb  10910  recj  10911  reneg  10912  readd  10913  resub  10914  remullem  10915  remul2  10917  redivap  10918  imcj  10919  imneg  10920  imadd  10921  imsub  10922  immul2  10924  imdivap  10925  cjcj  10927  cjadd  10928  ipcnval  10930  cjmulval  10932  cjneg  10934  imval2  10938  cjreim2  10948  cjap  10950  cnrecnv  10954  caucvgrelemrec  11023  cvg1nlemres  11029  recvguniqlem  11038  recvguniq  11039  resqrexlemover  11054  resqrexlemcalc1  11058  resqrexlemcalc2  11059  resqrexlemcalc3  11060  resqrexlemnmsq  11061  resqrexlemnm  11062  resqrexlemgt0  11064  resqrexlemoverl  11065  resqrexlemglsq  11066  remsqsqrt  11076  sqrtmul  11079  sqrtdiv  11086  sqrtmsq  11089  abs00ap  11106  absext  11107  abs00  11108  absdivap  11114  absid  11115  absexp  11123  absexpzap  11124  absimle  11128  abslt  11132  absle  11133  abssubap0  11134  abssubne0  11135  releabs  11140  recvalap  11141  abstri  11148  abs2difabs  11152  amgm2  11162  icodiamlt  11224  maxabsle  11248  maxabslemab  11250  maxabslemlub  11251  maxabslemval  11252  maxcl  11254  maxltsup  11262  max0addsup  11263  minmax  11273  minabs  11279  minclpr  11280  bdtrilem  11282  bdtri  11283  mul0inf  11284  mingeb  11285  climabs0  11350  reccn2ap  11356  climrecl  11367  climge0  11368  climle  11377  climsqz  11378  climsqz2  11379  climlec2  11384  climrecvg1n  11391  climcvg1nlem  11392  isumrecl  11472  isumge0  11473  fsumlessfi  11503  fsumge1  11504  fsum00  11505  fsumle  11506  fsumlt  11507  fsumabs  11508  iserabs  11518  isumrpcl  11537  isumle  11538  isumlessdc  11539  trireciplem  11543  trirecip  11544  expcnvre  11546  expcnv  11547  explecnv  11548  absltap  11552  geo2sum  11557  cvgratnnlembern  11566  cvgratnnlemnexp  11567  cvgratnnlemmn  11568  cvgratnnlemabsle  11570  cvgratnnlemsumlt  11571  cvgratnnlemfm  11572  cvgratnnlemrate  11573  cvgratz  11575  mertenslemi1  11578  mertenslem2  11579  fprodabs  11659  fprodle  11683  efcllemp  11701  ege2le3  11714  efaddlem  11717  efgt0  11727  reeftlcl  11732  eftlub  11733  effsumlt  11735  efltim  11741  eflegeo  11744  resin4p  11761  recos4p  11762  efeul  11777  ef01bndlem  11799  sin01bnd  11800  cos01bnd  11801  sin01gt0  11804  cos01gt0  11805  sin02gt0  11806  cos12dec  11810  absefi  11811  absef  11812  absefib  11813  efieq1re  11814  eirraplem  11819  dvdsaddre2b  11883  dvdslelemd  11884  odd2np1  11913  divalglemnqt  11960  infssuzcldc  11987  nn0seqcvgd  12076  sqnprm  12171  isprm5lem  12176  odzdvds  12280  pythagtriplem14  12312  pcid  12359  fldivp1  12383  pockthlem  12391  4sqlem5  12417  4sqlem10  12422  mul4sqlem  12428  4sqlem15  12440  4sqlem16  12441  mulgneg  13097  ghmmulg  13212  rege0subm  13904  metrtri  14354  bl2in  14380  blhalf  14385  blssps  14404  blss  14405  dedekindeu  14578  dedekindicclemicc  14587  ivthinclemlopn  14591  ivthinclemuopn  14593  ivthinc  14598  ivthdec  14599  dvcjbr  14649  dvfre  14651  dveflem  14664  reeff1olem  14669  reeff1oleme  14670  eflt  14673  sin0pilem1  14679  sin0pilem2  14680  pilem3  14681  sincosq2sgn  14725  sincosq3sgn  14726  sincosq4sgn  14727  sinq12gt0  14728  sinq34lt0t  14729  cosq14gt0  14730  cosq23lt0  14731  coseq0q4123  14732  coseq0negpitopi  14734  tanrpcl  14735  tangtx  14736  coskpi  14746  cosordlem  14747  cosq34lt1  14748  cos11  14751  reexplog  14769  relogexp  14770  logdivlti  14779  rpcxpef  14792  rpcncxpcl  14800  cxpap0  14802  rpcxpadd  14803  rpmulcxp  14807  cxpmul  14810  abscxp  14812  cxplt  14813  cxplt3  14817  logsqrt  14820  apcxp2  14835  rpabscxpbnd  14836  rplogbid1  14842  rplogb1  14843  rpelogb  14844  rplogbchbase  14845  rplogbreexp  14848  rprelogbmul  14850  rprelogbdiv  14852  rplogbcxp  14858  rpcxplogb  14859  logbgcd1irraplemexp  14863  logbgcd1irraplemap  14864  lgsvalmod  14898  lgsdilem  14906  lgsne0  14917  lgseisenlem1  14928  lgseisenlem2  14929  2sqlem1  14939  mul2sq  14941  2sqlem3  14942  2sqlem8  14948  qdencn  15254  refeq  15255  cvgcmp2nlemabs  15259  cvgcmp2n  15260  trilpolemisumle  15265  trilpolemeq1  15267  trilpolemlt1  15268  trirec0  15271  apdifflemf  15273  apdifflemr  15274  apdiff  15275  redc0  15284  reap0  15285  cndcap  15286  nconstwlpolem0  15290  nconstwlpolemgt0  15291  neap0mkv  15296  ltlenmkv  15297