Metamath Proof Explorer

Theorem eqeelen

Description: Two points are equal iff the square of the distance between them is zero. (Contributed by Scott Fenton, 10-Jun-2013) (Revised by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion eqeelen ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∑ i = 1 N A ⁡ i − B ⁡ i 2 = 0

Proof

Step Hyp Ref Expression
1 fveere ⊢ A ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℝ
2 1 adantlr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℝ
3 fveere ⊢ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → B ⁡ i ∈ ℝ
4 3 adantll ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → B ⁡ i ∈ ℝ
5 2 4 resubcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i ∈ ℝ
6 5 recnd ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i ∈ ℂ
7 sqeq0 ⊢ A ⁡ i − B ⁡ i ∈ ℂ → A ⁡ i − B ⁡ i 2 = 0 ↔ A ⁡ i − B ⁡ i = 0
8 6 7 syl ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i 2 = 0 ↔ A ⁡ i − B ⁡ i = 0
9 2 recnd ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℂ
10 4 recnd ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → B ⁡ i ∈ ℂ
11 9 10 subeq0ad ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i = 0 ↔ A ⁡ i = B ⁡ i
12 8 11 bitrd ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i 2 = 0 ↔ A ⁡ i = B ⁡ i
13 12 ralbidva ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∀ i ∈ 1 … N A ⁡ i − B ⁡ i 2 = 0 ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
14 fzfid ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → 1 … N ∈ Fin
15 5 resqcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i 2 ∈ ℝ
16 5 sqge0d ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → 0 ≤ A ⁡ i − B ⁡ i 2
17 14 15 16 fsum00 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∑ i = 1 N A ⁡ i − B ⁡ i 2 = 0 ↔ ∀ i ∈ 1 … N A ⁡ i − B ⁡ i 2 = 0
18 eqeefv ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
19 13 17 18 3bitr4rd ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∑ i = 1 N A ⁡ i − B ⁡ i 2 = 0