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=1}^N{\left(A\left(p\right)-B\left(p\right)\right)}^2$$
Assertion	axsegconlem5	$$⊢\left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\to 0\le \sqrt{S}$$

Proof

Step	Hyp	Ref	Expression
1		axsegconlem2.1	$$⊢S=\sum _{p=1}^N{\left(A\left(p\right)-B\left(p\right)\right)}^2$$
2	1	axsegconlem2	$$⊢\left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\to S\in ℝ$$
3	1	axsegconlem3	$$⊢\left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\to 0\le S$$
4	2 3	sqrtge0d	$$⊢\left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\to 0\le \sqrt{S}$$