Metamath Proof Explorer

Theorem axsegconlem6

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

Ref Expression
Hypothesis axsegconlem2.1 ⊢ S = ∑ p = 1 N A ⁡ p − B ⁡ p 2
Assertion axsegconlem6 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → 0 < S

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 ⊢ S = ∑ p = 1 N A ⁡ p − B ⁡ p 2
2 1 axsegconlem4 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → S ∈ ℝ
3 2 3adant3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → S ∈ ℝ
4 1 axsegconlem5 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → 0 ≤ S
5 4 3adant3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → 0 ≤ S
6 eqeelen ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∑ p = 1 N A ⁡ p − B ⁡ p 2 = 0
7 1 eqeq1i ⊢ S = 0 ↔ ∑ p = 1 N A ⁡ p − B ⁡ p 2 = 0
8 6 7 bitr4di ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ S = 0
9 1 axsegconlem2 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → S ∈ ℝ
10 1 axsegconlem3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → 0 ≤ S
11 sqrt00 ⊢ S ∈ ℝ ∧ 0 ≤ S → S = 0 ↔ S = 0
12 9 10 11 syl2anc ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → S = 0 ↔ S = 0
13 8 12 bitr4d ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ S = 0
14 13 necon3bid ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ≠ B ↔ S ≠ 0
15 14 biimp3a ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → S ≠ 0
16 3 5 15 ne0gt0d ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → 0 < S