Theorem axsegconlem2

Description: Lemma for axsegcon . Show that the square of 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	axsegconlem2	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> S e. RR )

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		fveere	|- ( ( B e. ( EE ` N ) /\ p e. ( 1 ... N ) ) -> ( B ` p ) e. RR )
5		resubcl	|- ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR ) -> ( ( A ` p ) - ( B ` p ) ) e. RR )
6	5	resqcld	|- ( ( ( A ` p ) e. RR /\ ( B ` p ) e. RR ) -> ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) e. RR )
7	3 4 6	syl2an	|- ( ( ( A e. ( EE ` N ) /\ p e. ( 1 ... N ) ) /\ ( B e. ( EE ` N ) /\ p e. ( 1 ... N ) ) ) -> ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) e. RR )
8	7	anandirs	|- ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ p e. ( 1 ... N ) ) -> ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) e. RR )
9	2 8	fsumrecl	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) e. RR )
10	1 9	eqeltrid	|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> S e. RR )