Theorem recnd 8307

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8130  ℝcr 8131

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8224

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226

This theorem is referenced by:  readdcan  8418  ltadd2  8698  ltadd1  8708  leadd2  8710  ltsubadd  8711  ltsubadd2  8712  lesubadd  8713  lesubadd2  8714  ltaddsub  8715  leaddsub  8717  lesub1  8735  lesub2  8736  ltsub1  8737  ltsub2  8738  ltnegcon1  8742  ltnegcon2  8743  add20  8753  subge0  8754  suble0  8755  lesub0  8758  eqord2  8763  possumd  8848  sublt0d  8849  rimul  8864  rereim  8865  apreap  8866  ltmul1a  8870  ltmul1  8871  reapmul1  8874  remulext2  8879  cru  8881  apreim  8882  mulreim  8883  apadd1  8887  apneg  8890  mulext1  8891  ltapd  8917  aprcl  8925  aptap  8929  rerecclap  9009  redivclap  9010  recgt0  9129  prodgt0gt0  9130  prodgt0  9131  prodge0  9133  lemul1a  9137  ltdiv1  9147  ltmuldiv  9153  ledivmul  9156  lt2mul2div  9158  ltrec  9162  lt2msq  9165  ltdiv2  9166  ltrec1  9167  lerec2  9168  ledivdiv  9169  lediv2  9170  ltdiv23  9171  lediv23  9172  lediv12a  9173  recp1lt1  9178  recreclt  9179  ledivp1  9182  mulle0r  9223  negiso  9234  avglt1  9482  avglt2  9483  div4p1lem1div2  9497  nn0cnd  9560  zcn  9587  peano2z  9618  zaddcllemneg  9621  ztri3or  9625  zeo  9689  zcnd  9707  eluzmn  9866  eluzelcn  9871  infrenegsupex  9932  supinfneg  9933  infsupneg  9934  supminfex  9935  irrmulap  9986  cnref1o  9989  rpcn  10001  rpcnd  10037  ltaddrp2d  10070  mul2lt0rlt0  10098  mul2lt0rgt0  10099  mul2lt0llt0  10100  mul2lt0lgt0  10101  mul2lt0np  10102  mul2lt0pn  10103  xpncan  10210  icoshftf1o  10330  lincmb01cmp  10342  lincmble  10343  iccf1o  10344  infssuzcldc  10602  qbtwnrelemcalc  10622  flhalf  10669  intfracq  10689  flqdiv  10690  modqid  10718  modqid0  10719  mulqaddmodid  10733  seqf1oglem1  10888  ser3le  10906  expcl2lemap  10920  expnegzap  10942  expaddzaplem  10951  expaddzap  10952  expmulzap  10954  ltexp2a  10960  leexp2a  10961  leexp2r  10962  exple1  10964  expubnd  10965  sq11  10981  resq01  11027  bernneq2  11031  expnbnd  11033  nn0ltexp2  11079  nn0opthlem2d  11091  faclbnd  11111  bcp1nk  11132  bcm1n  11139  remim  11553  reim0b  11555  rereb  11556  mulreap  11557  cjreb  11559  recj  11560  reneg  11561  readd  11562  resub  11563  remullem  11564  remul2  11566  redivap  11567  imcj  11568  imneg  11569  imadd  11570  imsub  11571  immul2  11573  imdivap  11574  cjcj  11576  cjadd  11577  ipcnval  11579  cjmulval  11581  cjneg  11583  imval2  11587  cjreim2  11597  cjap  11599  cnrecnv  11603  caucvgrelemrec  11672  cvg1nlemres  11678  recvguniqlem  11687  recvguniq  11688  resqrexlemover  11703  resqrexlemcalc1  11707  resqrexlemcalc2  11708  resqrexlemcalc3  11709  resqrexlemnmsq  11710  resqrexlemnm  11711  resqrexlemgt0  11713  resqrexlemoverl  11714  resqrexlemglsq  11715  remsqsqrt  11725  sqrtmul  11728  sqrtdiv  11735  sqrtmsq  11738  abs00ap  11755  absext  11756  abs00  11757  absdivap  11763  absid  11764  absexp  11772  absexpzap  11773  absimle  11777  abslt  11781  absle  11782  abssubap0  11783  abssubne0  11784  releabs  11789  recvalap  11790  abstri  11797  abs2difabs  11801  amgm2  11811  icodiamlt  11873  maxabsle  11897  maxabslemab  11899  maxabslemlub  11900  maxabslemval  11901  maxcl  11903  maxltsup  11911  max0addsup  11912  minmax  11923  minabs  11929  minclpr  11930  bdtrilem  11932  bdtri  11933  mul0inf  11934  mingeb  11935  climabs0  12000  reccn2ap  12006  climrecl  12017  climge0  12018  climle  12027  climsqz  12028  climsqz2  12029  climlec2  12034  climrecvg1n  12041  climcvg1nlem  12042  isumrecl  12123  isumge0  12124  fsumlessfi  12154  fsumge1  12155  fsum00  12156  fsumle  12157  fsumlt  12158  fsumabs  12159  iserabs  12169  isumrpcl  12188  isumle  12189  isumlessdc  12190  trireciplem  12194  trirecip  12195  expcnvre  12197  expcnv  12198  explecnv  12199  absltap  12203  geo2sum  12208  cvgratnnlembern  12217  cvgratnnlemnexp  12218  cvgratnnlemmn  12219  cvgratnnlemabsle  12221  cvgratnnlemsumlt  12222  cvgratnnlemfm  12223  cvgratnnlemrate  12224  cvgratz  12226  mertenslemi1  12229  mertenslem2  12230  fprodabs  12310  fprodle  12334  efcllemp  12352  ege2le3  12365  efaddlem  12368  efgt0  12378  reeftlcl  12383  eftlub  12384  effsumlt  12386  efltim  12392  eflegeo  12395  resin4p  12412  recos4p  12413  efeul  12428  ef01bndlem  12450  sin01bnd  12451  cos01bnd  12452  sin01gt0  12456  cos01gt0  12457  sin02gt0  12458  cos12dec  12462  absefi  12463  absef  12464  absefib  12465  efieq1re  12466  eirraplem  12471  dvdsaddre2b  12535  dvdslelemd  12537  odd2np1  12567  divalglemnqt  12614  bitsp1o  12647  bitsfzo  12649  bitscmp  12652  nn0seqcvgd  12746  sqnprm  12841  isprm5lem  12846  odzdvds  12951  pythagtriplem14  12983  pcid  13030  fldivp1  13054  pockthlem  13062  4sqlem5  13088  4sqlem10  13093  mul4sqlem  13099  4sqlem15  13111  4sqlem16  13112  mulgneg  13878  ghmmulg  13994  rege0subm  14781  metrtri  15291  bl2in  15317  blhalf  15322  blssps  15341  blss  15342  maxcncf  15529  mincncf  15530  dedekindeu  15537  dedekindicclemicc  15546  ivthinclemlopn  15550  ivthinclemuopn  15552  ivthinc  15557  ivthdec  15558  ivthreinc  15559  dvconstre  15610  dvidre  15611  dvcjbr  15622  dvfre  15624  dveflem  15640  plyrecj  15677  reeff1olem  15685  reeff1oleme  15686  eflt  15689  sin0pilem1  15695  sin0pilem2  15696  pilem3  15697  sincosq2sgn  15741  sincosq3sgn  15742  sincosq4sgn  15743  sinq12gt0  15744  sinq34lt0t  15745  cosq14gt0  15746  cosq23lt0  15747  coseq0q4123  15748  coseq0negpitopi  15750  tanrpcl  15751  tangtx  15752  coskpi  15762  cosordlem  15763  cosq34lt1  15764  cos11  15767  reexplog  15785  relogexp  15786  logdivlti  15795  rpcxpef  15808  rpcncxpcl  15816  cxpap0  15818  rpcxpadd  15819  rpmulcxp  15823  cxpmul  15826  abscxp  15829  cxplt  15830  cxplt3  15834  logsqrt  15837  apcxp2  15853  rpabscxpbnd  15854  rplogbid1  15861  rplogb1  15862  rpelogb  15863  rplogbchbase  15864  rplogbreexp  15867  rprelogbmul  15869  rprelogbdiv  15871  rplogbcxp  15877  rpcxplogb  15878  logbgcd1irraplemexp  15882  logbgcd1irraplemap  15883  pellexlem2  15895  mersenne  15914  lgsvalmod  15941  lgsdilem  15949  lgsne0  15960  gausslemma2dlem1a  15980  gausslemma2dlem6  15989  lgseisenlem1  15992  lgseisenlem2  15993  lgseisen  15996  lgsquadlem1  15999  lgsquadlem2  16000  2sqlem1  16036  mul2sq  16038  2sqlem3  16039  2sqlem8  16045  qdencn  16856  refeq  16857  repiecele0  16859  repiecege0  16860  cvgcmp2nlemabs  16865  cvgcmp2n  16866  trilpolemisumle  16871  trilpolemeq1  16873  trilpolemlt1  16874  trirec0  16877  apdifflemf  16879  apdifflemr  16880  apdiff  16881  qdiff  16882  redc0  16891  reap0  16892  cndcap  16893  nconstwlpolem0  16898  nconstwlpolemgt0  16899  neap0mkv  16904  ltlenmkv  16905