Theorem axsegconlem4

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

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

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	resqrtcld	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sqrt ` S ) e. RR )