Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axlowdimlem16 Structured version   Unicode version

Theorem axlowdimlem16 25901
Description: Lemma for axlowdim 25905. Set up a summation that will help establish distance. (Contributed by Scott Fenton, 21-Apr-2013.)
Hypotheses
Ref Expression
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
Ref Expression
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 ) )
Distinct variable groups:    P, i    i, I    i, N    Q, i

Proof of Theorem axlowdimlem16
StepHypRef Expression
1 elfz1eq 11073 . . . . . 6  |-  ( I  e.  ( 2 ... 2 )  ->  I  =  2 )
2 oveq1 6091 . . . . . . . . . . 11  |-  ( I  =  2  ->  (
I  +  1 )  =  ( 2  +  1 ) )
3 df-3 10064 . . . . . . . . . . 11  |-  3  =  ( 2  +  1 )
42, 3syl6reqr 2489 . . . . . . . . . 10  |-  ( I  =  2  ->  3  =  ( I  + 
1 ) )
54, 4oveq12d 6102 . . . . . . . . 9  |-  ( I  =  2  ->  (
3 ... 3 )  =  ( ( I  + 
1 ) ... (
I  +  1 ) ) )
65sumeq1d 12500 . . . . . . . 8  |-  ( I  =  2  ->  sum_ i  e.  ( 3 ... 3
) ( ( Q `
 i ) ^
2 )  =  sum_ i  e.  ( (
I  +  1 ) ... ( I  + 
1 ) ) ( ( Q `  i
) ^ 2 ) )
72, 3syl6eqr 2488 . . . . . . . . . 10  |-  ( I  =  2  ->  (
I  +  1 )  =  3 )
8 3nn 10139 . . . . . . . . . . 11  |-  3  e.  NN
98nnzi 10310 . . . . . . . . . 10  |-  3  e.  ZZ
107, 9syl6eqel 2526 . . . . . . . . 9  |-  ( I  =  2  ->  (
I  +  1 )  e.  ZZ )
11 ax-1cn 9053 . . . . . . . . . 10  |-  1  e.  CC
1211sqcli 11467 . . . . . . . . 9  |-  ( 1 ^ 2 )  e.  CC
13 fveq2 5731 . . . . . . . . . . . 12  |-  ( i  =  ( I  + 
1 )  ->  ( Q `  i )  =  ( Q `  ( I  +  1
) ) )
14 axlowdimlem16.2 . . . . . . . . . . . . 13  |-  Q  =  ( { <. (
I  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( I  + 
1 ) } )  X.  { 0 } ) )
1514axlowdimlem11 25896 . . . . . . . . . . . 12  |-  ( Q `
 ( I  + 
1 ) )  =  1
1613, 15syl6eq 2486 . . . . . . . . . . 11  |-  ( i  =  ( I  + 
1 )  ->  ( Q `  i )  =  1 )
1716oveq1d 6099 . . . . . . . . . 10  |-  ( i  =  ( I  + 
1 )  ->  (
( Q `  i
) ^ 2 )  =  ( 1 ^ 2 ) )
1817fsum1 12540 . . . . . . . . 9  |-  ( ( ( I  +  1 )  e.  ZZ  /\  ( 1 ^ 2 )  e.  CC )  ->  sum_ i  e.  ( ( I  +  1 ) ... ( I  +  1 ) ) ( ( Q `  i ) ^ 2 )  =  ( 1 ^ 2 ) )
1910, 12, 18sylancl 645 . . . . . . . 8  |-  ( I  =  2  ->  sum_ i  e.  ( ( I  + 
1 ) ... (
I  +  1 ) ) ( ( Q `
 i ) ^
2 )  =  ( 1 ^ 2 ) )
206, 19eqtrd 2470 . . . . . . 7  |-  ( I  =  2  ->  sum_ i  e.  ( 3 ... 3
) ( ( Q `
 i ) ^
2 )  =  ( 1 ^ 2 ) )
21 fveq2 5731 . . . . . . . . . . . 12  |-  ( i  =  3  ->  ( P `  i )  =  ( P ` 
3 ) )
22 axlowdimlem16.1 . . . . . . . . . . . . 13  |-  P  =  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) )
2322axlowdimlem8 25893 . . . . . . . . . . . 12  |-  ( P `
 3 )  = 
-u 1
2421, 23syl6eq 2486 . . . . . . . . . . 11  |-  ( i  =  3  ->  ( P `  i )  =  -u 1 )
2524oveq1d 6099 . . . . . . . . . 10  |-  ( i  =  3  ->  (
( P `  i
) ^ 2 )  =  ( -u 1 ^ 2 ) )
26 sqneg 11447 . . . . . . . . . . 11  |-  ( 1  e.  CC  ->  ( -u 1 ^ 2 )  =  ( 1 ^ 2 ) )
2711, 26ax-mp 5 . . . . . . . . . 10  |-  ( -u
1 ^ 2 )  =  ( 1 ^ 2 )
2825, 27syl6eq 2486 . . . . . . . . 9  |-  ( i  =  3  ->  (
( P `  i
) ^ 2 )  =  ( 1 ^ 2 ) )
2928fsum1 12540 . . . . . . . 8  |-  ( ( 3  e.  ZZ  /\  ( 1 ^ 2 )  e.  CC )  ->  sum_ i  e.  ( 3 ... 3 ) ( ( P `  i ) ^ 2 )  =  ( 1 ^ 2 ) )
309, 12, 29mp2an 655 . . . . . . 7  |-  sum_ i  e.  ( 3 ... 3
) ( ( P `
 i ) ^
2 )  =  ( 1 ^ 2 )
3120, 30syl6reqr 2489 . . . . . 6  |-  ( I  =  2  ->  sum_ i  e.  ( 3 ... 3
) ( ( P `
 i ) ^
2 )  =  sum_ i  e.  ( 3 ... 3 ) ( ( Q `  i
) ^ 2 ) )
321, 31syl 16 . . . . 5  |-  ( I  e.  ( 2 ... 2 )  ->  sum_ i  e.  ( 3 ... 3
) ( ( P `
 i ) ^
2 )  =  sum_ i  e.  ( 3 ... 3 ) ( ( Q `  i
) ^ 2 ) )
3332a1i 11 . . . 4  |-  ( N  =  3  ->  (
I  e.  ( 2 ... 2 )  ->  sum_ i  e.  ( 3 ... 3 ) ( ( P `  i
) ^ 2 )  =  sum_ i  e.  ( 3 ... 3 ) ( ( Q `  i ) ^ 2 ) ) )
34 oveq1 6091 . . . . . . 7  |-  ( N  =  3  ->  ( N  -  1 )  =  ( 3  -  1 ) )
35 3m1e2 10101 . . . . . . 7  |-  ( 3  -  1 )  =  2
3634, 35syl6eq 2486 . . . . . 6  |-  ( N  =  3  ->  ( N  -  1 )  =  2 )
3736oveq2d 6100 . . . . 5  |-  ( N  =  3  ->  (
2 ... ( N  - 
1 ) )  =  ( 2 ... 2
) )
3837eleq2d 2505 . . . 4  |-  ( N  =  3  ->  (
I  e.  ( 2 ... ( N  - 
1 ) )  <->  I  e.  ( 2 ... 2
) ) )
39 oveq2 6092 . . . . . 6  |-  ( N  =  3  ->  (
3 ... N )  =  ( 3 ... 3
) )
4039sumeq1d 12500 . . . . 5  |-  ( N  =  3  ->  sum_ i  e.  ( 3 ... N
) ( ( P `
 i ) ^
2 )  =  sum_ i  e.  ( 3 ... 3 ) ( ( P `  i
) ^ 2 ) )
4139sumeq1d 12500 . . . . 5  |-  ( N  =  3  ->  sum_ i  e.  ( 3 ... N
) ( ( Q `
 i ) ^
2 )  =  sum_ i  e.  ( 3 ... 3 ) ( ( Q `  i
) ^ 2 ) )
4240, 41eqeq12d 2452 . . . 4  |-  ( 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 ) ) )
4333, 38, 423imtr4d 261 . . 3  |-  ( N  =  3  ->  (
I  e.  ( 2 ... ( N  - 
1 ) )  ->  sum_ i  e.  ( 3 ... N ) ( ( P `  i
) ^ 2 )  =  sum_ i  e.  ( 3 ... N ) ( ( Q `  i ) ^ 2 ) ) )
4443adantld 455 . 2  |-  ( 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 ) ) )
45 simprl 734 . . . 4  |-  ( ( N  =/=  3  /\  ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) ) )  ->  N  e.  ( ZZ>= `  3 )
)
46 eluzle 10503 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  <_  N )
4746adantl 454 . . . . . 6  |-  ( ( N  =/=  3  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
3  <_  N )
48 simpl 445 . . . . . 6  |-  ( ( N  =/=  3  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  N  =/=  3 )
49 3re 10076 . . . . . . 7  |-  3  e.  RR
50 eluzelre 10502 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  RR )
5150adantl 454 . . . . . . 7  |-  ( ( N  =/=  3  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  N  e.  RR )
52 ltlen 9180 . . . . . . 7  |-  ( ( 3  e.  RR  /\  N  e.  RR )  ->  ( 3  <  N  <->  ( 3  <_  N  /\  N  =/=  3 ) ) )
5349, 51, 52sylancr 646 . . . . . 6  |-  ( ( N  =/=  3  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( 3  <  N  <->  ( 3  <_  N  /\  N  =/=  3 ) ) )
5447, 48, 53mpbir2and 890 . . . . 5  |-  ( ( N  =/=  3  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
3  <  N )
5554adantrr 699 . . . 4  |-  ( ( N  =/=  3  /\  ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) ) )  ->  3  <  N )
56 simprr 735 . . . 4  |-  ( ( N  =/=  3  /\  ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) ) )  ->  I  e.  ( 2 ... ( N  -  1 ) ) )
57 fzssp1 11100 . . . . . . . . . . . . 13  |-  ( 2 ... ( N  - 
1 ) )  C_  ( 2 ... (
( N  -  1 )  +  1 ) )
58 simp3 960 . . . . . . . . . . . . 13  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  ( 2 ... ( N  -  1 ) ) )
5957, 58sseldi 3348 . . . . . . . . . . . 12  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  ( 2 ... (
( N  -  1 )  +  1 ) ) )
60 eluzelz 10501 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ZZ )
61603ad2ant1 979 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  ZZ )
6261zcnd 10381 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  CC )
63 npcan 9319 . . . . . . . . . . . . . 14  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  - 
1 )  +  1 )  =  N )
6462, 11, 63sylancl 645 . . . . . . . . . . . . 13  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  =  N )
6564oveq2d 6100 . . . . . . . . . . . 12  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
2 ... ( ( N  -  1 )  +  1 ) )  =  ( 2 ... N
) )
6659, 65eleqtrd 2514 . . . . . . . . . . 11  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  ( 2 ... N
) )
67 elfzelz 11064 . . . . . . . . . . 11  |-  ( I  e.  ( 2 ... N )  ->  I  e.  ZZ )
6866, 67syl 16 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  ZZ )
6968zred 10380 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  RR )
7069ltp1d 9946 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  <  ( I  +  1 ) )
71 fzdisj 11083 . . . . . . . 8  |-  ( I  <  ( I  + 
1 )  ->  (
( 2 ... I
)  i^i  ( (
I  +  1 ) ... N ) )  =  (/) )
7270, 71syl 16 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
( 2 ... I
)  i^i  ( (
I  +  1 ) ... N ) )  =  (/) )
73 fzsplit 11082 . . . . . . . 8  |-  ( I  e.  ( 2 ... N )  ->  (
2 ... N )  =  ( ( 2 ... I )  u.  (
( I  +  1 ) ... N ) ) )
7466, 73syl 16 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
2 ... N )  =  ( ( 2 ... I )  u.  (
( I  +  1 ) ... N ) ) )
75 fzfid 11317 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
2 ... N )  e. 
Fin )
76 uznnssnn 10529 . . . . . . . . . . . . 13  |-  ( 3  e.  NN  ->  ( ZZ>=
`  3 )  C_  NN )
778, 76ax-mp 5 . . . . . . . . . . . 12  |-  ( ZZ>= ` 
3 )  C_  NN
7877sseli 3346 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  NN )
79 2nn 10138 . . . . . . . . . . . . . 14  |-  2  e.  NN
80 nnuz 10526 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  1 )
8179, 80eleqtri 2510 . . . . . . . . . . . . 13  |-  2  e.  ( ZZ>= `  1 )
82 fzss1 11096 . . . . . . . . . . . . 13  |-  ( 2  e.  ( ZZ>= `  1
)  ->  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) ) )
8381, 82ax-mp 5 . . . . . . . . . . . 12  |-  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) )
8483sseli 3346 . . . . . . . . . . 11  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  I  e.  ( 1 ... ( N  -  1 ) ) )
8514axlowdimlem10 25895 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  I  e.  ( 1 ... ( N  - 
1 ) ) )  ->  Q  e.  ( EE `  N ) )
8678, 84, 85syl2an 465 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  Q  e.  ( EE `  N
) )
87 fzss1 11096 . . . . . . . . . . . 12  |-  ( 2  e.  ( ZZ>= `  1
)  ->  ( 2 ... N )  C_  ( 1 ... N
) )
8881, 87ax-mp 5 . . . . . . . . . . 11  |-  ( 2 ... N )  C_  ( 1 ... N
)
8988sseli 3346 . . . . . . . . . 10  |-  ( i  e.  ( 2 ... N )  ->  i  e.  ( 1 ... N
) )
90 fveecn 25846 . . . . . . . . . 10  |-  ( ( Q  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( Q `  i )  e.  CC )
9186, 89, 90syl2an 465 . . . . . . . . 9  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) )  /\  i  e.  ( 2 ... N ) )  ->  ( Q `  i )  e.  CC )
9291sqcld 11526 . . . . . . . 8  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) )  /\  i  e.  ( 2 ... N ) )  ->  ( ( Q `  i ) ^ 2 )  e.  CC )
93923adantl2 1115 . . . . . . 7  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... N
) )  ->  (
( Q `  i
) ^ 2 )  e.  CC )
9472, 74, 75, 93fsumsplit 12538 . . . . . 6  |-  ( ( 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 ) ) )
95 fzss1 11096 . . . . . . . . . . . . . . . 16  |-  ( 2  e.  ( ZZ>= `  1
)  ->  ( 2 ... I )  C_  ( 1 ... I
) )
9681, 95ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( 2 ... I )  C_  ( 1 ... I
)
9796sseli 3346 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 2 ... I )  ->  i  e.  ( 1 ... I
) )
98 elfzelz 11064 . . . . . . . . . . . . . . . . . . . 20  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  I  e.  ZZ )
9998zred 10380 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  I  e.  RR )
100993ad2ant3 981 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  RR )
101503ad2ant1 979 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  RR )
102 peano2rem 9372 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  RR  ->  ( N  -  1 )  e.  RR )
103101, 102syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
104 elfzle2 11066 . . . . . . . . . . . . . . . . . . . 20  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  I  <_  ( N  -  1 ) )
1051043ad2ant3 981 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  <_  ( N  -  1 ) )
106101ltm1d 9948 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
107100, 103, 101, 105, 106lelttrd 9233 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  <  N )
108100, 101, 107ltled 9226 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  <_  N )
109983ad2ant3 981 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  ZZ )
110 eluz 10504 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  I )  <->  I  <_  N ) )
111109, 61, 110syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( N  e.  ( ZZ>= `  I )  <->  I  <_  N ) )
112108, 111mpbird 225 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  I )
)
113 fzss2 11097 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  I
)  ->  ( 1 ... I )  C_  ( 1 ... N
) )
114112, 113syl 16 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
1 ... I )  C_  ( 1 ... N
) )
115114sseld 3349 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
i  e.  ( 1 ... I )  -> 
i  e.  ( 1 ... N ) ) )
11697, 115syl5 31 . . . . . . . . . . . . 13  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
i  e.  ( 2 ... I )  -> 
i  e.  ( 1 ... N ) ) )
117116imp 420 . . . . . . . . . . . 12  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  i  e.  ( 1 ... N
) )
118 elfzelz 11064 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 2 ... I )  ->  i  e.  ZZ )
119118zred 10380 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 2 ... I )  ->  i  e.  RR )
120119adantl 454 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  i  e.  RR )
121100adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  I  e.  RR )
122 peano2re 9244 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  RR  ->  (
I  +  1 )  e.  RR )
12399, 122syl 16 . . . . . . . . . . . . . . . 16  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  (
I  +  1 )  e.  RR )
1241233ad2ant3 981 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
I  +  1 )  e.  RR )
125124adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  (
I  +  1 )  e.  RR )
126 elfzle2 11066 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 2 ... I )  ->  i  <_  I )
127126adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  i  <_  I )
128121ltp1d 9946 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  I  <  ( I  +  1 ) )
129120, 121, 125, 127, 128lelttrd 9233 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  i  <  ( I  +  1 ) )
130120, 129ltned 9214 . . . . . . . . . . . 12  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  i  =/=  ( I  +  1 ) )
13114axlowdimlem12 25897 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 1 ... N )  /\  i  =/=  ( I  + 
1 ) )  -> 
( Q `  i
)  =  0 )
132117, 130, 131syl2anc 644 . . . . . . . . . . 11  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  ( Q `  i )  =  0 )
133132sq0id 11480 . . . . . . . . . 10  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  (
( Q `  i
) ^ 2 )  =  0 )
134133sumeq2dv 12502 . . . . . . . . 9  |-  ( ( 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 )
135 fzfi 11316 . . . . . . . . . . 11  |-  ( 2 ... I )  e. 
Fin
136135olci 382 . . . . . . . . . 10  |-  ( ( 2 ... I ) 
C_  ( ZZ>= `  1
)  \/  ( 2 ... I )  e. 
Fin )
137 sumz 12521 . . . . . . . . . 10  |-  ( ( ( 2 ... I
)  C_  ( ZZ>= ` 
1 )  \/  (
2 ... I )  e. 
Fin )  ->  sum_ i  e.  ( 2 ... I
) 0  =  0 )
138136, 137ax-mp 5 . . . . . . . . 9  |-  sum_ i  e.  ( 2 ... I
) 0  =  0
139134, 138syl6eq 2486 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( 2 ... I
) ( ( Q `
 i ) ^
2 )  =  0 )
140109peano2zd 10383 . . . . . . . . . . 11  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
I  +  1 )  e.  ZZ )
141 sq1 11481 . . . . . . . . . . . . 13  |-  ( 1 ^ 2 )  =  1
14217, 141syl6eq 2486 . . . . . . . . . . . 12  |-  ( i  =  ( I  + 
1 )  ->  (
( Q `  i
) ^ 2 )  =  1 )
143142fsum1 12540 . . . . . . . . . . 11  |-  ( ( ( I  +  1 )  e.  ZZ  /\  1  e.  CC )  -> 
sum_ i  e.  ( ( I  +  1 ) ... ( I  +  1 ) ) ( ( Q `  i ) ^ 2 )  =  1 )
144140, 11, 143sylancl 645 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( ( I  + 
1 ) ... (
I  +  1 ) ) ( ( Q `
 i ) ^
2 )  =  1 )
145 oveq2 6092 . . . . . . . . . . . 12  |-  ( ( I  +  1 )  =  N  ->  (
( I  +  1 ) ... ( I  +  1 ) )  =  ( ( I  +  1 ) ... N ) )
146145sumeq1d 12500 . . . . . . . . . . 11  |-  ( ( I  +  1 )  =  N  ->  sum_ i  e.  ( ( I  + 
1 ) ... (
I  +  1 ) ) ( ( Q `
 i ) ^
2 )  =  sum_ i  e.  ( (
I  +  1 ) ... N ) ( ( Q `  i
) ^ 2 ) )
147146eqeq1d 2446 . . . . . . . . . 10  |-  ( ( I  +  1 )  =  N  ->  ( sum_ i  e.  ( ( I  +  1 ) ... ( I  + 
1 ) ) ( ( Q `  i
) ^ 2 )  =  1  <->  sum_ i  e.  ( ( I  + 
1 ) ... N
) ( ( Q `
 i ) ^
2 )  =  1 ) )
148144, 147syl5ib 212 . . . . . . . . 9  |-  ( ( I  +  1 )  =  N  ->  (
( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( ( I  + 
1 ) ... N
) ( ( Q `
 i ) ^
2 )  =  1 ) )
149109adantl 454 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  e.  ZZ )
150149zred 10380 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  e.  RR )
15161adantl 454 . . . . . . . . . . . . . . . . 17  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  N  e.  ZZ )
152151zred 10380 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  N  e.  RR )
153152, 102syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( N  -  1 )  e.  RR )
154105adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  <_  ( N  - 
1 ) )
155152ltm1d 9948 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( N  -  1 )  <  N )
156150, 153, 152, 154, 155lelttrd 9233 . . . . . . . . . . . . . 14  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  <  N )
157 1re 9095 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR
158157a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  1  e.  RR )
159 2re 10074 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
160159a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  2  e.  RR )
161 1lt2 10147 . . . . . . . . . . . . . . . . . . . . 21  |-  1  <  2
162157, 159, 161ltleii 9201 . . . . . . . . . . . . . . . . . . . 20  |-  1  <_  2
163162a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  1  <_  2 )
164 elfzle1 11065 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  2  <_  I )
165158, 160, 99, 163, 164letrd 9232 . . . . . . . . . . . . . . . . . 18  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  1  <_  I )
1661653ad2ant3 981 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  1  <_  I )
167166adantl 454 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
1  <_  I )
168 elnnz1 10312 . . . . . . . . . . . . . . . 16  |-  ( I  e.  NN  <->  ( I  e.  ZZ  /\  1  <_  I ) )
169149, 167, 168sylanbrc 647 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  e.  NN )
170783ad2ant1 979 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  NN )
171170adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  N  e.  NN )
172 nnltp1le 10335 . . . . . . . . . . . . . . 15  |-  ( ( I  e.  NN  /\  N  e.  NN )  ->  ( I  <  N  <->  ( I  +  1 )  <_  N ) )
173169, 171, 172syl2anc 644 . . . . . . . . . . . . . 14  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  <  N  <->  ( I  +  1 )  <_  N ) )
174156, 173mpbid 203 . . . . . . . . . . . . 13  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  +  1 )  <_  N )
175140adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  +  1 )  e.  ZZ )
176 eluz 10504 . . . . . . . . . . . . . 14  |-  ( ( ( I  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( I  + 
1 ) )  <->  ( I  +  1 )  <_  N ) )
177175, 151, 176syl2anc 644 . . . . . . . . . . . . 13  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( N  e.  (
ZZ>= `  ( I  + 
1 ) )  <->  ( I  +  1 )  <_  N ) )
178174, 177mpbird 225 . . . . . . . . . . . 12  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  N  e.  ( ZZ>= `  ( I  +  1
) ) )
179 simpr1 964 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  N  e.  ( ZZ>= ` 
3 ) )
180 simpr3 966 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  e.  ( 2 ... ( N  - 
1 ) ) )
181179, 180, 86syl2anc 644 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  Q  e.  ( EE `  N ) )
182181adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
I  +  1 ) ... N ) )  ->  Q  e.  ( EE `  N ) )
183169peano2nnd 10022 . . . . . . . . . . . . . . . . 17  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  +  1 )  e.  NN )
184183, 80syl6eleq 2528 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  +  1 )  e.  ( ZZ>= ` 
1 ) )
185 fzss1 11096 . . . . . . . . . . . . . . . 16  |-  ( ( I  +  1 )  e.  ( ZZ>= `  1
)  ->  ( (
I  +  1 ) ... N )  C_  ( 1 ... N
) )
186184, 185syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( ( I  + 
1 ) ... N
)  C_  ( 1 ... N ) )
187186sselda 3350 . . . . . . . . . . . . . 14  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
I  +  1 ) ... N ) )  ->  i  e.  ( 1 ... N ) )
188182, 187, 90syl2anc 644 . . . . . . . . . . . . 13  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
I  +  1 ) ... N ) )  ->  ( Q `  i )  e.  CC )
189188sqcld 11526 . . . . . . . . . . . 12  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
I  +  1 ) ... N ) )  ->  ( ( Q `
 i ) ^
2 )  e.  CC )
19013oveq1d 6099 . . . . . . . . . . . . 13  |-  ( i  =  ( I  + 
1 )  ->  (
( Q `  i
) ^ 2 )  =  ( ( Q `
 ( I  + 
1 ) ) ^
2 ) )
19115oveq1i 6094 . . . . . . . . . . . . . 14  |-  ( ( Q `  ( I  +  1 ) ) ^ 2 )  =  ( 1 ^ 2 )
192191, 141eqtri 2458 . . . . . . . . . . . . 13  |-  ( ( Q `  ( I  +  1 ) ) ^ 2 )  =  1
193190, 192syl6eq 2486 . . . . . . . . . . . 12  |-  ( i  =  ( I  + 
1 )  ->  (
( Q `  i
) ^ 2 )  =  1 )
194178, 189, 193fsum1p 12544 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
195183peano2nnd 10022 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( ( I  + 
1 )  +  1 )  e.  NN )
196195, 80syl6eleq 2528 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( ( I  + 
1 )  +  1 )  e.  ( ZZ>= ` 
1 ) )
197 fzss1 11096 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( I  +  1 )  +  1 )  e.  ( ZZ>= `  1
)  ->  ( (
( I  +  1 )  +  1 ) ... N )  C_  ( 1 ... N
) )
198196, 197syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( ( ( I  +  1 )  +  1 ) ... N
)  C_  ( 1 ... N ) )
199198sselda 3350 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
( I  +  1 )  +  1 ) ... N ) )  ->  i  e.  ( 1 ... N ) )
200150, 122syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  +  1 )  e.  RR )
201200adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
( I  +  1 )  +  1 ) ... N ) )  ->  ( I  + 
1 )  e.  RR )
202 peano2re 9244 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( I  +  1 )  e.  RR  ->  (
( I  +  1 )  +  1 )  e.  RR )
203201, 202syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
204 elfzelz 11064 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( ( ( I  +  1 )  +  1 ) ... N )  ->  i  e.  ZZ )
205204zred 10380 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( ( ( I  +  1 )  +  1 ) ... N )  ->  i  e.  RR )
206205adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
( I  +  1 )  +  1 ) ... N ) )  ->  i  e.  RR )
207201ltp1d 9946 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 ) )
208 elfzle1 11065 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( ( ( I  +  1 )  +  1 ) ... N )  ->  (
( I  +  1 )  +  1 )  <_  i )
209208adantl 454 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
( I  +  1 )  +  1 ) ... N ) )  ->  ( ( I  +  1 )  +  1 )  <_  i
)
210201, 203, 206, 207, 209ltletrd 9235 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
( I  +  1 )  +  1 ) ... N ) )  ->  ( I  + 
1 )  <  i
)
211201, 210gtned 9213 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
( I  +  1 )  +  1 ) ... N ) )  ->  i  =/=  (
I  +  1 ) )
212199, 211, 131syl2anc 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
( I  +  1 )  +  1 ) ... N ) )  ->  ( Q `  i )  =  0 )
213212sq0id 11480 . . . . . . . . . . . . . . 15  |-  ( ( ( ( I  + 
1 )  =/=  N  /\  ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  /\  i  e.  ( (
( I  +  1 )  +  1 ) ... N ) )  ->  ( ( Q `
 i ) ^
