Metamath Proof Explorer

Theorem eqeelen

Description: Two points are equal iff the square of the distance between them is zero. (Contributed by Scott Fenton, 10-Jun-2013) (Revised by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion eqeelen 
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 fveere 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
2 1 adantlr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
3 fveere 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
4 3 adantll 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
5 2 4 resubcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) - ( B ` i ) ) e. RR )
6 5 recnd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) - ( B ` i ) ) e. CC )
7 sqeq0 
 |-  ( ( ( A ` i ) - ( B ` i ) ) e. CC -> ( ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> ( ( A ` i ) - ( B ` i ) ) = 0 ) )
8 6 7 syl 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> ( ( A ` i ) - ( B ` i ) ) = 0 ) )
9 2 recnd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
10 4 recnd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
11 9 10 subeq0ad 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( A ` i ) - ( B ` i ) ) = 0 <-> ( A ` i ) = ( B ` i ) ) )
12 8 11 bitrd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> ( A ` i ) = ( B ` i ) ) )
13 12 ralbidva 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A. i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
14 fzfid 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( 1 ... N ) e. Fin )
15 5 resqcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) e. RR )
16 5 sqge0d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ i e. ( 1 ... N ) ) -> 0 <_ ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) )
17 14 15 16 fsum00 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 <-> A. i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 ) )
18 eqeefv 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
19 13 17 18 3bitr4rd 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> sum_ i e. ( 1 ... N ) ( ( ( A ` i ) - ( B ` i ) ) ^ 2 ) = 0 ) )