Theorem recnd 5315

Description: Deduction from real number to complex number.

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		recnt 5313	. 2 |- (A e. RR -> A e. CC)
3	1, 2	syl 10	1 |- (ph -> A e. CC)

Syntax hints:   -> wi 3   e. wcel 958  CCcc 5232  RRcr 5233

This theorem is referenced by:  recp1lt1 5901  recrecltt 5902  ledivp1t 5905  zcnt 6140  zeot 6199  fladdzt 6244  ceim1lt 6249  intfracqOLD 6255  icoshftf1oi 6409  expordit 6600  exple1t 6607  expubndt 6608  bernneq2 6653  discrlem3 6658  sqsqr 6721  cjclt 6764  imret 6773  reim0t 6774  reim0bt 6775  rerebt 6776  mulretOLD 6777  resubt 6806  imsubt 6809  recjt 6818  imcjt 6819  cj11t 6830  absexpt 6868  abs2difabst 6903  caure 6927  cauim 6928  ser1absdiflem 6929  facdivt 6942  faclbnd 6945  faclbnd5 6953  fsumcmpndx2 7042  fsumabs 7043  climrecl 7110  climge0 7112  climabs0 7113  climmullem3 7122  climmullem4 7123  climsqueeze 7140  climsqueeze2 7141  climabs 7149  climre 7151  climim 7152  caucvg 7163  caucvg3a 7164  caucvg3lem 7166  ser1cmp2 7177  cvgcmp2lem 7180  cvgcmp3c 7186  cvgcmp3cetlem1 7188  reccnv 7218  infcvglem2 7222  cvgratlem1 7250  cvgratlem2 7251  ivthlem6 7286  ivthlem7 7287  dsupivthlem 7291  erelem3 7321  efcj 7336  ef1tllem 7381  abspef01tlub 7395  resin4pt 7436  recos4pt 7437  efeult 7449  sin01bndlem2 7468  sin01bndlem3 7469  cos01bndlem2 7470  cos01bndlem3 7471  sin01gt0 7476  cos01gt0 7477  sin02gt0 7478  absefit 7482  metsym 7816  metge0 7819  lmle 7960  bcthlem1 7999  bcthlem25 8023  nvm1 8292  nvpi 8294  nvz0 8296  nvmtri 8299  nvabs 8301  nvge0 8302  nv1 8304  nmcnilem 8337  sm1cnilem 8347  ipval2lem4 8356  ipval2 8357  4ipval2 8358  4ipval3 8362  ipid 8363  ipcj 8367  ip0r 8370  ipz 8372  ip1cnilem3 8375  ip1cnilem5 8377  ip1cnilem6 8378  nmoub3i 8436  nmlno0lem 8453  nmblolbii 8459  blocnilem 8464  cnph 8478  ipasslem4 8493  ipasslem5 8494  ipblnfi 8516  ubthlem7 8535  ubthlem8 8536  ubthlem9 8537  ubthlem10 8538  ubthlem12 8540  minveclem9 8553  minveclem18 8562  minveclem25 8569  minveclem27 8571  minveclem30 8574  minveclem36 8580  minveclem38 8582  htthlem6 8625  pilem3 8673  sincosq2sgn 8705  sincosq3sgn 8706  sincosq4sgn 8707  sinq12gt0t 8708  sineq0 8713  efif1lem4 8733  shftefif1olem 8741  eff1lem 8743  eff1i 8744  effoi 8745  reeflogt 8761  relogeftb 8765  reexplogt 8773  relogexpt 8774  normpyct 9013  hhph 9045  bcs2t 9049  norm1t 9121  norm1ex 9122  projlem25 9210  projlem26 9211  pjthlem4 9222  pjthlem6 9224  pjthlem8 9226  pjthlem11 9229  pjspansnt 9500  osumlem3 9580  eigvalclt 9885  eighmortht 9888  nmlnop0ALT 9920  nmbdoplb 9949  nmcopexlem3 9953  nmcopexlem5 9955  nmcopexlem6 9956  nmcoplb 9958  lnopcon 9963  nmbdfnlb 9978  nmcfnexlem3 9982  nmcfnexlem5 9984  nmcfnexlem6 9985  nmcfnlb 9987  lnfncon 9990  riesz4 9996  cnlnadjlem2 10001  cnlnadjlem7 10006  nmopco 10028  nmopcoadj 10034  branmfnt 10038  leopnmidt 10071  hmopidmchlem 10078  hmopidmch 10079  hst1ht 10154  hstlet 10157  hstoht 10159  sto2 10164  stadd3 10175  strlem1 10177  golem1 10198  stcltrlem1 10203  cdj1 10360  cdj3lem1 10361  cdj3lem3b 10367  cdj3 10368  dmse1 10623  msr3 10625  msr4 10626  iintlem1 10632

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-pr 2779  ax-un 2866  ax-inf2 4625

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-reu 1651  df-rab 1652  df-v 1812  df-sbc 1942  df-csb 2002  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-pss 2055  df-nul 2281  df-if 2362  df-pw 2402  df-sn 2412  df-pr 2413  df-tp 2415  df-op 2416  df-uni 2504  df-int 2534  df-iun 2568  df-br 2620  df-opab 2667  df-tr 2681  df-eprel 2832  df-id 2835  df-po 2840  df-so 2850  df-fr 2917  df-we 2934  df-ord 2951  df-on 2952  df-lim 2953  df-suc 2954  df-om 3132  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-f 3194  df-fv 3198  df-rdg 3932  df-opr 3965  df-oprab 3966  df-1st 4079  df-2nd 4080  df-1o 4133  df-oadd 4135  df-omul 4136  df-er 4261  df-ec 4263  df-qs 4266  df-ni 5000  df-pli 5001  df-mi 5002  df-lti 5003  df-plpq 5035  df-mpq 5036  df-enq 5037  df-nq 5038  df-plq 5039  df-mq 5040  df-rq 5041  df-ltq 5042  df-1q 5043  df-np 5086  df-1p 5087  df-enr 5166  df-nr 5167  df-0r 5171  df-c 5240  df-r 5244

Copyright terms: Public domain