Theorem recnd 6851

Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)

Hypothesis

Ref	Expression
recnd.1	|- (ph -> A e. RR)

Assertion

Ref	Expression
recnd	|- (ph -> A e. CC)

Proof of Theorem recnd

Step	Hyp	Ref	Expression
1		recnd.1	. 2 |- (ph -> A e. RR)
2		recn 6812	. 2 |- (A e. RR -> A e. CC)
3	1, 2	syl 14	1 |- (ph -> A e. CC)

Syntax hints:   -> wi 4   e. wcel 1390   CCcc 6709   RRcr 6710

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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-resscn 6775

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-in 2918  df-ss 2925

This theorem is referenced by:  readdcan  6950  ltadd2  7212  ltadd1  7219  leadd2  7221  ltsubadd  7222  ltsubadd2  7223  lesubadd  7224  lesubadd2  7225  ltaddsub  7226  leaddsub  7228  lesub1  7246  lesub2  7247  ltsub1  7248  ltsub2  7249  ltnegcon1  7253  ltnegcon2  7254  add20  7264  subge0  7265  suble0  7266  lesub0  7269  rimul  7369  rereim  7370  apreap  7371  ltmul1a  7375  ltmul1  7376  reapmul1  7379  remulext2  7384  cru  7386  apreim  7387  mulreim  7388  apadd1  7392  apneg  7395  mulext1  7396  rerecclap  7488  redivclap  7489  recgt0  7597  prodgt0gt0  7598  prodgt0  7599  prodge0  7601  lemul1a  7605  ltdiv1  7615  ltmuldiv  7621  ledivmul  7624  lt2mul2div  7626  ltrec  7630  lt2msq  7633  ltdiv2  7634  ltrec1  7635  lerec2  7636  ledivdiv  7637  lediv2  7638  ltdiv23  7639  lediv23  7640  lediv12a  7641  recp1lt1  7646  recreclt  7647  ledivp1  7650  avglt1  7940  avglt2  7941  nn0cnd  8013  zcn  8026  peano2z  8057  zaddcllemneg  8060  ztri3or  8064  zeo  8119  zcnd  8137  eluzelcn  8260  cnref1o  8357  rpcn  8366  rpcnd  8399  ltaddrp2d  8427  icoshftf1o  8629  lincmb01cmp  8641  iccf1o  8642  expcl2lemap  8921  expnegzap  8943  expaddzaplem  8952  expaddzap  8953  expmulzap  8955  ltexp2a  8960  leexp2a  8961  leexp2r  8962  exple1  8964  expubnd  8965  sq11  8979  bernneq2  9023  expnbnd  9025  remim  9088  reim0b  9090  rereb  9091  mulreap  9092  cjreb  9094  recj  9095  reneg  9096  readd  9097  resub  9098  remullem  9099  remul2  9101  redivap  9102  imcj  9103  imneg  9104  imadd  9105  imsub  9106  immul2  9108  imdivap  9109  cjcj  9111  cjadd  9112  ipcnval  9114  cjmulval  9116  cjneg  9118  imval2  9122  cjreim2  9132  cjap  9134  cnrecnv  9138  sqrtmsq  9215  absid  9225