Metamath Proof Explorer

Theorem axsegconlem9

Description: Lemma for axsegcon . Show that B F is congruent to C D . (Contributed by Scott Fenton, 19-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 )
axsegconlem8.3 
|- F = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) )
Assertion axsegconlem9 
|- ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( F ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )

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 axsegconlem8.3 
 |-  F = ( k e. ( 1 ... N ) |-> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) )
4 fveq2 
 |-  ( k = i -> ( B ` k ) = ( B ` i ) )
5 4 oveq2d 
 |-  ( k = i -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) = ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) )
6 fveq2 
 |-  ( k = i -> ( A ` k ) = ( A ` i ) )
7 6 oveq2d 
 |-  ( k = i -> ( ( sqrt ` T ) x. ( A ` k ) ) = ( ( sqrt ` T ) x. ( A ` i ) ) )
8 5 7 oveq12d 
 |-  ( k = i -> ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) = ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) )
9 8 oveq1d 
 |-  ( k = i -> ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` k ) ) - ( ( sqrt ` T ) x. ( A ` k ) ) ) / ( sqrt ` S ) ) = ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) )
10 ovex 
 |-  ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) e. _V
11 9 3 10 fvmpt 
 |-  ( i e. ( 1 ... N ) -> ( F ` i ) = ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) )
12 11 adantl 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( F ` i ) = ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) )
13 12 oveq2d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( B ` i ) - ( F ` i ) ) = ( ( B ` i ) - ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) ) )
14 1 axsegconlem4 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sqrt ` S ) e. RR )
15 14 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) e. RR )
16 15 ad2antrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( sqrt ` S ) e. RR )
17 simpl2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
18 fveere 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
19 17 18 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
20 16 19 remulcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) x. ( B ` i ) ) e. RR )
21 20 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) x. ( B ` i ) ) e. CC )
22 2 axsegconlem4 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( sqrt ` T ) e. RR )
23 readdcl 
 |-  ( ( ( sqrt ` S ) e. RR /\ ( sqrt ` T ) e. RR ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) e. RR )
