Metamath Proof Explorer

Theorem axsegconlem6

Description: Lemma for axsegcon . Show that the distance between two distinct points is positive. (Contributed by Scott Fenton, 17-Sep-2013)

Ref Expression
Hypothesis axsegconlem2.1 
|- S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
Assertion axsegconlem6 
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 < ( sqrt ` S ) )

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 
 |-  S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
2 1 axsegconlem4 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sqrt ` S ) e. RR )
3 2 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) e. RR )
4 1 axsegconlem5 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ ( sqrt ` S ) )
5 4 3adant3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 <_ ( sqrt ` S ) )
6 eqeelen 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) = 0 ) )
7 1 eqeq1i 
 |-  ( S = 0 <-> sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) = 0 )
8 6 7 bitr4di 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> S = 0 ) )
9 1 axsegconlem2 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> S e. RR )
10 1 axsegconlem3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ S )
11 sqrt00 
 |-  ( ( S e. RR /\ 0 <_ S ) -> ( ( sqrt ` S ) = 0 <-> S = 0 ) )
12 9 10 11 syl2anc 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( sqrt ` S ) = 0 <-> S = 0 ) )
13 8 12 bitr4d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> ( sqrt ` S ) = 0 ) )
14 13 necon3bid 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A =/= B <-> ( sqrt ` S ) =/= 0 ) )
15 14 biimp3a 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) =/= 0 )
16 3 5 15 ne0gt0d 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 < ( sqrt ` S ) )