Metamath Proof Explorer

Theorem xaddf

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

Ref Expression
Assertion xaddf 
|- +e : ( RR* X. RR* ) --> RR*

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 pnfxr 
 |-  +oo e. RR*
3 1 2 ifcli 
 |-  if ( y = -oo , 0 , +oo ) e. RR*
4 3 a1i 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ x = +oo ) -> if ( y = -oo , 0 , +oo ) e. RR* )
5 mnfxr 
 |-  -oo e. RR*
6 1 5 ifcli 
 |-  if ( y = +oo , 0 , -oo ) e. RR*
7 6 a1i 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ -. x = +oo ) /\ x = -oo ) -> if ( y = +oo , 0 , -oo ) e. RR* )
8 2 a1i 
 |-  ( ( ( ( x e. RR* /\ ( -. x = +oo /\ -. x = -oo ) ) /\ y e. RR* ) /\ y = +oo ) -> +oo e. RR* )
9 5 a1i 
 |-  ( ( ( ( ( x e. RR* /\ ( -. x = +oo /\ -. x = -oo ) ) /\ y e. RR* ) /\ -. y = +oo ) /\ y = -oo ) -> -oo e. RR* )
10 ioran 
 |-  ( -. ( x = +oo \/ x = -oo ) <-> ( -. x = +oo /\ -. x = -oo ) )
11 elxr 
 |-  ( x e. RR* <-> ( x e. RR \/ x = +oo \/ x = -oo ) )
12 3orass 
 |-  ( ( x e. RR \/ x = +oo \/ x = -oo ) <-> ( x e. RR \/ ( x = +oo \/ x = -oo ) ) )
13 11 12 sylbb 
 |-  ( x e. RR* -> ( x e. RR \/ ( x = +oo \/ x = -oo ) ) )
14 13 ord 
 |-  ( x e. RR* -> ( -. x e. RR -> ( x = +oo \/ x = -oo ) ) )
15 14 con1d 
 |-  ( x e. RR* -> ( -. ( x = +oo \/ x = -oo ) -> x e. RR ) )
16 15 imp 
 |-  ( ( x e. RR* /\ -. ( x = +oo \/ x = -oo ) ) -> x e. RR )
17 10 16 sylan2br 
 |-  ( ( x e. RR* /\ ( -. x = +oo /\ -. x = -oo ) ) -> x e. RR )
18 ioran 
 |-  ( -. ( y = +oo \/ y = -oo ) <-> ( -. y = +oo /\ -. y = -oo ) )
19 elxr 
 |-  ( y e. RR* <-> ( y e. RR \/ y = +oo \/ y = -oo ) )
20 3orass 
 |-  ( ( y e. RR \/ y = +oo \/ y = -oo ) <-> ( y e. RR \/ ( y = +oo \/ y = -oo ) ) )
21 19 20 sylbb 
 |-  ( y e. RR* -> ( y e. RR \/ ( y = +oo \/ y = -oo ) ) )
22 21 ord 
 |-  ( y e. RR* -> ( -. y e. RR -> ( y = +oo \/ y = -oo ) ) )
23 22 con1d 
 |-  ( y e. RR* -> ( -. ( y = +oo \/ y = -oo ) -> y e. RR ) )
24 23 imp 
 |-  ( ( y e. RR* /\ -. ( y = +oo \/ y = -oo ) ) -> y e. RR )
25 18 24 sylan2br 
 |-  ( ( y e. RR* /\ ( -. y = +oo /\ -. y = -oo ) ) -> y e. RR )
26 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
27 17 25 26 syl2an 
 |-  ( ( ( x e. RR* /\ ( -. x = +oo /\ -. x = -oo ) ) /\ ( y e. RR* /\ ( -. y = +oo /\ -. y = -oo ) ) ) -> ( x + y ) e. RR )
28 27 rexrd 
 |-  ( ( ( x e. RR* /\ ( -. x = +oo /\ -. x = -oo ) ) /\ ( y e. RR* /\ ( -. y = +oo /\ -. y = -oo ) ) ) -> ( x + y ) e. RR* )
29 28 anassrs 
 |-  ( ( ( ( x e. RR* /\ ( -. x = +oo /\ -. x = -oo ) ) /\ y e. RR* ) /\ ( -. y = +oo /\ -. y = -oo ) ) -> ( x + y ) e. RR* )
30 29 anassrs 
 |-  ( ( ( ( ( x e. RR* /\ ( -. x = +oo /\ -. x = -oo ) ) /\ y e. RR* ) /\ -. y = +oo ) /\ -. y = -oo ) -> ( x + y ) e. RR* )
31 9 30 ifclda 
 |-  ( ( ( ( x e. RR* /\ ( -. x = +oo /\ -. x = -oo ) ) /\ y e. RR* ) /\ -. y = +oo ) -> if ( y = -oo , -oo , ( x + y ) ) e. RR* )
32 8 31 ifclda 
 |-  ( ( ( x e. RR* /\ ( -. x = +oo /\ -. x = -oo ) ) /\ y e. RR* ) -> if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) e. RR* )
33 32 an32s 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ ( -. x = +oo /\ -. x = -oo ) ) -> if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) e. RR* )
34 33 anassrs 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ -. x = +oo ) /\ -. x = -oo ) -> if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) e. RR* )
35 7 34 ifclda 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ -. x = +oo ) -> if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) e. RR* )
36 4 35 ifclda 
 |-  ( ( x e. RR* /\ y e. RR* ) -> if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) ) e. RR* )
37 36 rgen2 
 |-  A. x e. RR* A. y e. RR* if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) ) e. RR*
38 df-xadd 
 |-  +e = ( x e. RR* , y e. RR* |-> if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) ) )
39 38 fmpo 
 |-  ( A. x e. RR* A. y e. RR* if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) ) e. RR* <-> +e : ( RR* X. RR* ) --> RR* )
40 37 39 mpbi 
 |-  +e : ( RR* X. RR* ) --> RR*