Theorem recnd 8361

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

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

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 8278

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  8474  ltadd2  8755  ltadd1  8765  leadd2  8767  ltsubadd  8768  ltsubadd2  8769  lesubadd  8770  lesubadd2  8771  ltaddsub  8772  leaddsub  8774  lesub1  8792  lesub2  8793  ltsub1  8794  ltsub2  8795  ltnegcon1  8799  ltnegcon2  8800  add20  8810  subge0  8811  suble0  8812  lesub0  8815  eqord2  8820  lesub3d  8899  possumd  8906  sublt0d  8907  rimul  8922  rereim  8923  apreap  8924  ltmul1a  8928  ltmul1  8929  reapmul1  8932  remulext2  8937  cru  8939  apreim  8940  mulreim  8941  apadd1  8945  apneg  8948  mulext1  8949  ltapd  8975  aprcl  8983  aptap  8987  rerecclap  9069  redivclap  9070  recgt0  9189  prodgt0gt0  9190  prodgt0  9191  prodge0  9193  lemul1a  9197  ltdiv1  9207  ltmuldiv  9213  ledivmul  9216  lt2mul2div  9218  ltrec  9222  lt2msq  9225  ltdiv2  9226  ltrec1  9227  lerec2  9228  ledivdiv  9229  lediv2  9230  ltdiv23  9231  lediv23  9232  lediv12a  9233  recp1lt1  9238  recreclt  9239  ledivp1  9242  mulle0r  9283  negiso  9294  avglt1  9556  avglt2  9557  div4p1lem1div2  9571  nn0cnd  9634  zcn  9661  peano2z  9692  zaddcllemneg  9695  ztri3or  9699  zeo  9763  zcnd  9781  eluzmn  9945  eluzelcn  9950  infrenegsupex  10011  supinfneg  10012  infsupneg  10013  supminfex  10014  irraddap  10064  irrmulap  10066  cnref1o  10069  rpcn  10081  rpcnd  10117  ltaddrp2d  10150  mul2lt0rlt0  10178  mul2lt0rgt0  10179  mul2lt0llt0  10180  mul2lt0lgt0  10181  mul2lt0np  10182  mul2lt0pn  10183  xpncan  10291  icoshftf1o  10411  lincmb01cmp  10423  lincmble  10424  iccf1o  10425  infssuzcldc  10686  qbtwnrelemcalc  10708  flhalf  10759  intfracq  10779  flqdiv  10780  modqid  10808  modqid0  10809  mulqaddmodid  10823  seqf1oglem1  10978  ser3le  10996  expcl2lemap  11010  expnegzap  11032  expaddzaplem  11041  expaddzap  11042  expmulzap  11044  ltexp2a  11050  leexp2a  11051  leexp2r  11052  exple1  11054  expubnd  11055  sq11  11071  resq01  11117  bernneq2  11121  expnbnd  11123  nn0ltexp2  11170  nn0opthlem2d  11182  faclbnd  11202  bcp1nk  11223  bcm1n  11230  remim  11648  reim0b  11650  rereb  11651  mulreap  11652  cjreb  11654  recj  11655  reneg  11656  readd  11657  resub  11658  remullem  11659  remul2  11661  redivap  11662  imcj  11663  imneg  11664  imadd  11665  imsub  11666  immul2  11668  imdivap  11669  cjcj  11671  cjadd  11672  ipcnval  11674  cjmulval  11676  cjneg  11678  imval2  11682  sq01  11683  cjreim2  11693  cjap  11695  cnrecnv  11699  caucvgrelemrec  11768  cvg1nlemres  11774  recvguniqlem  11783  recvguniq  11784  resqrexlemover  11799  resqrexlemcalc1  11803  resqrexlemcalc2  11804  resqrexlemcalc3  11805  resqrexlemnmsq  11806  resqrexlemnm  11807  resqrexlemgt0  11809  resqrexlemoverl  11810  resqrexlemglsq  11811  remsqsqrt  11821  sqrtmul  11824  sqrtdiv  11831  sqrtmsq  11834  abs00ap  11851  absext  11852  abs00  11853  absdivap  11859  absid  11860  absexp  11869  absexpzap  11870  absimle  11874  abslt  11878  absle  11879  abssubap0  11880  abssubne0  11881  releabs  11886  recvalap  11887  abstri  11894  abs2difabs  11898  amgm2  11908  icodiamlt  11970  maxabsle  11994  maxabslemab  11996  maxabslemlub  11997  maxabslemval  11998  maxcl  12000  maxltsup  12008  max0addsup  12009  minmax  12021  minabs  12027  minclpr  12028  bdtrilem  12031  bdtri  12032  mul0inf  12033  mingeb  12034  climabs0  12099  reccn2ap  12105  climrecl  12116  climge0  12117  climle  12126  climsqz  12127  climsqz2  12128  climlec2  12133  climrecvg1n  12140  climcvg1nlem  12141  isumrecl  12222  isumge0  12223  fsumlessfi  12253  fsumge1  12254  fsum00  12255  fsumle  12256  fsumlt  12257  fsumabs  12258  iserabs  12268  isumrpcl  12287  isumle  12288  isumlessdc  12289  trireciplem  12293  trirecip  12294  expcnvre  12296  expcnv  12297  explecnv  12298  absltap  12302  geo2sum  12307  cvgratnnlembern  12316  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  cvgratnnlemabsle  12320  cvgratnnlemsumlt  12321  cvgratnnlemfm  12322  cvgratnnlemrate  12323  cvgratz  12325  mertenslemi1  12328  mertenslem2  12329  fprodabs  12409  fprodle  12433  efcllemp  12451  ege2le3  12464  efaddlem  12467  efgt0  12477  reeftlcl  12482  eftlub  12483  effsumlt  12485  efltim  12491  eflegeo  12494  resin4p  12511  recos4p  12512  efeul  12527  ef01bndlem  12549  sin01bnd  12550  cos01bnd  12551  sin01gt0  12555  cos01gt0  12556  sin02gt0  12557  cos12dec  12561  absefi  12562  absef  12563  absefib  12564  efieq1re  12565  eirraplem  12570  dvdsaddre2b  12634  dvdslelemd  12636  odd2np1  12666  divalglemnqt  12713  bitsp1o  12746  bitsfzo  12748  bitscmp  12751  nn0seqcvgd  12845  sqnprm  12941  isprm5lem  12946  nn0sqdcq  13014  odzdvds  13054  pythagtriplem14  13086  pcid  13133  fldivp1  13157  pockthlem  13165  4sqlem5  13191  4sqlem10  13196  mul4sqlem  13202  4sqlem15  13214  4sqlem16  13215  ballotfilemsi  13317  mulgneg  14003  ghmmulg  14119  rege0subm  15031  metrtri  15615  bl2in  15641  blhalf  15646  blssps  15665  blss  15666  maxcncf  15853  mincncf  15854  dedekindeu  15861  dedekindicclemicc  15870  ivthinclemlopn  15874  ivthinclemuopn  15876  ivthinc  15881  ivthdec  15882  ivthreinc  15883  dvconstre  15934  dvidre  15935  dvcjbr  15946  dvfre  15948  dveflem  15964  plyrecj  16001  reeff1olem  16009  reeff1oleme  16010  eflt  16013  efap1p  16017  sin0pilem1  16020  sin0pilem2  16021  pilem3  16022  sincosq2sgn  16066  sincosq3sgn  16067  sincosq4sgn  16068  sinq12gt0  16069  sinq34lt0t  16070  cosq14gt0  16071  cosq23lt0  16072  coseq0q4123  16073  coseq0negpitopi  16075  tanrpcl  16076  tangtx  16077  coskpi  16087  cosordlem  16089  cosq34lt1  16090  cos11  16093  reexplog  16113  relogexp  16114  logdivlti  16123  logdivlt  16136  logfac  16138  rpcxpef  16139  rpcncxpcl  16147  cxpap0  16149  rpcxpadd  16150  rpmulcxp  16154  cxpmul  16157  rpcxpmul2z  16160  abscxp  16162  cxplt  16163  cxplt3  16167  logsqrt  16170  apcxp2  16186  rpabscxpbnd  16187  rplogbid1  16195  rplogb1  16196  rpelogb  16197  rplogbchbase  16198  rplogbreexp  16201  rprelogbmul  16203  rprelogbdiv  16205  rplogbcxp  16211  rpcxplogb  16212  logbgcd1irraplemexp  16216  logbgcd1irraplemap  16217  zprmlogbaplem2  16228  log2tlbndlog2  16232  log2ublem2  16234  birthdaylem2  16238  birthdaylem3  16239  pellexlem2  16242  efnnfsumcl  16251  chtprm  16273  chtdif  16276  efchtqdvds  16277  prmorcht  16294  ppiqub  16305  chtqleppi  16306  chtublem  16307  chtqub  16308  mersenne  16309  bcmax  16317  bcp1ctr  16318  bposlem1  16323  bposlem9  16331  lgsvalmod  16355  lgsdilem  16363  lgsne0  16374  gausslemma2dlem1a  16394  gausslemma2dlem6  16403  lgseisenlem1  16406  lgseisenlem2  16407  lgseisen  16410  lgsquadlem1  16413  lgsquadlem2  16414  2sqlem1  16450  mul2sq  16452  2sqlem3  16453  2sqlem8  16459  dichmul0orlem1  16970  dichmul0orlem4  16973  dichmul0orlem5  16974  dichmul0orlem6  16975  dichmul0orlem7  16976  qdencn  17290  refeq  17291  repiecele0  17293  repiecege0  17294  cvgcmp2nlemabs  17299  cvgcmp2n  17300  trilpolemisumle  17306  trilpolemeq1  17308  trilpolemlt1  17309  trirec0  17312  apdifflemf  17314  apdifflemr  17315  apdiff  17316  qdiff  17317  redc0  17326  reap0  17327  cndcap  17328  nconstwlpolem0  17332  nconstwlpolemgt0  17333  neap0mkv  17338  ltlenmkv  17339