Theorem recnd 8183

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8005  ℝcr 8006

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8099

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  readdcan  8294  ltadd2  8574  ltadd1  8584  leadd2  8586  ltsubadd  8587  ltsubadd2  8588  lesubadd  8589  lesubadd2  8590  ltaddsub  8591  leaddsub  8593  lesub1  8611  lesub2  8612  ltsub1  8613  ltsub2  8614  ltnegcon1  8618  ltnegcon2  8619  add20  8629  subge0  8630  suble0  8631  lesub0  8634  eqord2  8639  possumd  8724  sublt0d  8725  rimul  8740  rereim  8741  apreap  8742  ltmul1a  8746  ltmul1  8747  reapmul1  8750  remulext2  8755  cru  8757  apreim  8758  mulreim  8759  apadd1  8763  apneg  8766  mulext1  8767  ltapd  8793  aprcl  8801  aptap  8805  rerecclap  8885  redivclap  8886  recgt0  9005  prodgt0gt0  9006  prodgt0  9007  prodge0  9009  lemul1a  9013  ltdiv1  9023  ltmuldiv  9029  ledivmul  9032  lt2mul2div  9034  ltrec  9038  lt2msq  9041  ltdiv2  9042  ltrec1  9043  lerec2  9044  ledivdiv  9045  lediv2  9046  ltdiv23  9047  lediv23  9048  lediv12a  9049  recp1lt1  9054  recreclt  9055  ledivp1  9058  mulle0r  9099  negiso  9110  avglt1  9358  avglt2  9359  div4p1lem1div2  9373  nn0cnd  9432  zcn  9459  peano2z  9490  zaddcllemneg  9493  ztri3or  9497  zeo  9560  zcnd  9578  eluzelcn  9741  infrenegsupex  9797  supinfneg  9798  infsupneg  9799  supminfex  9800  irrmulap  9851  cnref1o  9854  rpcn  9866  rpcnd  9902  ltaddrp2d  9935  mul2lt0rlt0  9963  mul2lt0rgt0  9964  mul2lt0llt0  9965  mul2lt0lgt0  9966  mul2lt0np  9967  mul2lt0pn  9968  xpncan  10075  icoshftf1o  10195  lincmb01cmp  10207  iccf1o  10208  infssuzcldc  10463  qbtwnrelemcalc  10483  flhalf  10530  intfracq  10550  flqdiv  10551  modqid  10579  modqid0  10580  mulqaddmodid  10594  seqf1oglem1  10749  ser3le  10767  expcl2lemap  10781  expnegzap  10803  expaddzaplem  10812  expaddzap  10813  expmulzap  10815  ltexp2a  10821  leexp2a  10822  leexp2r  10823  exple1  10825  expubnd  10826  sq11  10842  bernneq2  10891  expnbnd  10893  nn0ltexp2  10939  nn0opthlem2d  10951  faclbnd  10971  bcp1nk  10992  remim  11379  reim0b  11381  rereb  11382  mulreap  11383  cjreb  11385  recj  11386  reneg  11387  readd  11388  resub  11389  remullem  11390  remul2  11392  redivap  11393  imcj  11394  imneg  11395  imadd  11396  imsub  11397  immul2  11399  imdivap  11400  cjcj  11402  cjadd  11403  ipcnval  11405  cjmulval  11407  cjneg  11409  imval2  11413  cjreim2  11423  cjap  11425  cnrecnv  11429  caucvgrelemrec  11498  cvg1nlemres  11504  recvguniqlem  11513  recvguniq  11514  resqrexlemover  11529  resqrexlemcalc1  11533  resqrexlemcalc2  11534  resqrexlemcalc3  11535  resqrexlemnmsq  11536  resqrexlemnm  11537  resqrexlemgt0  11539  resqrexlemoverl  11540  resqrexlemglsq  11541  remsqsqrt  11551  sqrtmul  11554  sqrtdiv  11561  sqrtmsq  11564  abs00ap  11581  absext  11582  abs00  11583  absdivap  11589  absid  11590  absexp  11598  absexpzap  11599  absimle  11603  abslt  11607  absle  11608  abssubap0  11609  abssubne0  11610  releabs  11615  recvalap  11616  abstri  11623  abs2difabs  11627  amgm2  11637  icodiamlt  11699  maxabsle  11723  maxabslemab  11725  maxabslemlub  11726  maxabslemval  11727  maxcl  11729  maxltsup  11737  max0addsup  11738  minmax  11749  minabs  11755  minclpr  11756  bdtrilem  11758  bdtri  11759  mul0inf  11760  mingeb  11761  climabs0  11826  reccn2ap  11832  climrecl  11843  climge0  11844  climle  11853  climsqz  11854  climsqz2  11855  climlec2  11860  climrecvg1n  11867  climcvg1nlem  11868  isumrecl  11948  isumge0  11949  fsumlessfi  11979  fsumge1  11980  fsum00  11981  fsumle  11982  fsumlt  11983  fsumabs  11984  iserabs  11994  isumrpcl  12013  isumle  12014  isumlessdc  12015  trireciplem  12019  trirecip  12020  expcnvre  12022  expcnv  12023  explecnv  12024  absltap  12028  geo2sum  12033  cvgratnnlembern  12042  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  cvgratnnlemabsle  12046  cvgratnnlemsumlt  12047  cvgratnnlemfm  12048  cvgratnnlemrate  12049  cvgratz  12051  mertenslemi1  12054  mertenslem2  12055  fprodabs  12135  fprodle  12159  efcllemp  12177  ege2le3  12190  efaddlem  12193  efgt0  12203  reeftlcl  12208  eftlub  12209  effsumlt  12211  efltim  12217  eflegeo  12220  resin4p  12237  recos4p  12238  efeul  12253  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  sin01gt0  12281  cos01gt0  12282  sin02gt0  12283  cos12dec  12287  absefi  12288  absef  12289  absefib  12290  efieq1re  12291  eirraplem  12296  dvdsaddre2b  12360  dvdslelemd  12362  odd2np1  12392  divalglemnqt  12439  bitsp1o  12472  bitsfzo  12474  bitscmp  12477  nn0seqcvgd  12571  sqnprm  12666  isprm5lem  12671  odzdvds  12776  pythagtriplem14  12808  pcid  12855  fldivp1  12879  pockthlem  12887  4sqlem5  12913  4sqlem10  12918  mul4sqlem  12924  4sqlem15  12936  4sqlem16  12937  mulgneg  13685  ghmmulg  13801  rege0subm  14556  metrtri  15059  bl2in  15085  blhalf  15090  blssps  15109  blss  15110  maxcncf  15297  mincncf  15298  dedekindeu  15305  dedekindicclemicc  15314  ivthinclemlopn  15318  ivthinclemuopn  15320  ivthinc  15325  ivthdec  15326  ivthreinc  15327  dvconstre  15378  dvidre  15379  dvcjbr  15390  dvfre  15392  dveflem  15408  plyrecj  15445  reeff1olem  15453  reeff1oleme  15454  eflt  15457  sin0pilem1  15463  sin0pilem2  15464  pilem3  15465  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  sinq12gt0  15512  sinq34lt0t  15513  cosq14gt0  15514  cosq23lt0  15515  coseq0q4123  15516  coseq0negpitopi  15518  tanrpcl  15519  tangtx  15520  coskpi  15530  cosordlem  15531  cosq34lt1  15532  cos11  15535  reexplog  15553  relogexp  15554  logdivlti  15563  rpcxpef  15576  rpcncxpcl  15584  cxpap0  15586  rpcxpadd  15587  rpmulcxp  15591  cxpmul  15594  abscxp  15597  cxplt  15598  cxplt3  15602  logsqrt  15605  apcxp2  15621  rpabscxpbnd  15622  rplogbid1  15629  rplogb1  15630  rpelogb  15631  rplogbchbase  15632  rplogbreexp  15635  rprelogbmul  15637  rprelogbdiv  15639  rplogbcxp  15645  rpcxplogb  15646  logbgcd1irraplemexp  15650  logbgcd1irraplemap  15651  mersenne  15679  lgsvalmod  15706  lgsdilem  15714  lgsne0  15725  gausslemma2dlem1a  15745  gausslemma2dlem6  15754  lgseisenlem1  15757  lgseisenlem2  15758  lgseisen  15761  lgsquadlem1  15764  lgsquadlem2  15765  2sqlem1  15801  mul2sq  15803  2sqlem3  15804  2sqlem8  15810  qdencn  16425  refeq  16426  cvgcmp2nlemabs  16430  cvgcmp2n  16431  trilpolemisumle  16436  trilpolemeq1  16438  trilpolemlt1  16439  trirec0  16442  apdifflemf  16444  apdifflemr  16445  apdiff  16446  redc0  16455  reap0  16456  cndcap  16457  nconstwlpolem0  16461  nconstwlpolemgt0  16462  neap0mkv  16467  ltlenmkv  16468