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	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
2		opex	⊢ ⟨ 𝐶 , 𝐷 ⟩ ∈ V
3		eleq1	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) )
4	3	anbi1d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ) )
5		fveq2	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
6	5	fveq1d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) = ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) )
7		fveq2	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
8	7	fveq1d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) = ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) )
9	6 8	oveq12d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) )
10	9	oveq1d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) )
11	10	sumeq2sdv	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) )
12	11	eqeq1d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) )
13	4 12	anbi12d	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) ) )
14	13	rexbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) ) )
15		eleq1	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) )
16	15	anbi2d	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ) )
17		fveq2	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 1^st ‘ 𝑦 ) = ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
18	17	fveq1d	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) = ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) )
19		fveq2	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 2^nd ‘ 𝑦 ) = ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
20	19	fveq1d	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) = ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) )
21	18 20	oveq12d	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) = ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) )
22	21	oveq1d	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) )
23	22	sumeq2sdv	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) )
24	23	eqeq2d	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) )
25	16 24	anbi12d	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) ) )
26	25	rexbidv	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) ) )
27		df-cgr	⊢ Cgr = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑥 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑥 ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ 𝑦 ) ‘ 𝑖 ) − ( ( 2^nd ‘ 𝑦 ) ‘ 𝑖 ) ) ↑ 2 ) ) }
28	1 2 14 26 27	brab	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) )
29		opelxp2	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) )
30	29	ad2antll	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) )
31		simplrr	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
32		eedimeq	⊢ ( ( 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑛 = 𝑁 )
33	30 31 32	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ) → 𝑛 = 𝑁 )
34	33	adantlr	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ) → 𝑛 = 𝑁 )
35		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
36	35	sumeq1d	⊢ ( 𝑛 = 𝑁 → Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) )
37	35	sumeq1d	⊢ ( 𝑛 = 𝑁 → Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) )
38	36 37	eqeq12d	⊢ ( 𝑛 = 𝑁 → ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) )
39	34 38	syl	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) )
40		op1stg	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
41	40	fveq1d	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
42		op2ndg	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
43	42	fveq1d	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) )
44	41 43	oveq12d	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) )
45	44	oveq1d	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) )
46	45	sumeq2sdv	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) )
47		op1stg	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
48	47	fveq1d	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) = ( 𝐶 ‘ 𝑖 ) )
49		op2ndg	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
50	49	fveq1d	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) = ( 𝐷 ‘ 𝑖 ) )
51	48 50	oveq12d	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) = ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) )
52	51	oveq1d	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
53	52	sumeq2sdv	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
54	46 53	eqeqan12d	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
55	54	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
56	39 55	bitrd	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
57	56	biimpd	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
58	57	expimpd	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
59	58	rexlimdva	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
60		eleenn	⊢ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )
61	60	ad2antll	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
62		opelxpi	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) )
63		opelxpi	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) )
64	62 63	anim12i	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ) )
65	64	adantr	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ) )
66	54	biimpar	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) )
67	65 66	jca	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) )
68		fveq2	⊢ ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
69	68	sqxpeqd	⊢ ( 𝑛 = 𝑁 → ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) = ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) )
70	69	eleq2d	⊢ ( 𝑛 = 𝑁 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ) )
71	69	eleq2d	⊢ ( 𝑛 = 𝑁 → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ) )
72	70 71	anbi12d	⊢ ( 𝑛 = 𝑁 → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ) ) )
73	72 38	anbi12d	⊢ ( 𝑛 = 𝑁 → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) ) )
74	73	rspcev	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑁 ) × ( 𝔼 ‘ 𝑁 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) ) → ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) )
75	67 74	sylan2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) → ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) )
76	75	exp32	⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) → ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) ) ) )
77	61 76	mpcom	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) → ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) ) )
78	59 77	impbid	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑛 ∈ ℕ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( ( 𝔼 ‘ 𝑛 ) × ( 𝔼 ‘ 𝑛 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑛 ) ( ( ( ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) − ( ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ‘ 𝑖 ) ) ↑ 2 ) ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
79	28 78	syl5bb	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )

Metamath Proof Explorer

Theorem brcgr

Proof