24 15 22 23 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 )
25 24 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) e. RR )
26 25 19 remulcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) e. RR )
27 22 ad2antlr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( sqrt ` T ) e. RR )
28 simpl1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
29 fveere 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
30 28 29 sylan 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
31 27 30 remulcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) x. ( A ` i ) ) e. RR )
32 26 31 resubcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) e. RR )
33 32 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) e. CC )
34 16 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( sqrt ` S ) e. CC )
35 1 axsegconlem6 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 < ( sqrt ` S ) )
36 35 gt0ne0d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) =/= 0 )
37 36 ad2antrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( sqrt ` S ) =/= 0 )
38 21 33 34 37 divsubdird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) x. ( B ` i ) ) - ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) ) / ( sqrt ` S ) ) = ( ( ( ( sqrt ` S ) x. ( B ` i ) ) / ( sqrt ` S ) ) - ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) ) )
39 26 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) e. CC )
40 31 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) x. ( A ` i ) ) e. CC )
41 21 39 40 subsubd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) x. ( B ` i ) ) - ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) ) = ( ( ( ( sqrt ` S ) x. ( B ` i ) ) - ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) ) + ( ( sqrt ` T ) x. ( A ` i ) ) ) )
42 27 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( sqrt ` T ) e. CC )
43 19 renegcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> -u ( B ` i ) e. RR )
44 43 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> -u ( B ` i ) e. CC )
45 30 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
46 42 44 45 adddid 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) x. ( -u ( B ` i ) + ( A ` i ) ) ) = ( ( ( sqrt ` T ) x. -u ( B ` i ) ) + ( ( sqrt ` T ) x. ( A ` i ) ) ) )
47 44 45 addcomd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( -u ( B ` i ) + ( A ` i ) ) = ( ( A ` i ) + -u ( B ` i ) ) )
48 19 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
49 45 48 negsubd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) + -u ( B ` i ) ) = ( ( A ` i ) - ( B ` i ) ) )
50 47 49 eqtrd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( -u ( B ` i ) + ( A ` i ) ) = ( ( A ` i ) - ( B ` i ) ) )
51 50 oveq2d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) x. ( -u ( B ` i ) + ( A ` i ) ) ) = ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) )
52 25 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) + ( sqrt ` T ) ) e. CC )
53 52 34 negsubdi2d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> -u ( ( ( sqrt ` S ) + ( sqrt ` T ) ) - ( sqrt ` S ) ) = ( ( sqrt ` S ) - ( ( sqrt ` S ) + ( sqrt ` T ) ) ) )
54 34 42 pncan2d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) + ( sqrt ` T ) ) - ( sqrt ` S ) ) = ( sqrt ` T ) )
55 54 negeqd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> -u ( ( ( sqrt ` S ) + ( sqrt ` T ) ) - ( sqrt ` S ) ) = -u ( sqrt ` T ) )
56 53 55 eqtr3d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) - ( ( sqrt ` S ) + ( sqrt ` T ) ) ) = -u ( sqrt ` T ) )
57 56 oveq1d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) - ( ( sqrt ` S ) + ( sqrt ` T ) ) ) x. ( B ` i ) ) = ( -u ( sqrt ` T ) x. ( B ` i ) ) )
58 34 52 48 subdird 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) - ( ( sqrt ` S ) + ( sqrt ` T ) ) ) x. ( B ` i ) ) = ( ( ( sqrt ` S ) x. ( B ` i ) ) - ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) ) )
59 mulneg12 
 |-  ( ( ( sqrt ` T ) e. CC /\ ( B ` i ) e. CC ) -> ( -u ( sqrt ` T ) x. ( B ` i ) ) = ( ( sqrt ` T ) x. -u ( B ` i ) ) )
60 42 48 59 syl2anc 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( -u ( sqrt ` T ) x. ( B ` i ) ) = ( ( sqrt ` T ) x. -u ( B ` i ) ) )
61 57 58 60 3eqtr3rd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) x. -u ( B ` i ) ) = ( ( ( sqrt ` S ) x. ( B ` i ) ) - ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) ) )
62 61 oveq1d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) x. -u ( B ` i ) ) + ( ( sqrt ` T ) x. ( A ` i ) ) ) = ( ( ( ( sqrt ` S ) x. ( B ` i ) ) - ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) ) + ( ( sqrt ` T ) x. ( A ` i ) ) ) )
63 46 51 62 3eqtr3rd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) x. ( B ` i ) ) - ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) ) + ( ( sqrt ` T ) x. ( A ` i ) ) ) = ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) )
64 41 63 eqtrd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) x. ( B ` i ) ) - ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) ) = ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) )
65 64 oveq1d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) x. ( B ` i ) ) - ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) ) / ( sqrt ` S ) ) = ( ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) / ( sqrt ` S ) ) )
66 48 34 37 divcan3d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` S ) x. ( B ` i ) ) / ( sqrt ` S ) ) = ( B ` i ) )
67 66 oveq1d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` S ) x. ( B ` i ) ) / ( sqrt ` S ) ) - ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) ) = ( ( B ` i ) - ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) ) )
68 38 65 67 3eqtr3rd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( B ` i ) - ( ( ( ( ( sqrt ` S ) + ( sqrt ` T ) ) x. ( B ` i ) ) - ( ( sqrt ` T ) x. ( A ` i ) ) ) / ( sqrt ` S ) ) ) = ( ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) / ( sqrt ` S ) ) )
69 13 68 eqtrd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( B ` i ) - ( F ` i ) ) = ( ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) / ( sqrt ` S ) ) )
70 69 oveq1d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( B ` i ) - ( F ` i ) ) ^ 2 ) = ( ( ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) / ( sqrt ` S ) ) ^ 2 ) )
71 30 19 resubcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) - ( B ` i ) ) e. RR )
72 27 71 remulcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) e. RR )
73 72 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) e. CC )
74 73 34 37 sqdivd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) / ( sqrt ` S ) ) ^ 2 ) = ( ( ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) ^ 2 ) / ( ( sqrt ` S ) ^ 2 ) ) )
75 71 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) - ( B ` i ) ) e. CC )
76 42 75 sqmuld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) ^ 2 ) = ( ( ( sqrt ` T ) ^ 2 ) x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) )
77 2 axsegconlem2 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> T e. RR )
78 77 ad2antlr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> T e. RR )
79 2 axsegconlem3 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> 0 <_ T )
80 79 ad2antlr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> 0 <_ T )
81 resqrtth 
 |-  ( ( T e. RR /\ 0 <_ T ) -> ( ( sqrt ` T ) ^ 2 ) = T )
82 78 80 81 syl2anc 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` T ) ^ 2 ) = T )
83 82 oveq1d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) ^ 2 ) x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) = ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) )
84 76 83 eqtrd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) ^ 2 ) = ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) )
85 1 axsegconlem2 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> S e. RR )
86 1 axsegconlem3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ S )
87 resqrtth 
 |-  ( ( S e. RR /\ 0 <_ S ) -> ( ( sqrt ` S ) ^ 2 ) = S )
