Metamath Proof Explorer

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 = 1}^{N} {(A (p) - B (p))}^{2}$
	Assertion	axsegconlem2	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to S \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		axsegconlem2.1	$⊢ S = \sum_{p = 1}^{N} {(A (p) - B (p))}^{2}$
2		fzfid	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to (1 \dots N) \in Fin$
3		fveere	$⊢ (A \in 𝔼 (N) \land p \in (1 \dots N)) \to A (p) \in ℝ$
4		fveere	$⊢ (B \in 𝔼 (N) \land p \in (1 \dots N)) \to B (p) \in ℝ$
5		resubcl	$⊢ (A (p) \in ℝ \land B (p) \in ℝ) \to A (p) - B (p) \in ℝ$
6	5	resqcld	$⊢ (A (p) \in ℝ \land B (p) \in ℝ) \to {(A (p) - B (p))}^{2} \in ℝ$
7	3 4 6	syl2an	$⊢ ((A \in 𝔼 (N) \land p \in (1 \dots N)) \land (B \in 𝔼 (N) \land p \in (1 \dots N))) \to {(A (p) - B (p))}^{2} \in ℝ$
8	7	anandirs	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land p \in (1 \dots N)) \to {(A (p) - B (p))}^{2} \in ℝ$
9	2 8	fsumrecl	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to \sum_{p = 1}^{N} {(A (p) - B (p))}^{2} \in ℝ$
10	1 9	eqeltrid	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to S \in ℝ$