Theorem recnd 8213

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

Syntax hints:   → wi 4   ∈ wcel 2201  ℂcc 8035  ℝcr 8036

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-resscn 8129

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212

This theorem is referenced by:  readdcan  8324  ltadd2  8604  ltadd1  8614  leadd2  8616  ltsubadd  8617  ltsubadd2  8618  lesubadd  8619  lesubadd2  8620  ltaddsub  8621  leaddsub  8623  lesub1  8641  lesub2  8642  ltsub1  8643  ltsub2  8644  ltnegcon1  8648  ltnegcon2  8649  add20  8659  subge0  8660  suble0  8661  lesub0  8664  eqord2  8669  possumd  8754  sublt0d  8755  rimul  8770  rereim  8771  apreap  8772  ltmul1a  8776  ltmul1  8777  reapmul1  8780  remulext2  8785  cru  8787  apreim  8788  mulreim  8789  apadd1  8793  apneg  8796  mulext1  8797  ltapd  8823  aprcl  8831  aptap  8835  rerecclap  8915  redivclap  8916  recgt0  9035  prodgt0gt0  9036  prodgt0  9037  prodge0  9039  lemul1a  9043  ltdiv1  9053  ltmuldiv  9059  ledivmul  9062  lt2mul2div  9064  ltrec  9068  lt2msq  9071  ltdiv2  9072  ltrec1  9073  lerec2  9074  ledivdiv  9075  lediv2  9076  ltdiv23  9077  lediv23  9078  lediv12a  9079  recp1lt1  9084  recreclt  9085  ledivp1  9088  mulle0r  9129  negiso  9140  avglt1  9388  avglt2  9389  div4p1lem1div2  9403  nn0cnd  9462  zcn  9489  peano2z  9520  zaddcllemneg  9523  ztri3or  9527  zeo  9590  zcnd  9608  eluzmn  9767  eluzelcn  9772  infrenegsupex  9833  supinfneg  9834  infsupneg  9835  supminfex  9836  irrmulap  9887  cnref1o  9890  rpcn  9902  rpcnd  9938  ltaddrp2d  9971  mul2lt0rlt0  9999  mul2lt0rgt0  10000  mul2lt0llt0  10001  mul2lt0lgt0  10002  mul2lt0np  10003  mul2lt0pn  10004  xpncan  10111  icoshftf1o  10231  lincmb01cmp  10243  iccf1o  10244  infssuzcldc  10501  qbtwnrelemcalc  10521  flhalf  10568  intfracq  10588  flqdiv  10589  modqid  10617  modqid0  10618  mulqaddmodid  10632  seqf1oglem1  10787  ser3le  10805  expcl2lemap  10819  expnegzap  10841  expaddzaplem  10850  expaddzap  10851  expmulzap  10853  ltexp2a  10859  leexp2a  10860  leexp2r  10861  exple1  10863  expubnd  10864  sq11  10880  bernneq2  10929  expnbnd  10931  nn0ltexp2  10977  nn0opthlem2d  10989  faclbnd  11009  bcp1nk  11030  remim  11443  reim0b  11445  rereb  11446  mulreap  11447  cjreb  11449  recj  11450  reneg  11451  readd  11452  resub  11453  remullem  11454  remul2  11456  redivap  11457  imcj  11458  imneg  11459  imadd  11460  imsub  11461  immul2  11463  imdivap  11464  cjcj  11466  cjadd  11467  ipcnval  11469  cjmulval  11471  cjneg  11473  imval2  11477  cjreim2  11487  cjap  11489  cnrecnv  11493  caucvgrelemrec  11562  cvg1nlemres  11568  recvguniqlem  11577  recvguniq  11578  resqrexlemover  11593  resqrexlemcalc1  11597  resqrexlemcalc2  11598  resqrexlemcalc3  11599  resqrexlemnmsq  11600  resqrexlemnm  11601  resqrexlemgt0  11603  resqrexlemoverl  11604  resqrexlemglsq  11605  remsqsqrt  11615  sqrtmul  11618  sqrtdiv  11625  sqrtmsq  11628  abs00ap  11645  absext  11646  abs00  11647  absdivap  11653  absid  11654  absexp  11662  absexpzap  11663  absimle  11667  abslt  11671  absle  11672  abssubap0  11673  abssubne0  11674  releabs  11679  recvalap  11680  abstri  11687  abs2difabs  11691  amgm2  11701  icodiamlt  11763  maxabsle  11787  maxabslemab  11789  maxabslemlub  11790  maxabslemval  11791  maxcl  11793  maxltsup  11801  max0addsup  11802  minmax  11813  minabs  11819  minclpr  11820  bdtrilem  11822  bdtri  11823  mul0inf  11824  mingeb  11825  climabs0  11890  reccn2ap  11896  climrecl  11907  climge0  11908  climle  11917  climsqz  11918  climsqz2  11919  climlec2  11924  climrecvg1n  11931  climcvg1nlem  11932  isumrecl  12013  isumge0  12014  fsumlessfi  12044  fsumge1  12045  fsum00  12046  fsumle  12047  fsumlt  12048  fsumabs  12049  iserabs  12059  isumrpcl  12078  isumle  12079  isumlessdc  12080  trireciplem  12084  trirecip  12085  expcnvre  12087  expcnv  12088  explecnv  12089  absltap  12093  geo2sum  12098  cvgratnnlembern  12107  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  cvgratnnlemabsle  12111  cvgratnnlemsumlt  12112  cvgratnnlemfm  12113  cvgratnnlemrate  12114  cvgratz  12116  mertenslemi1  12119  mertenslem2  12120  fprodabs  12200  fprodle  12224  efcllemp  12242  ege2le3  12255  efaddlem  12258  efgt0  12268  reeftlcl  12273  eftlub  12274  effsumlt  12276  efltim  12282  eflegeo  12285  resin4p  12302  recos4p  12303  efeul  12318  ef01bndlem  12340  sin01bnd  12341  cos01bnd  12342  sin01gt0  12346  cos01gt0  12347  sin02gt0  12348  cos12dec  12352  absefi  12353  absef  12354  absefib  12355  efieq1re  12356  eirraplem  12361  dvdsaddre2b  12425  dvdslelemd  12427  odd2np1  12457  divalglemnqt  12504  bitsp1o  12537  bitsfzo  12539  bitscmp  12542  nn0seqcvgd  12636  sqnprm  12731  isprm5lem  12736  odzdvds  12841  pythagtriplem14  12873  pcid  12920  fldivp1  12944  pockthlem  12952  4sqlem5  12978  4sqlem10  12983  mul4sqlem  12989  4sqlem15  13001  4sqlem16  13002  mulgneg  13750  ghmmulg  13866  rege0subm  14622  metrtri  15130  bl2in  15156  blhalf  15161  blssps  15180  blss  15181  maxcncf  15368  mincncf  15369  dedekindeu  15376  dedekindicclemicc  15385  ivthinclemlopn  15389  ivthinclemuopn  15391  ivthinc  15396  ivthdec  15397  ivthreinc  15398  dvconstre  15449  dvidre  15450  dvcjbr  15461  dvfre  15463  dveflem  15479  plyrecj  15516  reeff1olem  15524  reeff1oleme  15525  eflt  15528  sin0pilem1  15534  sin0pilem2  15535  pilem3  15536  sincosq2sgn  15580  sincosq3sgn  15581  sincosq4sgn  15582  sinq12gt0  15583  sinq34lt0t  15584  cosq14gt0  15585  cosq23lt0  15586  coseq0q4123  15587  coseq0negpitopi  15589  tanrpcl  15590  tangtx  15591  coskpi  15601  cosordlem  15602  cosq34lt1  15603  cos11  15606  reexplog  15624  relogexp  15625  logdivlti  15634  rpcxpef  15647  rpcncxpcl  15655  cxpap0  15657  rpcxpadd  15658  rpmulcxp  15662  cxpmul  15665  abscxp  15668  cxplt  15669  cxplt3  15673  logsqrt  15676  apcxp2  15692  rpabscxpbnd  15693  rplogbid1  15700  rplogb1  15701  rpelogb  15702  rplogbchbase  15703  rplogbreexp  15706  rprelogbmul  15708  rprelogbdiv  15710  rplogbcxp  15716  rpcxplogb  15717  logbgcd1irraplemexp  15721  logbgcd1irraplemap  15722  mersenne  15750  lgsvalmod  15777  lgsdilem  15785  lgsne0  15796  gausslemma2dlem1a  15816  gausslemma2dlem6  15825  lgseisenlem1  15828  lgseisenlem2  15829  lgseisen  15832  lgsquadlem1  15835  lgsquadlem2  15836  2sqlem1  15872  mul2sq  15874  2sqlem3  15875  2sqlem8  15881  qdencn  16694  refeq  16695  repiecele0  16697  repiecege0  16698  cvgcmp2nlemabs  16703  cvgcmp2n  16704  trilpolemisumle  16709  trilpolemeq1  16711  trilpolemlt1  16712  trirec0  16715  apdifflemf  16717  apdifflemr  16718  apdiff  16719  qdiff  16720  redc0  16729  reap0  16730  cndcap  16731  nconstwlpolem0  16735  nconstwlpolemgt0  16736  neap0mkv  16741  ltlenmkv  16742