Metamath Proof Explorer

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 ⊢ S = ∑ p = 1 N A ⁡ p − B ⁡ p 2
Assertion axsegconlem2 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → S ∈ ℝ

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 ⊢ S = ∑ p = 1 N A ⁡ p − B ⁡ p 2
2 fzfid ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → 1 … N ∈ Fin
3 fveere ⊢ A ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N → A ⁡ p ∈ ℝ
4 fveere ⊢ B ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N → B ⁡ p ∈ ℝ
5 resubcl ⊢ A ⁡ p ∈ ℝ ∧ B ⁡ p ∈ ℝ → A ⁡ p − B ⁡ p ∈ ℝ
6 5 resqcld ⊢ A ⁡ p ∈ ℝ ∧ B ⁡ p ∈ ℝ → A ⁡ p − B ⁡ p 2 ∈ ℝ
7 3 4 6 syl2an ⊢ A ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N ∧ B ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N → A ⁡ p − B ⁡ p 2 ∈ ℝ
8 7 anandirs ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N → A ⁡ p − B ⁡ p 2 ∈ ℝ
9 2 8 fsumrecl ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∑ p = 1 N A ⁡ p − B ⁡ p 2 ∈ ℝ
10 1 9 eqeltrid ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → S ∈ ℝ