axlowdimlem17

Description: Lemma for axlowdim . Establish a congruence result. (Contributed by Scott Fenton, 22-Apr-2013) (Proof shortened by Mario Carneiro, 22-May-2014)

	Ref	Expression
Hypotheses	axlowdimlem16.1	$⊢ P = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
	axlowdimlem16.2	$⊢ Q = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
	axlowdimlem17.3	$⊢ A = \{⟨1, X⟩, ⟨2, Y⟩\} \cup ((3 \dots N) \times \{0\})$
	axlowdimlem17.4	$⊢ X \in ℝ$
	axlowdimlem17.5	$⊢ Y \in ℝ$
Assertion	axlowdimlem17	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to ⟨P, A⟩ Cgr ⟨Q, A⟩$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem16.1	$⊢ P = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
2		axlowdimlem16.2	$⊢ Q = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
3		axlowdimlem17.3	$⊢ A = \{⟨1, X⟩, ⟨2, Y⟩\} \cup ((3 \dots N) \times \{0\})$
4		axlowdimlem17.4	$⊢ X \in ℝ$
5		axlowdimlem17.5	$⊢ Y \in ℝ$
6		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
7	6	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to N \in ℤ_{\geq 2}$
8		fzss2	$⊢ N \in ℤ_{\geq 2} \to (1 \dots 2) \subseteq (1 \dots N)$
9	7 8	syl	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to (1 \dots 2) \subseteq (1 \dots N)$
10		simpr	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to i \in (1 \dots 2)$
11	9 10	sseldd	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to i \in (1 \dots N)$
12		fznuz	$⊢ i \in (1 \dots 2) \to \neg i \in ℤ_{\geq (2 + 1)}$
13	12	adantl	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to \neg i \in ℤ_{\geq (2 + 1)}$
14		3z	$⊢ 3 \in ℤ$
15		uzid	$⊢ 3 \in ℤ \to 3 \in ℤ_{\geq 3}$
16	14 15	ax-mp	$⊢ 3 \in ℤ_{\geq 3}$
17		df-3	$⊢ 3 = 2 + 1$
18	17	fveq2i	$⊢ ℤ_{\geq 3} = ℤ_{\geq (2 + 1)}$
19	16 18	eleqtri	$⊢ 3 \in ℤ_{\geq (2 + 1)}$
20		eleq1	$⊢ i = 3 \to (i \in ℤ_{\geq (2 + 1)} \leftrightarrow 3 \in ℤ_{\geq (2 + 1)})$
21	19 20	mpbiri	$⊢ i = 3 \to i \in ℤ_{\geq (2 + 1)}$
22	21	necon3bi	$⊢ \neg i \in ℤ_{\geq (2 + 1)} \to i \neq 3$
23	13 22	syl	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to i \neq 3$
24	1	axlowdimlem9	$⊢ (i \in (1 \dots N) \land i \neq 3) \to P (i) = 0$
25	11 23 24	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to P (i) = 0$
26		elfzuz	$⊢ I \in (2 \dots N - 1) \to I \in ℤ_{\geq 2}$
27	26	ad2antlr	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to I \in ℤ_{\geq 2}$
28		eluzp1p1	$⊢ I \in ℤ_{\geq 2} \to I + 1 \in ℤ_{\geq (2 + 1)}$
29	27 28	syl	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to I + 1 \in ℤ_{\geq (2 + 1)}$
30		uzss	$⊢ I + 1 \in ℤ_{\geq (2 + 1)} \to ℤ_{\geq (I + 1)} \subseteq ℤ_{\geq (2 + 1)}$
31	29 30	syl	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to ℤ_{\geq (I + 1)} \subseteq ℤ_{\geq (2 + 1)}$
32	31 13	ssneldd	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to \neg i \in ℤ_{\geq (I + 1)}$
33		eluzelz	$⊢ I + 1 \in ℤ_{\geq (2 + 1)} \to I + 1 \in ℤ$
34	29 33	syl	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to I + 1 \in ℤ$
35		uzid	$⊢ I + 1 \in ℤ \to I + 1 \in ℤ_{\geq (I + 1)}$
36	34 35	syl	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to I + 1 \in ℤ_{\geq (I + 1)}$
37		eleq1	$⊢ i = I + 1 \to (i \in ℤ_{\geq (I + 1)} \leftrightarrow I + 1 \in ℤ_{\geq (I + 1)})$
38	36 37	syl5ibrcom	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to (i = I + 1 \to i \in ℤ_{\geq (I + 1)})$
39	38	necon3bd	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to (\neg i \in ℤ_{\geq (I + 1)} \to i \neq I + 1)$
40	32 39	mpd	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to i \neq I + 1$
41	2	axlowdimlem12	$⊢ (i \in (1 \dots N) \land i \neq I + 1) \to Q (i) = 0$
42	11 40 41	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to Q (i) = 0$
43	25 42	eqtr4d	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to P (i) = Q (i)$
44	43	oveq1d	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to P (i) - A (i) = Q (i) - A (i)$
45	44	oveq1d	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots 2)) \to {(P (i) - A (i))}^{2} = {(Q (i) - A (i))}^{2}$
46	45	sumeq2dv	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to \sum_{i = 1}^{2} {(P (i) - A (i))}^{2} = \sum_{i = 1}^{2} {(Q (i) - A (i))}^{2}$
47	1 2	axlowdimlem16	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to \sum_{i = 3}^{N} {P (i)}^{2} = \sum_{i = 3}^{N} {Q (i)}^{2}$
48	3	fveq1i	$⊢ A (i) = (\{⟨1, X⟩, ⟨2, Y⟩\} \cup ((3 \dots N) \times \{0\})) (i)$
49		axlowdimlem2	$⊢ (1 \dots 2) \cap (3 \dots N) = \emptyset$
50	4 5	axlowdimlem4	$⊢ \{⟨1, X⟩, ⟨2, Y⟩\} : (1 \dots 2) ⟶ ℝ$
51		ffn	$⊢ \{⟨1, X⟩, ⟨2, Y⟩\} : (1 \dots 2) ⟶ ℝ \to \{⟨1, X⟩, ⟨2, Y⟩\} Fn (1 \dots 2)$
52	50 51	ax-mp	$⊢ \{⟨1, X⟩, ⟨2, Y⟩\} Fn (1 \dots 2)$
53		axlowdimlem1	$⊢ ((3 \dots N) \times \{0\}) : (3 \dots N) ⟶ ℝ$
54		ffn	$⊢ ((3 \dots N) \times \{0\}) : (3 \dots N) ⟶ ℝ \to ((3 \dots N) \times \{0\}) Fn (3 \dots N)$
55	53 54	ax-mp	$⊢ ((3 \dots N) \times \{0\}) Fn (3 \dots N)$
56		fvun2	$⊢ (\{⟨1, X⟩, ⟨2, Y⟩\} Fn (1 \dots 2) \land ((3 \dots N) \times \{0\}) Fn (3 \dots N) \land ((1 \dots 2) \cap (3 \dots N) = \emptyset \land i \in (3 \dots N))) \to (\{⟨1, X⟩, ⟨2, Y⟩\} \cup ((3 \dots N) \times \{0\})) (i) = ((3 \dots N) \times \{0\}) (i)$
57	52 55 56	mp3an12	$⊢ ((1 \dots 2) \cap (3 \dots N) = \emptyset \land i \in (3 \dots N)) \to (\{⟨1, X⟩, ⟨2, Y⟩\} \cup ((3 \dots N) \times \{0\})) (i) = ((3 \dots N) \times \{0\}) (i)$
58	49 57	mpan	$⊢ i \in (3 \dots N) \to (\{⟨1, X⟩, ⟨2, Y⟩\} \cup ((3 \dots N) \times \{0\})) (i) = ((3 \dots N) \times \{0\}) (i)$
59	48 58	syl5eq	$⊢ i \in (3 \dots N) \to A (i) = ((3 \dots N) \times \{0\}) (i)$
60		c0ex	$⊢ 0 \in V$
61	60	fvconst2	$⊢ i \in (3 \dots N) \to ((3 \dots N) \times \{0\}) (i) = 0$
62	59 61	eqtrd	$⊢ i \in (3 \dots N) \to A (i) = 0$
63	62	adantl	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to A (i) = 0$
64	63	oveq2d	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to P (i) - A (i) = P (i) - 0$
65	1	axlowdimlem7	$⊢ N \in ℤ_{\geq 3} \to P \in 𝔼 (N)$
66	65	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to P \in 𝔼 (N)$
67		3nn	$⊢ 3 \in ℕ$
68		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
69	67 68	eleqtri	$⊢ 3 \in ℤ_{\geq 1}$
70		fzss1	$⊢ 3 \in ℤ_{\geq 1} \to (3 \dots N) \subseteq (1 \dots N)$
71	69 70	ax-mp	$⊢ (3 \dots N) \subseteq (1 \dots N)$
72	71	sseli	$⊢ i \in (3 \dots N) \to i \in (1 \dots N)$
73	72	adantl	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to i \in (1 \dots N)$
74		fveecn	$⊢ (P \in 𝔼 (N) \land i \in (1 \dots N)) \to P (i) \in ℂ$
75	66 73 74	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to P (i) \in ℂ$
76	75	subid1d	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to P (i) - 0 = P (i)$
77	64 76	eqtrd	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to P (i) - A (i) = P (i)$
78	77	oveq1d	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to {(P (i) - A (i))}^{2} = {P (i)}^{2}$
79	78	sumeq2dv	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to \sum_{i = 3}^{N} {(P (i) - A (i))}^{2} = \sum_{i = 3}^{N} {P (i)}^{2}$
80	63	oveq2d	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to Q (i) - A (i) = Q (i) - 0$
81		eluzge3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
82		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
83		fzss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 \dots N - 1) \subseteq (1 \dots N - 1)$
84	82 83	ax-mp	$⊢ (2 \dots N - 1) \subseteq (1 \dots N - 1)$
85	84	sseli	$⊢ I \in (2 \dots N - 1) \to I \in (1 \dots N - 1)$
86	2	axlowdimlem10	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to Q \in 𝔼 (N)$
87	81 85 86	syl2an	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to Q \in 𝔼 (N)$
88		fveecn	$⊢ (Q \in 𝔼 (N) \land i \in (1 \dots N)) \to Q (i) \in ℂ$
89	87 72 88	syl2an	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to Q (i) \in ℂ$
90	89	subid1d	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to Q (i) - 0 = Q (i)$
91	80 90	eqtrd	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to Q (i) - A (i) = Q (i)$
92	91	oveq1d	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to {(Q (i) - A (i))}^{2} = {Q (i)}^{2}$
93	92	sumeq2dv	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to \sum_{i = 3}^{N} {(Q (i) - A (i))}^{2} = \sum_{i = 3}^{N} {Q (i)}^{2}$
94	47 79 93	3eqtr4d	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to \sum_{i = 3}^{N} {(P (i) - A (i))}^{2} = \sum_{i = 3}^{N} {(Q (i) - A (i))}^{2}$
95	46 94	oveq12d	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to \sum_{i = 1}^{2} {(P (i) - A (i))}^{2} + \sum_{i = 3}^{N} {(P (i) - A (i))}^{2} = \sum_{i = 1}^{2} {(Q (i) - A (i))}^{2} + \sum_{i = 3}^{N} {(Q (i) - A (i))}^{2}$
96	49	a1i	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to (1 \dots 2) \cap (3 \dots N) = \emptyset$
97		eluzelre	$⊢ N \in ℤ_{\geq 3} \to N \in ℝ$
98		eluzle	$⊢ N \in ℤ_{\geq 3} \to 3 \leq N$
99		2re	$⊢ 2 \in ℝ$
100		3re	$⊢ 3 \in ℝ$
101		2lt3	$⊢ 2 < 3$
102	99 100 101	ltleii	$⊢ 2 \leq 3$
103		letr	$⊢ (2 \in ℝ \land 3 \in ℝ \land N \in ℝ) \to ((2 \leq 3 \land 3 \leq N) \to 2 \leq N)$
104	99 100 103	mp3an12	$⊢ N \in ℝ \to ((2 \leq 3 \land 3 \leq N) \to 2 \leq N)$
105	102 104	mpani	$⊢ N \in ℝ \to (3 \leq N \to 2 \leq N)$
106	97 98 105	sylc	$⊢ N \in ℤ_{\geq 3} \to 2 \leq N$
107		1le2	$⊢ 1 \leq 2$
108	106 107	jctil	$⊢ N \in ℤ_{\geq 3} \to (1 \leq 2 \land 2 \leq N)$
109	108	adantr	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to (1 \leq 2 \land 2 \leq N)$
110		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
111	110	adantr	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to N \in ℤ$
112		2z	$⊢ 2 \in ℤ$
113		1z	$⊢ 1 \in ℤ$
114		elfz	$⊢ (2 \in ℤ \land 1 \in ℤ \land N \in ℤ) \to (2 \in (1 \dots N) \leftrightarrow (1 \leq 2 \land 2 \leq N))$
115	112 113 114	mp3an12	$⊢ N \in ℤ \to (2 \in (1 \dots N) \leftrightarrow (1 \leq 2 \land 2 \leq N))$
116	111 115	syl	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to (2 \in (1 \dots N) \leftrightarrow (1 \leq 2 \land 2 \leq N))$
117	109 116	mpbird	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to 2 \in (1 \dots N)$
118		fzsplit	$⊢ 2 \in (1 \dots N) \to (1 \dots N) = (1 \dots 2) \cup (2 + 1 \dots N)$
119	117 118	syl	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to (1 \dots N) = (1 \dots 2) \cup (2 + 1 \dots N)$
120	17	oveq1i	$⊢ (3 \dots N) = (2 + 1 \dots N)$
121	120	uneq2i	$⊢ (1 \dots 2) \cup (3 \dots N) = (1 \dots 2) \cup (2 + 1 \dots N)$
122	119 121	eqtr4di	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to (1 \dots N) = (1 \dots 2) \cup (3 \dots N)$
123		fzfid	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to (1 \dots N) \in Fin$
124	65	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots N)) \to P \in 𝔼 (N)$
125	124 74	sylancom	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots N)) \to P (i) \in ℂ$
126	4 5	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, X⟩, ⟨2, Y⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
127	3 126	eqeltrid	$⊢ N \in ℤ_{\geq 2} \to A \in 𝔼 (N)$
128	6 127	syl	$⊢ N \in ℤ_{\geq 3} \to A \in 𝔼 (N)$
129	128	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots N)) \to A \in 𝔼 (N)$
130		fveecn	$⊢ (A \in 𝔼 (N) \land i \in (1 \dots N)) \to A (i) \in ℂ$
131	129 130	sylancom	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots N)) \to A (i) \in ℂ$
132	125 131	subcld	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots N)) \to P (i) - A (i) \in ℂ$
133	132	sqcld	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots N)) \to {(P (i) - A (i))}^{2} \in ℂ$
134	96 122 123 133	fsumsplit	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to \sum_{i = 1}^{N} {(P (i) - A (i))}^{2} = \sum_{i = 1}^{2} {(P (i) - A (i))}^{2} + \sum_{i = 3}^{N} {(P (i) - A (i))}^{2}$
135	87 88	sylan	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots N)) \to Q (i) \in ℂ$
136	135 131	subcld	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots N)) \to Q (i) - A (i) \in ℂ$
137	136	sqcld	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (1 \dots N)) \to {(Q (i) - A (i))}^{2} \in ℂ$
138	96 122 123 137	fsumsplit	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to \sum_{i = 1}^{N} {(Q (i) - A (i))}^{2} = \sum_{i = 1}^{2} {(Q (i) - A (i))}^{2} + \sum_{i = 3}^{N} {(Q (i) - A (i))}^{2}$
139	95 134 138	3eqtr4d	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to \sum_{i = 1}^{N} {(P (i) - A (i))}^{2} = \sum_{i = 1}^{N} {(Q (i) - A (i))}^{2}$
140	65	adantr	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to P \in 𝔼 (N)$
141	128	adantr	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to A \in 𝔼 (N)$
142		brcgr	$⊢ ((P \in 𝔼 (N) \land A \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land A \in 𝔼 (N))) \to (⟨P, A⟩ Cgr ⟨Q, A⟩ \leftrightarrow \sum_{i = 1}^{N} {(P (i) - A (i))}^{2} = \sum_{i = 1}^{N} {(Q (i) - A (i))}^{2})$
143	140 141 87 141 142	syl22anc	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to (⟨P, A⟩ Cgr ⟨Q, A⟩ \leftrightarrow \sum_{i = 1}^{N} {(P (i) - A (i))}^{2} = \sum_{i = 1}^{N} {(Q (i) - A (i))}^{2})$
144	139 143	mpbird	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to ⟨P, A⟩ Cgr ⟨Q, A⟩$

Metamath Proof Explorer

Theorem axlowdimlem17

Proof