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