Theorem recnd 8354

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8177  ℝcr 8178

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8271

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  readdcan  8466  ltadd2  8747  ltadd1  8757  leadd2  8759  ltsubadd  8760  ltsubadd2  8761  lesubadd  8762  lesubadd2  8763  ltaddsub  8764  leaddsub  8766  lesub1  8784  lesub2  8785  ltsub1  8786  ltsub2  8787  ltnegcon1  8791  ltnegcon2  8792  add20  8802  subge0  8803  suble0  8804  lesub0  8807  eqord2  8812  lesub3d  8891  possumd  8898  sublt0d  8899  rimul  8914  rereim  8915  apreap  8916  ltmul1a  8920  ltmul1  8921  reapmul1  8924  remulext2  8929  cru  8931  apreim  8932  mulreim  8933  apadd1  8937  apneg  8940  mulext1  8941  ltapd  8967  aprcl  8975  aptap  8979  rerecclap  9061  redivclap  9062  recgt0  9181  prodgt0gt0  9182  prodgt0  9183  prodge0  9185  lemul1a  9189  ltdiv1  9199  ltmuldiv  9205  ledivmul  9208  lt2mul2div  9210  ltrec  9214  lt2msq  9217  ltdiv2  9218  ltrec1  9219  lerec2  9220  ledivdiv  9221  lediv2  9222  ltdiv23  9223  lediv23  9224  lediv12a  9225  recp1lt1  9230  recreclt  9231  ledivp1  9234  mulle0r  9275  negiso  9286  avglt1  9546  avglt2  9547  div4p1lem1div2  9561  nn0cnd  9624  zcn  9651  peano2z  9682  zaddcllemneg  9685  ztri3or  9689  zeo  9753  zcnd  9771  eluzmn  9930  eluzelcn  9935  infrenegsupex  9996  supinfneg  9997  infsupneg  9998  supminfex  9999  irrmulap  10050  cnref1o  10053  rpcn  10065  rpcnd  10101  ltaddrp2d  10134  mul2lt0rlt0  10162  mul2lt0rgt0  10163  mul2lt0llt0  10164  mul2lt0lgt0  10165  mul2lt0np  10166  mul2lt0pn  10167  xpncan  10275  icoshftf1o  10395  lincmb01cmp  10407  lincmble  10408  iccf1o  10409  infssuzcldc  10670  qbtwnrelemcalc  10692  flhalf  10739  intfracq  10759  flqdiv  10760  modqid  10788  modqid0  10789  mulqaddmodid  10803  seqf1oglem1  10958  ser3le  10976  expcl2lemap  10990  expnegzap  11012  expaddzaplem  11021  expaddzap  11022  expmulzap  11024  ltexp2a  11030  leexp2a  11031  leexp2r  11032  exple1  11034  expubnd  11035  sq11  11051  resq01  11097  bernneq2  11101  expnbnd  11103  nn0ltexp2  11149  nn0opthlem2d  11161  faclbnd  11181  bcp1nk  11202  bcm1n  11209  remim  11627  reim0b  11629  rereb  11630  mulreap  11631  cjreb  11633  recj  11634  reneg  11635  readd  11636  resub  11637  remullem  11638  remul2  11640  redivap  11641  imcj  11642  imneg  11643  imadd  11644  imsub  11645  immul2  11647  imdivap  11648  cjcj  11650  cjadd  11651  ipcnval  11653  cjmulval  11655  cjneg  11657  imval2  11661  sq01  11662  cjreim2  11672  cjap  11674  cnrecnv  11678  caucvgrelemrec  11747  cvg1nlemres  11753  recvguniqlem  11762  recvguniq  11763  resqrexlemover  11778  resqrexlemcalc1  11782  resqrexlemcalc2  11783  resqrexlemcalc3  11784  resqrexlemnmsq  11785  resqrexlemnm  11786  resqrexlemgt0  11788  resqrexlemoverl  11789  resqrexlemglsq  11790  remsqsqrt  11800  sqrtmul  11803  sqrtdiv  11810  sqrtmsq  11813  abs00ap  11830  absext  11831  abs00  11832  absdivap  11838  absid  11839  absexp  11847  absexpzap  11848  absimle  11852  abslt  11856  absle  11857  abssubap0  11858  abssubne0  11859  releabs  11864  recvalap  11865  abstri  11872  abs2difabs  11876  amgm2  11886  icodiamlt  11948  maxabsle  11972  maxabslemab  11974  maxabslemlub  11975  maxabslemval  11976  maxcl  11978  maxltsup  11986  max0addsup  11987  minmax  11998  minabs  12004  minclpr  12005  bdtrilem  12007  bdtri  12008  mul0inf  12009  mingeb  12010  climabs0  12075  reccn2ap  12081  climrecl  12092  climge0  12093  climle  12102  climsqz  12103  climsqz2  12104  climlec2  12109  climrecvg1n  12116  climcvg1nlem  12117  isumrecl  12198  isumge0  12199  fsumlessfi  12229  fsumge1  12230  fsum00  12231  fsumle  12232  fsumlt  12233  fsumabs  12234  iserabs  12244  isumrpcl  12263  isumle  12264  isumlessdc  12265  trireciplem  12269  trirecip  12270  expcnvre  12272  expcnv  12273  explecnv  12274  absltap  12278  geo2sum  12283  cvgratnnlembern  12292  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  cvgratnnlemabsle  12296  cvgratnnlemsumlt  12297  cvgratnnlemfm  12298  cvgratnnlemrate  12299  cvgratz  12301  mertenslemi1  12304  mertenslem2  12305  fprodabs  12385  fprodle  12409  efcllemp  12427  ege2le3  12440  efaddlem  12443  efgt0  12453  reeftlcl  12458  eftlub  12459  effsumlt  12461  efltim  12467  eflegeo  12470  resin4p  12487  recos4p  12488  efeul  12503  ef01bndlem  12525  sin01bnd  12526  cos01bnd  12527  sin01gt0  12531  cos01gt0  12532  sin02gt0  12533  cos12dec  12537  absefi  12538  absef  12539  absefib  12540  efieq1re  12541  eirraplem  12546  dvdsaddre2b  12610  dvdslelemd  12612  odd2np1  12642  divalglemnqt  12689  bitsp1o  12722  bitsfzo  12724  bitscmp  12727  nn0seqcvgd  12821  sqnprm  12916  isprm5lem  12921  odzdvds  13026  pythagtriplem14  13058  pcid  13105  fldivp1  13129  pockthlem  13137  4sqlem5  13163  4sqlem10  13168  mul4sqlem  13174  4sqlem15  13186  4sqlem16  13187  ballotfilemsi  13260  mulgneg  13945  ghmmulg  14061  rege0subm  14923  metrtri  15480  bl2in  15506  blhalf  15511  blssps  15530  blss  15531  maxcncf  15718  mincncf  15719  dedekindeu  15726  dedekindicclemicc  15735  ivthinclemlopn  15739  ivthinclemuopn  15741  ivthinc  15746  ivthdec  15747  ivthreinc  15748  dvconstre  15799  dvidre  15800  dvcjbr  15811  dvfre  15813  dveflem  15829  plyrecj  15866  reeff1olem  15874  reeff1oleme  15875  eflt  15878  efap1p  15882  sin0pilem1  15885  sin0pilem2  15886  pilem3  15887  sincosq2sgn  15931  sincosq3sgn  15932  sincosq4sgn  15933  sinq12gt0  15934  sinq34lt0t  15935  cosq14gt0  15936  cosq23lt0  15937  coseq0q4123  15938  coseq0negpitopi  15940  tanrpcl  15941  tangtx  15942  coskpi  15952  cosordlem  15953  cosq34lt1  15954  cos11  15957  reexplog  15976  relogexp  15977  logdivlti  15986  logdivlt  15999  logfac  16001  rpcxpef  16002  rpcncxpcl  16010  cxpap0  16012  rpcxpadd  16013  rpmulcxp  16017  cxpmul  16020  abscxp  16023  cxplt  16024  cxplt3  16028  logsqrt  16031  apcxp2  16047  rpabscxpbnd  16048  rplogbid1  16055  rplogb1  16056  rpelogb  16057  rplogbchbase  16058  rplogbreexp  16061  rprelogbmul  16063  rprelogbdiv  16065  rplogbcxp  16071  rpcxplogb  16072  logbgcd1irraplemexp  16076  logbgcd1irraplemap  16077  log2tlbndlog2  16088  log2ublem2  16090  birthdaylem2  16094  birthdaylem3  16095  pellexlem2  16098  mersenne  16117  bcmax  16125  bcp1ctr  16126  lgsvalmod  16150  lgsdilem  16158  lgsne0  16169  gausslemma2dlem1a  16189  gausslemma2dlem6  16198  lgseisenlem1  16201  lgseisenlem2  16202  lgseisen  16205  lgsquadlem1  16208  lgsquadlem2  16209  2sqlem1  16245  mul2sq  16247  2sqlem3  16248  2sqlem8  16254  dichmul0orlem1  16765  dichmul0orlem4  16768  dichmul0orlem5  16769  dichmul0orlem6  16770  dichmul0orlem7  16771  qdencn  17084  refeq  17085  repiecele0  17087  repiecege0  17088  cvgcmp2nlemabs  17093  cvgcmp2n  17094  trilpolemisumle  17099  trilpolemeq1  17101  trilpolemlt1  17102  trirec0  17105  apdifflemf  17107  apdifflemr  17108  apdiff  17109  qdiff  17110  redc0  17119  reap0  17120  cndcap  17121  nconstwlpolem0  17125  nconstwlpolemgt0  17126  neap0mkv  17131  ltlenmkv  17132