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

Definition df-segle 24137
Description: Define the segment length comparison relationship. This relationship expresses that the segment 
A B is no longer than  C D. In this section, we establish various properties of this relationship showing that it is a transitive, reflexive relationship on pairs of points that is substitutive under congruence. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 11-Oct-2013.)
Assertion
Ref Expression
df-segle  |-  Seg<_  =  { <. p ,  q >.  |  E. n  e.  NN  E. a  e.  ( EE
`  n ) E. b  e.  ( EE
`  n ) E. c  e.  ( EE
`  n ) E. d  e.  ( EE
`  n ) ( p  =  <. a ,  b >.  /\  q  =  <. c ,  d
>.  /\  E. y  e.  ( EE `  n
) ( y  Btwn  <.
c ,  d >.  /\  <. a ,  b
>.Cgr <. c ,  y
>. ) ) }
Distinct variable group:    q, p, n, a, b, c, d, y

Detailed syntax breakdown of Definition df-segle
StepHypRef Expression
1 csegle 24136 . 2  class  Seg<_
2 vp . . . . . . . . . . 11  set  p
32cv 1627 . . . . . . . . . 10  class  p
4 va . . . . . . . . . . . 12  set  a
54cv 1627 . . . . . . . . . . 11  class  a
6 vb . . . . . . . . . . . 12  set  b
76cv 1627 . . . . . . . . . . 11  class  b
85, 7cop 3644 . . . . . . . . . 10  class  <. a ,  b >.
93, 8wceq 1628 . . . . . . . . 9  wff  p  = 
<. a ,  b >.
10 vq . . . . . . . . . . 11  set  q
1110cv 1627 . . . . . . . . . 10  class  q
12 vc . . . . . . . . . . . 12  set  c
1312cv 1627 . . . . . . . . . . 11  class  c
14 vd . . . . . . . . . . . 12  set  d
1514cv 1627 . . . . . . . . . . 11  class  d
1613, 15cop 3644 . . . . . . . . . 10  class  <. c ,  d >.
1711, 16wceq 1628 . . . . . . . . 9  wff  q  = 
<. c ,  d >.
18 vy . . . . . . . . . . . . 13  set  y
1918cv 1627 . . . . . . . . . . . 12  class  y
20 cbtwn 23924 . . . . . . . . . . . 12  class  Btwn
2119, 16, 20wbr 4024 . . . . . . . . . . 11  wff  y  Btwn  <.
c ,  d >.
2213, 19cop 3644 . . . . . . . . . . . 12  class  <. c ,  y >.
23 ccgr 23925 . . . . . . . . . . . 12  class Cgr
248, 22, 23wbr 4024 . . . . . . . . . . 11  wff  <. a ,  b >.Cgr <. c ,  y >.
2521, 24wa 360 . . . . . . . . . 10  wff  ( y 
Btwn  <. c ,  d
>.  /\  <. a ,  b
>.Cgr <. c ,  y
>. )
26 vn . . . . . . . . . . . 12  set  n
2726cv 1627 . . . . . . . . . . 11  class  n
28 cee 23923 . . . . . . . . . . 11  class  EE
2927, 28cfv 5221 . . . . . . . . . 10  class  ( EE
`  n )
3025, 18, 29wrex 2545 . . . . . . . . 9  wff  E. y  e.  ( EE `  n
) ( y  Btwn  <.
c ,  d >.  /\  <. a ,  b
>.Cgr <. c ,  y
>. )
319, 17, 30w3a 939 . . . . . . . 8  wff  ( p  =  <. a ,  b
>.  /\  q  =  <. c ,  d >.  /\  E. y  e.  ( EE `  n ) ( y 
Btwn  <. c ,  d
>.  /\  <. a ,  b
>.Cgr <. c ,  y
>. ) )
3231, 14, 29wrex 2545 . . . . . . 7  wff  E. d  e.  ( EE `  n
) ( p  = 
<. a ,  b >.  /\  q  =  <. c ,  d >.  /\  E. y  e.  ( EE `  n ) ( y 
Btwn  <. c ,  d
>.  /\  <. a ,  b
>.Cgr <. c ,  y
>. ) )
3332, 12, 29wrex 2545 . . . . . 6  wff  E. c  e.  ( EE `  n
) E. d  e.  ( EE `  n
) ( p  = 
<. a ,  b >.  /\  q  =  <. c ,  d >.  /\  E. y  e.  ( EE `  n ) ( y 
Btwn  <. c ,  d
>.  /\  <. a ,  b
>.Cgr <. c ,  y
>. ) )
3433, 6, 29wrex 2545 . . . . 5  wff  E. b  e.  ( EE `  n
) E. c  e.  ( EE `  n
) E. d  e.  ( EE `  n
) ( p  = 
<. a ,  b >.  /\  q  =  <. c ,  d >.  /\  E. y  e.  ( EE `  n ) ( y 
Btwn  <. c ,  d
>.  /\  <. a ,  b
>.Cgr <. c ,  y
>. ) )
3534, 4, 29wrex 2545 . . . 4  wff  E. a  e.  ( EE `  n
) E. b  e.  ( EE `  n
) E. c  e.  ( EE `  n
) E. d  e.  ( EE `  n
) ( p  = 
<. a ,  b >.  /\  q  =  <. c ,  d >.  /\  E. y  e.  ( EE `  n ) ( y 
Btwn  <. c ,  d
>.  /\  <. a ,  b
>.Cgr <. c ,  y
>. ) )
36 cn 9741 . . . 4  class  NN
3735, 26, 36wrex 2545 . . 3  wff  E. n  e.  NN  E. a  e.  ( EE `  n
) E. b  e.  ( EE `  n
) E. c  e.  ( EE `  n
) E. d  e.  ( EE `  n
) ( p  = 
<. a ,  b >.  /\  q  =  <. c ,  d >.  /\  E. y  e.  ( EE `  n ) ( y 
Btwn  <. c ,  d
>.  /\  <. a ,  b
>.Cgr <. c ,  y
>. ) )
3837, 2, 10copab 4077 . 2  class  { <. p ,  q >.  |  E. n  e.  NN  E. a  e.  ( EE `  n
) E. b  e.  ( EE `  n
) E. c  e.  ( EE `  n
) E. d  e.  ( EE `  n
) ( p  = 
<. a ,  b >.  /\  q  =  <. c ,  d >.  /\  E. y  e.  ( EE `  n ) ( y 
Btwn  <. c ,  d
>.  /\  <. a ,  b
>.Cgr <. c ,  y
>. ) ) }
391, 38wceq 1628 1  wff  Seg<_  =  { <. p ,  q >.  |  E. n  e.  NN  E. a  e.  ( EE
`  n ) E. b  e.  ( EE
`  n ) E. c  e.  ( EE
`  n ) E. d  e.  ( EE
`  n ) ( p  =  <. a ,  b >.  /\  q  =  <. c ,  d
>.  /\  E. y  e.  ( EE `  n
) ( y  Btwn  <.
c ,  d >.  /\  <. a ,  b
>.Cgr <. c ,  y
>. ) ) }
Colors of variables: wff set class
This definition is referenced by:  brsegle  24138
  Copyright terms: Public domain W3C validator