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

Proof

Step	Hyp	Ref	Expression
1		axsegconlem2.1	⊢ 𝑆 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
2		fzfid	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 1 ... 𝑁 ) ∈ Fin )
3		fveere	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑝 ) ∈ ℝ )
4		fveere	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑝 ) ∈ ℝ )
5		resubcl	⊢ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ) → ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ∈ ℝ )
6	5	resqcld	⊢ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ) → ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ∈ ℝ )
7	3 4 6	syl2an	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ∈ ℝ )
8	7	anandirs	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ∈ ℝ )
9	2 8	fsumrecl	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ∈ ℝ )
10	1 9	eqeltrid	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑆 ∈ ℝ )