MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xmul Unicode version

Definition df-xmul 10454
Description: Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
df-xmul  |-  x 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 ) ) ) ) )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-xmul
StepHypRef Expression
1 cxmu 10451 . 2  class  x e
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 8866 . . 3  class  RR*
52cv 1622 . . . . . 6  class  x
6 cc0 8737 . . . . . 6  class  0
75, 6wceq 1623 . . . . 5  wff  x  =  0
83cv 1622 . . . . . 6  class  y
98, 6wceq 1623 . . . . 5  wff  y  =  0
107, 9wo 357 . . . 4  wff  ( x  =  0  \/  y  =  0 )
11 clt 8867 . . . . . . . . 9  class  <
126, 8, 11wbr 4023 . . . . . . . 8  wff  0  <  y
13 cpnf 8864 . . . . . . . . 9  class  +oo
145, 13wceq 1623 . . . . . . . 8  wff  x  = 
+oo
1512, 14wa 358 . . . . . . 7  wff  ( 0  <  y  /\  x  =  +oo )
168, 6, 11wbr 4023 . . . . . . . 8  wff  y  <  0
17 cmnf 8865 . . . . . . . . 9  class  -oo
185, 17wceq 1623 . . . . . . . 8  wff  x  = 
-oo
1916, 18wa 358 . . . . . . 7  wff  ( y  <  0  /\  x  =  -oo )
2015, 19wo 357 . . . . . 6  wff  ( ( 0  <  y  /\  x  =  +oo )  \/  ( y  <  0  /\  x  =  -oo ) )
216, 5, 11wbr 4023 . . . . . . . 8  wff  0  <  x
228, 13wceq 1623 . . . . . . . 8  wff  y  = 
+oo
2321, 22wa 358 . . . . . . 7  wff  ( 0  <  x  /\  y  =  +oo )
245, 6, 11wbr 4023 . . . . . . . 8  wff  x  <  0
258, 17wceq 1623 . . . . . . . 8  wff  y  = 
-oo
2624, 25wa 358 . . . . . . 7  wff  ( x  <  0  /\  y  =  -oo )
2723, 26wo 357 . . . . . 6  wff  ( ( 0  <  x  /\  y  =  +oo )  \/  ( x  <  0  /\  y  =  -oo ) )
2820, 27wo 357 . . . . 5  wff  ( ( ( 0  <  y  /\  x  =  +oo )  \/  ( y  <  0  /\  x  = 
-oo ) )  \/  ( ( 0  < 
x  /\  y  =  +oo )  \/  (
x  <  0  /\  y  =  -oo ) ) )
2912, 18wa 358 . . . . . . . 8  wff  ( 0  <  y  /\  x  =  -oo )
3016, 14wa 358 . . . . . . . 8  wff  ( y  <  0  /\  x  =  +oo )
3129, 30wo 357 . . . . . . 7  wff  ( ( 0  <  y  /\  x  =  -oo )  \/  ( y  <  0  /\  x  =  +oo ) )
3221, 25wa 358 . . . . . . . 8  wff  ( 0  <  x  /\  y  =  -oo )
3324, 22wa 358 . . . . . . . 8  wff  ( x  <  0  /\  y  =  +oo )
3432, 33wo 357 . . . . . . 7  wff  ( ( 0  <  x  /\  y  =  -oo )  \/  ( x  <  0  /\  y  =  +oo ) )
3531, 34wo 357 . . . . . 6  wff  ( ( ( 0  <  y  /\  x  =  -oo )  \/  ( y  <  0  /\  x  = 
+oo ) )  \/  ( ( 0  < 
x  /\  y  =  -oo )  \/  (
x  <  0  /\  y  =  +oo ) ) )
36 cmul 8742 . . . . . . 7  class  x.
375, 8, 36co 5858 . . . . . 6  class  ( x  x.  y )
3835, 17, 37cif 3565 . . . . 5  class  if ( ( ( ( 0  <  y  /\  x  =  -oo )  \/  (
y  <  0  /\  x  =  +oo ) )  \/  ( ( 0  <  x  /\  y  =  -oo )  \/  (
x  <  0  /\  y  =  +oo ) ) ) ,  -oo , 
( x  x.  y
) )
3928, 13, 38cif 3565 . . . 4  class  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 ) ) )
4010, 6, 39cif 3565 . . 3  class  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 ) ) ) )
412, 3, 4, 4, 40cmpt2 5860 . 2  class  ( 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 ) ) ) ) )
421, 41wceq 1623 1  wff  x 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 ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  xmulval  10552  xmulf  10592
  Copyright terms: Public domain W3C validator