Metamath Proof Explorer

Theorem btwnsegle

Description: If B falls between A and C , then A B is no longer than A C . (Contributed by Scott Fenton, 16-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion btwnsegle 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. -> <. A , B >. Seg<_ <. A , C >. ) )

Proof

Step Hyp Ref Expression
1 simplr2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ B Btwn <. A , C >. ) -> B e. ( EE ` N ) )
2 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ B Btwn <. A , C >. ) -> B Btwn <. A , C >. )
3 simpl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> N e. NN )
4 simpr1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
5 simpr2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
6 3 4 5 cgrrflxd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> <. A , B >. Cgr <. A , B >. )
7 6 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ B Btwn <. A , C >. ) -> <. A , B >. Cgr <. A , B >. )
8 breq1 
 |-  ( x = B -> ( x Btwn <. A , C >. <-> B Btwn <. A , C >. ) )
9 opeq2 
 |-  ( x = B -> <. A , x >. = <. A , B >. )
10 9 breq2d 
 |-  ( x = B -> ( <. A , B >. Cgr <. A , x >. <-> <. A , B >. Cgr <. A , B >. ) )
11 8 10 anbi12d 
 |-  ( x = B -> ( ( x Btwn <. A , C >. /\ <. A , B >. Cgr <. A , x >. ) <-> ( B Btwn <. A , C >. /\ <. A , B >. Cgr <. A , B >. ) ) )
12 11 rspcev 
 |-  ( ( B e. ( EE ` N ) /\ ( B Btwn <. A , C >. /\ <. A , B >. Cgr <. A , B >. ) ) -> E. x e. ( EE ` N ) ( x Btwn <. A , C >. /\ <. A , B >. Cgr <. A , x >. ) )
13 1 2 7 12 syl12anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ B Btwn <. A , C >. ) -> E. x e. ( EE ` N ) ( x Btwn <. A , C >. /\ <. A , B >. Cgr <. A , x >. ) )
14 simpr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
15 brsegle 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. A , C >. <-> E. x e. ( EE ` N ) ( x Btwn <. A , C >. /\ <. A , B >. Cgr <. A , x >. ) ) )
16 3 4 5 4 14 15 syl122anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. A , C >. <-> E. x e. ( EE ` N ) ( x Btwn <. A , C >. /\ <. A , B >. Cgr <. A , x >. ) ) )
17 16 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ B Btwn <. A , C >. ) -> ( <. A , B >. Seg<_ <. A , C >. <-> E. x e. ( EE ` N ) ( x Btwn <. A , C >. /\ <. A , B >. Cgr <. A , x >. ) ) )
18 13 17 mpbird 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ B Btwn <. A , C >. ) -> <. A , B >. Seg<_ <. A , C >. )
19 18 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. -> <. A , B >. Seg<_ <. A , C >. ) )