Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-btwn Unicode version

Definition df-btwn 24520
Description: Define the Euclidean betweenness predicate. For details, see brbtwn 24527. (Contributed by Scott Fenton, 3-Jun-2013.)
Assertion
Ref Expression
df-btwn  |-  Btwn  =  `' { <. <. x ,  z
>. ,  y >.  |  E. n  e.  NN  ( ( x  e.  ( EE `  n
)  /\  z  e.  ( EE `  n )  /\  y  e.  ( EE `  n ) )  /\  E. t  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... n
) ( y `  i )  =  ( ( ( 1  -  t )  x.  (
x `  i )
)  +  ( t  x.  ( z `  i ) ) ) ) }
Distinct variable group:    x, n, y, z, t, i

Detailed syntax breakdown of Definition df-btwn
StepHypRef Expression
1 cbtwn 24517 . 2  class  Btwn
2 vx . . . . . . . . 9  set  x
32cv 1622 . . . . . . . 8  class  x
4 vn . . . . . . . . . 10  set  n
54cv 1622 . . . . . . . . 9  class  n
6 cee 24516 . . . . . . . . 9  class  EE
75, 6cfv 5255 . . . . . . . 8  class  ( EE
`  n )
83, 7wcel 1684 . . . . . . 7  wff  x  e.  ( EE `  n
)
9 vz . . . . . . . . 9  set  z
109cv 1622 . . . . . . . 8  class  z
1110, 7wcel 1684 . . . . . . 7  wff  z  e.  ( EE `  n
)
12 vy . . . . . . . . 9  set  y
1312cv 1622 . . . . . . . 8  class  y
1413, 7wcel 1684 . . . . . . 7  wff  y  e.  ( EE `  n
)
158, 11, 14w3a 934 . . . . . 6  wff  ( x  e.  ( EE `  n )  /\  z  e.  ( EE `  n
)  /\  y  e.  ( EE `  n ) )
16 vi . . . . . . . . . . 11  set  i
1716cv 1622 . . . . . . . . . 10  class  i
1817, 13cfv 5255 . . . . . . . . 9  class  ( y `
 i )
19 c1 8738 . . . . . . . . . . . 12  class  1
20 vt . . . . . . . . . . . . 13  set  t
2120cv 1622 . . . . . . . . . . . 12  class  t
22 cmin 9037 . . . . . . . . . . . 12  class  -
2319, 21, 22co 5858 . . . . . . . . . . 11  class  ( 1  -  t )
2417, 3cfv 5255 . . . . . . . . . . 11  class  ( x `
 i )
25 cmul 8742 . . . . . . . . . . 11  class  x.
2623, 24, 25co 5858 . . . . . . . . . 10  class  ( ( 1  -  t )  x.  ( x `  i ) )
2717, 10cfv 5255 . . . . . . . . . . 11  class  ( z `
 i )
2821, 27, 25co 5858 . . . . . . . . . 10  class  ( t  x.  ( z `  i ) )
29 caddc 8740 . . . . . . . . . 10  class  +
3026, 28, 29co 5858 . . . . . . . . 9  class  ( ( ( 1  -  t
)  x.  ( x `
 i ) )  +  ( t  x.  ( z `  i
) ) )
3118, 30wceq 1623 . . . . . . . 8  wff  ( y `
 i )  =  ( ( ( 1  -  t )  x.  ( x `  i
) )  +  ( t  x.  ( z `
 i ) ) )
32 cfz 10782 . . . . . . . . 9  class  ...
3319, 5, 32co 5858 . . . . . . . 8  class  ( 1 ... n )
3431, 16, 33wral 2543 . . . . . . 7  wff  A. i  e.  ( 1 ... n
) ( y `  i )  =  ( ( ( 1  -  t )  x.  (
x `  i )
)  +  ( t  x.  ( z `  i ) ) )
35 cc0 8737 . . . . . . . 8  class  0
36 cicc 10659 . . . . . . . 8  class  [,]
3735, 19, 36co 5858 . . . . . . 7  class  ( 0 [,] 1 )
3834, 20, 37wrex 2544 . . . . . 6  wff  E. t  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... n
) ( y `  i )  =  ( ( ( 1  -  t )  x.  (
x `  i )
)  +  ( t  x.  ( z `  i ) ) )
3915, 38wa 358 . . . . 5  wff  ( ( x  e.  ( EE
`  n )  /\  z  e.  ( EE `  n )  /\  y  e.  ( EE `  n
) )  /\  E. t  e.  ( 0 [,] 1 ) A. i  e.  ( 1 ... n ) ( y `  i )  =  ( ( ( 1  -  t )  x.  ( x `  i ) )  +  ( t  x.  (
z `  i )
) ) )
40 cn 9746 . . . . 5  class  NN
4139, 4, 40wrex 2544 . . . 4  wff  E. n  e.  NN  ( ( x  e.  ( EE `  n )  /\  z  e.  ( EE `  n
)  /\  y  e.  ( EE `  n ) )  /\  E. t  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... n
) ( y `  i )  =  ( ( ( 1  -  t )  x.  (
x `  i )
)  +  ( t  x.  ( z `  i ) ) ) )
4241, 2, 9, 12coprab 5859 . . 3  class  { <. <.
x ,  z >. ,  y >.  |  E. n  e.  NN  (
( x  e.  ( EE `  n )  /\  z  e.  ( EE `  n )  /\  y  e.  ( EE `  n ) )  /\  E. t  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... n
) ( y `  i )  =  ( ( ( 1  -  t )  x.  (
x `  i )
)  +  ( t  x.  ( z `  i ) ) ) ) }
4342ccnv 4688 . 2  class  `' { <. <. x ,  z
>. ,  y >.  |  E. n  e.  NN  ( ( x  e.  ( EE `  n
)  /\  z  e.  ( EE `  n )  /\  y  e.  ( EE `  n ) )  /\  E. t  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... n
) ( y `  i )  =  ( ( ( 1  -  t )  x.  (
x `  i )
)  +  ( t  x.  ( z `  i ) ) ) ) }
441, 43wceq 1623 1  wff  Btwn  =  `' { <. <. x ,  z
>. ,  y >.  |  E. n  e.  NN  ( ( x  e.  ( EE `  n
)  /\  z  e.  ( EE `  n )  /\  y  e.  ( EE `  n ) )  /\  E. t  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... n
) ( y `  i )  =  ( ( ( 1  -  t )  x.  (
x `  i )
)  +  ( t  x.  ( z `  i ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  brbtwn  24527
  Copyright terms: Public domain W3C validator