2 )  =  0 )
214213sumeq2dv 12502 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
215 fzfi 11316 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  +  1 ) ... N )  e. 
Fin
216215olci 382 . . . . . . . . . . . . . . 15  |-  ( ( ( ( I  + 
1 )  +  1 ) ... N ) 
C_  ( ZZ>= `  1
)  \/  ( ( ( I  +  1 )  +  1 ) ... N )  e. 
Fin )
217 sumz 12521 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( I  +  1 )  +  1 ) ... N
)  C_  ( ZZ>= ` 
1 )  \/  (
( ( I  + 
1 )  +  1 ) ... N )  e.  Fin )  ->  sum_ i  e.  ( ( ( I  +  1 )  +  1 ) ... N ) 0  =  0 )
218216, 217ax-mp 5 . . . . . . . . . . . . . 14  |-  sum_ i  e.  ( ( ( I  +  1 )  +  1 ) ... N
) 0  =  0
219214, 218syl6eq 2486 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
220219oveq2d 6100 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
22111addid1i 9258 . . . . . . . . . . . 12  |-  ( 1  +  0 )  =  1
222220, 221syl6eq 2486 . . . . . . . . . . 11  |-  ( ( ( 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 )
223194, 222eqtrd 2470 . . . . . . . . . 10  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  sum_ i  e.  ( ( I  +  1 ) ... N ) ( ( Q `  i
) ^ 2 )  =  1 )
224223ex 425 . . . . . . . . 9  |-  ( ( I  +  1 )  =/=  N  ->  (
( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( ( I  + 
1 ) ... N
) ( ( Q `
 i ) ^
2 )  =  1 ) )
225148, 224pm2.61ine 2682 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( ( I  + 
1 ) ... N
) ( ( Q `
 i ) ^
2 )  =  1 )
226139, 225oveq12d 6102 . . . . . . 7  |-  ( ( 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 ) )
227 0p1e1 10098 . . . . . . 7  |-  ( 0  +  1 )  =  1
228226, 227syl6eq 2486 . . . . . 6  |-  ( ( 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 )
22994, 228eqtrd 2470 . . . . 5  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( 2 ... N
) ( ( Q `
 i ) ^
2 )  =  1 )
230 simp1 958 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  3 )
)
231 2lt3 10148 . . . . . . . . . 10  |-  2  <  3
232159, 49, 231ltleii 9201 . . . . . . . . 9  |-  2  <_  3
233 2z 10317 . . . . . . . . . 10  |-  2  e.  ZZ
234233eluz1i 10500 . . . . . . . . 9  |-  ( 3  e.  ( ZZ>= `  2
)  <->  ( 3  e.  ZZ  /\  2  <_ 
3 ) )
2359, 232, 234mpbir2an 888 . . . . . . . 8  |-  3  e.  ( ZZ>= `  2 )
236 uztrn 10507 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  e.  ( ZZ>= `  2 )
)  ->  N  e.  ( ZZ>= `  2 )
)
237230, 235, 236sylancl 645 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  2 )
)
238 fveq2 5731 . . . . . . . 8  |-  ( i  =  2  ->  ( Q `  i )  =  ( Q ` 
2 ) )
239238oveq1d 6099 . . . . . . 7  |-  ( i  =  2  ->  (
( Q `  i
) ^ 2 )  =  ( ( Q `
 2 ) ^
2 ) )
240237, 93, 239fsum1p 12544 . . . . . 6  |-  ( ( 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 ) ) )
24160adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  N  e.  ZZ )
242241zred 10380 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  N  e.  RR )
243 lttr 9157 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  3  e.  RR  /\  N  e.  RR )  ->  (
( 2  <  3  /\  3  <  N )  ->  2  <  N
) )
244159, 49, 243mp3an12 1270 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  RR  ->  (
( 2  <  3  /\  3  <  N )  ->  2  <  N
) )
245231, 244mpani 659 . . . . . . . . . . . . . . . 16  |-  ( N  e.  RR  ->  (
3  <  N  ->  2  <  N ) )
24650, 245syl 16 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  <  N  ->  2  <  N ) )
247246imp 420 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  2  <  N )
248 ltle 9168 . . . . . . . . . . . . . . 15  |-  ( ( 2  e.  RR  /\  N  e.  RR )  ->  ( 2  <  N  ->  2  <_  N )
)
249159, 248mpan 653 . . . . . . . . . . . . . 14  |-  ( N  e.  RR  ->  (
2  <  N  ->  2  <_  N ) )
250242, 247, 249sylc 59 . . . . . . . . . . . . 13  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  2  <_  N )
251250, 162jctil 525 . . . . . . . . . . . 12  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  (
1  <_  2  /\  2  <_  N ) )
252 1z 10316 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
253 elfz 11054 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  ZZ  /\  1  e.  ZZ  /\  N  e.  ZZ )  ->  (
2  e.  ( 1 ... N )  <->  ( 1  <_  2  /\  2  <_  N ) ) )
254233, 252, 253mp3an12 1270 . . . . . . . . . . . . 13  |-  ( N  e.  ZZ  ->  (
2  e.  ( 1 ... N )  <->  ( 1  <_  2  /\  2  <_  N ) ) )
255241, 254syl 16 . . . . . . . . . . . 12  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  (
2  e.  ( 1 ... N )  <->  ( 1  <_  2  /\  2  <_  N ) ) )
256251, 255mpbird 225 . . . . . . . . . . 11  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  2  e.  ( 1 ... N
) )
2572563adant3 978 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  2  e.  ( 1 ... N
) )
25899ltp1d 9946 . . . . . . . . . . . . . 14  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  I  <  ( I  +  1 ) )
259160, 99, 123, 164, 258lelttrd 9233 . . . . . . . . . . . . 13  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  2  <  ( I  +  1 ) )
2602593ad2ant3 981 . . . . . . . . . . . 12  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  2  <  ( I  +  1 ) )
261 ltne 9175 . . . . . . . . . . . 12  |-  ( ( 2  e.  RR  /\  2  <  ( I  + 
1 ) )  -> 
( I  +  1 )  =/=  2 )
262159, 260, 261sylancr 646 . . . . . . . . . . 11  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
I  +  1 )  =/=  2 )
263262necomd 2689 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  2  =/=  ( I  +  1 ) )
26414axlowdimlem12 25897 . . . . . . . . . 10  |-  ( ( 2  e.  ( 1 ... N )  /\  2  =/=  ( I  + 
1 ) )  -> 
( Q `  2
)  =  0 )
265257, 263, 264syl2anc 644 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( Q `  2 )  =  0 )
266265sq0id 11480 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
( Q `  2
) ^ 2 )  =  0 )
267266oveq1d 6099 . . . . . . 7  |-  ( ( 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 ) ) )
2683oveq1i 6094 . . . . . . . . 9  |-  ( 3 ... N )  =  ( ( 2  +  1 ) ... N
)
269268sumeq1i 12497 . . . . . . . 8  |-  sum_ i  e.  ( 3 ... N
) ( ( Q `
 i ) ^
