Metamath Proof Explorer

Theorem brcgr

Description: The binary relation form of the congruence predicate. The statement <. A , B >. Cgr <. C , D >. should be read informally as "the N dimensional point A is as far from B as C is from D , or "the line segment A B is congruent to the line segment C D . This particular definition is encapsulated by Tarski's axioms later on. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion brcgr ${⊢}\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩↔\sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)$

Proof

Step Hyp Ref Expression
1 opex ${⊢}⟨{A},{B}⟩\in \mathrm{V}$
2 opex ${⊢}⟨{C},{D}⟩\in \mathrm{V}$
3 eleq1 ${⊢}{x}=⟨{A},{B}⟩\to \left({x}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)↔⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)$
4 3 anbi1d ${⊢}{x}=⟨{A},{B}⟩\to \left(\left({x}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge {y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)↔\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge {y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\right)$
5 fveq2 ${⊢}{x}=⟨{A},{B}⟩\to {1}^{st}\left({x}\right)={1}^{st}\left(⟨{A},{B}⟩\right)$
6 5 fveq1d ${⊢}{x}=⟨{A},{B}⟩\to {1}^{st}\left({x}\right)\left({i}\right)={1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)$
7 fveq2 ${⊢}{x}=⟨{A},{B}⟩\to {2}^{nd}\left({x}\right)={2}^{nd}\left(⟨{A},{B}⟩\right)$
8 7 fveq1d ${⊢}{x}=⟨{A},{B}⟩\to {2}^{nd}\left({x}\right)\left({i}\right)={2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)$
9 6 8 oveq12d ${⊢}{x}=⟨{A},{B}⟩\to {1}^{st}\left({x}\right)\left({i}\right)-{2}^{nd}\left({x}\right)\left({i}\right)={1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)$
10 9 oveq1d ${⊢}{x}=⟨{A},{B}⟩\to {\left({1}^{st}\left({x}\right)\left({i}\right)-{2}^{nd}\left({x}\right)\left({i}\right)\right)}^{2}={\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}$
11 10 sumeq2sdv ${⊢}{x}=⟨{A},{B}⟩\to \sum _{{i}=1}^{{n}}{\left({1}^{st}\left({x}\right)\left({i}\right)-{2}^{nd}\left({x}\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}$
12 11 eqeq1d ${⊢}{x}=⟨{A},{B}⟩\to \left(\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({x}\right)\left({i}\right)-{2}^{nd}\left({x}\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}↔\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}\right)$
13 4 12 anbi12d ${⊢}{x}=⟨{A},{B}⟩\to \left(\left(\left({x}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge {y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left({x}\right)\left({i}\right)-{2}^{nd}\left({x}\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}\right)↔\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge {y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}\right)\right)$
14 13 rexbidv ${⊢}{x}=⟨{A},{B}⟩\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({x}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge {y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left({x}\right)\left({i}\right)-{2}^{nd}\left({x}\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge {y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}\right)\right)$
15 eleq1 ${⊢}{y}=⟨{C},{D}⟩\to \left({y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)↔⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)$
16 15 anbi2d ${⊢}{y}=⟨{C},{D}⟩\to \left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge {y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)↔\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\right)$
17 fveq2 ${⊢}{y}=⟨{C},{D}⟩\to {1}^{st}\left({y}\right)={1}^{st}\left(⟨{C},{D}⟩\right)$
18 17 fveq1d ${⊢}{y}=⟨{C},{D}⟩\to {1}^{st}\left({y}\right)\left({i}\right)={1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)$
19 fveq2 ${⊢}{y}=⟨{C},{D}⟩\to {2}^{nd}\left({y}\right)={2}^{nd}\left(⟨{C},{D}⟩\right)$
20 19 fveq1d ${⊢}{y}=⟨{C},{D}⟩\to {2}^{nd}\left({y}\right)\left({i}\right)={2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)$
21 18 20 oveq12d ${⊢}{y}=⟨{C},{D}⟩\to {1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)={1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)$
22 21 oveq1d ${⊢}{y}=⟨{C},{D}⟩\to {\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}={\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}$
23 22 sumeq2sdv ${⊢}{y}=⟨{C},{D}⟩\to \sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}$
24 23 eqeq2d ${⊢}{y}=⟨{C},{D}⟩\to \left(\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}↔\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)$
25 16 24 anbi12d ${⊢}{y}=⟨{C},{D}⟩\to \left(\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge {y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}\right)↔\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)\right)$
26 25 rexbidv ${⊢}{y}=⟨{C},{D}⟩\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge {y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)\right)$
27 df-cgr ${⊢}\mathrm{Cgr}=\left\{⟨{x},{y}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({x}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge {y}\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left({x}\right)\left({i}\right)-{2}^{nd}\left({x}\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left({y}\right)\left({i}\right)-{2}^{nd}\left({y}\right)\left({i}\right)\right)}^{2}\right)\right\}$
28 1 2 14 26 27 brab ${⊢}⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)$
29 opelxp2 ${⊢}⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\to {D}\in 𝔼\left({n}\right)$
30 29 ad2antll ${⊢}\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\right)\to {D}\in 𝔼\left({n}\right)$
31 simplrr ${⊢}\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\right)\to {D}\in 𝔼\left({N}\right)$
32 eedimeq ${⊢}\left({D}\in 𝔼\left({n}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\to {n}={N}$
33 30 31 32 syl2anc ${⊢}\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge \left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\right)\to {n}={N}$
34 33 adantlr ${⊢}\left(\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {n}\in ℕ\right)\wedge \left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\right)\to {n}={N}$
35 oveq2 ${⊢}{n}={N}\to \left(1\dots {n}\right)=\left(1\dots {N}\right)$
36 35 sumeq1d ${⊢}{n}={N}\to \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}$
37 35 sumeq1d ${⊢}{n}={N}\to \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}$
38 36 37 eqeq12d ${⊢}{n}={N}\to \left(\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}↔\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)$
39 34 38 syl ${⊢}\left(\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {n}\in ℕ\right)\wedge \left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\right)\to \left(\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}↔\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)$
40 op1stg ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to {1}^{st}\left(⟨{A},{B}⟩\right)={A}$
41 40 fveq1d ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to {1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)={A}\left({i}\right)$
42 op2ndg ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to {2}^{nd}\left(⟨{A},{B}⟩\right)={B}$
43 42 fveq1d ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to {2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)={B}\left({i}\right)$
44 41 43 oveq12d ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to {1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)={A}\left({i}\right)-{B}\left({i}\right)$
45 44 oveq1d ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to {\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}={\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}$
46 45 sumeq2sdv ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to \sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}$
47 op1stg ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\to {1}^{st}\left(⟨{C},{D}⟩\right)={C}$
48 47 fveq1d ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\to {1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)={C}\left({i}\right)$
49 op2ndg ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\to {2}^{nd}\left(⟨{C},{D}⟩\right)={D}$
50 49 fveq1d ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\to {2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)={D}\left({i}\right)$
51 48 50 oveq12d ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\to {1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)={C}\left({i}\right)-{D}\left({i}\right)$
52 51 oveq1d ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\to {\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}={\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}$
53 52 sumeq2sdv ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\to \sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}$
54 46 53 eqeqan12d ${⊢}\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}↔\sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)$
55 54 ad2antrr ${⊢}\left(\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {n}\in ℕ\right)\wedge \left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\right)\to \left(\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}↔\sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)$
56 39 55 bitrd ${⊢}\left(\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {n}\in ℕ\right)\wedge \left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\right)\to \left(\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}↔\sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)$
57 56 biimpd ${⊢}\left(\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {n}\in ℕ\right)\wedge \left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\right)\to \left(\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\to \sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)$
58 57 expimpd ${⊢}\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge {n}\in ℕ\right)\to \left(\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)\to \sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)$
59 58 rexlimdva ${⊢}\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)\to \sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)$
60 eleenn ${⊢}{D}\in 𝔼\left({N}\right)\to {N}\in ℕ$
61 60 ad2antll ${⊢}\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to {N}\in ℕ$
62 opelxpi ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to ⟨{A},{B}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)$
63 opelxpi ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\to ⟨{C},{D}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)$
64 62 63 anim12i ${⊢}\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{B}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\right)$
65 64 adantr ${⊢}\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge \sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)\to \left(⟨{A},{B}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\right)$
66 54 biimpar ${⊢}\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge \sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)\to \sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}$
67 65 66 jca ${⊢}\left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge \sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)\to \left(\left(⟨{A},{B}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\right)\wedge \sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)$
68 fveq2 ${⊢}{n}={N}\to 𝔼\left({n}\right)=𝔼\left({N}\right)$
69 68 sqxpeqd ${⊢}{n}={N}\to 𝔼\left({n}\right)×𝔼\left({n}\right)=𝔼\left({N}\right)×𝔼\left({N}\right)$
70 69 eleq2d ${⊢}{n}={N}\to \left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)↔⟨{A},{B}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\right)$
71 69 eleq2d ${⊢}{n}={N}\to \left(⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)↔⟨{C},{D}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\right)$
72 70 71 anbi12d ${⊢}{n}={N}\to \left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)↔\left(⟨{A},{B}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\right)\right)$
73 72 38 anbi12d ${⊢}{n}={N}\to \left(\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)↔\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\right)\wedge \sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)\right)$
74 73 rspcev ${⊢}\left({N}\in ℕ\wedge \left(\left(⟨{A},{B}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({N}\right)×𝔼\left({N}\right)\right)\right)\wedge \sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)$
75 67 74 sylan2 ${⊢}\left({N}\in ℕ\wedge \left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\wedge \sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)$
76 75 exp32 ${⊢}{N}\in ℕ\to \left(\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)\right)\right)$
77 61 76 mpcom ${⊢}\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)\right)$
78 59 77 impbid ${⊢}\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left(⟨{A},{B}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\wedge ⟨{C},{D}⟩\in \left(𝔼\left({n}\right)×𝔼\left({n}\right)\right)\right)\wedge \sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{A},{B}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{A},{B}⟩\right)\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{n}}{\left({1}^{st}\left(⟨{C},{D}⟩\right)\left({i}\right)-{2}^{nd}\left(⟨{C},{D}⟩\right)\left({i}\right)\right)}^{2}\right)↔\sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)$
79 28 78 syl5bb ${⊢}\left(\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{C},{D}⟩↔\sum _{{i}=1}^{{N}}{\left({A}\left({i}\right)-{B}\left({i}\right)\right)}^{2}=\sum _{{i}=1}^{{N}}{\left({C}\left({i}\right)-{D}\left({i}\right)\right)}^{2}\right)$