Theorem recnd 7985

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7808  ℝcr 7809

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7902

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  readdcan  8096  ltadd2  8375  ltadd1  8385  leadd2  8387  ltsubadd  8388  ltsubadd2  8389  lesubadd  8390  lesubadd2  8391  ltaddsub  8392  leaddsub  8394  lesub1  8412  lesub2  8413  ltsub1  8414  ltsub2  8415  ltnegcon1  8419  ltnegcon2  8420  add20  8430  subge0  8431  suble0  8432  lesub0  8435  eqord2  8440  possumd  8525  sublt0d  8526  rimul  8541  rereim  8542  apreap  8543  ltmul1a  8547  ltmul1  8548  reapmul1  8551  remulext2  8556  cru  8558  apreim  8559  mulreim  8560  apadd1  8564  apneg  8567  mulext1  8568  ltapd  8594  aprcl  8602  aptap  8606  rerecclap  8686  redivclap  8687  recgt0  8806  prodgt0gt0  8807  prodgt0  8808  prodge0  8810  lemul1a  8814  ltdiv1  8824  ltmuldiv  8830  ledivmul  8833  lt2mul2div  8835  ltrec  8839  lt2msq  8842  ltdiv2  8843  ltrec1  8844  lerec2  8845  ledivdiv  8846  lediv2  8847  ltdiv23  8848  lediv23  8849  lediv12a  8850  recp1lt1  8855  recreclt  8856  ledivp1  8859  mulle0r  8900  negiso  8911  avglt1  9156  avglt2  9157  div4p1lem1div2  9171  nn0cnd  9230  zcn  9257  peano2z  9288  zaddcllemneg  9291  ztri3or  9295  zeo  9357  zcnd  9375  eluzelcn  9538  infrenegsupex  9593  supinfneg  9594  infsupneg  9595  supminfex  9596  cnref1o  9649  rpcn  9661  rpcnd  9697  ltaddrp2d  9730  mul2lt0rlt0  9758  mul2lt0rgt0  9759  mul2lt0llt0  9760  mul2lt0lgt0  9761  mul2lt0np  9762  mul2lt0pn  9763  xpncan  9870  icoshftf1o  9990  lincmb01cmp  10002  iccf1o  10003  qbtwnrelemcalc  10255  flhalf  10301  intfracq  10319  flqdiv  10320  modqid  10348  modqid0  10349  mulqaddmodid  10363  ser3le  10517  expcl2lemap  10531  expnegzap  10553  expaddzaplem  10562  expaddzap  10563  expmulzap  10565  ltexp2a  10571  leexp2a  10572  leexp2r  10573  exple1  10575  expubnd  10576  sq11  10592  bernneq2  10641  expnbnd  10643  nn0ltexp2  10688  nn0opthlem2d  10700  faclbnd  10720  bcp1nk  10741  remim  10868  reim0b  10870  rereb  10871  mulreap  10872  cjreb  10874  recj  10875  reneg  10876  readd  10877  resub  10878  remullem  10879  remul2  10881  redivap  10882  imcj  10883  imneg  10884  imadd  10885  imsub  10886  immul2  10888  imdivap  10889  cjcj  10891  cjadd  10892  ipcnval  10894  cjmulval  10896  cjneg  10898  imval2  10902  cjreim2  10912  cjap  10914  cnrecnv  10918  caucvgrelemrec  10987  cvg1nlemres  10993  recvguniqlem  11002  recvguniq  11003  resqrexlemover  11018  resqrexlemcalc1  11022  resqrexlemcalc2  11023  resqrexlemcalc3  11024  resqrexlemnmsq  11025  resqrexlemnm  11026  resqrexlemgt0  11028  resqrexlemoverl  11029  resqrexlemglsq  11030  remsqsqrt  11040  sqrtmul  11043  sqrtdiv  11050  sqrtmsq  11053  abs00ap  11070  absext  11071  abs00  11072  absdivap  11078  absid  11079  absexp  11087  absexpzap  11088  absimle  11092  abslt  11096  absle  11097  abssubap0  11098  abssubne0  11099  releabs  11104  recvalap  11105  abstri  11112  abs2difabs  11116  amgm2  11126  icodiamlt  11188  maxabsle  11212  maxabslemab  11214  maxabslemlub  11215  maxabslemval  11216  maxcl  11218  maxltsup  11226  max0addsup  11227  minmax  11237  minabs  11243  minclpr  11244  bdtrilem  11246  bdtri  11247  mul0inf  11248  mingeb  11249  climabs0  11314  reccn2ap  11320  climrecl  11331  climge0  11332  climle  11341  climsqz  11342  climsqz2  11343  climlec2  11348  climrecvg1n  11355  climcvg1nlem  11356  isumrecl  11436  isumge0  11437  fsumlessfi  11467  fsumge1  11468  fsum00  11469  fsumle  11470  fsumlt  11471  fsumabs  11472  iserabs  11482  isumrpcl  11501  isumle  11502  isumlessdc  11503  trireciplem  11507  trirecip  11508  expcnvre  11510  expcnv  11511  explecnv  11512  absltap  11516  geo2sum  11521  cvgratnnlembern  11530  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratnnlemabsle  11534  cvgratnnlemsumlt  11535  cvgratnnlemfm  11536  cvgratnnlemrate  11537  cvgratz  11539  mertenslemi1  11542  mertenslem2  11543  fprodabs  11623  fprodle  11647  efcllemp  11665  ege2le3  11678  efaddlem  11681  efgt0  11691  reeftlcl  11696  eftlub  11697  effsumlt  11699  efltim  11705  eflegeo  11708  resin4p  11725  recos4p  11726  efeul  11741  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  sin01gt0  11768  cos01gt0  11769  sin02gt0  11770  cos12dec  11774  absefi  11775  absef  11776  absefib  11777  efieq1re  11778  eirraplem  11783  dvdsaddre2b  11847  dvdslelemd  11848  odd2np1  11877  divalglemnqt  11924  infssuzcldc  11951  nn0seqcvgd  12040  sqnprm  12135  isprm5lem  12140  odzdvds  12244  pythagtriplem14  12276  pcid  12322  fldivp1  12345  pockthlem  12353  4sqlem5  12379  4sqlem10  12384  mul4sqlem  12390  mulgneg  13000  rege0subm  13448  metrtri  13847  bl2in  13873  blhalf  13878  blssps  13897  blss  13898  dedekindeu  14071  dedekindicclemicc  14080  ivthinclemlopn  14084  ivthinclemuopn  14086  ivthinc  14091  ivthdec  14092  dvcjbr  14142  dvfre  14144  dveflem  14157  reeff1olem  14162  reeff1oleme  14163  eflt  14166  sin0pilem1  14172  sin0pilem2  14173  pilem3  14174  sincosq2sgn  14218  sincosq3sgn  14219  sincosq4sgn  14220  sinq12gt0  14221  sinq34lt0t  14222  cosq14gt0  14223  cosq23lt0  14224  coseq0q4123  14225  coseq0negpitopi  14227  tanrpcl  14228  tangtx  14229  coskpi  14239  cosordlem  14240  cosq34lt1  14241  cos11  14244  reexplog  14262  relogexp  14263  logdivlti  14272  rpcxpef  14285  rpcncxpcl  14293  cxpap0  14295  rpcxpadd  14296  rpmulcxp  14300  cxpmul  14303  abscxp  14305  cxplt  14306  cxplt3  14310  logsqrt  14313  apcxp2  14328  rpabscxpbnd  14329  rplogbid1  14335  rplogb1  14336  rpelogb  14337  rplogbchbase  14338  rplogbreexp  14341  rprelogbmul  14343  rprelogbdiv  14345  rplogbcxp  14351  rpcxplogb  14352  logbgcd1irraplemexp  14356  logbgcd1irraplemap  14357  lgsvalmod  14390  lgsdilem  14398  lgsne0  14409  lgseisenlem1  14420  lgseisenlem2  14421  2sqlem1  14431  mul2sq  14433  2sqlem3  14434  2sqlem8  14440  qdencn  14745  refeq  14746  cvgcmp2nlemabs  14750  cvgcmp2n  14751  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  trirec0  14762  apdifflemf  14764  apdifflemr  14765  apdiff  14766  redc0  14775  reap0  14776  nconstwlpolem0  14780  nconstwlpolemgt0  14781  neap0mkv  14786  ltlenmkv  14787