ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  recnd GIF version

Theorem recnd 7052
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
StepHypRef Expression
1 recnd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 recn 7012 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
31, 2syl 14 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393  cc 6885  cr 6886
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-resscn 6974
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931
This theorem is referenced by:  readdcan  7151  ltadd2  7414  ltadd1  7422  leadd2  7424  ltsubadd  7425  ltsubadd2  7426  lesubadd  7427  lesubadd2  7428  ltaddsub  7429  leaddsub  7431  lesub1  7449  lesub2  7450  ltsub1  7451  ltsub2  7452  ltnegcon1  7456  ltnegcon2  7457  add20  7467  subge0  7468  suble0  7469  lesub0  7472  possumd  7558  sublt0d  7559  rimul  7574  rereim  7575  apreap  7576  ltmul1a  7580  ltmul1  7581  reapmul1  7584  remulext2  7589  cru  7591  apreim  7592  mulreim  7593  apadd1  7597  apneg  7600  mulext1  7601  ltapd  7625  rerecclap  7704  redivclap  7705  recgt0  7814  prodgt0gt0  7815  prodgt0  7816  prodge0  7818  lemul1a  7822  ltdiv1  7832  ltmuldiv  7838  ledivmul  7841  lt2mul2div  7843  ltrec  7847  lt2msq  7850  ltdiv2  7851  ltrec1  7852  lerec2  7853  ledivdiv  7854  lediv2  7855  ltdiv23  7856  lediv23  7857  lediv12a  7858  recp1lt1  7863  recreclt  7864  ledivp1  7867  avglt1  8161  avglt2  8162  div4p1lem1div2  8175  nn0cnd  8235  zcn  8248  peano2z  8279  zaddcllemneg  8282  ztri3or  8286  zeo  8341  zcnd  8359  eluzelcn  8482  cnref1o  8580  rpcn  8589  rpcnd  8622  ltaddrp2d  8655  icoshftf1o  8857  lincmb01cmp  8869  iccf1o  8870  qbtwnrelemcalc  9108  flhalf  9142  serile  9227  expcl2lemap  9241  expnegzap  9263  expaddzaplem  9272  expaddzap  9273  expmulzap  9275  ltexp2a  9280  leexp2a  9281  leexp2r  9282  exple1  9284  expubnd  9285  sq11  9300  bernneq2  9344  expnbnd  9346  remim  9434  reim0b  9436  rereb  9437  mulreap  9438  cjreb  9440  recj  9441  reneg  9442  readd  9443  resub  9444  remullem  9445  remul2  9447  redivap  9448  imcj  9449  imneg  9450  imadd  9451  imsub  9452  immul2  9454  imdivap  9455  cjcj  9457  cjadd  9458  ipcnval  9460  cjmulval  9462  cjneg  9464  imval2  9468  cjreim2  9478  cjap  9480  cnrecnv  9484  caucvgrelemrec  9552  cvg1nlemres  9558  recvguniqlem  9566  recvguniq  9567  resqrexlemover  9582  resqrexlemcalc1  9586  resqrexlemcalc2  9587  resqrexlemcalc3  9588  resqrexlemnmsq  9589  resqrexlemnm  9590  resqrexlemgt0  9592  resqrexlemoverl  9593  resqrexlemglsq  9594  remsqsqrt  9604  sqrtmul  9607  sqrtdiv  9614  sqrtmsq  9617  abs00ap  9634  absext  9635  abs00  9636  absdivap  9642  absid  9643  absexp  9649  absexpzap  9650  absimle  9654  abslt  9658  absle  9659  abssubap0  9660  abssubne0  9661  releabs  9666  recvalap  9667  abstri  9674  abs2difabs  9678  amgm2  9688  icodiamlt  9750  climabs0  9802  climrecl  9818  climge0  9819  climle  9828  climsqz  9829  climsqz2  9830  climlec2  9835  climserile  9839  climrecvg1n  9841  climcvg1nlem  9842  nn0seqcvgd  9854
  Copyright terms: Public domain W3C validator