88 85 86 87 syl2anc 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( sqrt ` S ) ^ 2 ) = S )
89 88 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( ( sqrt ` S ) ^ 2 ) = S )
90 89 ad2antrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( sqrt ` S ) ^ 2 ) = S )
91 84 90 oveq12d 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( sqrt ` T ) x. ( ( A ` i ) - ( B ` i ) ) ) ^ 2 ) / ( ( sqrt ` S ) ^ 2 ) ) = ( ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) / S ) )
92 70 74 91 3eqtrd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( B ` i ) - ( F ` i ) ) ^ 2 ) = ( ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) / S ) )
93 92 sumeq2dv 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( F ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) / S ) )
94 fzfid 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( 1 ... N ) e. Fin )
95 77 adantl 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> T e. RR )
96 95 recnd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> T e. CC )
97 71 resqcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) e. RR )
98 97 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) e. CC )
99 94 96 98 fsummulc2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( T x. sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) = sum_ i e. ( 1 ... N ) ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) )
100 99 oveq1d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( T x. sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) / S ) = ( sum_ i e. ( 1 ... N ) ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) / S ) )
101 fveq2 
 |-  ( p = i -> ( C ` p ) = ( C ` i ) )
102 fveq2 
 |-  ( p = i -> ( D ` p ) = ( D ` i ) )
103 101 102 oveq12d 
 |-  ( p = i -> ( ( C ` p ) - ( D ` p ) ) = ( ( C ` i ) - ( D ` i ) ) )
104 103 oveq1d 
 |-  ( p = i -> ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) = ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
105 104 cbvsumv 
 |-  sum_ p e. ( 1 ... N ) ( ( ( C ` p ) - ( D ` p ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 )
106 2 105 eqtri 
 |-  T = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 )
107 fveq2 
 |-  ( i = p -> ( A ` i ) = ( A ` p ) )
108 fveq2 
 |-  ( i = p -> ( B ` i ) = ( B ` p ) )
109 107 108 oveq12d 
 |-  ( i = p -> ( ( A ` i ) - ( B ` i ) ) = ( ( A ` p ) - ( B ` p ) ) )
110 109 oveq1d 
 |-  ( i = p -> ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) )
111 110 cbvsumv 
 |-  sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
112 111 1 eqtr4i 
 |-  sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = S
113 106 112 oveq12i 
 |-  ( T x. sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) = ( sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) x. S )
114 eqid 
 |-  sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 )
115 114 axsegconlem2 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) e. RR )
116 115 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) e. RR )
117 116 adantr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) e. RR )
118 95 117 remulcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( T x. sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) e. RR )
119 118 recnd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( T x. sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) e. CC )
120 eqid 
 |-  sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 )
121 120 axsegconlem2 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) e. RR )
122 121 adantl 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) e. RR )
123 122 recnd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) e. CC )
124 85 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> S e. RR )
125 124 adantr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> S e. RR )
126 125 recnd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> S e. CC )
127 86 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 <_ S )
128 sqrt00 
 |-  ( ( S e. RR /\ 0 <_ S ) -> ( ( sqrt ` S ) = 0 <-> S = 0 ) )
129 128 necon3bid 
 |-  ( ( S e. RR /\ 0 <_ S ) -> ( ( sqrt ` S ) =/= 0 <-> S =/= 0 ) )
130 124 127 129 syl2anc 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( ( sqrt ` S ) =/= 0 <-> S =/= 0 ) )
131 36 130 mpbid 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> S =/= 0 )
132 131 adantr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> S =/= 0 )
133 119 123 126 132 divmul3d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( ( T x. sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) / S ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) <-> ( T x. sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) = ( sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) x. S ) ) )
134 113 133 mpbiri 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( T x. sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) / S ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
135 78 97 remulcld 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) e. RR )
136 135 recnd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) e. CC )
137 94 126 136 132 fsumdivc 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( sum_ i e. ( 1 ... N ) ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) / S ) = sum_ i e. ( 1 ... N ) ( ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) / S ) )
138 100 134 137 3eqtr3rd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> sum_ i e. ( 1 ... N ) ( ( T x. ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) ) / S ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
139 93 138 eqtrd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> sum_ i e. ( 1 ... N ) ( ( ( B ` i ) - ( F ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )