Metamath Proof Explorer

Theorem axsegconlem3

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

		Ref	Expression
	Hypothesis	axsegconlem2.1	$⊢ S = \sum_{p = 1}^{N} {(A (p) - B (p))}^{2}$
	Assertion	axsegconlem3	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to 0 \leq S$

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	3	adantlr	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land p \in (1 \dots N)) \to A (p) \in ℝ$
5		fveere	$⊢ (B \in 𝔼 (N) \land p \in (1 \dots N)) \to B (p) \in ℝ$
6	5	adantll	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land p \in (1 \dots N)) \to B (p) \in ℝ$
7	4 6	resubcld	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land p \in (1 \dots N)) \to A (p) - B (p) \in ℝ$
8	7	resqcld	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land p \in (1 \dots N)) \to {(A (p) - B (p))}^{2} \in ℝ$
9	7	sqge0d	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land p \in (1 \dots N)) \to 0 \leq {(A (p) - B (p))}^{2}$
10	2 8 9	fsumge0	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to 0 \leq \sum_{p = 1}^{N} {(A (p) - B (p))}^{2}$
11	10 1	breqtrrdi	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N)) \to 0 \leq S$