Theorem recnd 7453

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

Syntax hints:   → wi 4   ∈ wcel 1436  ℂcc 7285  ℝcr 7286

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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-resscn 7374

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001

This theorem is referenced by:  readdcan  7559  ltadd2  7834  ltadd1  7844  leadd2  7846  ltsubadd  7847  ltsubadd2  7848  lesubadd  7849  lesubadd2  7850  ltaddsub  7851  leaddsub  7853  lesub1  7871  lesub2  7872  ltsub1  7873  ltsub2  7874  ltnegcon1  7878  ltnegcon2  7879  add20  7889  subge0  7890  suble0  7891  lesub0  7894  possumd  7980  sublt0d  7981  rimul  7996  rereim  7997  apreap  7998  ltmul1a  8002  ltmul1  8003  reapmul1  8006  remulext2  8011  cru  8013  apreim  8014  mulreim  8015  apadd1  8019  apneg  8022  mulext1  8023  ltapd  8047  rerecclap  8129  redivclap  8130  recgt0  8239  prodgt0gt0  8240  prodgt0  8241  prodge0  8243  lemul1a  8247  ltdiv1  8257  ltmuldiv  8263  ledivmul  8266  lt2mul2div  8268  ltrec  8272  lt2msq  8275  ltdiv2  8276  ltrec1  8277  lerec2  8278  ledivdiv  8279  lediv2  8280  ltdiv23  8281  lediv23  8282  lediv12a  8283  recp1lt1  8288  recreclt  8289  ledivp1  8292  mulle0r  8333  negiso  8344  avglt1  8580  avglt2  8581  div4p1lem1div2  8595  nn0cnd  8654  zcn  8681  peano2z  8712  zaddcllemneg  8715  ztri3or  8719  zeo  8777  zcnd  8795  eluzelcn  8955  infrenegsupex  9007  supinfneg  9008  infsupneg  9009  supminfex  9010  cnref1o  9058  rpcn  9067  rpcnd  9100  ltaddrp2d  9133  icoshftf1o  9333  lincmb01cmp  9345  iccf1o  9346  qbtwnrelemcalc  9588  flhalf  9630  intfracq  9648  flqdiv  9649  modqid  9677  modqid0  9678  mulqaddmodid  9692  serile  9844  expcl2lemap  9858  expnegzap  9880  expaddzaplem  9889  expaddzap  9890  expmulzap  9892  ltexp2a  9898  leexp2a  9899  leexp2r  9900  exple1  9902  expubnd  9903  sq11  9918  bernneq2  9964  expnbnd  9966  nn0opthlem2d  10018  faclbnd  10038  bcp1nk  10059  remim  10182  reim0b  10184  rereb  10185  mulreap  10186  cjreb  10188  recj  10189  reneg  10190  readd  10191  resub  10192  remullem  10193  remul2  10195  redivap  10196  imcj  10197  imneg  10198  imadd  10199  imsub  10200  immul2  10202  imdivap  10203  cjcj  10205  cjadd  10206  ipcnval  10208  cjmulval  10210  cjneg  10212  imval2  10216  cjreim2  10226  cjap  10228  cnrecnv  10232  caucvgrelemrec  10300  cvg1nlemres  10306  recvguniqlem  10315  recvguniq  10316  resqrexlemover  10331  resqrexlemcalc1  10335  resqrexlemcalc2  10336  resqrexlemcalc3  10337  resqrexlemnmsq  10338  resqrexlemnm  10339  resqrexlemgt0  10341  resqrexlemoverl  10342  resqrexlemglsq  10343  remsqsqrt  10353  sqrtmul  10356  sqrtdiv  10363  sqrtmsq  10366  abs00ap  10383  absext  10384  abs00  10385  absdivap  10391  absid  10392  absexp  10400  absexpzap  10401  absimle  10405  abslt  10409  absle  10410  abssubap0  10411  abssubne0  10412  releabs  10417  recvalap  10418  abstri  10425  abs2difabs  10429  amgm2  10439  icodiamlt  10501  maxabsle  10525  maxabslemab  10527  maxabslemlub  10528  maxabslemval  10529  maxcl  10531  maxltsup  10539  max0addsup  10540  minmax  10547  climabs0  10581  climrecl  10597  climge0  10598  climle  10607  climsqz  10608  climsqz2  10609  climlec2  10614  climserile  10618  climrecvg1n  10620  climcvg1nlem  10621  dvdslelemd  10711  odd2np1  10740  divalglemnqt  10787  infssuzcldc  10814  nn0seqcvgd  10890  sqnprm  10984  qdencn  11345