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 ) ) |
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 ) ) |