Metamath Proof Explorer

Theorem axsegconlem7

Description: Lemma for axsegcon . Show that a particular ratio of distances is in the closed unit interval. (Contributed by Scott Fenton, 18-Sep-2013)

Ref Expression
Hypotheses axsegconlem2.1 
|- S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
axsegconlem7.2 
|- T = sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 )
Assertion axsegconlem7 
|- ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) e. ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 
 |-  S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
2 axsegconlem7.2 
 |-  T = sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 )
3 2 axsegconlem5 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> 0 <_ ( sqrt ` T ) )
4 3 adantl 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> 0 <_ ( sqrt ` T ) )
5 1 axsegconlem4 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sqrt ` S ) e. RR )
6 5 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) e. RR )
7 2 axsegconlem4 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( sqrt ` T ) e. RR )
8 addge01 
 |-  ( ( ( sqrt ` S ) e. RR /\ ( sqrt ` T ) e. RR ) -> ( 0 <_ ( sqrt ` T ) <-> ( sqrt ` S ) <_ ( ( sqrt ` S ) + ( sqrt ` T ) ) ) )
9 6 7 8 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( 0 <_ ( sqrt ` T ) <-> ( sqrt ` S ) <_ ( ( sqrt ` S ) + ( sqrt ` T ) ) ) )
10 4 9 mpbid 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( sqrt ` S ) <_ ( ( sqrt ` S ) + ( sqrt ` T ) ) )
11 6 adantr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( sqrt ` S ) e. RR )
12 1 axsegconlem5 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ ( sqrt ` S ) )
13 12 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 <_ ( sqrt ` S ) )
14 13 adantr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> 0 <_ ( sqrt ` S ) )
15 readdcl 
 |-  ( ( ( sqrt ` S ) e. RR /\ ( sqrt ` T ) e. RR ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) e. RR )
16 6 7 15 syl2an 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) e. RR )
17 0red 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> 0 e. RR )
18 1 axsegconlem6 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 < ( sqrt ` S ) )
19 18 adantr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> 0 < ( sqrt ` S ) )
20 17 11 16 19 10 ltletrd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> 0 < ( ( sqrt ` S ) + ( sqrt ` T ) ) )
21 divelunit 
 |-  ( ( ( ( sqrt ` S ) e. RR /\ 0 <_ ( sqrt ` S ) ) /\ ( ( ( sqrt ` S ) + ( sqrt ` T ) ) e. RR /\ 0 < ( ( sqrt ` S ) + ( sqrt ` T ) ) ) ) -> ( ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) e. ( 0 [,] 1 ) <-> ( sqrt ` S ) <_ ( ( sqrt ` S ) + ( sqrt ` T ) ) ) )
22 11 14 16 20 21 syl22anc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) e. ( 0 [,] 1 ) <-> ( sqrt ` S ) <_ ( ( sqrt ` S ) + ( sqrt ` T ) ) ) )
23 10 22 mpbird 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( sqrt ` S ) / ( ( sqrt ` S ) + ( sqrt ` T ) ) ) e. ( 0 [,] 1 ) )