Metamath Proof Explorer

Theorem brcgr

Description: The binary relation form of the congruence predicate. The statement <. A , B >. Cgr <. C , D >. should be read informally as "the N dimensional point A is as far from B as C is from D , or "the line segment A B is congruent to the line segment C D . This particular definition is encapsulated by Tarski's axioms later on. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion brcgr 
|- ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. C , D >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. A , B >. e. _V
2 opex 
 |-  <. C , D >. e. _V
3 eleq1 
 |-  ( x = <. A , B >. -> ( x e. ( ( EE ` n ) X. ( EE ` n ) ) <-> <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) )
4 3 anbi1d 
 |-  ( x = <. A , B >. -> ( ( x e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) <-> ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) ) )
5 fveq2 
 |-  ( x = <. A , B >. -> ( 1st ` x ) = ( 1st ` <. A , B >. ) )
6 5 fveq1d 
 |-  ( x = <. A , B >. -> ( ( 1st ` x ) ` i ) = ( ( 1st ` <. A , B >. ) ` i ) )
7 fveq2 
 |-  ( x = <. A , B >. -> ( 2nd ` x ) = ( 2nd ` <. A , B >. ) )
8 7 fveq1d 
 |-  ( x = <. A , B >. -> ( ( 2nd ` x ) ` i ) = ( ( 2nd ` <. A , B >. ) ` i ) )
9 6 8 oveq12d 
 |-  ( x = <. A , B >. -> ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) = ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) )
10 9 oveq1d 
 |-  ( x = <. A , B >. -> ( ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) ^ 2 ) = ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) )
11 10 sumeq2sdv 
 |-  ( x = <. A , B >. -> sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) )
12 11 eqeq1d 
 |-  ( x = <. A , B >. -> ( sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) <-> sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) ) )
13 4 12 anbi12d 
 |-  ( x = <. A , B >. -> ( ( ( x e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) ) <-> ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) ) ) )
14 13 rexbidv 
 |-  ( x = <. A , B >. -> ( E. n e. NN ( ( x e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) ) <-> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) ) ) )
15 eleq1 
 |-  ( y = <. C , D >. -> ( y e. ( ( EE ` n ) X. ( EE ` n ) ) <-> <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) )
16 15 anbi2d 
 |-  ( y = <. C , D >. -> ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) <-> ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) ) )
17 fveq2 
 |-  ( y = <. C , D >. -> ( 1st ` y ) = ( 1st ` <. C , D >. ) )
18 17 fveq1d 
 |-  ( y = <. C , D >. -> ( ( 1st ` y ) ` i ) = ( ( 1st ` <. C , D >. ) ` i ) )
19 fveq2 
 |-  ( y = <. C , D >. -> ( 2nd ` y ) = ( 2nd ` <. C , D >. ) )
20 19 fveq1d 
 |-  ( y = <. C , D >. -> ( ( 2nd ` y ) ` i ) = ( ( 2nd ` <. C , D >. ) ` i ) )
21 18 20 oveq12d 
 |-  ( y = <. C , D >. -> ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) = ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) )
22 21 oveq1d 
 |-  ( y = <. C , D >. -> ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) = ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) )
23 22 sumeq2sdv 
 |-  ( y = <. C , D >. -> sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) )
24 23 eqeq2d 
 |-  ( y = <. C , D >. -> ( sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) <-> sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) )
25 16 24 anbi12d 
 |-  ( y = <. C , D >. -> ( ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) ) <-> ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) ) )
26 25 rexbidv 
 |-  ( y = <. C , D >. -> ( E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) ) <-> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) ) )
27 df-cgr 
 |-  Cgr = { <. x , y >. | E. n e. NN ( ( x e. ( ( EE ` n ) X. ( EE ` n ) ) /\ y e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` x ) ` i ) - ( ( 2nd ` x ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` y ) ` i ) - ( ( 2nd ` y ) ` i ) ) ^ 2 ) ) }
28 1 2 14 26 27 brab 
 |-  ( <. A , B >. Cgr <. C , D >. <-> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) )
29 opelxp2 
 |-  ( <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) -> D e. ( EE ` n ) )
