Theorem xaddf 12611

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 10682	. . . . . 6 ⊢ 0 ∈ ℝ*
2		pnfxr 10689	. . . . . 6 ⊢ +∞ ∈ ℝ*
3	1, 2	ifcli 4512	. . . . 5 ⊢ if(𝑦 = -∞, 0, +∞) ∈ ℝ*
4	3	a1i 11	. . . 4 ⊢ (((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ 𝑥 = +∞) → if(𝑦 = -∞, 0, +∞) ∈ ℝ*)
5		mnfxr 10692	. . . . . . 7 ⊢ -∞ ∈ ℝ*
6	1, 5	ifcli 4512	. . . . . 6 ⊢ if(𝑦 = +∞, 0, -∞) ∈ ℝ*
7	6	a1i 11	. . . . 5 ⊢ ((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ 𝑥 = -∞) → if(𝑦 = +∞, 0, -∞) ∈ ℝ*)
8	2	a1i 11	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ* ∧ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞)) ∧ 𝑦 ∈ ℝ*) ∧ 𝑦 = +∞) → +∞ ∈ ℝ*)
9	5	a1i 11	. . . . . . . . 9 ⊢ (((((𝑥 ∈ ℝ* ∧ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞)) ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑦 = +∞) ∧ 𝑦 = -∞) → -∞ ∈ ℝ*)
10		ioran 980	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑥 = +∞ ∨ 𝑥 = -∞) ↔ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞))
11		elxr 12505	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ* ↔ (𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞))
12		3orass 1086	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞) ↔ (𝑥 ∈ ℝ ∨ (𝑥 = +∞ ∨ 𝑥 = -∞)))
13	11, 12	sylbb 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ* → (𝑥 ∈ ℝ ∨ (𝑥 = +∞ ∨ 𝑥 = -∞)))
14	13	ord 860	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ* → (¬ 𝑥 ∈ ℝ → (𝑥 = +∞ ∨ 𝑥 = -∞)))
15	14	con1d 147	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ* → (¬ (𝑥 = +∞ ∨ 𝑥 = -∞) → 𝑥 ∈ ℝ))
16	15	imp 409	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ* ∧ ¬ (𝑥 = +∞ ∨ 𝑥 = -∞)) → 𝑥 ∈ ℝ)
17	10, 16	sylan2br 596	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ* ∧ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞)) → 𝑥 ∈ ℝ)
18		ioran 980	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑦 = +∞ ∨ 𝑦 = -∞) ↔ (¬ 𝑦 = +∞ ∧ ¬ 𝑦 = -∞))
19		elxr 12505	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ* ↔ (𝑦 ∈ ℝ ∨ 𝑦 = +∞ ∨ 𝑦 = -∞))
20		3orass 1086	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ℝ ∨ 𝑦 = +∞ ∨ 𝑦 = -∞) ↔ (𝑦 ∈ ℝ ∨ (𝑦 = +∞ ∨ 𝑦 = -∞)))
21	19, 20	sylbb 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℝ* → (𝑦 ∈ ℝ ∨ (𝑦 = +∞ ∨ 𝑦 = -∞)))
22	21	ord 860	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ* → (¬ 𝑦 ∈ ℝ → (𝑦 = +∞ ∨ 𝑦 = -∞)))
23	22	con1d 147	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ* → (¬ (𝑦 = +∞ ∨ 𝑦 = -∞) → 𝑦 ∈ ℝ))
24	23	imp 409	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ* ∧ ¬ (𝑦 = +∞ ∨ 𝑦 = -∞)) → 𝑦 ∈ ℝ)
25	18, 24	sylan2br 596	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ* ∧ (¬ 𝑦 = +∞ ∧ ¬ 𝑦 = -∞)) → 𝑦 ∈ ℝ)
26		readdcl 10614	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
27	17, 25, 26	syl2an 597	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ* ∧ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞)) ∧ (𝑦 ∈ ℝ* ∧ (¬ 𝑦 = +∞ ∧ ¬ 𝑦 = -∞))) → (𝑥 + 𝑦) ∈ ℝ)
28	27	rexrd 10685	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ* ∧ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞)) ∧ (𝑦 ∈ ℝ* ∧ (¬ 𝑦 = +∞ ∧ ¬ 𝑦 = -∞))) → (𝑥 + 𝑦) ∈ ℝ*)
29	28	anassrs 470	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ* ∧ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞)) ∧ 𝑦 ∈ ℝ*) ∧ (¬ 𝑦 = +∞ ∧ ¬ 𝑦 = -∞)) → (𝑥 + 𝑦) ∈ ℝ*)
30	29	anassrs 470	. . . . . . . . 9 ⊢ (((((𝑥 ∈ ℝ* ∧ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞)) ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑦 = -∞) → (𝑥 + 𝑦) ∈ ℝ*)
31	9, 30	ifclda 4500	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ* ∧ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞)) ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑦 = +∞) → if(𝑦 = -∞, -∞, (𝑥 + 𝑦)) ∈ ℝ*)
32	8, 31	ifclda 4500	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ* ∧ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞)) ∧ 𝑦 ∈ ℝ*) → if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))) ∈ ℝ*)
33	32	an32s 650	. . . . . 6 ⊢ (((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ (¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞)) → if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))) ∈ ℝ*)
34	33	anassrs 470	. . . . 5 ⊢ ((((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) ∧ ¬ 𝑥 = -∞) → if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))) ∈ ℝ*)
35	7, 34	ifclda 4500	. . . 4 ⊢ (((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) ∧ ¬ 𝑥 = +∞) → if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦)))) ∈ ℝ*)
36	4, 35	ifclda 4500	. . 3 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))) ∈ ℝ*)
37	36	rgen2 3203	. 2 ⊢ ∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ* if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))) ∈ ℝ*
38		df-xadd 12502	. . 3 ⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
39	38	fmpo 7760	. 2 ⊢ (∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ* if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))) ∈ ℝ* ↔ +𝑒 :(ℝ* × ℝ*)⟶ℝ*)
40	37, 39	mpbi 232	1 ⊢ +𝑒 :(ℝ* × ℝ*)⟶ℝ*

Syntax hints:  ¬ wn 3   ∧ wa 398   ∨ wo 843   ∨ w3o 1082   = wceq 1533   ∈ wcel 2110  ∀wral 3138  ifcif 4466   × cxp 5547  ⟶wf 6345  (class class class)co 7150  ℝcr 10530  0cc0 10531   + caddc 10534  +∞cpnf 10666  -∞cmnf 10667  ℝ^*cxr 10668   +_𝑒 cxad 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-1cn 10589  ax-addrcl 10592  ax-rnegex 10602  ax-cnre 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-oprab 7154  df-mpo 7155  df-1st 7683  df-2nd 7684  df-pnf 10671  df-mnf 10672  df-xr 10673  df-xadd 12502

This theorem is referenced by:  xaddcl  12626  xrsadd  20556  xrofsup  30486  xrge0pluscn  31178  xrge0tmdALT  31184