Theorem xaddf 9801

Description: The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)

Assertion

Ref	Expression
xaddf	⊢ +𝑒 :(ℝ* × ℝ*)⟶ℝ*

Proof of Theorem xaddf

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0xr 7966	. . . . . . 7 ⊢ 0 ∈ ℝ*
2	1	a1i 9	. . . . . 6 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → 0 ∈ ℝ*)
3		pnfxr 7972	. . . . . . 7 ⊢ +∞ ∈ ℝ*
4	3	a1i 9	. . . . . 6 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → +∞ ∈ ℝ*)
5		xrmnfdc 9800	. . . . . . 7 ⊢ (𝑦 ∈ ℝ* → DECID 𝑦 = -∞)
6	5	adantl 275	. . . . . 6 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → DECID 𝑦 = -∞)
7	2, 4, 6	ifcldcd 3561	. . . . 5 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(𝑦 = -∞, 0, +∞) ∈ ℝ*)
8	7	adantr 274	. . . 4 ⊢ (((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 = +∞) → if(𝑦 = -∞, 0, +∞) ∈ ℝ*)
9	1	a1i 9	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ 𝑥 = -∞) → 0 ∈ ℝ*)
10		mnfxr 7976	. . . . . . 7 ⊢ -∞ ∈ ℝ*
11	10	a1i 9	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ 𝑥 = -∞) → -∞ ∈ ℝ*)
12		xrpnfdc 9799	. . . . . . 7 ⊢ (𝑦 ∈ ℝ* → DECID 𝑦 = +∞)
13	12	ad3antlr 490	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ 𝑥 = -∞) → DECID 𝑦 = +∞)
14	9, 11, 13	ifcldcd 3561	. . . . 5 ⊢ ((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ 𝑥 = -∞) → if(𝑦 = +∞, 0, -∞) ∈ ℝ*)
15	3	a1i 9	. . . . . 6 ⊢ (((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ 𝑦 = +∞) → +∞ ∈ ℝ*)
16	10	a1i 9	. . . . . . 7 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ 𝑦 = -∞) → -∞ ∈ ℝ*)
17		simp-4r 537	. . . . . . . . . 10 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → ¬ 𝑥 = +∞)
18		simp-5l 538	. . . . . . . . . . 11 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → 𝑥 ∈ ℝ*)
19		simpllr 529	. . . . . . . . . . . 12 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → ¬ 𝑥 = -∞)
20	19	neqned 2347	. . . . . . . . . . 11 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → 𝑥 ≠ -∞)
21		xrnemnf 9734	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞) ↔ (𝑥 ∈ ℝ ∨ 𝑥 = +∞))
22	21	biimpi 119	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞) → (𝑥 ∈ ℝ ∨ 𝑥 = +∞))
23	18, 20, 22	syl2anc 409	. . . . . . . . . 10 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → (𝑥 ∈ ℝ ∨ 𝑥 = +∞))
24	17, 23	ecased 1344	. . . . . . . . 9 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → 𝑥 ∈ ℝ)
25		simplr 525	. . . . . . . . . 10 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → ¬ 𝑦 = +∞)
26		simp-5r 539	. . . . . . . . . . 11 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → 𝑦 ∈ ℝ*)
27		neqne 2348	. . . . . . . . . . . 12 ⊢ (¬ 𝑦 = -∞ → 𝑦 ≠ -∞)
28	27	adantl 275	. . . . . . . . . . 11 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → 𝑦 ≠ -∞)
29		xrnemnf 9734	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ* ∧ 𝑦 ≠ -∞) ↔ (𝑦 ∈ ℝ ∨ 𝑦 = +∞))
30	29	biimpi 119	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ* ∧ 𝑦 ≠ -∞) → (𝑦 ∈ ℝ ∨ 𝑦 = +∞))
31	26, 28, 30	syl2anc 409	. . . . . . . . . 10 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → (𝑦 ∈ ℝ ∨ 𝑦 = +∞))
32	25, 31	ecased 1344	. . . . . . . . 9 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → 𝑦 ∈ ℝ)
33	24, 32	readdcld 7949	. . . . . . . 8 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → (𝑥 + 𝑦) ∈ ℝ)
34	33	rexrd 7969	. . . . . . 7 ⊢ ((((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → (𝑥 + 𝑦) ∈ ℝ*)
35	6	ad3antrrr 489	. . . . . . 7 ⊢ (((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) → DECID 𝑦 = -∞)
36	16, 34, 35	ifcldadc 3555	. . . . . 6 ⊢ (((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) ∧ ¬ 𝑦 = +∞) → if(𝑦 = -∞, -∞, (𝑥 + 𝑦)) ∈ ℝ*)
37	12	ad3antlr 490	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) → DECID 𝑦 = +∞)
38	15, 36, 37	ifcldadc 3555	. . . . 5 ⊢ ((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) → if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))) ∈ ℝ*)
39		xrmnfdc 9800	. . . . . 6 ⊢ (𝑥 ∈ ℝ* → DECID 𝑥 = -∞)
40	39	ad2antrr 485	. . . . 5 ⊢ (((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) → DECID 𝑥 = -∞)
41	14, 38, 40	ifcldadc 3555	. . . 4 ⊢ (((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) → if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦)))) ∈ ℝ*)
42		xrpnfdc 9799	. . . . 5 ⊢ (𝑥 ∈ ℝ* → DECID 𝑥 = +∞)
43	42	adantr 274	. . . 4 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → DECID 𝑥 = +∞)
44	8, 41, 43	ifcldadc 3555	. . 3 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))) ∈ ℝ*)
45	44	rgen2a 2524	. 2 ⊢ ∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ* if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))) ∈ ℝ*
46		df-xadd 9730	. . 3 ⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
47	46	fmpo 6180	. 2 ⊢ (∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ* if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))) ∈ ℝ* ↔ +𝑒 :(ℝ* × ℝ*)⟶ℝ*)
48	45, 47	mpbi 144	1 ⊢ +𝑒 :(ℝ* × ℝ*)⟶ℝ*

Syntax hints:  ¬ wn 3   ∧ wa 103   ∨ wo 703  DECID wdc 829   = wceq 1348   ∈ wcel 2141   ≠ wne 2340  ∀wral 2448  ifcif 3526   × cxp 4609  ⟶wf 5194  (class class class)co 5853  ℝcr 7773  0cc0 7774   + caddc 7777  +∞cpnf 7951  -∞cmnf 7952  ℝ^*cxr 7953   +_𝑒 cxad 9727

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-cnex 7865  ax-resscn 7866  ax-1re 7868  ax-addrcl 7871  ax-rnegex 7883

This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-fv 5206  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-pnf 7956  df-mnf 7957  df-xr 7958  df-xadd 9730

This theorem is referenced by:  xaddcl  9817