30 29 ad2antll 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) ) -> D e. ( EE ` n ) )
31 simplrr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) ) -> D e. ( EE ` N ) )
32 eedimeq 
 |-  ( ( D e. ( EE ` n ) /\ D e. ( EE ` N ) ) -> n = N )
33 30 31 32 syl2anc 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) ) -> n = N )
34 33 adantlr 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) ) -> n = N )
35 oveq2 
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
36 35 sumeq1d 
 |-  ( n = N -> sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) )
37 35 sumeq1d 
 |-  ( n = N -> sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) )
38 36 37 eqeq12d 
 |-  ( n = N -> ( sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) <-> sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) )
39 34 38 syl 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) ) -> ( sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) <-> sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) )
40 op1stg 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( 1st ` <. A , B >. ) = A )
41 40 fveq1d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( 1st ` <. A , B >. ) ` i ) = ( A ` i ) )
42 op2ndg 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( 2nd ` <. A , B >. ) = B )
43 42 fveq1d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( 2nd ` <. A , B >. ) ` i ) = ( B ` i ) )
44 41 43 oveq12d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) = ( ( A ` i ) - ( B ` i ) ) )
45 44 oveq1d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) )
46 45 sumeq2sdv 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) )
47 op1stg 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( 1st ` <. C , D >. ) = C )
48 47 fveq1d 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( ( 1st ` <. C , D >. ) ` i ) = ( C ` i ) )
49 op2ndg 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( 2nd ` <. C , D >. ) = D )
50 49 fveq1d 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( ( 2nd ` <. C , D >. ) ` i ) = ( D ` i ) )
51 48 50 oveq12d 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) = ( ( C ` i ) - ( D ` i ) ) )
52 51 oveq1d 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) = ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
53 52 sumeq2sdv 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) )
54 46 53 eqeqan12d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
55 54 ad2antrr 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
56 39 55 bitrd 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) ) -> ( sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
57 56 biimpd 
 |-  ( ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) ) -> ( sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) -> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
58 57 expimpd 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) -> ( ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) -> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
59 58 rexlimdva 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) -> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
60 eleenn 
 |-  ( D e. ( EE ` N ) -> N e. NN )
61 60 ad2antll 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> N e. NN )
62 opelxpi 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) )
63 opelxpi 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) )
64 62 63 anim12i 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) ) )
65 64 adantr 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) -> ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) ) )
66 54 biimpar 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) -> sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) )
67 65 66 jca 
 |-  ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) -> ( ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) )
68 fveq2 
 |-  ( n = N -> ( EE ` n ) = ( EE ` N ) )
69 68 sqxpeqd 
 |-  ( n = N -> ( ( EE ` n ) X. ( EE ` n ) ) = ( ( EE ` N ) X. ( EE ` N ) ) )
70 69 eleq2d 
 |-  ( n = N -> ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) <-> <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) ) )
71 69 eleq2d 
 |-  ( n = N -> ( <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) <-> <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) ) )
72 70 71 anbi12d 
 |-  ( n = N -> ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) <-> ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) ) ) )
73 72 38 anbi12d 
 |-  ( n = N -> ( ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) <-> ( ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) ) )
74 73 rspcev 
 |-  ( ( N e. NN /\ ( ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) ) -> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) )
75 67 74 sylan2 
 |-  ( ( N e. NN /\ ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) ) -> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) )
76 75 exp32 
 |-  ( N e. NN -> ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) -> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) ) ) )
77 61 76 mpcom 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) -> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) ) )
78 59 77 impbid 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) /\ sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. A , B >. ) ` i ) - ( ( 2nd ` <. A , B >. ) ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... n ) ( ( ( ( 1st ` <. C , D >. ) ` i ) - ( ( 2nd ` <. C , D >. ) ` i ) ) ^ 2 ) ) <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )
79 28 78 syl5bb 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. C , D >. <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = sum_ i e. ( 1 ... N ) ( ( ( C ` i ) - ( D ` i ) ) ^ 2 ) ) )