Metamath Proof Explorer

Theorem axsegconlem3

Description: Lemma for axsegcon . Show that the square of the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013)

Ref Expression
Hypothesis axsegconlem2.1 ⊢ S = ∑ p = 1 N A ⁡ p − B ⁡ p 2
Assertion axsegconlem3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → 0 ≤ 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 3 adantlr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N → A ⁡ p ∈ ℝ
5 fveere ⊢ B ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N → B ⁡ p ∈ ℝ
6 5 adantll ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N → B ⁡ p ∈ ℝ
7 4 6 resubcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N → A ⁡ p − B ⁡ p ∈ ℝ
8 7 resqcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N → A ⁡ p − B ⁡ p 2 ∈ ℝ
9 7 sqge0d ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ p ∈ 1 … N → 0 ≤ A ⁡ p − B ⁡ p 2
10 2 8 9 fsumge0 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → 0 ≤ ∑ p = 1 N A ⁡ p − B ⁡ p 2
11 10 1 breqtrrdi ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → 0 ≤ S