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

Theorem recnd 7025
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 6986 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
31, 2syl 14 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393  cc 6859  cr 6860
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 6948
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 2921  df-ss 2928
This theorem is referenced by:  readdcan  7124  ltadd2  7386  ltadd1  7393  leadd2  7395  ltsubadd  7396  ltsubadd2  7397  lesubadd  7398  lesubadd2  7399  ltaddsub  7400  leaddsub  7402  lesub1  7420  lesub2  7421  ltsub1  7422  ltsub2  7423  ltnegcon1  7427  ltnegcon2  7428  add20  7438  subge0  7439  suble0  7440  lesub0  7443  rimul  7543  rereim  7544  apreap  7545  ltmul1a  7549  ltmul1  7550  reapmul1  7553  remulext2  7558  cru  7560  apreim  7561  mulreim  7562  apadd1  7566  apneg  7569  mulext1  7570  ltapd  7594  rerecclap  7673  redivclap  7674  recgt0  7783  prodgt0gt0  7784  prodgt0  7785  prodge0  7787  lemul1a  7791  ltdiv1  7801  ltmuldiv  7807  ledivmul  7810  lt2mul2div  7812  ltrec  7816  lt2msq  7819  ltdiv2  7820  ltrec1  7821  lerec2  7822  ledivdiv  7823  lediv2  7824  ltdiv23  7825  lediv23  7826  lediv12a  7827  recp1lt1  7832  recreclt  7833  ledivp1  7836  avglt1  8127  avglt2  8128  nn0cnd  8200  zcn  8213  peano2z  8244  zaddcllemneg  8247  ztri3or  8251  zeo  8306  zcnd  8324  eluzelcn  8447  cnref1o  8544  rpcn  8553  rpcnd  8586  ltaddrp2d  8615  icoshftf1o  8817  lincmb01cmp  8829  iccf1o  8830  serile  9122  expcl2lemap  9136  expnegzap  9158  expaddzaplem  9167  expaddzap  9168  expmulzap  9170  ltexp2a  9175  leexp2a  9176  leexp2r  9177  exple1  9179  expubnd  9180  sq11  9195  bernneq2  9239  expnbnd  9241  remim  9329  reim0b  9331  rereb  9332  mulreap  9333  cjreb  9335  recj  9336  reneg  9337  readd  9338  resub  9339  remullem  9340  remul2  9342  redivap  9343  imcj  9344  imneg  9345  imadd  9346  imsub  9347  immul2  9349  imdivap  9350  cjcj  9352  cjadd  9353  ipcnval  9355  cjmulval  9357  cjneg  9359  imval2  9363  cjreim2  9373  cjap  9375  cnrecnv  9379  caucvgrelemrec  9447  cvg1nlemres  9453  recvguniqlem  9461  recvguniq  9462  resqrexlemover  9477  resqrexlemcalc1  9481  resqrexlemcalc2  9482  resqrexlemcalc3  9483  resqrexlemnmsq  9484  resqrexlemnm  9485  resqrexlemgt0  9487  resqrexlemoverl  9488  resqrexlemglsq  9489  remsqsqrt  9499  sqrtmul  9502  sqrtdiv  9509  sqrtmsq  9512  abs00ap  9529  absext  9530  abs00  9531  absdivap  9537  absid  9538  absexp  9544  absexpzap  9545  absimle  9549  abslt  9553  absle  9554  abssubap0  9555  abssubne0  9556  releabs  9561  recvalap  9562  abstri  9569  abs2difabs  9573  amgm2  9583  icodiamlt  9645  climabs0  9696  climrecl  9712  climge0  9713  climle  9722  climsqz  9723  climsqz2  9724  climlec2  9729  climserile  9733  climrecvg1n  9735  climcvg1nlem  9736  nn0seqcvgd  9748
  Copyright terms: Public domain W3C validator