ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-xmul Unicode version

Definition df-xmul 9529
Description: Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
df-xmul  |-  xe  =  ( 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 9526 . 2  class  xe
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cxr 7767 . . 3  class  RR*
52cv 1315 . . . . . 6  class  x
6 cc0 7588 . . . . . 6  class  0
75, 6wceq 1316 . . . . 5  wff  x  =  0
83cv 1315 . . . . . 6  class  y
98, 6wceq 1316 . . . . 5  wff  y  =  0
107, 9wo 682 . . . 4  wff  ( x  =  0  \/  y  =  0 )
11 clt 7768 . . . . . . . . 9  class  <
126, 8, 11wbr 3899 . . . . . . . 8  wff  0  <  y
13 cpnf 7765 . . . . . . . . 9  class +oo
145, 13wceq 1316 . . . . . . . 8  wff  x  = +oo
1512, 14wa 103 . . . . . . 7  wff  ( 0  <  y  /\  x  = +oo )
168, 6, 11wbr 3899 . . . . . . . 8  wff  y  <  0
17 cmnf 7766 . . . . . . . . 9  class -oo
185, 17wceq 1316 . . . . . . . 8  wff  x  = -oo
1916, 18wa 103 . . . . . . 7  wff  ( y  <  0  /\  x  = -oo )
2015, 19wo 682 . . . . . 6  wff  ( ( 0  <  y  /\  x  = +oo )  \/  ( y  <  0  /\  x  = -oo ) )
216, 5, 11wbr 3899 . . . . . . . 8  wff  0  <  x
228, 13wceq 1316 . . . . . . . 8  wff  y  = +oo
2321, 22wa 103 . . . . . . 7  wff  ( 0  <  x  /\  y  = +oo )
245, 6, 11wbr 3899 . . . . . . . 8  wff  x  <  0
258, 17wceq 1316 . . . . . . . 8  wff  y  = -oo
2624, 25wa 103 . . . . . . 7  wff  ( x  <  0  /\  y  = -oo )
2723, 26wo 682 . . . . . 6  wff  ( ( 0  <  x  /\  y  = +oo )  \/  ( x  <  0  /\  y  = -oo ) )
2820, 27wo 682 . . . . 5  wff  ( ( ( 0  <  y  /\  x  = +oo )  \/  ( y  <  0  /\  x  = -oo ) )  \/  ( ( 0  < 
x  /\  y  = +oo )  \/  (
x  <  0  /\  y  = -oo )
) )
2912, 18wa 103 . . . . . . . 8  wff  ( 0  <  y  /\  x  = -oo )
3016, 14wa 103 . . . . . . . 8  wff  ( y  <  0  /\  x  = +oo )
3129, 30wo 682 . . . . . . 7  wff  ( ( 0  <  y  /\  x  = -oo )  \/  ( y  <  0  /\  x  = +oo ) )
3221, 25wa 103 . . . . . . . 8  wff  ( 0  <  x  /\  y  = -oo )
3324, 22wa 103 . . . . . . . 8  wff  ( x  <  0  /\  y  = +oo )
3432, 33wo 682 . . . . . . 7  wff  ( ( 0  <  x  /\  y  = -oo )  \/  ( x  <  0  /\  y  = +oo ) )
3531, 34wo 682 . . . . . 6  wff  ( ( ( 0  <  y  /\  x  = -oo )  \/  ( y  <  0  /\  x  = +oo ) )  \/  ( ( 0  < 
x  /\  y  = -oo )  \/  (
x  <  0  /\  y  = +oo )
) )
36 cmul 7593 . . . . . . 7  class  x.
375, 8, 36co 5742 . . . . . 6  class  ( x  x.  y )
3835, 17, 37cif 3444 . . . . 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 3444 . . . 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 3444 . . 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, 40cmpo 5744 . 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 1316 1  wff  xe  =  ( 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: (None)
  Copyright terms: Public domain W3C validator