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=1NA⁡i−B⁡i2=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⁡i2=0↔A⁡i−B⁡i=0
8 6 7 syl ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧i∈1…N→A⁡i−B⁡i2=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⁡i2=0↔A⁡i=B⁡i
13 12 ralbidva ⊢A∈𝔼⁡N∧B∈𝔼⁡N→∀i∈1…NA⁡i−B⁡i2=0↔∀i∈1…NA⁡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⁡i2∈ℝ
16 5 sqge0d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧i∈1…N→0≤A⁡i−B⁡i2
17 14 15 16 fsum00 ⊢A∈𝔼⁡N∧B∈𝔼⁡N→∑i=1NA⁡i−B⁡i2=0↔∀i∈1…NA⁡i−B⁡i2=0
18 eqeefv ⊢A∈𝔼⁡N∧B∈𝔼⁡N→A=B↔∀i∈1…NA⁡i=B⁡i
19 13 17 18 3bitr4rd ⊢A∈𝔼⁡N∧B∈𝔼⁡N→A=B↔∑i=1NA⁡i−B⁡i2=0