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	⊢ 𝑆 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
Assertion	axsegconlem5	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 0 ≤ ( √ ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		axsegconlem2.1	⊢ 𝑆 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
2	1	axsegconlem2	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑆 ∈ ℝ )
3	1	axsegconlem3	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 0 ≤ 𝑆 )
4	2 3	sqrtge0d	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 0 ≤ ( √ ‘ 𝑆 ) )