Theorem recnd 8355

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

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

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 8272

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  8468  ltadd2  8749  ltadd1  8759  leadd2  8761  ltsubadd  8762  ltsubadd2  8763  lesubadd  8764  lesubadd2  8765  ltaddsub  8766  leaddsub  8768  lesub1  8786  lesub2  8787  ltsub1  8788  ltsub2  8789  ltnegcon1  8793  ltnegcon2  8794  add20  8804  subge0  8805  suble0  8806  lesub0  8809  eqord2  8814  lesub3d  8893  possumd  8900  sublt0d  8901  rimul  8916  rereim  8917  apreap  8918  ltmul1a  8922  ltmul1  8923  reapmul1  8926  remulext2  8931  cru  8933  apreim  8934  mulreim  8935  apadd1  8939  apneg  8942  mulext1  8943  ltapd  8969  aprcl  8977  aptap  8981  rerecclap  9063  redivclap  9064  recgt0  9183  prodgt0gt0  9184  prodgt0  9185  prodge0  9187  lemul1a  9191  ltdiv1  9201  ltmuldiv  9207  ledivmul  9210  lt2mul2div  9212  ltrec  9216  lt2msq  9219  ltdiv2  9220  ltrec1  9221  lerec2  9222  ledivdiv  9223  lediv2  9224  ltdiv23  9225  lediv23  9226  lediv12a  9227  recp1lt1  9232  recreclt  9233  ledivp1  9236  mulle0r  9277  negiso  9288  avglt1  9549  avglt2  9550  div4p1lem1div2  9564  nn0cnd  9627  zcn  9654  peano2z  9685  zaddcllemneg  9688  ztri3or  9692  zeo  9756  zcnd  9774  eluzmn  9938  eluzelcn  9943  infrenegsupex  10004  supinfneg  10005  infsupneg  10006  supminfex  10007  irraddap  10057  irrmulap  10059  cnref1o  10062  rpcn  10074  rpcnd  10110  ltaddrp2d  10143  mul2lt0rlt0  10171  mul2lt0rgt0  10172  mul2lt0llt0  10173  mul2lt0lgt0  10174  mul2lt0np  10175  mul2lt0pn  10176  xpncan  10284  icoshftf1o  10404  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  infssuzcldc  10679  qbtwnrelemcalc  10701  flhalf  10752  intfracq  10772  flqdiv  10773  modqid  10801  modqid0  10802  mulqaddmodid  10816  seqf1oglem1  10971  ser3le  10989  expcl2lemap  11003  expnegzap  11025  expaddzaplem  11034  expaddzap  11035  expmulzap  11037  ltexp2a  11043  leexp2a  11044  leexp2r  11045  exple1  11047  expubnd  11048  sq11  11064  resq01  11110  bernneq2  11114  expnbnd  11116  nn0ltexp2  11163  nn0opthlem2d  11175  faclbnd  11195  bcp1nk  11216  bcm1n  11223  remim  11641  reim0b  11643  rereb  11644  mulreap  11645  cjreb  11647  recj  11648  reneg  11649  readd  11650  resub  11651  remullem  11652  remul2  11654  redivap  11655  imcj  11656  imneg  11657  imadd  11658  imsub  11659  immul2  11661  imdivap  11662  cjcj  11664  cjadd  11665  ipcnval  11667  cjmulval  11669  cjneg  11671  imval2  11675  sq01  11676  cjreim2  11686  cjap  11688  cnrecnv  11692  caucvgrelemrec  11761  cvg1nlemres  11767  recvguniqlem  11776  recvguniq  11777  resqrexlemover  11792  resqrexlemcalc1  11796  resqrexlemcalc2  11797  resqrexlemcalc3  11798  resqrexlemnmsq  11799  resqrexlemnm  11800  resqrexlemgt0  11802  resqrexlemoverl  11803  resqrexlemglsq  11804  remsqsqrt  11814  sqrtmul  11817  sqrtdiv  11824  sqrtmsq  11827  abs00ap  11844  absext  11845  abs00  11846  absdivap  11852  absid  11853  absexp  11862  absexpzap  11863  absimle  11867  abslt  11871  absle  11872  abssubap0  11873  abssubne0  11874  releabs  11879  recvalap  11880  abstri  11887  abs2difabs  11891  amgm2  11901  icodiamlt  11963  maxabsle  11987  maxabslemab  11989  maxabslemlub  11990  maxabslemval  11991  maxcl  11993  maxltsup  12001  max0addsup  12002  minmax  12014  minabs  12020  minclpr  12021  bdtrilem  12024  bdtri  12025  mul0inf  12026  mingeb  12027  climabs0  12092  reccn2ap  12098  climrecl  12109  climge0  12110  climle  12119  climsqz  12120  climsqz2  12121  climlec2  12126  climrecvg1n  12133  climcvg1nlem  12134  isumrecl  12215  isumge0  12216  fsumlessfi  12246  fsumge1  12247  fsum00  12248  fsumle  12249  fsumlt  12250  fsumabs  12251  iserabs  12261  isumrpcl  12280  isumle  12281  isumlessdc  12282  trireciplem  12286  trirecip  12287  expcnvre  12289  expcnv  12290  explecnv  12291  absltap  12295  geo2sum  12300  cvgratnnlembern  12309  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemabsle  12313  cvgratnnlemsumlt  12314  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratz  12318  mertenslemi1  12321  mertenslem2  12322  fprodabs  12402  fprodle  12426  efcllemp  12444  ege2le3  12457  efaddlem  12460  efgt0  12470  reeftlcl  12475  eftlub  12476  effsumlt  12478  efltim  12484  eflegeo  12487  resin4p  12504  recos4p  12505  efeul  12520  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  cos12dec  12554  absefi  12555  absef  12556  absefib  12557  efieq1re  12558  eirraplem  12563  dvdsaddre2b  12627  dvdslelemd  12629  odd2np1  12659  divalglemnqt  12706  bitsp1o  12739  bitsfzo  12741  bitscmp  12744  nn0seqcvgd  12838  sqnprm  12934  isprm5lem  12939  nn0sqdcq  13007  odzdvds  13047  pythagtriplem14  13079  pcid  13126  fldivp1  13150  pockthlem  13158  4sqlem5  13184  4sqlem10  13189  mul4sqlem  13195  4sqlem15  13207  4sqlem16  13208  ballotfilemsi  13310  mulgneg  13996  ghmmulg  14112  rege0subm  15005  metrtri  15569  bl2in  15595  blhalf  15600  blssps  15619  blss  15620  maxcncf  15807  mincncf  15808  dedekindeu  15815  dedekindicclemicc  15824  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthinc  15835  ivthdec  15836  ivthreinc  15837  dvconstre  15888  dvidre  15889  dvcjbr  15900  dvfre  15902  dveflem  15918  plyrecj  15955  reeff1olem  15963  reeff1oleme  15964  eflt  15967  efap1p  15971  sin0pilem1  15974  sin0pilem2  15975  pilem3  15976  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  sinq34lt0t  16024  cosq14gt0  16025  cosq23lt0  16026  coseq0q4123  16027  coseq0negpitopi  16029  tanrpcl  16030  tangtx  16031  coskpi  16041  cosordlem  16043  cosq34lt1  16044  cos11  16047  reexplog  16067  relogexp  16068  logdivlti  16077  logdivlt  16090  logfac  16092  rpcxpef  16093  rpcncxpcl  16101  cxpap0  16103  rpcxpadd  16104  rpmulcxp  16108  cxpmul  16111  rpcxpmul2z  16114  abscxp  16116  cxplt  16117  cxplt3  16121  logsqrt  16124  apcxp2  16140  rpabscxpbnd  16141  rplogbid1  16149  rplogb1  16150  rpelogb  16151  rplogbchbase  16152  rplogbreexp  16155  rprelogbmul  16157  rprelogbdiv  16159  rplogbcxp  16165  rpcxplogb  16166  logbgcd1irraplemexp  16170  logbgcd1irraplemap  16171  zprmlogbaplem2  16182  log2tlbndlog2  16186  log2ublem2  16188  birthdaylem2  16192  birthdaylem3  16193  pellexlem2  16196  efnnfsumcl  16205  chtprm  16227  chtdif  16230  efchtqdvds  16231  prmorcht  16248  ppiqub  16259  chtqleppi  16260  chtublem  16261  chtqub  16262  mersenne  16263  bcmax  16271  bcp1ctr  16272  bposlem1  16277  bposlem9  16285  lgsvalmod  16309  lgsdilem  16317  lgsne0  16328  gausslemma2dlem1a  16348  gausslemma2dlem6  16357  lgseisenlem1  16360  lgseisenlem2  16361  lgseisen  16364  lgsquadlem1  16367  lgsquadlem2  16368  2sqlem1  16404  mul2sq  16406  2sqlem3  16407  2sqlem8  16413  dichmul0orlem1  16924  dichmul0orlem4  16927  dichmul0orlem5  16928  dichmul0orlem6  16929  dichmul0orlem7  16930  qdencn  17243  refeq  17244  repiecele0  17246  repiecege0  17247  cvgcmp2nlemabs  17252  cvgcmp2n  17253  trilpolemisumle  17259  trilpolemeq1  17261  trilpolemlt1  17262  trirec0  17265  apdifflemf  17267  apdifflemr  17268  apdiff  17269  qdiff  17270  redc0  17279  reap0  17280  cndcap  17281  nconstwlpolem0  17285  nconstwlpolemgt0  17286  neap0mkv  17291  ltlenmkv  17292