Metamath Proof Explorer

Theorem axcgrid

Description: If there is no distance between A and B , then A = B . Axiom A3 of Schwabhauser p. 10. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion axcgrid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B Cgr C C → A = B

Proof

Step Hyp Ref Expression
1 fveecn ⊢ C ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → C ⁡ i ∈ ℂ
2 subid ⊢ C ⁡ i ∈ ℂ → C ⁡ i − C ⁡ i = 0
3 2 sq0id ⊢ C ⁡ i ∈ ℂ → C ⁡ i − C ⁡ i 2 = 0
4 1 3 syl ⊢ C ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → C ⁡ i − C ⁡ i 2 = 0
5 4 sumeq2dv ⊢ C ∈ 𝔼 ⁡ N → ∑ i = 1 N C ⁡ i − C ⁡ i 2 = ∑ i = 1 N 0
6 fzfid ⊢ C ∈ 𝔼 ⁡ N → 1 … N ∈ Fin
7 sumz ⊢ 1 … N ⊆ ℤ ≥ 1 ∨ 1 … N ∈ Fin → ∑ i = 1 N 0 = 0
8 7 olcs ⊢ 1 … N ∈ Fin → ∑ i = 1 N 0 = 0
9 6 8 syl ⊢ C ∈ 𝔼 ⁡ N → ∑ i = 1 N 0 = 0
10 5 9 eqtrd ⊢ C ∈ 𝔼 ⁡ N → ∑ i = 1 N C ⁡ i − C ⁡ i 2 = 0
11 10 3ad2ant3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∑ i = 1 N C ⁡ i − C ⁡ i 2 = 0
12 11 eqeq2d ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∑ i = 1 N A ⁡ i − B ⁡ i 2 = ∑ i = 1 N C ⁡ i − C ⁡ i 2 ↔ ∑ i = 1 N A ⁡ i − B ⁡ i 2 = 0
13 fzfid ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → 1 … N ∈ Fin
14 fveere ⊢ A ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℝ
15 14 adantlr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℝ
16 fveere ⊢ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → B ⁡ i ∈ ℝ
17 16 adantll ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → B ⁡ i ∈ ℝ
18 15 17 resubcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i ∈ ℝ
19 18 resqcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i 2 ∈ ℝ
20 18 sqge0d ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → 0 ≤ A ⁡ i − B ⁡ i 2
21 13 19 20 fsum00 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∑ i = 1 N A ⁡ i − B ⁡ i 2 = 0 ↔ ∀ i ∈ 1 … N A ⁡ i − B ⁡ i 2 = 0
22 fveecn ⊢ A ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℂ
23 fveecn ⊢ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → B ⁡ i ∈ ℂ
24 subcl ⊢ A ⁡ i ∈ ℂ ∧ B ⁡ i ∈ ℂ → A ⁡ i − B ⁡ i ∈ ℂ
25 sqeq0 ⊢ A ⁡ i − B ⁡ i ∈ ℂ → A ⁡ i − B ⁡ i 2 = 0 ↔ A ⁡ i − B ⁡ i = 0
26 24 25 syl ⊢ A ⁡ i ∈ ℂ ∧ B ⁡ i ∈ ℂ → A ⁡ i − B ⁡ i 2 = 0 ↔ A ⁡ i − B ⁡ i = 0
27 subeq0 ⊢ A ⁡ i ∈ ℂ ∧ B ⁡ i ∈ ℂ → A ⁡ i − B ⁡ i = 0 ↔ A ⁡ i = B ⁡ i
28 26 27 bitrd ⊢ A ⁡ i ∈ ℂ ∧ B ⁡ i ∈ ℂ → A ⁡ i − B ⁡ i 2 = 0 ↔ A ⁡ i = B ⁡ i
29 22 23 28 syl2an ⊢ A ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i 2 = 0 ↔ A ⁡ i = B ⁡ i
30 29 anandirs ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i 2 = 0 ↔ A ⁡ i = B ⁡ i
31 30 ralbidva ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∀ i ∈ 1 … N A ⁡ i − B ⁡ i 2 = 0 ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
32 21 31 bitrd ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∑ i = 1 N A ⁡ i − B ⁡ i 2 = 0 ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
33 32 3adant3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∑ i = 1 N A ⁡ i − B ⁡ i 2 = 0 ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
34 12 33 bitrd ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∑ i = 1 N A ⁡ i − B ⁡ i 2 = ∑ i = 1 N C ⁡ i − C ⁡ i 2 ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
35 simp1 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
36 simp2 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
37 simp3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
38 brcgr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B Cgr C C ↔ ∑ i = 1 N A ⁡ i − B ⁡ i 2 = ∑ i = 1 N C ⁡ i − C ⁡ i 2
39 35 36 37 37 38 syl22anc ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B Cgr C C ↔ ∑ i = 1 N A ⁡ i − B ⁡ i 2 = ∑ i = 1 N C ⁡ i − C ⁡ i 2
40 eqeefv ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
41 40 3adant3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
42 34 39 41 3bitr4d ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B Cgr C C ↔ A = B
43 42 biimpd ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B Cgr C C → A = B
44 43 adantl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A B Cgr C C → A = B