Theorem xaddcld 13218

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 13156	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7358  ℝ^*cxr 11167   +_𝑒 cxad 13026

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-cnex 11084  ax-1cn 11086  ax-addrcl 11089  ax-rnegex 11099  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4947  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-fv 6499  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-pnf 11170  df-mnf 11171  df-xr 11172  df-xadd 13029

This theorem is referenced by:  xadd4d  13220  imasdsf1olem  24319  bldisj  24344  xblss2ps  24347  xblss2  24348  blcld  24451  comet  24459  stdbdxmet  24461  metdstri  24798  metdscnlem  24802  iscau3  25236  xlt2addrd  32818  xrge0addcld  32821  xrge0subcld  32822  xrofsup  32826  xrsmulgzz  33070  xrge0adddir  33079  xrge0adddi  33080  esumle  34194  esumlef  34198  omssubadd  34436  inelcarsg  34447  carsgclctunlem2  34455  carsgclctunlem3  34456  carsgclctun  34457  xle2addd  45618  infrpge  45633  xrlexaddrp  45634  infleinflem1  45651  infleinflem2  45652  limsupgtlem  46058  ismbl3  46267  ismbl4  46274  sge0prle  46682  sge0split  46690  sge0iunmptlemre  46696  sge0xaddlem1  46714  omeunle  46797  carageniuncl  46804  ovnsubaddlem1  46851  hspmbl  46910  ovolval5lem1  46933