Metamath Proof Explorer

Theorem axsegconlem3

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

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

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 
 |-  S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
2 fzfid 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( 1 ... N ) e. Fin )
3 fveere 
 |-  ( ( A e. ( EE ` N ) /\ p e. ( 1 ... N ) ) -> ( A ` p ) e. RR )
4 3 adantlr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ p e. ( 1 ... N ) ) -> ( A ` p ) e. RR )
5 fveere 
 |-  ( ( B e. ( EE ` N ) /\ p e. ( 1 ... N ) ) -> ( B ` p ) e. RR )
6 5 adantll 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ p e. ( 1 ... N ) ) -> ( B ` p ) e. RR )
7 4 6 resubcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ p e. ( 1 ... N ) ) -> ( ( A ` p ) - ( B ` p ) ) e. RR )
8 7 resqcld 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ p e. ( 1 ... N ) ) -> ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) e. RR )
9 7 sqge0d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ p e. ( 1 ... N ) ) -> 0 <_ ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) )
10 2 8 9 fsumge0 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) )
11 10 1 breqtrrdi 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ S )