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

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	resqrtcld	$$⊢\left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\to \sqrt{S}\in ℝ$$