Metamath Proof Explorer


Theorem axsegconlem5

Description: Lemma for axsegcon . Show that 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 axsegconlem5
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ ( sqrt ` S ) )

Proof

Step Hyp Ref Expression
1 axsegconlem2.1
 |-  S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 )
2 1 axsegconlem2
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> S e. RR )
3 1 axsegconlem3
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ S )
4 2 3 sqrtge0d
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ ( sqrt ` S ) )