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	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨C, D⟩ \leftrightarrow \sum_{i = 1}^{N} {(A (i) - B (i))}^{2} = \sum_{i = 1}^{N} {(C (i) - D (i))}^{2})$

Proof

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

Metamath Proof Explorer

Theorem brcgr

Proof