axlowdimlem16

Description: Lemma for axlowdim . Set up a summation that will help establish distance. (Contributed by Scott Fenton, 21-Apr-2013)

	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\})$
Assertion	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}$

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		elfz1eq	$⊢ I \in (2 \dots 2) \to I = 2$
4		3z	$⊢ 3 \in ℤ$
5		ax-1cn	$⊢ 1 \in ℂ$
6	5	sqcli	$⊢ 1^{2} \in ℂ$
7		fveq2	$⊢ i = 3 \to P (i) = P (3)$
8	1	axlowdimlem8	$⊢ P (3) = - 1$
9	7 8	eqtrdi	$⊢ i = 3 \to P (i) = - 1$
10	9	oveq1d	$⊢ i = 3 \to {P (i)}^{2} = {(- 1)}^{2}$
11		sqneg	$⊢ 1 \in ℂ \to {(- 1)}^{2} = 1^{2}$
12	5 11	ax-mp	$⊢ {(- 1)}^{2} = 1^{2}$
13	10 12	eqtrdi	$⊢ i = 3 \to {P (i)}^{2} = 1^{2}$
14	13	fsum1	$⊢ (3 \in ℤ \land 1^{2} \in ℂ) \to \sum_{i = 3}^{3} {P (i)}^{2} = 1^{2}$
15	4 6 14	mp2an	$⊢ \sum_{i = 3}^{3} {P (i)}^{2} = 1^{2}$
16		df-3	$⊢ 3 = 2 + 1$
17		oveq1	$⊢ I = 2 \to I + 1 = 2 + 1$
18	16 17	eqtr4id	$⊢ I = 2 \to 3 = I + 1$
19	18 18	oveq12d	$⊢ I = 2 \to (3 \dots 3) = (I + 1 \dots I + 1)$
20	19	sumeq1d	$⊢ I = 2 \to \sum_{i = 3}^{3} {Q (i)}^{2} = \sum_{i = I + 1}^{I + 1} {Q (i)}^{2}$
21	17 16	eqtr4di	$⊢ I = 2 \to I + 1 = 3$
22	21 4	eqeltrdi	$⊢ I = 2 \to I + 1 \in ℤ$
23		fveq2	$⊢ i = I + 1 \to Q (i) = Q (I + 1)$
24	2	axlowdimlem11	$⊢ Q (I + 1) = 1$
25	23 24	eqtrdi	$⊢ i = I + 1 \to Q (i) = 1$
26	25	oveq1d	$⊢ i = I + 1 \to {Q (i)}^{2} = 1^{2}$
27	26	fsum1	$⊢ (I + 1 \in ℤ \land 1^{2} \in ℂ) \to \sum_{i = I + 1}^{I + 1} {Q (i)}^{2} = 1^{2}$
28	22 6 27	sylancl	$⊢ I = 2 \to \sum_{i = I + 1}^{I + 1} {Q (i)}^{2} = 1^{2}$
29	20 28	eqtrd	$⊢ I = 2 \to \sum_{i = 3}^{3} {Q (i)}^{2} = 1^{2}$
30	15 29	eqtr4id	$⊢ I = 2 \to \sum_{i = 3}^{3} {P (i)}^{2} = \sum_{i = 3}^{3} {Q (i)}^{2}$
31	3 30	syl	$⊢ I \in (2 \dots 2) \to \sum_{i = 3}^{3} {P (i)}^{2} = \sum_{i = 3}^{3} {Q (i)}^{2}$
32	31	a1i	$⊢ N = 3 \to (I \in (2 \dots 2) \to \sum_{i = 3}^{3} {P (i)}^{2} = \sum_{i = 3}^{3} {Q (i)}^{2})$
33		oveq1	$⊢ N = 3 \to N - 1 = 3 - 1$
34		3m1e2	$⊢ 3 - 1 = 2$
35	33 34	eqtrdi	$⊢ N = 3 \to N - 1 = 2$
36	35	oveq2d	$⊢ N = 3 \to (2 \dots N - 1) = (2 \dots 2)$
37	36	eleq2d	$⊢ N = 3 \to (I \in (2 \dots N - 1) \leftrightarrow I \in (2 \dots 2))$
38		oveq2	$⊢ N = 3 \to (3 \dots N) = (3 \dots 3)$
39	38	sumeq1d	$⊢ N = 3 \to \sum_{i = 3}^{N} {P (i)}^{2} = \sum_{i = 3}^{3} {P (i)}^{2}$
40	38	sumeq1d	$⊢ N = 3 \to \sum_{i = 3}^{N} {Q (i)}^{2} = \sum_{i = 3}^{3} {Q (i)}^{2}$
41	39 40	eqeq12d	$⊢ N = 3 \to (\sum_{i = 3}^{N} {P (i)}^{2} = \sum_{i = 3}^{N} {Q (i)}^{2} \leftrightarrow \sum_{i = 3}^{3} {P (i)}^{2} = \sum_{i = 3}^{3} {Q (i)}^{2})$
42	32 37 41	3imtr4d	$⊢ N = 3 \to (I \in (2 \dots N - 1) \to \sum_{i = 3}^{N} {P (i)}^{2} = \sum_{i = 3}^{N} {Q (i)}^{2})$
43	42	adantld	$⊢ N = 3 \to ((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})$
44		simprl	$⊢ (N \neq 3 \land (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1))) \to N \in ℤ_{\geq 3}$
45		eluzle	$⊢ N \in ℤ_{\geq 3} \to 3 \leq N$
46	45	adantl	$⊢ (N \neq 3 \land N \in ℤ_{\geq 3}) \to 3 \leq N$
47		simpl	$⊢ (N \neq 3 \land N \in ℤ_{\geq 3}) \to N \neq 3$
48		3re	$⊢ 3 \in ℝ$
49		eluzelre	$⊢ N \in ℤ_{\geq 3} \to N \in ℝ$
50	49	adantl	$⊢ (N \neq 3 \land N \in ℤ_{\geq 3}) \to N \in ℝ$
51		ltlen	$⊢ (3 \in ℝ \land N \in ℝ) \to (3 < N \leftrightarrow (3 \leq N \land N \neq 3))$
52	48 50 51	sylancr	$⊢ (N \neq 3 \land N \in ℤ_{\geq 3}) \to (3 < N \leftrightarrow (3 \leq N \land N \neq 3))$
53	46 47 52	mpbir2and	$⊢ (N \neq 3 \land N \in ℤ_{\geq 3}) \to 3 < N$
54	53	adantrr	$⊢ (N \neq 3 \land (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1))) \to 3 < N$
55		simprr	$⊢ (N \neq 3 \land (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1))) \to I \in (2 \dots N - 1)$
56		fzssp1	$⊢ (2 \dots N - 1) \subseteq (2 \dots N - 1 + 1)$
57		simp3	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I \in (2 \dots N - 1)$
58	56 57	sselid	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I \in (2 \dots N - 1 + 1)$
59		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
60	59	3ad2ant1	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to N \in ℤ$
61	60	zcnd	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to N \in ℂ$
62		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
63	61 5 62	sylancl	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to N - 1 + 1 = N$
64	63	oveq2d	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to (2 \dots N - 1 + 1) = (2 \dots N)$
65	58 64	eleqtrd	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I \in (2 \dots N)$
66		elfzelz	$⊢ I \in (2 \dots N) \to I \in ℤ$
67	65 66	syl	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I \in ℤ$
68	67	zred	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I \in ℝ$
69	68	ltp1d	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I < I + 1$
70		fzdisj	$⊢ I < I + 1 \to (2 \dots I) \cap (I + 1 \dots N) = \emptyset$
71	69 70	syl	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to (2 \dots I) \cap (I + 1 \dots N) = \emptyset$
72		fzsplit	$⊢ I \in (2 \dots N) \to (2 \dots N) = (2 \dots I) \cup (I + 1 \dots N)$
73	65 72	syl	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to (2 \dots N) = (2 \dots I) \cup (I + 1 \dots N)$
74		fzfid	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to (2 \dots N) \in Fin$
75		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
76		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
77		fzss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 \dots N - 1) \subseteq (1 \dots N - 1)$
78	76 77	ax-mp	$⊢ (2 \dots N - 1) \subseteq (1 \dots N - 1)$
79	78	sseli	$⊢ I \in (2 \dots N - 1) \to I \in (1 \dots N - 1)$
80	2	axlowdimlem10	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to Q \in 𝔼 (N)$
81	75 79 80	syl2an	$⊢ (N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \to Q \in 𝔼 (N)$
82		fzss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 \dots N) \subseteq (1 \dots N)$
83	76 82	ax-mp	$⊢ (2 \dots N) \subseteq (1 \dots N)$
84	83	sseli	$⊢ i \in (2 \dots N) \to i \in (1 \dots N)$
85		fveecn	$⊢ (Q \in 𝔼 (N) \land i \in (1 \dots N)) \to Q (i) \in ℂ$
86	81 84 85	syl2an	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (2 \dots N)) \to Q (i) \in ℂ$
87	86	sqcld	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (2 \dots N)) \to {Q (i)}^{2} \in ℂ$
88	87	3adantl2	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots N)) \to {Q (i)}^{2} \in ℂ$
89	71 73 74 88	fsumsplit	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 2}^{N} {Q (i)}^{2} = \sum_{i = 2}^{I} {Q (i)}^{2} + \sum_{i = I + 1}^{N} {Q (i)}^{2}$
90		elfzelz	$⊢ I \in (2 \dots N - 1) \to I \in ℤ$
91	90	zred	$⊢ I \in (2 \dots N - 1) \to I \in ℝ$
92	91	3ad2ant3	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I \in ℝ$
93	49	3ad2ant1	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to N \in ℝ$
94		peano2rem	$⊢ N \in ℝ \to N - 1 \in ℝ$
95	93 94	syl	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to N - 1 \in ℝ$
96		elfzle2	$⊢ I \in (2 \dots N - 1) \to I \leq N - 1$
97	96	3ad2ant3	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I \leq N - 1$
98	93	ltm1d	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to N - 1 < N$
99	92 95 93 97 98	lelttrd	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I < N$
100	92 93 99	ltled	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I \leq N$
101	90	3ad2ant3	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I \in ℤ$
102		eluz	$⊢ (I \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq I} \leftrightarrow I \leq N)$
103	101 60 102	syl2anc	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to (N \in ℤ_{\geq I} \leftrightarrow I \leq N)$
104	100 103	mpbird	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to N \in ℤ_{\geq I}$
105		fzss2	$⊢ N \in ℤ_{\geq I} \to (1 \dots I) \subseteq (1 \dots N)$
106	104 105	syl	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to (1 \dots I) \subseteq (1 \dots N)$
107	106	sseld	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to (i \in (1 \dots I) \to i \in (1 \dots N))$
108		fzss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 \dots I) \subseteq (1 \dots I)$
109	76 108	ax-mp	$⊢ (2 \dots I) \subseteq (1 \dots I)$
110	109	sseli	$⊢ i \in (2 \dots I) \to i \in (1 \dots I)$
111	107 110	impel	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots I)) \to i \in (1 \dots N)$
112		elfzelz	$⊢ i \in (2 \dots I) \to i \in ℤ$
113	112	zred	$⊢ i \in (2 \dots I) \to i \in ℝ$
114	113	adantl	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots I)) \to i \in ℝ$
115	92	adantr	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots I)) \to I \in ℝ$
116		peano2re	$⊢ I \in ℝ \to I + 1 \in ℝ$
117	91 116	syl	$⊢ I \in (2 \dots N - 1) \to I + 1 \in ℝ$
118	117	3ad2ant3	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I + 1 \in ℝ$
119	118	adantr	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots I)) \to I + 1 \in ℝ$
120		elfzle2	$⊢ i \in (2 \dots I) \to i \leq I$
121	120	adantl	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots I)) \to i \leq I$
122	115	ltp1d	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots I)) \to I < I + 1$
123	114 115 119 121 122	lelttrd	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots I)) \to i < I + 1$
124	114 123	ltned	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots I)) \to i \neq I + 1$
125	2	axlowdimlem12	$⊢ (i \in (1 \dots N) \land i \neq I + 1) \to Q (i) = 0$
126	111 124 125	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots I)) \to Q (i) = 0$
127	126	sq0id	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (2 \dots I)) \to {Q (i)}^{2} = 0$
128	127	sumeq2dv	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 2}^{I} {Q (i)}^{2} = \sum_{i = 2}^{I} 0$
129		fzfi	$⊢ (2 \dots I) \in Fin$
130	129	olci	$⊢ ((2 \dots I) \subseteq ℤ_{\geq 1} \lor (2 \dots I) \in Fin)$
131		sumz	$⊢ ((2 \dots I) \subseteq ℤ_{\geq 1} \lor (2 \dots I) \in Fin) \to \sum_{i = 2}^{I} 0 = 0$
132	130 131	ax-mp	$⊢ \sum_{i = 2}^{I} 0 = 0$
133	128 132	eqtrdi	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 2}^{I} {Q (i)}^{2} = 0$
134	101	peano2zd	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I + 1 \in ℤ$
135		sq1	$⊢ 1^{2} = 1$
136	26 135	eqtrdi	$⊢ i = I + 1 \to {Q (i)}^{2} = 1$
137	136	fsum1	$⊢ (I + 1 \in ℤ \land 1 \in ℂ) \to \sum_{i = I + 1}^{I + 1} {Q (i)}^{2} = 1$
138	134 5 137	sylancl	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = I + 1}^{I + 1} {Q (i)}^{2} = 1$
139		oveq2	$⊢ I + 1 = N \to (I + 1 \dots I + 1) = (I + 1 \dots N)$
140	139	sumeq1d	$⊢ I + 1 = N \to \sum_{i = I + 1}^{I + 1} {Q (i)}^{2} = \sum_{i = I + 1}^{N} {Q (i)}^{2}$
141	140	eqeq1d	$⊢ I + 1 = N \to (\sum_{i = I + 1}^{I + 1} {Q (i)}^{2} = 1 \leftrightarrow \sum_{i = I + 1}^{N} {Q (i)}^{2} = 1)$
142	138 141	imbitrid	$⊢ I + 1 = N \to ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = I + 1}^{N} {Q (i)}^{2} = 1)$
143	101	adantl	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I \in ℤ$
144	143	zred	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I \in ℝ$
145	60	adantl	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to N \in ℤ$
146	145	zred	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to N \in ℝ$
147	146 94	syl	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to N - 1 \in ℝ$
148	97	adantl	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I \leq N - 1$
149	146	ltm1d	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to N - 1 < N$
150	144 147 146 148 149	lelttrd	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I < N$
151		1red	$⊢ I \in (2 \dots N - 1) \to 1 \in ℝ$
152		2re	$⊢ 2 \in ℝ$
153	152	a1i	$⊢ I \in (2 \dots N - 1) \to 2 \in ℝ$
154		1le2	$⊢ 1 \leq 2$
155	154	a1i	$⊢ I \in (2 \dots N - 1) \to 1 \leq 2$
156		elfzle1	$⊢ I \in (2 \dots N - 1) \to 2 \leq I$
157	151 153 91 155 156	letrd	$⊢ I \in (2 \dots N - 1) \to 1 \leq I$
158	157	3ad2ant3	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to 1 \leq I$
159	158	adantl	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to 1 \leq I$
160		elnnz1	$⊢ I \in ℕ \leftrightarrow (I \in ℤ \land 1 \leq I)$
161	143 159 160	sylanbrc	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I \in ℕ$
162	75	3ad2ant1	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to N \in ℕ$
163	162	adantl	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to N \in ℕ$
164		nnltp1le	$⊢ (I \in ℕ \land N \in ℕ) \to (I < N \leftrightarrow I + 1 \leq N)$
165	161 163 164	syl2anc	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to (I < N \leftrightarrow I + 1 \leq N)$
166	150 165	mpbid	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I + 1 \leq N$
167		eluz	$⊢ (I + 1 \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (I + 1)} \leftrightarrow I + 1 \leq N)$
168	134 145 167	syl2an2	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to (N \in ℤ_{\geq (I + 1)} \leftrightarrow I + 1 \leq N)$
169	166 168	mpbird	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to N \in ℤ_{\geq (I + 1)}$
170		simpr1	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to N \in ℤ_{\geq 3}$
171		simpr3	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I \in (2 \dots N - 1)$
172	170 171 81	syl2anc	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to Q \in 𝔼 (N)$
173	172	adantr	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 \dots N)) \to Q \in 𝔼 (N)$
174	161	peano2nnd	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I + 1 \in ℕ$
175		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
176	174 175	eleqtrdi	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I + 1 \in ℤ_{\geq 1}$
177		fzss1	$⊢ I + 1 \in ℤ_{\geq 1} \to (I + 1 \dots N) \subseteq (1 \dots N)$
178	176 177	syl	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to (I + 1 \dots N) \subseteq (1 \dots N)$
179	178	sselda	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 \dots N)) \to i \in (1 \dots N)$
180	173 179 85	syl2anc	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 \dots N)) \to Q (i) \in ℂ$
181	180	sqcld	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 \dots N)) \to {Q (i)}^{2} \in ℂ$
182	23	oveq1d	$⊢ i = I + 1 \to {Q (i)}^{2} = {Q (I + 1)}^{2}$
183	24	oveq1i	$⊢ {Q (I + 1)}^{2} = 1^{2}$
184	183 135	eqtri	$⊢ {Q (I + 1)}^{2} = 1$
185	182 184	eqtrdi	$⊢ i = I + 1 \to {Q (i)}^{2} = 1$
186	169 181 185	fsum1p	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to \sum_{i = I + 1}^{N} {Q (i)}^{2} = 1 + \sum_{i = I + 1 + 1}^{N} {Q (i)}^{2}$
187	174	peano2nnd	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I + 1 + 1 \in ℕ$
188	187 175	eleqtrdi	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I + 1 + 1 \in ℤ_{\geq 1}$
189		fzss1	$⊢ I + 1 + 1 \in ℤ_{\geq 1} \to (I + 1 + 1 \dots N) \subseteq (1 \dots N)$
190	188 189	syl	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to (I + 1 + 1 \dots N) \subseteq (1 \dots N)$
191	190	sselda	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 + 1 \dots N)) \to i \in (1 \dots N)$
192	144 116	syl	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to I + 1 \in ℝ$
193	192	adantr	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 + 1 \dots N)) \to I + 1 \in ℝ$
194		peano2re	$⊢ I + 1 \in ℝ \to I + 1 + 1 \in ℝ$
195	193 194	syl	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 + 1 \dots N)) \to I + 1 + 1 \in ℝ$
196		elfzelz	$⊢ i \in (I + 1 + 1 \dots N) \to i \in ℤ$
197	196	zred	$⊢ i \in (I + 1 + 1 \dots N) \to i \in ℝ$
198	197	adantl	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 + 1 \dots N)) \to i \in ℝ$
199	193	ltp1d	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 + 1 \dots N)) \to I + 1 < I + 1 + 1$
200		elfzle1	$⊢ i \in (I + 1 + 1 \dots N) \to I + 1 + 1 \leq i$
201	200	adantl	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 + 1 \dots N)) \to I + 1 + 1 \leq i$
202	193 195 198 199 201	ltletrd	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 + 1 \dots N)) \to I + 1 < i$
203	193 202	gtned	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 + 1 \dots N)) \to i \neq I + 1$
204	191 203 125	syl2anc	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 + 1 \dots N)) \to Q (i) = 0$
205	204	sq0id	$⊢ ((I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \land i \in (I + 1 + 1 \dots N)) \to {Q (i)}^{2} = 0$
206	205	sumeq2dv	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to \sum_{i = I + 1 + 1}^{N} {Q (i)}^{2} = \sum_{i = I + 1 + 1}^{N} 0$
207		fzfi	$⊢ (I + 1 + 1 \dots N) \in Fin$
208	207	olci	$⊢ ((I + 1 + 1 \dots N) \subseteq ℤ_{\geq 1} \lor (I + 1 + 1 \dots N) \in Fin)$
209		sumz	$⊢ ((I + 1 + 1 \dots N) \subseteq ℤ_{\geq 1} \lor (I + 1 + 1 \dots N) \in Fin) \to \sum_{i = I + 1 + 1}^{N} 0 = 0$
210	208 209	ax-mp	$⊢ \sum_{i = I + 1 + 1}^{N} 0 = 0$
211	206 210	eqtrdi	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to \sum_{i = I + 1 + 1}^{N} {Q (i)}^{2} = 0$
212	211	oveq2d	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to 1 + \sum_{i = I + 1 + 1}^{N} {Q (i)}^{2} = 1 + 0$
213		1p0e1	$⊢ 1 + 0 = 1$
214	212 213	eqtrdi	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to 1 + \sum_{i = I + 1 + 1}^{N} {Q (i)}^{2} = 1$
215	186 214	eqtrd	$⊢ (I + 1 \neq N \land (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1))) \to \sum_{i = I + 1}^{N} {Q (i)}^{2} = 1$
216	215	ex	$⊢ I + 1 \neq N \to ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = I + 1}^{N} {Q (i)}^{2} = 1)$
217	142 216	pm2.61ine	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = I + 1}^{N} {Q (i)}^{2} = 1$
218	133 217	oveq12d	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 2}^{I} {Q (i)}^{2} + \sum_{i = I + 1}^{N} {Q (i)}^{2} = 0 + 1$
219		0p1e1	$⊢ 0 + 1 = 1$
220	218 219	eqtrdi	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 2}^{I} {Q (i)}^{2} + \sum_{i = I + 1}^{N} {Q (i)}^{2} = 1$
221	89 220	eqtrd	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 2}^{N} {Q (i)}^{2} = 1$
222		simp1	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to N \in ℤ_{\geq 3}$
223		2lt3	$⊢ 2 < 3$
224	152 48 223	ltleii	$⊢ 2 \leq 3$
225		2z	$⊢ 2 \in ℤ$
226	225	eluz1i	$⊢ 3 \in ℤ_{\geq 2} \leftrightarrow (3 \in ℤ \land 2 \leq 3)$
227	4 224 226	mpbir2an	$⊢ 3 \in ℤ_{\geq 2}$
228		uztrn	$⊢ (N \in ℤ_{\geq 3} \land 3 \in ℤ_{\geq 2}) \to N \in ℤ_{\geq 2}$
229	222 227 228	sylancl	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to N \in ℤ_{\geq 2}$
230		fveq2	$⊢ i = 2 \to Q (i) = Q (2)$
231	230	oveq1d	$⊢ i = 2 \to {Q (i)}^{2} = {Q (2)}^{2}$
232	229 88 231	fsum1p	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 2}^{N} {Q (i)}^{2} = {Q (2)}^{2} + \sum_{i = 2 + 1}^{N} {Q (i)}^{2}$
233	59	adantr	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to N \in ℤ$
234	233	zred	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to N \in ℝ$
235		lttr	$⊢ (2 \in ℝ \land 3 \in ℝ \land N \in ℝ) \to ((2 < 3 \land 3 < N) \to 2 < N)$
236	152 48 235	mp3an12	$⊢ N \in ℝ \to ((2 < 3 \land 3 < N) \to 2 < N)$
237	223 236	mpani	$⊢ N \in ℝ \to (3 < N \to 2 < N)$
238	49 237	syl	$⊢ N \in ℤ_{\geq 3} \to (3 < N \to 2 < N)$
239	238	imp	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to 2 < N$
240		ltle	$⊢ (2 \in ℝ \land N \in ℝ) \to (2 < N \to 2 \leq N)$
241	152 240	mpan	$⊢ N \in ℝ \to (2 < N \to 2 \leq N)$
242	234 239 241	sylc	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to 2 \leq N$
243	242 154	jctil	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to (1 \leq 2 \land 2 \leq N)$
244		1z	$⊢ 1 \in ℤ$
245		elfz	$⊢ (2 \in ℤ \land 1 \in ℤ \land N \in ℤ) \to (2 \in (1 \dots N) \leftrightarrow (1 \leq 2 \land 2 \leq N))$
246	225 244 233 245	mp3an12i	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to (2 \in (1 \dots N) \leftrightarrow (1 \leq 2 \land 2 \leq N))$
247	243 246	mpbird	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to 2 \in (1 \dots N)$
248	247	3adant3	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to 2 \in (1 \dots N)$
249	91	ltp1d	$⊢ I \in (2 \dots N - 1) \to I < I + 1$
250	153 91 117 156 249	lelttrd	$⊢ I \in (2 \dots N - 1) \to 2 < I + 1$
251	250	3ad2ant3	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to 2 < I + 1$
252		ltne	$⊢ (2 \in ℝ \land 2 < I + 1) \to I + 1 \neq 2$
253	152 251 252	sylancr	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to I + 1 \neq 2$
254	253	necomd	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to 2 \neq I + 1$
255	2	axlowdimlem12	$⊢ (2 \in (1 \dots N) \land 2 \neq I + 1) \to Q (2) = 0$
256	248 254 255	syl2anc	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to Q (2) = 0$
257	256	sq0id	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to {Q (2)}^{2} = 0$
258	257	oveq1d	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to {Q (2)}^{2} + \sum_{i = 2 + 1}^{N} {Q (i)}^{2} = 0 + \sum_{i = 2 + 1}^{N} {Q (i)}^{2}$
259	16	oveq1i	$⊢ (3 \dots N) = (2 + 1 \dots N)$
260	259	sumeq1i	$⊢ \sum_{i = 3}^{N} {Q (i)}^{2} = \sum_{i = 2 + 1}^{N} {Q (i)}^{2}$
261	260	oveq2i	$⊢ 0 + \sum_{i = 3}^{N} {Q (i)}^{2} = 0 + \sum_{i = 2 + 1}^{N} {Q (i)}^{2}$
262	258 261	eqtr4di	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to {Q (2)}^{2} + \sum_{i = 2 + 1}^{N} {Q (i)}^{2} = 0 + \sum_{i = 3}^{N} {Q (i)}^{2}$
263		fzfid	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to (3 \dots N) \in Fin$
264		3nn	$⊢ 3 \in ℕ$
265	264 175	eleqtri	$⊢ 3 \in ℤ_{\geq 1}$
266		fzss1	$⊢ 3 \in ℤ_{\geq 1} \to (3 \dots N) \subseteq (1 \dots N)$
267	265 266	ax-mp	$⊢ (3 \dots N) \subseteq (1 \dots N)$
268	267	sseli	$⊢ i \in (3 \dots N) \to i \in (1 \dots N)$
269	81 268 85	syl2an	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to Q (i) \in ℂ$
270	269	sqcld	$⊢ ((N \in ℤ_{\geq 3} \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to {Q (i)}^{2} \in ℂ$
271	270	3adantl2	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \land i \in (3 \dots N)) \to {Q (i)}^{2} \in ℂ$
272	263 271	fsumcl	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 3}^{N} {Q (i)}^{2} \in ℂ$
273	272	addlidd	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to 0 + \sum_{i = 3}^{N} {Q (i)}^{2} = \sum_{i = 3}^{N} {Q (i)}^{2}$
274	232 262 273	3eqtrrd	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 3}^{N} {Q (i)}^{2} = \sum_{i = 2}^{N} {Q (i)}^{2}$
275		simpl	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to N \in ℤ_{\geq 3}$
276	1	axlowdimlem7	$⊢ N \in ℤ_{\geq 3} \to P \in 𝔼 (N)$
277	276	ad2antrr	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N) \land i \in (3 \dots N)) \to P \in 𝔼 (N)$
278	268	adantl	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N) \land i \in (3 \dots N)) \to i \in (1 \dots N)$
279		fveecn	$⊢ (P \in 𝔼 (N) \land i \in (1 \dots N)) \to P (i) \in ℂ$
280	277 278 279	syl2anc	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N) \land i \in (3 \dots N)) \to P (i) \in ℂ$
281	280	sqcld	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N) \land i \in (3 \dots N)) \to {P (i)}^{2} \in ℂ$
282		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
283	10 282	eqtrdi	$⊢ i = 3 \to {P (i)}^{2} = 1$
284	275 281 283	fsum1p	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to \sum_{i = 3}^{N} {P (i)}^{2} = 1 + \sum_{i = 3 + 1}^{N} {P (i)}^{2}$
285		1re	$⊢ 1 \in ℝ$
286		zaddcl	$⊢ (3 \in ℤ \land 1 \in ℤ) \to 3 + 1 \in ℤ$
287	4 244 286	mp2an	$⊢ 3 + 1 \in ℤ$
288	287	zrei	$⊢ 3 + 1 \in ℝ$
289		1lt3	$⊢ 1 < 3$
290	48	ltp1i	$⊢ 3 < 3 + 1$
291	285 48 288	lttri	$⊢ (1 < 3 \land 3 < 3 + 1) \to 1 < 3 + 1$
292	289 290 291	mp2an	$⊢ 1 < 3 + 1$
293	285 288 292	ltleii	$⊢ 1 \leq 3 + 1$
294		eluz	$⊢ (1 \in ℤ \land 3 + 1 \in ℤ) \to (3 + 1 \in ℤ_{\geq 1} \leftrightarrow 1 \leq 3 + 1)$
295	244 287 294	mp2an	$⊢ 3 + 1 \in ℤ_{\geq 1} \leftrightarrow 1 \leq 3 + 1$
296	293 295	mpbir	$⊢ 3 + 1 \in ℤ_{\geq 1}$
297		fzss1	$⊢ 3 + 1 \in ℤ_{\geq 1} \to (3 + 1 \dots N) \subseteq (1 \dots N)$
298	296 297	ax-mp	$⊢ (3 + 1 \dots N) \subseteq (1 \dots N)$
299	298	sseli	$⊢ i \in (3 + 1 \dots N) \to i \in (1 \dots N)$
300	48 288	ltnlei	$⊢ 3 < 3 + 1 \leftrightarrow \neg 3 + 1 \leq 3$
301	290 300	mpbi	$⊢ \neg 3 + 1 \leq 3$
302	301	intnanr	$⊢ \neg (3 + 1 \leq 3 \land 3 \leq N)$
303		elfz	$⊢ (3 \in ℤ \land 3 + 1 \in ℤ \land N \in ℤ) \to (3 \in (3 + 1 \dots N) \leftrightarrow (3 + 1 \leq 3 \land 3 \leq N))$
304	4 287 233 303	mp3an12i	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to (3 \in (3 + 1 \dots N) \leftrightarrow (3 + 1 \leq 3 \land 3 \leq N))$
305	302 304	mtbiri	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to \neg 3 \in (3 + 1 \dots N)$
306		eleq1	$⊢ i = 3 \to (i \in (3 + 1 \dots N) \leftrightarrow 3 \in (3 + 1 \dots N))$
307	306	notbid	$⊢ i = 3 \to (\neg i \in (3 + 1 \dots N) \leftrightarrow \neg 3 \in (3 + 1 \dots N))$
308	305 307	syl5ibrcom	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to (i = 3 \to \neg i \in (3 + 1 \dots N))$
309	308	necon2ad	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to (i \in (3 + 1 \dots N) \to i \neq 3)$
310	309	imp	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N) \land i \in (3 + 1 \dots N)) \to i \neq 3$
311	1	axlowdimlem9	$⊢ (i \in (1 \dots N) \land i \neq 3) \to P (i) = 0$
312	299 310 311	syl2an2	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N) \land i \in (3 + 1 \dots N)) \to P (i) = 0$
313	312	sq0id	$⊢ ((N \in ℤ_{\geq 3} \land 3 < N) \land i \in (3 + 1 \dots N)) \to {P (i)}^{2} = 0$
314	313	sumeq2dv	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to \sum_{i = 3 + 1}^{N} {P (i)}^{2} = \sum_{i = 3 + 1}^{N} 0$
315		fzfi	$⊢ (3 + 1 \dots N) \in Fin$
316	315	olci	$⊢ ((3 + 1 \dots N) \subseteq ℤ_{\geq 1} \lor (3 + 1 \dots N) \in Fin)$
317		sumz	$⊢ ((3 + 1 \dots N) \subseteq ℤ_{\geq 1} \lor (3 + 1 \dots N) \in Fin) \to \sum_{i = 3 + 1}^{N} 0 = 0$
318	316 317	ax-mp	$⊢ \sum_{i = 3 + 1}^{N} 0 = 0$
319	314 318	eqtrdi	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to \sum_{i = 3 + 1}^{N} {P (i)}^{2} = 0$
320	319	oveq2d	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to 1 + \sum_{i = 3 + 1}^{N} {P (i)}^{2} = 1 + 0$
321	284 320	eqtrd	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to \sum_{i = 3}^{N} {P (i)}^{2} = 1 + 0$
322	321 213	eqtrdi	$⊢ (N \in ℤ_{\geq 3} \land 3 < N) \to \sum_{i = 3}^{N} {P (i)}^{2} = 1$
323	322	3adant3	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 3}^{N} {P (i)}^{2} = 1$
324	221 274 323	3eqtr4rd	$⊢ (N \in ℤ_{\geq 3} \land 3 < N \land I \in (2 \dots N - 1)) \to \sum_{i = 3}^{N} {P (i)}^{2} = \sum_{i = 3}^{N} {Q (i)}^{2}$
325	44 54 55 324	syl3anc	$⊢ (N \neq 3 \land (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}$
326	325	ex	$⊢ N \neq 3 \to ((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})$
327	43 326	pm2.61ine	$⊢ (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}$

Metamath Proof Explorer

Theorem axlowdimlem16

Proof