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  10751  intfracq  10771  flqdiv  10772  modqid  10800  modqid0  10801  mulqaddmodid  10815  seqf1oglem1  10970  ser3le  10988  expcl2lemap  11002  expnegzap  11024  expaddzaplem  11033  expaddzap  11034  expmulzap  11036  ltexp2a  11042  leexp2a  11043  leexp2r  11044  exple1  11046  expubnd  11047  sq11  11063  resq01  11109  bernneq2  11113  expnbnd  11115  nn0ltexp2  11162  nn0opthlem2d  11174  faclbnd  11194  bcp1nk  11215  bcm1n  11222  remim  11640  reim0b  11642  rereb  11643  mulreap  11644  cjreb  11646  recj  11647  reneg  11648  readd  11649  resub  11650  remullem  11651  remul2  11653  redivap  11654  imcj  11655  imneg  11656  imadd  11657  imsub  11658  immul2  11660  imdivap  11661  cjcj  11663  cjadd  11664  ipcnval  11666  cjmulval  11668  cjneg  11670  imval2  11674  sq01  11675  cjreim2  11685  cjap  11687  cnrecnv  11691  caucvgrelemrec  11760  cvg1nlemres  11766  recvguniqlem  11775  recvguniq  11776  resqrexlemover  11791  resqrexlemcalc1  11795  resqrexlemcalc2  11796  resqrexlemcalc3  11797  resqrexlemnmsq  11798  resqrexlemnm  11799  resqrexlemgt0  11801  resqrexlemoverl  11802  resqrexlemglsq  11803  remsqsqrt  11813  sqrtmul  11816  sqrtdiv  11823  sqrtmsq  11826  abs00ap  11843  absext  11844  abs00  11845  absdivap  11851  absid  11852  absexp  11861  absexpzap  11862  absimle  11866  abslt  11870  absle  11871  abssubap0  11872  abssubne0  11873  releabs  11878  recvalap  11879  abstri  11886  abs2difabs  11890  amgm2  11900  icodiamlt  11962  maxabsle  11986  maxabslemab  11988  maxabslemlub  11989  maxabslemval  11990  maxcl  11992  maxltsup  12000  max0addsup  12001  minmax  12013  minabs  12019  minclpr  12020  bdtrilem  12023  bdtri  12024  mul0inf  12025  mingeb  12026  climabs0  12091  reccn2ap  12097  climrecl  12108  climge0  12109  climle  12118  climsqz  12119  climsqz2  12120  climlec2  12125  climrecvg1n  12132  climcvg1nlem  12133  isumrecl  12214  isumge0  12215  fsumlessfi  12245  fsumge1  12246  fsum00  12247  fsumle  12248  fsumlt  12249  fsumabs  12250  iserabs  12260  isumrpcl  12279  isumle  12280  isumlessdc  12281  trireciplem  12285  trirecip  12286  expcnvre  12288  expcnv  12289  explecnv  12290  absltap  12294  geo2sum  12299  cvgratnnlembern  12308  cvgratnnlemnexp  12309  cvgratnnlemmn  12310  cvgratnnlemabsle  12312  cvgratnnlemsumlt  12313  cvgratnnlemfm  12314  cvgratnnlemrate  12315  cvgratz  12317  mertenslemi1  12320  mertenslem2  12321  fprodabs  12401  fprodle  12425  efcllemp  12443  ege2le3  12456  efaddlem  12459  efgt0  12469  reeftlcl  12474  eftlub  12475  effsumlt  12477  efltim  12483  eflegeo  12486  resin4p  12503  recos4p  12504  efeul  12519  ef01bndlem  12541  sin01bnd  12542  cos01bnd  12543  sin01gt0  12547  cos01gt0  12548  sin02gt0  12549  cos12dec  12553  absefi  12554  absef  12555  absefib  12556  efieq1re  12557  eirraplem  12562  dvdsaddre2b  12626  dvdslelemd  12628  odd2np1  12658  divalglemnqt  12705  bitsp1o  12738  bitsfzo  12740  bitscmp  12743  nn0seqcvgd  12837  sqnprm  12933  isprm5lem  12938  nn0sqdcq  13006  odzdvds  13046  pythagtriplem14  13078  pcid  13125  fldivp1  13149  pockthlem  13157  4sqlem5  13183  4sqlem10  13188  mul4sqlem  13194  4sqlem15  13206  4sqlem16  13207  ballotfilemsi  13309  mulgneg  13994  ghmmulg  14110  rege0subm  14972  metrtri  15530  bl2in  15556  blhalf  15561  blssps  15580  blss  15581  maxcncf  15768  mincncf  15769  dedekindeu  15776  dedekindicclemicc  15785  ivthinclemlopn  15789  ivthinclemuopn  15791  ivthinc  15796  ivthdec  15797  ivthreinc  15798  dvconstre  15849  dvidre  15850  dvcjbr  15861  dvfre  15863  dveflem  15879  plyrecj  15916  reeff1olem  15924  reeff1oleme  15925  eflt  15928  efap1p  15932  sin0pilem1  15935  sin0pilem2  15936  pilem3  15937  sincosq2sgn  15981  sincosq3sgn  15982  sincosq4sgn  15983  sinq12gt0  15984  sinq34lt0t  15985  cosq14gt0  15986  cosq23lt0  15987  coseq0q4123  15988  coseq0negpitopi  15990  tanrpcl  15991  tangtx  15992  coskpi  16002  cosordlem  16003  cosq34lt1  16004  cos11  16007  reexplog  16026  relogexp  16027  logdivlti  16036  logdivlt  16049  logfac  16051  rpcxpef  16052  rpcncxpcl  16060  cxpap0  16062  rpcxpadd  16063  rpmulcxp  16067  cxpmul  16070  abscxp  16073  cxplt  16074  cxplt3  16078  logsqrt  16081  apcxp2  16097  rpabscxpbnd  16098  rplogbid1  16105  rplogb1  16106  rpelogb  16107  rplogbchbase  16108  rplogbreexp  16111  rprelogbmul  16113  rprelogbdiv  16115  rplogbcxp  16121  rpcxplogb  16122  logbgcd1irraplemexp  16126  logbgcd1irraplemap  16127  zprmlogbaplem2  16138  log2tlbndlog2  16142  log2ublem2  16144  birthdaylem2  16148  birthdaylem3  16149  pellexlem2  16152  efnnfsumcl  16161  chtprm  16183  chtdif  16186  efchtqdvds  16187  prmorcht  16204  ppiqub  16215  chtqleppi  16216  chtublem  16217  chtqub  16218  mersenne  16219  bcmax  16227  bcp1ctr  16228  bposlem1  16233  lgsvalmod  16260  lgsdilem  16268  lgsne0  16279  gausslemma2dlem1a  16299  gausslemma2dlem6  16308  lgseisenlem1  16311  lgseisenlem2  16312  lgseisen  16315  lgsquadlem1  16318  lgsquadlem2  16319  2sqlem1  16355  mul2sq  16357  2sqlem3  16358  2sqlem8  16364  dichmul0orlem1  16875  dichmul0orlem4  16878  dichmul0orlem5  16879  dichmul0orlem6  16880  dichmul0orlem7  16881  qdencn  17194  refeq  17195  repiecele0  17197  repiecege0  17198  cvgcmp2nlemabs  17203  cvgcmp2n  17204  trilpolemisumle  17209  trilpolemeq1  17211  trilpolemlt1  17212  trirec0  17215  apdifflemf  17217  apdifflemr  17218  apdiff  17219  qdiff  17220  redc0  17229  reap0  17230  cndcap  17231  nconstwlpolem0  17235  nconstwlpolemgt0  17236  neap0mkv  17241  ltlenmkv  17242