xaddcld - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > xaddcld		GIF version

Theorem xaddcld 10048

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

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

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

**Proof of Theorem xaddcld**
Step	Hyp	Ref	Expression
1		xaddcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
2		xaddcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
3		xaddcl 10024	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐴 +_𝑒 𝐵) ∈ ℝ^)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 +_𝑒 𝐵) ∈ ℝ^*)

Colors of variables: wff set class

Syntax hints: → wi 4 ∈ wcel 2180 (class class class)co 5974 ℝ^*cxr 8148 +_𝑒 cxad 9934

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 713 ax-5 1473 ax-7 1474 ax-gen 1475 ax-ie1 1519 ax-ie2 1520 ax-8 1530 ax-10 1531 ax-11 1532 ax-i12 1533 ax-bndl 1535 ax-4 1536 ax-17 1552 ax-i9 1556 ax-ial 1560 ax-i5r 1561 ax-13 2182 ax-14 2183 ax-ext 2191 ax-sep 4181 ax-pow 4237 ax-pr 4272 ax-un 4501 ax-setind 4606 ax-cnex 8058 ax-resscn 8059 ax-1re 8061 ax-addrcl 8064 ax-rnegex 8076

This theorem depends on definitions: df-bi 117 df-dc 839 df-3or 984 df-3an 985 df-tru 1378 df-fal 1381 df-nf 1487 df-sb 1789 df-eu 2060 df-mo 2061 df-clab 2196 df-cleq 2202 df-clel 2205 df-nfc 2341 df-ne 2381 df-nel 2476 df-ral 2493 df-rex 2494 df-rab 2497 df-v 2781 df-sbc 3009 df-csb 3105 df-dif 3179 df-un 3181 df-in 3183 df-ss 3190 df-if 3583 df-pw 3631 df-sn 3652 df-pr 3653 df-op 3655 df-uni 3868 df-iun 3946 df-br 4063 df-opab 4125 df-mpt 4126 df-id 4361 df-xp 4702 df-rel 4703 df-cnv 4704 df-co 4705 df-dm 4706 df-rn 4707 df-res 4708 df-ima 4709 df-iota 5254 df-fun 5296 df-fn 5297 df-f 5298 df-fv 5302 df-ov 5977 df-oprab 5978 df-mpo 5979 df-1st 6256 df-2nd 6257 df-pnf 8151 df-mnf 8152 df-xr 8153 df-xadd 9937

This theorem is referenced by: xadd4d 10049 xleaddadd 10051 xrmaxaddlem 11737 xrmaxadd 11738 xrminadd 11752 xrbdtri 11753 bldisj 15040 xblss2ps 15043 xblss2 15044 comet 15138 bdxmet 15140 xmetxp 15146