Theorem xaddcld 13339

Description: The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
xnegcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ*)
xaddcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ*)

Assertion

Ref	Expression
xaddcld	⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈ ℝ*)

Proof of Theorem xaddcld

Step	Hyp	Ref	Expression
1		xnegcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
2		xaddcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
3		xaddcl 13277	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7430  ℝ^*cxr 11291   +_𝑒 cxad 13149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-1cn 11210  ax-addrcl 11213  ax-rnegex 11223  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-pnf 11294  df-mnf 11295  df-xr 11296  df-xadd 13152

This theorem is referenced by:  xadd4d  13341  imasdsf1olem  24398  bldisj  24423  xblss2ps  24426  xblss2  24427  blcld  24533  comet  24541  stdbdxmet  24543  metdstri  24886  metdscnlem  24890  iscau3  25325  xlt2addrd  32768  xrge0addcld  32772  xrge0subcld  32773  xrofsup  32777  xrsmulgzz  32993  xrge0adddir  33005  xrge0adddi  33006  esumle  34038  esumlef  34042  omssubadd  34281  inelcarsg  34292  carsgclctunlem2  34300  carsgclctunlem3  34301  carsgclctun  34302  xle2addd  45285  infrpge  45300  xrlexaddrp  45301  infleinflem1  45319  infleinflem2  45320  limsupgtlem  45732  ismbl3  45941  ismbl4  45948  sge0prle  46356  sge0split  46364  sge0iunmptlemre  46370  sge0xaddlem1  46388  omeunle  46471  carageniuncl  46478  ovnsubaddlem1  46525  hspmbl  46584  ovolval5lem1  46607