2 )  =  sum_ i  e.  ( (
2  +  1 ) ... N ) ( ( Q `  i
) ^ 2 )
270269oveq2i 6095 . . . . . . 7  |-  ( 0  +  sum_ i  e.  ( 3 ... N ) ( ( Q `  i ) ^ 2 ) )  =  ( 0  +  sum_ i  e.  ( ( 2  +  1 ) ... N
) ( ( Q `
 i ) ^
2 ) )
271267, 270syl6eqr 2488 . . . . . 6  |-  ( ( 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 ) ) )
272 fzfid 11317 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
3 ... N )  e. 
Fin )
2738, 80eleqtri 2510 . . . . . . . . . . . . 13  |-  3  e.  ( ZZ>= `  1 )
274 fzss1 11096 . . . . . . . . . . . . 13  |-  ( 3  e.  ( ZZ>= `  1
)  ->  ( 3 ... N )  C_  ( 1 ... N
) )
275273, 274ax-mp 5 . . . . . . . . . . . 12  |-  ( 3 ... N )  C_  ( 1 ... N
)
276275sseli 3346 . . . . . . . . . . 11  |-  ( i  e.  ( 3 ... N )  ->  i  e.  ( 1 ... N
) )
27786, 276, 90syl2an 465 . . . . . . . . . 10  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) )  /\  i  e.  ( 3 ... N ) )  ->  ( Q `  i )  e.  CC )
278277sqcld 11526 . . . . . . . . 9  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) )  /\  i  e.  ( 3 ... N ) )  ->  ( ( Q `  i ) ^ 2 )  e.  CC )
2792783adantl2 1115 . . . . . . . 8  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 3 ... N
) )  ->  (
( Q `  i
) ^ 2 )  e.  CC )
280272, 279fsumcl 12532 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( 3 ... N
) ( ( Q `
 i ) ^
2 )  e.  CC )
281280addid2d 9272 . . . . . 6  |-  ( ( 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 ) )
282240, 271, 2813eqtrrd 2475 . . . . 5  |-  ( ( 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 ) )
283 simpl 445 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  N  e.  ( ZZ>= `  3 )
)
28422axlowdimlem7 25892 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  P  e.  ( EE `  N ) )
285284ad2antrr 708 . . . . . . . . . . 11  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( 3 ... N ) )  ->  P  e.  ( EE `  N ) )
286276adantl 454 . . . . . . . . . . 11  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( 3 ... N ) )  ->  i  e.  ( 1 ... N ) )
287 fveecn 25846 . . . . . . . . . . 11  |-  ( ( P  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( P `  i )  e.  CC )
288285, 286, 287syl2anc 644 . . . . . . . . . 10  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( 3 ... N ) )  ->  ( P `  i )  e.  CC )
289288sqcld 11526 . . . . . . . . 9  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( 3 ... N ) )  ->  ( ( P `
 i ) ^
2 )  e.  CC )
29027, 141eqtri 2458 . . . . . . . . . 10  |-  ( -u
1 ^ 2 )  =  1
29125, 290syl6eq 2486 . . . . . . . . 9  |-  ( i  =  3  ->  (
( P `  i
) ^ 2 )  =  1 )
292283, 289, 291fsum1p 12544 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  sum_ i  e.  ( 3 ... N
) ( ( P `
 i ) ^
2 )  =  ( 1  +  sum_ i  e.  ( ( 3  +  1 ) ... N
) ( ( P `
 i ) ^
2 ) ) )
293 zaddcl 10322 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 3  e.  ZZ  /\  1  e.  ZZ )  ->  ( 3  +  1 )  e.  ZZ )
2949, 252, 293mp2an 655 . . . . . . . . . . . . . . . . . . 19  |-  ( 3  +  1 )  e.  ZZ
295294zrei 10293 . . . . . . . . . . . . . . . . . 18  |-  ( 3  +  1 )  e.  RR
296 1lt3 10149 . . . . . . . . . . . . . . . . . . 19  |-  1  <  3
29749ltp1i 9919 . . . . . . . . . . . . . . . . . . 19  |-  3  <  ( 3  +  1 )
298157, 49, 295lttri 9204 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  <  3  /\  3  <  ( 3  +  1 ) )  ->  1  <  (
3  +  1 ) )
299296, 297, 298mp2an 655 . . . . . . . . . . . . . . . . . 18  |-  1  <  ( 3  +  1 )
300157, 295, 299ltleii 9201 . . . . . . . . . . . . . . . . 17  |-  1  <_  ( 3  +  1 )
301 eluz 10504 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  ZZ  /\  ( 3  +  1 )  e.  ZZ )  ->  ( ( 3  +  1 )  e.  ( ZZ>= `  1 )  <->  1  <_  ( 3  +  1 ) ) )
302252, 294, 301mp2an 655 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  +  1 )  e.  ( ZZ>= `  1
)  <->  1  <_  (
3  +  1 ) )
303300, 302mpbir 202 . . . . . . . . . . . . . . . 16  |-  ( 3  +  1 )  e.  ( ZZ>= `  1 )
304 fzss1 11096 . . . . . . . . . . . . . . . 16  |-  ( ( 3  +  1 )  e.  ( ZZ>= `  1
)  ->  ( (
3  +  1 ) ... N )  C_  ( 1 ... N
) )
305303, 304ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( 3  +  1 ) ... N )  C_  ( 1 ... N
)
306305sseli 3346 . . . . . . . . . . . . . 14  |-  ( i  e.  ( ( 3  +  1 ) ... N )  ->  i  e.  ( 1 ... N
) )
307306adantl 454 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( (
3  +  1 ) ... N ) )  ->  i  e.  ( 1 ... N ) )
30849, 295ltnlei 9199 . . . . . . . . . . . . . . . . . . 19  |-  ( 3  <  ( 3  +  1 )  <->  -.  (
3  +  1 )  <_  3 )
309297, 308mpbi 201 . . . . . . . . . . . . . . . . . 18  |-  -.  (
3  +  1 )  <_  3
310309intnanr 883 . . . . . . . . . . . . . . . . 17  |-  -.  (
( 3  +  1 )  <_  3  /\  3  <_  N )
311 elfz 11054 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 3  e.  ZZ  /\  ( 3  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( 3  e.  ( ( 3  +  1 ) ... N )  <-> 
( ( 3  +  1 )  <_  3  /\  3  <_  N ) ) )
3129, 294, 311mp3an12 1270 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ZZ  ->  (
3  e.  ( ( 3  +  1 ) ... N )  <->  ( (
3  +  1 )  <_  3  /\  3  <_  N ) ) )
313241, 312syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  (
3  e.  ( ( 3  +  1 ) ... N )  <->  ( (
3  +  1 )  <_  3  /\  3  <_  N ) ) )
314310, 313mtbiri 296 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  -.  3  e.  ( (
3  +  1 ) ... N ) )
315 eleq1 2498 . . . . . . . . . . . . . . . . 17  |-  ( i  =  3  ->  (
i  e.  ( ( 3  +  1 ) ... N )  <->  3  e.  ( ( 3  +  1 ) ... N
) ) )
316315notbid 287 . . . . . . . . . . . . . . . 16  |-  ( i  =  3  ->  ( -.  i  e.  (
( 3  +  1 ) ... N )  <->  -.  3  e.  (
( 3  +  1 ) ... N ) ) )
317314, 316syl5ibrcom 215 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  (
i  =  3  ->  -.  i  e.  (
( 3  +  1 ) ... N ) ) )
318317necon2ad 2654 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  (
i  e.  ( ( 3  +  1 ) ... N )  -> 
i  =/=  3 ) )
319318imp 420 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( (
3  +  1 ) ... N ) )  ->  i  =/=  3
)
32022axlowdimlem9 25894 . . . . . . . . . . . . 13  |-  ( ( i  e.  ( 1 ... N )  /\  i  =/=  3 )  -> 
( P `  i
)  =  0 )
321307, 319, 320syl2anc 644 . . . . . . . . . . . 12  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( (
3  +  1 ) ... N ) )  ->  ( P `  i )  =  0 )
322321sq0id 11480 . . . . . . . . . . 11  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( (
3  +  1 ) ... N ) )  ->  ( ( P `
 i ) ^
2 )  =  0 )
323322sumeq2dv 12502 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  sum_ i  e.  ( ( 3  +  1 ) ... N
) ( ( P `
 i ) ^
2 )  =  sum_ i  e.  ( (
3  +  1 ) ... N ) 0 )
324 fzfi 11316 . . . . . . . . . . . 12  |-  ( ( 3  +  1 ) ... N )  e. 
Fin
325324olci 382 . . . . . . . . . . 11  |-  ( ( ( 3  +  1 ) ... N ) 
C_  ( ZZ>= `  1
)  \/  ( ( 3  +  1 ) ... N )  e. 
Fin )
326 sumz 12521 . . . . . . . . . . 11  |-  ( ( ( ( 3  +  1 ) ... N
)  C_  ( ZZ>= ` 
1 )  \/  (
( 3  +  1 ) ... N )  e.  Fin )  ->  sum_ i  e.  ( ( 3  +  1 ) ... N ) 0  =  0 )
327325, 326ax-mp 5 . . . . . . . . . 10  |-  sum_ i  e.  ( ( 3  +  1 ) ... N
) 0  =  0
328323, 327syl6eq 2486 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  sum_ i  e.  ( ( 3  +  1 ) ... N
) ( ( P `
 i ) ^
2 )  =  0 )
329328oveq2d 6100 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  (
1  +  sum_ i  e.  ( ( 3  +  1 ) ... N
) ( ( P `
 i ) ^
2 ) )  =  ( 1  +  0 ) )
330292, 329eqtrd 2470 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  sum_ i  e.  ( 3 ... N
) ( ( P `
 i ) ^
2 )  =  ( 1  +  0 ) )
331330, 221syl6eq 2486 . . . . . 6  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  sum_ i  e.  ( 3 ... N
) ( ( P `
 i ) ^
2 )  =  1 )
3323313adant3 978 . . . . 5  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( 3 ... N
) ( ( P `
 i ) ^
2 )  =  1 )
333229, 282, 3323eqtr4rd 2481 . . . 4  |-  ( ( 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 ) )
33445, 55, 56, 333syl3anc 1185 . . 3  |-  ( ( 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 ) )
335334ex 425 . 2  |-  ( 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 ) ) )
33644, 335pm2.61ine 2682 1  |-  ( ( 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 ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    \/ wo 359    /\ wa 360    /\ w3a 937    = wceq 1653    e. wcel 1726    =/= wne 2601    \ cdif 3319    u. cun 3320    i^i cin 3321    C_ wss 3322   (/)c0 3630   {csn 3816   <.cop 3819   class class class wbr 4215    X. cxp 4879   ` cfv 5457  (class class class)co 6084   Fincfn 7112   CCcc 8993   RRcr 8994   0cc0 8995   1c1 8996    + caddc 8998    < clt 9125    <_ cle 9126    - cmin 9296   -ucneg 9297   NNcn 10005   2c2 10054   3c3 10055   ZZcz 10287   ZZ>=cuz 10493   ...cfz 11048   ^cexp 11387   sum_csu 12484   EEcee 25832
This theorem is referenced by:  axlowdimlem17  25902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-inf2 7599  ax-cnex 9051  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072  ax-pre-sup 9073
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-se 4545  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-isom 5466  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-riota 6552  df-recs 6636  df-rdg 6671  df-1o 6727  df-oadd 6731  df-er 6908  df-map 7023  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-sup 7449  df-oi 7482  df-card 7831  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-div 9683  df-nn 10006  df-2 10063  df-3 10064  df-n0 10227  df-z 10288  df-uz 10494  df-rp 10618  df-fz 11049  df-fzo 11141  df-seq 11329  df-exp 11388  df-hash 11624  df-cj 11909  df-re 11910  df-im 11911  df-sqr 12045  df-abs 12046  df-clim 12287  df-sum 12485  df-ee 25835
  Copyright terms: Public domain W3C validator