Theorem xaddcld 13320

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

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7419  ℝ^*cxr 11284   +_𝑒 cxad 13130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11201  ax-1cn 11203  ax-addrcl 11206  ax-rnegex 11216  ax-cnre 11218

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7994  df-2nd 7995  df-pnf 11287  df-mnf 11288  df-xr 11289  df-xadd 13133

This theorem is referenced by:  xadd4d  13322  imasdsf1olem  24328  bldisj  24353  xblss2ps  24356  xblss2  24357  blcld  24463  comet  24471  stdbdxmet  24473  metdstri  24816  metdscnlem  24820  iscau3  25255  xlt2addrd  32615  xrge0addcld  32619  xrge0subcld  32620  xrofsup  32624  xrsmulgzz  32830  xrge0adddir  32842  xrge0adddi  32843  esumle  33810  esumlef  33814  omssubadd  34053  inelcarsg  34064  carsgclctunlem2  34072  carsgclctunlem3  34073  carsgclctun  34074  xle2addd  44858  infrpge  44873  xrlexaddrp  44874  infleinflem1  44892  infleinflem2  44893  limsupgtlem  45305  ismbl3  45514  ismbl4  45521  sge0prle  45929  sge0split  45937  sge0iunmptlemre  45943  sge0xaddlem1  45961  omeunle  46044  carageniuncl  46051  ovnsubaddlem1  46098  hspmbl  46157  ovolval5lem1  46180