Metamath Proof Explorer

Theorem axcgrrflx

Description: A is as far from B as B is from A . Axiom A1 of Schwabhauser p. 10. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion axcgrrflx ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A B Cgr B A

Proof

Step Hyp Ref Expression
1 fveecn ⊢ A ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℂ
2 fveecn ⊢ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → B ⁡ i ∈ ℂ
3 sqsubswap ⊢ A ⁡ i ∈ ℂ ∧ B ⁡ i ∈ ℂ → A ⁡ i − B ⁡ i 2 = B ⁡ i − A ⁡ i 2
4 1 2 3 syl2an ⊢ A ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i 2 = B ⁡ i − A ⁡ i 2
5 4 anandirs ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i − B ⁡ i 2 = B ⁡ i − A ⁡ i 2
6 5 sumeq2dv ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∑ i = 1 N A ⁡ i − B ⁡ i 2 = ∑ i = 1 N B ⁡ i − A ⁡ i 2
7 id ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
8 simpr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
9 simpl ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
10 brcgr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → A B Cgr B A ↔ ∑ i = 1 N A ⁡ i − B ⁡ i 2 = ∑ i = 1 N B ⁡ i − A ⁡ i 2
11 7 8 9 10 syl12anc ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A B Cgr B A ↔ ∑ i = 1 N A ⁡ i − B ⁡ i 2 = ∑ i = 1 N B ⁡ i − A ⁡ i 2
12 6 11 mpbird ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A B Cgr B A
13 12 3adant1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A B Cgr B A