Theorem recnd 8108

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℂcc 7930  ℝcr 7931

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8024

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3173  df-ss 3180

This theorem is referenced by:  readdcan  8219  ltadd2  8499  ltadd1  8509  leadd2  8511  ltsubadd  8512  ltsubadd2  8513  lesubadd  8514  lesubadd2  8515  ltaddsub  8516  leaddsub  8518  lesub1  8536  lesub2  8537  ltsub1  8538  ltsub2  8539  ltnegcon1  8543  ltnegcon2  8544  add20  8554  subge0  8555  suble0  8556  lesub0  8559  eqord2  8564  possumd  8649  sublt0d  8650  rimul  8665  rereim  8666  apreap  8667  ltmul1a  8671  ltmul1  8672  reapmul1  8675  remulext2  8680  cru  8682  apreim  8683  mulreim  8684  apadd1  8688  apneg  8691  mulext1  8692  ltapd  8718  aprcl  8726  aptap  8730  rerecclap  8810  redivclap  8811  recgt0  8930  prodgt0gt0  8931  prodgt0  8932  prodge0  8934  lemul1a  8938  ltdiv1  8948  ltmuldiv  8954  ledivmul  8957  lt2mul2div  8959  ltrec  8963  lt2msq  8966  ltdiv2  8967  ltrec1  8968  lerec2  8969  ledivdiv  8970  lediv2  8971  ltdiv23  8972  lediv23  8973  lediv12a  8974  recp1lt1  8979  recreclt  8980  ledivp1  8983  mulle0r  9024  negiso  9035  avglt1  9283  avglt2  9284  div4p1lem1div2  9298  nn0cnd  9357  zcn  9384  peano2z  9415  zaddcllemneg  9418  ztri3or  9422  zeo  9485  zcnd  9503  eluzelcn  9666  infrenegsupex  9722  supinfneg  9723  infsupneg  9724  supminfex  9725  irrmulap  9776  cnref1o  9779  rpcn  9791  rpcnd  9827  ltaddrp2d  9860  mul2lt0rlt0  9888  mul2lt0rgt0  9889  mul2lt0llt0  9890  mul2lt0lgt0  9891  mul2lt0np  9892  mul2lt0pn  9893  xpncan  10000  icoshftf1o  10120  lincmb01cmp  10132  iccf1o  10133  infssuzcldc  10385  qbtwnrelemcalc  10405  flhalf  10452  intfracq  10472  flqdiv  10473  modqid  10501  modqid0  10502  mulqaddmodid  10516  seqf1oglem1  10671  ser3le  10689  expcl2lemap  10703  expnegzap  10725  expaddzaplem  10734  expaddzap  10735  expmulzap  10737  ltexp2a  10743  leexp2a  10744  leexp2r  10745  exple1  10747  expubnd  10748  sq11  10764  bernneq2  10813  expnbnd  10815  nn0ltexp2  10861  nn0opthlem2d  10873  faclbnd  10893  bcp1nk  10914  remim  11215  reim0b  11217  rereb  11218  mulreap  11219  cjreb  11221  recj  11222  reneg  11223  readd  11224  resub  11225  remullem  11226  remul2  11228  redivap  11229  imcj  11230  imneg  11231  imadd  11232  imsub  11233  immul2  11235  imdivap  11236  cjcj  11238  cjadd  11239  ipcnval  11241  cjmulval  11243  cjneg  11245  imval2  11249  cjreim2  11259  cjap  11261  cnrecnv  11265  caucvgrelemrec  11334  cvg1nlemres  11340  recvguniqlem  11349  recvguniq  11350  resqrexlemover  11365  resqrexlemcalc1  11369  resqrexlemcalc2  11370  resqrexlemcalc3  11371  resqrexlemnmsq  11372  resqrexlemnm  11373  resqrexlemgt0  11375  resqrexlemoverl  11376  resqrexlemglsq  11377  remsqsqrt  11387  sqrtmul  11390  sqrtdiv  11397  sqrtmsq  11400  abs00ap  11417  absext  11418  abs00  11419  absdivap  11425  absid  11426  absexp  11434  absexpzap  11435  absimle  11439  abslt  11443  absle  11444  abssubap0  11445  abssubne0  11446  releabs  11451  recvalap  11452  abstri  11459  abs2difabs  11463  amgm2  11473  icodiamlt  11535  maxabsle  11559  maxabslemab  11561  maxabslemlub  11562  maxabslemval  11563  maxcl  11565  maxltsup  11573  max0addsup  11574  minmax  11585  minabs  11591  minclpr  11592  bdtrilem  11594  bdtri  11595  mul0inf  11596  mingeb  11597  climabs0  11662  reccn2ap  11668  climrecl  11679  climge0  11680  climle  11689  climsqz  11690  climsqz2  11691  climlec2  11696  climrecvg1n  11703  climcvg1nlem  11704  isumrecl  11784  isumge0  11785  fsumlessfi  11815  fsumge1  11816  fsum00  11817  fsumle  11818  fsumlt  11819  fsumabs  11820  iserabs  11830  isumrpcl  11849  isumle  11850  isumlessdc  11851  trireciplem  11855  trirecip  11856  expcnvre  11858  expcnv  11859  explecnv  11860  absltap  11864  geo2sum  11869  cvgratnnlembern  11878  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  cvgratnnlemabsle  11882  cvgratnnlemsumlt  11883  cvgratnnlemfm  11884  cvgratnnlemrate  11885  cvgratz  11887  mertenslemi1  11890  mertenslem2  11891  fprodabs  11971  fprodle  11995  efcllemp  12013  ege2le3  12026  efaddlem  12029  efgt0  12039  reeftlcl  12044  eftlub  12045  effsumlt  12047  efltim  12053  eflegeo  12056  resin4p  12073  recos4p  12074  efeul  12089  ef01bndlem  12111  sin01bnd  12112  cos01bnd  12113  sin01gt0  12117  cos01gt0  12118  sin02gt0  12119  cos12dec  12123  absefi  12124  absef  12125  absefib  12126  efieq1re  12127  eirraplem  12132  dvdsaddre2b  12196  dvdslelemd  12198  odd2np1  12228  divalglemnqt  12275  bitsp1o  12308  bitsfzo  12310  bitscmp  12313  nn0seqcvgd  12407  sqnprm  12502  isprm5lem  12507  odzdvds  12612  pythagtriplem14  12644  pcid  12691  fldivp1  12715  pockthlem  12723  4sqlem5  12749  4sqlem10  12754  mul4sqlem  12760  4sqlem15  12772  4sqlem16  12773  mulgneg  13520  ghmmulg  13636  rege0subm  14390  metrtri  14893  bl2in  14919  blhalf  14924  blssps  14943  blss  14944  maxcncf  15131  mincncf  15132  dedekindeu  15139  dedekindicclemicc  15148  ivthinclemlopn  15152  ivthinclemuopn  15154  ivthinc  15159  ivthdec  15160  ivthreinc  15161  dvconstre  15212  dvidre  15213  dvcjbr  15224  dvfre  15226  dveflem  15242  plyrecj  15279  reeff1olem  15287  reeff1oleme  15288  eflt  15291  sin0pilem1  15297  sin0pilem2  15298  pilem3  15299  sincosq2sgn  15343  sincosq3sgn  15344  sincosq4sgn  15345  sinq12gt0  15346  sinq34lt0t  15347  cosq14gt0  15348  cosq23lt0  15349  coseq0q4123  15350  coseq0negpitopi  15352  tanrpcl  15353  tangtx  15354  coskpi  15364  cosordlem  15365  cosq34lt1  15366  cos11  15369  reexplog  15387  relogexp  15388  logdivlti  15397  rpcxpef  15410  rpcncxpcl  15418  cxpap0  15420  rpcxpadd  15421  rpmulcxp  15425  cxpmul  15428  abscxp  15431  cxplt  15432  cxplt3  15436  logsqrt  15439  apcxp2  15455  rpabscxpbnd  15456  rplogbid1  15463  rplogb1  15464  rpelogb  15465  rplogbchbase  15466  rplogbreexp  15469  rprelogbmul  15471  rprelogbdiv  15473  rplogbcxp  15479  rpcxplogb  15480  logbgcd1irraplemexp  15484  logbgcd1irraplemap  15485  mersenne  15513  lgsvalmod  15540  lgsdilem  15548  lgsne0  15559  gausslemma2dlem1a  15579  gausslemma2dlem6  15588  lgseisenlem1  15591  lgseisenlem2  15592  lgseisen  15595  lgsquadlem1  15598  lgsquadlem2  15599  2sqlem1  15635  mul2sq  15637  2sqlem3  15638  2sqlem8  15644  qdencn  16040  refeq  16041  cvgcmp2nlemabs  16045  cvgcmp2n  16046  trilpolemisumle  16051  trilpolemeq1  16053  trilpolemlt1  16054  trirec0  16057  apdifflemf  16059  apdifflemr  16060  apdiff  16061  redc0  16070  reap0  16071  cndcap  16072  nconstwlpolem0  16076  nconstwlpolemgt0  16077  neap0mkv  16082  ltlenmkv  16083