Metamath Proof Explorer

Theorem 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 , -u 1 >. } u. ( ( ( 1 ... N ) \ { 3 } ) X. { 0 } ) )
axlowdimlem16.2 
|- Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) )
Assertion axlowdimlem16 
|- ( ( N e. ( ZZ>= ` 3 ) /\ I e. ( 2 ... ( N - 1 ) ) ) -> sum_ i e. ( 3 ... N ) ( ( P ` i ) ^ 2 ) = sum_ i e. ( 3 ... N ) ( ( Q ` i ) ^ 2 ) )

Proof

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