Metamath Proof Explorer

Theorem xmulf

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

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

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 1 a1i 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ ( x = 0 \/ y = 0 ) ) -> 0 e. RR* )
3 pnfxr 
 |-  +oo e. RR*
4 3 a1i 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ -. ( x = 0 \/ y = 0 ) ) /\ ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) ) -> +oo e. RR* )
5 mnfxr 
 |-  -oo e. RR*
6 5 a1i 
 |-  ( ( ( ( ( x e. RR* /\ y e. RR* ) /\ -. ( x = 0 \/ y = 0 ) ) /\ -. ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) ) /\ ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) ) -> -oo e. RR* )
7 xmullem 
 |-  ( ( ( ( ( x e. RR* /\ y e. RR* ) /\ -. ( x = 0 \/ y = 0 ) ) /\ -. ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) ) /\ -. ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) ) -> x e. RR )
8 ancom 
 |-  ( ( x e. RR* /\ y e. RR* ) <-> ( y e. RR* /\ x e. RR* ) )
9 orcom 
 |-  ( ( x = 0 \/ y = 0 ) <-> ( y = 0 \/ x = 0 ) )
10 9 notbii 
 |-  ( -. ( x = 0 \/ y = 0 ) <-> -. ( y = 0 \/ x = 0 ) )
11 8 10 anbi12i 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ -. ( x = 0 \/ y = 0 ) ) <-> ( ( y e. RR* /\ x e. RR* ) /\ -. ( y = 0 \/ x = 0 ) ) )
12 orcom 
 |-  ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) <-> ( ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) \/ ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) ) )
13 12 notbii 
 |-  ( -. ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) <-> -. ( ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) \/ ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) ) )
14 11 13 anbi12i 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ -. ( x = 0 \/ y = 0 ) ) /\ -. ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) ) <-> ( ( ( y e. RR* /\ x e. RR* ) /\ -. ( y = 0 \/ x = 0 ) ) /\ -. ( ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) \/ ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) ) ) )
15 orcom 
 |-  ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) <-> ( ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) \/ ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) ) )
16 15 notbii 
 |-  ( -. ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) <-> -. ( ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) \/ ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) ) )
17 xmullem 
 |-  ( ( ( ( ( y e. RR* /\ x e. RR* ) /\ -. ( y = 0 \/ x = 0 ) ) /\ -. ( ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) \/ ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) ) ) /\ -. ( ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) \/ ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) ) ) -> y e. RR )
18 14 16 17 syl2anb 
 |-  ( ( ( ( ( x e. RR* /\ y e. RR* ) /\ -. ( x = 0 \/ y = 0 ) ) /\ -. ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) ) /\ -. ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) ) -> y e. RR )
19 7 18 remulcld 
 |-  ( ( ( ( ( x e. RR* /\ y e. RR* ) /\ -. ( x = 0 \/ y = 0 ) ) /\ -. ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) ) /\ -. ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) ) -> ( x x. y ) e. RR )
20 19 rexrd 
 |-  ( ( ( ( ( x e. RR* /\ y e. RR* ) /\ -. ( x = 0 \/ y = 0 ) ) /\ -. ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) ) /\ -. ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) ) -> ( x x. y ) e. RR* )
21 6 20 ifclda 
 |-  ( ( ( ( x e. RR* /\ y e. RR* ) /\ -. ( x = 0 \/ y = 0 ) ) /\ -. ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) ) -> if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) e. RR* )
22 4 21 ifclda 
 |-  ( ( ( x e. RR* /\ y e. RR* ) /\ -. ( x = 0 \/ y = 0 ) ) -> if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) e. RR* )
23 2 22 ifclda 
 |-  ( ( x e. RR* /\ y e. RR* ) -> if ( ( x = 0 \/ y = 0 ) , 0 , if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) ) e. RR* )
24 23 rgen2 
 |-  A. x e. RR* A. y e. RR* if ( ( x = 0 \/ y = 0 ) , 0 , if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) ) e. RR*
25 df-xmul 
 |-  *e = ( x e. RR* , y e. RR* |-> if ( ( x = 0 \/ y = 0 ) , 0 , if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) ) )
26 25 fmpo 
 |-  ( A. x e. RR* A. y e. RR* if ( ( x = 0 \/ y = 0 ) , 0 , if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) ) e. RR* <-> *e : ( RR* X. RR* ) --> RR* )
27 24 26 mpbi 
 |-  *e : ( RR* X. RR* ) --> RR*