Theorem recnd 8191

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8013  ℝcr 8014

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8107

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  readdcan  8302  ltadd2  8582  ltadd1  8592  leadd2  8594  ltsubadd  8595  ltsubadd2  8596  lesubadd  8597  lesubadd2  8598  ltaddsub  8599  leaddsub  8601  lesub1  8619  lesub2  8620  ltsub1  8621  ltsub2  8622  ltnegcon1  8626  ltnegcon2  8627  add20  8637  subge0  8638  suble0  8639  lesub0  8642  eqord2  8647  possumd  8732  sublt0d  8733  rimul  8748  rereim  8749  apreap  8750  ltmul1a  8754  ltmul1  8755  reapmul1  8758  remulext2  8763  cru  8765  apreim  8766  mulreim  8767  apadd1  8771  apneg  8774  mulext1  8775  ltapd  8801  aprcl  8809  aptap  8813  rerecclap  8893  redivclap  8894  recgt0  9013  prodgt0gt0  9014  prodgt0  9015  prodge0  9017  lemul1a  9021  ltdiv1  9031  ltmuldiv  9037  ledivmul  9040  lt2mul2div  9042  ltrec  9046  lt2msq  9049  ltdiv2  9050  ltrec1  9051  lerec2  9052  ledivdiv  9053  lediv2  9054  ltdiv23  9055  lediv23  9056  lediv12a  9057  recp1lt1  9062  recreclt  9063  ledivp1  9066  mulle0r  9107  negiso  9118  avglt1  9366  avglt2  9367  div4p1lem1div2  9381  nn0cnd  9440  zcn  9467  peano2z  9498  zaddcllemneg  9501  ztri3or  9505  zeo  9568  zcnd  9586  eluzmn  9745  eluzelcn  9750  infrenegsupex  9806  supinfneg  9807  infsupneg  9808  supminfex  9809  irrmulap  9860  cnref1o  9863  rpcn  9875  rpcnd  9911  ltaddrp2d  9944  mul2lt0rlt0  9972  mul2lt0rgt0  9973  mul2lt0llt0  9974  mul2lt0lgt0  9975  mul2lt0np  9976  mul2lt0pn  9977  xpncan  10084  icoshftf1o  10204  lincmb01cmp  10216  iccf1o  10217  infssuzcldc  10472  qbtwnrelemcalc  10492  flhalf  10539  intfracq  10559  flqdiv  10560  modqid  10588  modqid0  10589  mulqaddmodid  10603  seqf1oglem1  10758  ser3le  10776  expcl2lemap  10790  expnegzap  10812  expaddzaplem  10821  expaddzap  10822  expmulzap  10824  ltexp2a  10830  leexp2a  10831  leexp2r  10832  exple1  10834  expubnd  10835  sq11  10851  bernneq2  10900  expnbnd  10902  nn0ltexp2  10948  nn0opthlem2d  10960  faclbnd  10980  bcp1nk  11001  remim  11392  reim0b  11394  rereb  11395  mulreap  11396  cjreb  11398  recj  11399  reneg  11400  readd  11401  resub  11402  remullem  11403  remul2  11405  redivap  11406  imcj  11407  imneg  11408  imadd  11409  imsub  11410  immul2  11412  imdivap  11413  cjcj  11415  cjadd  11416  ipcnval  11418  cjmulval  11420  cjneg  11422  imval2  11426  cjreim2  11436  cjap  11438  cnrecnv  11442  caucvgrelemrec  11511  cvg1nlemres  11517  recvguniqlem  11526  recvguniq  11527  resqrexlemover  11542  resqrexlemcalc1  11546  resqrexlemcalc2  11547  resqrexlemcalc3  11548  resqrexlemnmsq  11549  resqrexlemnm  11550  resqrexlemgt0  11552  resqrexlemoverl  11553  resqrexlemglsq  11554  remsqsqrt  11564  sqrtmul  11567  sqrtdiv  11574  sqrtmsq  11577  abs00ap  11594  absext  11595  abs00  11596  absdivap  11602  absid  11603  absexp  11611  absexpzap  11612  absimle  11616  abslt  11620  absle  11621  abssubap0  11622  abssubne0  11623  releabs  11628  recvalap  11629  abstri  11636  abs2difabs  11640  amgm2  11650  icodiamlt  11712  maxabsle  11736  maxabslemab  11738  maxabslemlub  11739  maxabslemval  11740  maxcl  11742  maxltsup  11750  max0addsup  11751  minmax  11762  minabs  11768  minclpr  11769  bdtrilem  11771  bdtri  11772  mul0inf  11773  mingeb  11774  climabs0  11839  reccn2ap  11845  climrecl  11856  climge0  11857  climle  11866  climsqz  11867  climsqz2  11868  climlec2  11873  climrecvg1n  11880  climcvg1nlem  11881  isumrecl  11961  isumge0  11962  fsumlessfi  11992  fsumge1  11993  fsum00  11994  fsumle  11995  fsumlt  11996  fsumabs  11997  iserabs  12007  isumrpcl  12026  isumle  12027  isumlessdc  12028  trireciplem  12032  trirecip  12033  expcnvre  12035  expcnv  12036  explecnv  12037  absltap  12041  geo2sum  12046  cvgratnnlembern  12055  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  cvgratnnlemabsle  12059  cvgratnnlemsumlt  12060  cvgratnnlemfm  12061  cvgratnnlemrate  12062  cvgratz  12064  mertenslemi1  12067  mertenslem2  12068  fprodabs  12148  fprodle  12172  efcllemp  12190  ege2le3  12203  efaddlem  12206  efgt0  12216  reeftlcl  12221  eftlub  12222  effsumlt  12224  efltim  12230  eflegeo  12233  resin4p  12250  recos4p  12251  efeul  12266  ef01bndlem  12288  sin01bnd  12289  cos01bnd  12290  sin01gt0  12294  cos01gt0  12295  sin02gt0  12296  cos12dec  12300  absefi  12301  absef  12302  absefib  12303  efieq1re  12304  eirraplem  12309  dvdsaddre2b  12373  dvdslelemd  12375  odd2np1  12405  divalglemnqt  12452  bitsp1o  12485  bitsfzo  12487  bitscmp  12490  nn0seqcvgd  12584  sqnprm  12679  isprm5lem  12684  odzdvds  12789  pythagtriplem14  12821  pcid  12868  fldivp1  12892  pockthlem  12900  4sqlem5  12926  4sqlem10  12931  mul4sqlem  12937  4sqlem15  12949  4sqlem16  12950  mulgneg  13698  ghmmulg  13814  rege0subm  14569  metrtri  15072  bl2in  15098  blhalf  15103  blssps  15122  blss  15123  maxcncf  15310  mincncf  15311  dedekindeu  15318  dedekindicclemicc  15327  ivthinclemlopn  15331  ivthinclemuopn  15333  ivthinc  15338  ivthdec  15339  ivthreinc  15340  dvconstre  15391  dvidre  15392  dvcjbr  15403  dvfre  15405  dveflem  15421  plyrecj  15458  reeff1olem  15466  reeff1oleme  15467  eflt  15470  sin0pilem1  15476  sin0pilem2  15477  pilem3  15478  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  sinq12gt0  15525  sinq34lt0t  15526  cosq14gt0  15527  cosq23lt0  15528  coseq0q4123  15529  coseq0negpitopi  15531  tanrpcl  15532  tangtx  15533  coskpi  15543  cosordlem  15544  cosq34lt1  15545  cos11  15548  reexplog  15566  relogexp  15567  logdivlti  15576  rpcxpef  15589  rpcncxpcl  15597  cxpap0  15599  rpcxpadd  15600  rpmulcxp  15604  cxpmul  15607  abscxp  15610  cxplt  15611  cxplt3  15615  logsqrt  15618  apcxp2  15634  rpabscxpbnd  15635  rplogbid1  15642  rplogb1  15643  rpelogb  15644  rplogbchbase  15645  rplogbreexp  15648  rprelogbmul  15650  rprelogbdiv  15652  rplogbcxp  15658  rpcxplogb  15659  logbgcd1irraplemexp  15663  logbgcd1irraplemap  15664  mersenne  15692  lgsvalmod  15719  lgsdilem  15727  lgsne0  15738  gausslemma2dlem1a  15758  gausslemma2dlem6  15767  lgseisenlem1  15770  lgseisenlem2  15771  lgseisen  15774  lgsquadlem1  15777  lgsquadlem2  15778  2sqlem1  15814  mul2sq  15816  2sqlem3  15817  2sqlem8  15823  qdencn  16509  refeq  16510  cvgcmp2nlemabs  16514  cvgcmp2n  16515  trilpolemisumle  16520  trilpolemeq1  16522  trilpolemlt1  16523  trirec0  16526  apdifflemf  16528  apdifflemr  16529  apdiff  16530  redc0  16539  reap0  16540  cndcap  16541  nconstwlpolem0  16545  nconstwlpolemgt0  16546  neap0mkv  16551  ltlenmkv  16552