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

Theorem axlowdimlem16 25800
Description: Lemma for axlowdim 25804. 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 11024 . . . . . 6  |-  ( I  e.  ( 2 ... 2 )  ->  I  =  2 )
2 oveq1 6047 . . . . . . . . . . 11  |-  ( I  =  2  ->  (
I  +  1 )  =  ( 2  +  1 ) )
3 df-3 10015 . . . . . . . . . . 11  |-  3  =  ( 2  +  1 )
42, 3syl6reqr 2455 . . . . . . . . . 10  |-  ( I  =  2  ->  3  =  ( I  + 
1 ) )
54, 4oveq12d 6058 . . . . . . . . 9  |-  ( I  =  2  ->  (
3 ... 3 )  =  ( ( I  + 
1 ) ... (
I  +  1 ) ) )
65sumeq1d 12450 . . . . . . . 8  |-  ( I  =  2  ->  sum_ i  e.  ( 3 ... 3
) ( ( Q `
 i ) ^
2 )  =  sum_ i  e.  ( (
I  +  1 ) ... ( I  + 
1 ) ) ( ( Q `  i
) ^ 2 ) )
72, 3syl6eqr 2454 . . . . . . . . . 10  |-  ( I  =  2  ->  (
I  +  1 )  =  3 )
8 3nn 10090 . . . . . . . . . . 11  |-  3  e.  NN
98nnzi 10261 . . . . . . . . . 10  |-  3  e.  ZZ
107, 9syl6eqel 2492 . . . . . . . . 9  |-  ( I  =  2  ->  (
I  +  1 )  e.  ZZ )
11 ax-1cn 9004 . . . . . . . . . 10  |-  1  e.  CC
1211sqcli 11417 . . . . . . . . 9  |-  ( 1 ^ 2 )  e.  CC
13 fveq2 5687 . . . . . . . . . . . 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 25795 . . . . . . . . . . . 12  |-  ( Q `
 ( I  + 
1 ) )  =  1
1613, 15syl6eq 2452 . . . . . . . . . . 11  |-  ( i  =  ( I  + 
1 )  ->  ( Q `  i )  =  1 )
1716oveq1d 6055 . . . . . . . . . 10  |-  ( i  =  ( I  + 
1 )  ->  (
( Q `  i
) ^ 2 )  =  ( 1 ^ 2 ) )
1817fsum1 12490 . . . . . . . . 9  |-  ( ( ( I  +  1 )  e.  ZZ  /\  ( 1 ^ 2 )  e.  CC )  ->  sum_ i  e.  ( ( I  +  1 ) ... ( I  +  1 ) ) ( ( Q `  i ) ^ 2 )  =  ( 1 ^ 2 ) )
1910, 12, 18sylancl 644 . . . . . . . 8  |-  ( I  =  2  ->  sum_ i  e.  ( ( I  + 
1 ) ... (
I  +  1 ) ) ( ( Q `
 i ) ^
2 )  =  ( 1 ^ 2 ) )
206, 19eqtrd 2436 . . . . . . 7  |-  ( I  =  2  ->  sum_ i  e.  ( 3 ... 3
) ( ( Q `
 i ) ^
2 )  =  ( 1 ^ 2 ) )
21 fveq2 5687 . . . . . . . . . . . 12  |-  ( i  =  3  ->  ( P `  i )  =  ( P ` 
3 ) )
22 axlowdimlem16.1 . . . . . . . . . . . . 13  |-  P  =  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) )
2322axlowdimlem8 25792 . . . . . . . . . . . 12  |-  ( P `
 3 )  = 
-u 1
2421, 23syl6eq 2452 . . . . . . . . . . 11  |-  ( i  =  3  ->  ( P `  i )  =  -u 1 )
2524oveq1d 6055 . . . . . . . . . 10  |-  ( i  =  3  ->  (
( P `  i
) ^ 2 )  =  ( -u 1 ^ 2 ) )
26 sqneg 11397 . . . . . . . . . . 11  |-  ( 1  e.  CC  ->  ( -u 1 ^ 2 )  =  ( 1 ^ 2 ) )
2711, 26ax-mp 8 . . . . . . . . . 10  |-  ( -u
1 ^ 2 )  =  ( 1 ^ 2 )
2825, 27syl6eq 2452 . . . . . . . . 9  |-  ( i  =  3  ->  (
( P `  i
) ^ 2 )  =  ( 1 ^ 2 ) )
2928fsum1 12490 . . . . . . . 8  |-  ( ( 3  e.  ZZ  /\  ( 1 ^ 2 )  e.  CC )  ->  sum_ i  e.  ( 3 ... 3 ) ( ( P `  i ) ^ 2 )  =  ( 1 ^ 2 ) )
309, 12, 29mp2an 654 . . . . . . 7  |-  sum_ i  e.  ( 3 ... 3
) ( ( P `
 i ) ^
2 )  =  ( 1 ^ 2 )
3120, 30syl6reqr 2455 . . . . . 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 6047 . . . . . . 7  |-  ( N  =  3  ->  ( N  -  1 )  =  ( 3  -  1 ) )
35 3m1e2 10052 . . . . . . 7  |-  ( 3  -  1 )  =  2
3634, 35syl6eq 2452 . . . . . 6  |-  ( N  =  3  ->  ( N  -  1 )  =  2 )
3736oveq2d 6056 . . . . 5  |-  ( N  =  3  ->  (
2 ... ( N  - 
1 ) )  =  ( 2 ... 2
) )
3837eleq2d 2471 . . . 4  |-  ( N  =  3  ->  (
I  e.  ( 2 ... ( N  - 
1 ) )  <->  I  e.  ( 2 ... 2
) ) )
39 oveq2 6048 . . . . . 6  |-  ( N  =  3  ->  (
3 ... N )  =  ( 3 ... 3
) )
4039sumeq1d 12450 . . . . 5  |-  ( N  =  3  ->  sum_ i  e.  ( 3 ... N
) ( ( P `
 i ) ^
2 )  =  sum_ i  e.  ( 3 ... 3 ) ( ( P `  i
) ^ 2 ) )
4139sumeq1d 12450 . . . . 5  |-  ( N  =  3  ->  sum_ i  e.  ( 3 ... N
) ( ( Q `
 i ) ^
2 )  =  sum_ i  e.  ( 3 ... 3 ) ( ( Q `  i
) ^ 2 ) )
4240, 41eqeq12d 2418 . . . 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 260 . . 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 454 . 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 733 . . . 4  |-  ( ( N  =/=  3  /\  ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) ) )  ->  N  e.  ( ZZ>= `  3 )
)
46 eluzle 10454 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  <_  N )
4746adantl 453 . . . . . 6  |-  ( ( N  =/=  3  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
3  <_  N )
48 simpl 444 . . . . . 6  |-  ( ( N  =/=  3  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  N  =/=  3 )
49 3re 10027 . . . . . . 7  |-  3  e.  RR
50 eluzelre 10453 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  RR )
5150adantl 453 . . . . . . 7  |-  ( ( N  =/=  3  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  N  e.  RR )
52 ltlen 9131 . . . . . . 7  |-  ( ( 3  e.  RR  /\  N  e.  RR )  ->  ( 3  <  N  <->  ( 3  <_  N  /\  N  =/=  3 ) ) )
5349, 51, 52sylancr 645 . . . . . 6  |-  ( ( N  =/=  3  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( 3  <  N  <->  ( 3  <_  N  /\  N  =/=  3 ) ) )
5447, 48, 53mpbir2and 889 . . . . 5  |-  ( ( N  =/=  3  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
3  <  N )
5554adantrr 698 . . . 4  |-  ( ( N  =/=  3  /\  ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) ) )  ->  3  <  N )
56 simprr 734 . . . 4  |-  ( ( N  =/=  3  /\  ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) ) )  ->  I  e.  ( 2 ... ( N  -  1 ) ) )
57 fzssp1 11051 . . . . . . . . . . . . 13  |-  ( 2 ... ( N  - 
1 ) )  C_  ( 2 ... (
( N  -  1 )  +  1 ) )
58 simp3 959 . . . . . . . . . . . . 13  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  ( 2 ... ( N  -  1 ) ) )
5957, 58sseldi 3306 . . . . . . . . . . . 12  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  ( 2 ... (
( N  -  1 )  +  1 ) ) )
60 eluzelz 10452 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ZZ )
61603ad2ant1 978 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  ZZ )
6261zcnd 10332 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  CC )
63 npcan 9270 . . . . . . . . . . . . . 14  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  - 
1 )  +  1 )  =  N )
6462, 11, 63sylancl 644 . . . . . . . . . . . . 13  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  =  N )
6564oveq2d 6056 . . . . . . . . . . . 12  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
2 ... ( ( N  -  1 )  +  1 ) )  =  ( 2 ... N
) )
6659, 65eleqtrd 2480 . . . . . . . . . . 11  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  ( 2 ... N
) )
67 elfzelz 11015 . . . . . . . . . . 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 10331 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  RR )
7069ltp1d 9897 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  <  ( I  +  1 ) )
71 fzdisj 11034 . . . . . . . 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 11033 . . . . . . . 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 11267 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
2 ... N )  e. 
Fin )
76 uznnssnn 10480 . . . . . . . . . . . . 13  |-  ( 3  e.  NN  ->  ( ZZ>=
`  3 )  C_  NN )
778, 76ax-mp 8 . . . . . . . . . . . 12  |-  ( ZZ>= ` 
3 )  C_  NN
7877sseli 3304 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  NN )
79 2nn 10089 . . . . . . . . . . . . . 14  |-  2  e.  NN
80 nnuz 10477 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  1 )
8179, 80eleqtri 2476 . . . . . . . . . . . . 13  |-  2  e.  ( ZZ>= `  1 )
82 fzss1 11047 . . . . . . . . . . . . 13  |-  ( 2  e.  ( ZZ>= `  1
)  ->  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) ) )
8381, 82ax-mp 8 . . . . . . . . . . . 12  |-  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) )
8483sseli 3304 . . . . . . . . . . 11  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  I  e.  ( 1 ... ( N  -  1 ) ) )
8514axlowdimlem10 25794 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  I  e.  ( 1 ... ( N  - 
1 ) ) )  ->  Q  e.  ( EE `  N ) )
8678, 84, 85syl2an 464 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  Q  e.  ( EE `  N
) )
87 fzss1 11047 . . . . . . . . . . . 12  |-  ( 2  e.  ( ZZ>= `  1
)  ->  ( 2 ... N )  C_  ( 1 ... N
) )
8881, 87ax-mp 8 . . . . . . . . . . 11  |-  ( 2 ... N )  C_  ( 1 ... N
)
8988sseli 3304 . . . . . . . . . 10  |-  ( i  e.  ( 2 ... N )  ->  i  e.  ( 1 ... N
) )
90 fveecn 25745 . . . . . . . . . 10  |-  ( ( Q  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( Q `  i )  e.  CC )
9186, 89, 90syl2an 464 . . . . . . . . 9  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) )  /\  i  e.  ( 2 ... N ) )  ->  ( Q `  i )  e.  CC )
9291sqcld 11476 . . . . . . . 8  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) )  /\  i  e.  ( 2 ... N ) )  ->  ( ( Q `  i ) ^ 2 )  e.  CC )
93923adantl2 1114 . . . . . . 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 12488 . . . . . 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 11047 . . . . . . . . . . . . . . . 16  |-  ( 2  e.  ( ZZ>= `  1
)  ->  ( 2 ... I )  C_  ( 1 ... I
) )
9681, 95ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( 2 ... I )  C_  ( 1 ... I
)
9796sseli 3304 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 2 ... I )  ->  i  e.  ( 1 ... I
) )
98 elfzelz 11015 . . . . . . . . . . . . . . . . . . . 20  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  I  e.  ZZ )
9998zred 10331 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  I  e.  RR )
100993ad2ant3 980 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  RR )
101503ad2ant1 978 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  RR )
102 peano2rem 9323 . . . . . . . . . . . . . . . . . . . 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 11017 . . . . . . . . . . . . . . . . . . . 20  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  I  <_  ( N  -  1 ) )
1051043ad2ant3 980 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  <_  ( N  -  1 ) )
106101ltm1d 9899 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
107100, 103, 101, 105, 106lelttrd 9184 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  <  N )
108100, 101, 107ltled 9177 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  <_  N )
109983ad2ant3 980 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  I  e.  ZZ )
110 eluz 10455 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  I )  <->  I  <_  N ) )
111109, 61, 110syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( N  e.  ( ZZ>= `  I )  <->  I  <_  N ) )
112108, 111mpbird 224 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  I )
)
113 fzss2 11048 . . . . . . . . . . . . . . . 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 3307 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
i  e.  ( 1 ... I )  -> 
i  e.  ( 1 ... N ) ) )
11697, 115syl5 30 . . . . . . . . . . . . 13  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
i  e.  ( 2 ... I )  -> 
i  e.  ( 1 ... N ) ) )
117116imp 419 . . . . . . . . . . . 12  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  i  e.  ( 1 ... N
) )
118 elfzelz 11015 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 2 ... I )  ->  i  e.  ZZ )
119118zred 10331 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 2 ... I )  ->  i  e.  RR )
120119adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  i  e.  RR )
121100adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  I  e.  RR )
122 peano2re 9195 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  RR  ->  (
I  +  1 )  e.  RR )
12399, 122syl 16 . . . . . . . . . . . . . . . 16  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  (
I  +  1 )  e.  RR )
1241233ad2ant3 980 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
I  +  1 )  e.  RR )
125124adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  (
I  +  1 )  e.  RR )
126 elfzle2 11017 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 2 ... I )  ->  i  <_  I )
127126adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  i  <_  I )
128121ltp1d 9897 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  I  <  ( I  +  1 ) )
129120, 121, 125, 127, 128lelttrd 9184 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  i  <  ( I  +  1 ) )
130120, 129ltned 9165 . . . . . . . . . . . 12  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  i  =/=  ( I  +  1 ) )
13114axlowdimlem12 25796 . . . . . . . . . . . 12  |-  ( ( i  e.  ( 1 ... N )  /\  i  =/=  ( I  + 
1 ) )  -> 
( Q `  i
)  =  0 )
132117, 130, 131syl2anc 643 . . . . . . . . . . 11  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  ( Q `  i )  =  0 )
133132sq0id 11430 . . . . . . . . . 10  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 2 ... I
) )  ->  (
( Q `  i
) ^ 2 )  =  0 )
134133sumeq2dv 12452 . . . . . . . . 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 11266 . . . . . . . . . . 11  |-  ( 2 ... I )  e. 
Fin
136135olci 381 . . . . . . . . . 10  |-  ( ( 2 ... I ) 
C_  ( ZZ>= `  1
)  \/  ( 2 ... I )  e. 
Fin )
137 sumz 12471 . . . . . . . . . 10  |-  ( ( ( 2 ... I
)  C_  ( ZZ>= ` 
1 )  \/  (
2 ... I )  e. 
Fin )  ->  sum_ i  e.  ( 2 ... I
) 0  =  0 )
138136, 137ax-mp 8 . . . . . . . . 9  |-  sum_ i  e.  ( 2 ... I
) 0  =  0
139134, 138syl6eq 2452 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( 2 ... I
) ( ( Q `
 i ) ^
2 )  =  0 )
140109peano2zd 10334 . . . . . . . . . . 11  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
I  +  1 )  e.  ZZ )
141 sq1 11431 . . . . . . . . . . . . 13  |-  ( 1 ^ 2 )  =  1
14217, 141syl6eq 2452 . . . . . . . . . . . 12  |-  ( i  =  ( I  + 
1 )  ->  (
( Q `  i
) ^ 2 )  =  1 )
143142fsum1 12490 . . . . . . . . . . 11  |-  ( ( ( I  +  1 )  e.  ZZ  /\  1  e.  CC )  -> 
sum_ i  e.  ( ( I  +  1 ) ... ( I  +  1 ) ) ( ( Q `  i ) ^ 2 )  =  1 )
144140, 11, 143sylancl 644 . . . . . . . . . 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 6048 . . . . . . . . . . . 12  |-  ( ( I  +  1 )  =  N  ->  (
( I  +  1 ) ... ( I  +  1 ) )  =  ( ( I  +  1 ) ... N ) )
146145sumeq1d 12450 . . . . . . . . . . 11  |-  ( ( I  +  1 )  =  N  ->  sum_ i  e.  ( ( I  + 
1 ) ... (
I  +  1 ) ) ( ( Q `
 i ) ^
2 )  =  sum_ i  e.  ( (
I  +  1 ) ... N ) ( ( Q `  i
) ^ 2 ) )
147146eqeq1d 2412 . . . . . . . . . 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 211 . . . . . . . . 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 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  e.  ZZ )
150149zred 10331 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  e.  RR )
15161adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  N  e.  ZZ )
152151zred 10331 . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  <_  ( N  - 
1 ) )
155152ltm1d 9899 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( N  -  1 )  <  N )
156150, 153, 152, 154, 155lelttrd 9184 . . . . . . . . . . . . . 14  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  <  N )
157 1re 9046 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR
158157a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  1  e.  RR )
159 2re 10025 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
160159a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  2  e.  RR )
161 1lt2 10098 . . . . . . . . . . . . . . . . . . . . 21  |-  1  <  2
162157, 159, 161ltleii 9152 . . . . . . . . . . . . . . . . . . . 20  |-  1  <_  2
163162a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  1  <_  2 )
164 elfzle1 11016 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  2  <_  I )
165158, 160, 99, 163, 164letrd 9183 . . . . . . . . . . . . . . . . . 18  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  1  <_  I )
1661653ad2ant3 980 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  1  <_  I )
167166adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
1  <_  I )
168 elnnz1 10263 . . . . . . . . . . . . . . . 16  |-  ( I  e.  NN  <->  ( I  e.  ZZ  /\  1  <_  I ) )
169149, 167, 168sylanbrc 646 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  e.  NN )
170783ad2ant1 978 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  NN )
171170adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  N  e.  NN )
172 nnltp1le 10286 . . . . . . . . . . . . . . 15  |-  ( ( I  e.  NN  /\  N  e.  NN )  ->  ( I  <  N  <->  ( I  +  1 )  <_  N ) )
173169, 171, 172syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  <  N  <->  ( I  +  1 )  <_  N ) )
174156, 173mpbid 202 . . . . . . . . . . . . 13  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  +  1 )  <_  N )
175140adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  +  1 )  e.  ZZ )
176 eluz 10455 . . . . . . . . . . . . . 14  |-  ( ( ( I  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( I  + 
1 ) )  <->  ( I  +  1 )  <_  N ) )
177175, 151, 176syl2anc 643 . . . . . . . . . . . . 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 224 . . . . . . . . . . . 12  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  N  e.  ( ZZ>= `  ( I  +  1
) ) )
179 simpr1 963 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  N  e.  ( ZZ>= ` 
3 ) )
180 simpr3 965 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  I  e.  ( 2 ... ( N  - 
1 ) ) )
181179, 180, 86syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  ->  Q  e.  ( EE `  N ) )
182181adantr 452 . . . . . . . . . . . . . 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 9973 . . . . . . . . . . . . . . . . 17  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  +  1 )  e.  NN )
184183, 80syl6eleq 2494 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( I  +  1 )  e.  ( ZZ>= ` 
1 ) )
185 fzss1 11047 . . . . . . . . . . . . . . . 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 3308 . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . 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 11476 . . . . . . . . . . . 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 6055 . . . . . . . . . . . . 13  |-  ( i  =  ( I  + 
1 )  ->  (
( Q `  i
) ^ 2 )  =  ( ( Q `
 ( I  + 
1 ) ) ^
2 ) )
19115oveq1i 6050 . . . . . . . . . . . . . 14  |-  ( ( Q `  ( I  +  1 ) ) ^ 2 )  =  ( 1 ^ 2 )
192191, 141eqtri 2424 . . . . . . . . . . . . 13  |-  ( ( Q `  ( I  +  1 ) ) ^ 2 )  =  1
193190, 192syl6eq 2452 . . . . . . . . . . . 12  |-  ( i  =  ( I  + 
1 )  ->  (
( Q `  i
) ^ 2 )  =  1 )
194178, 189, 193fsum1p 12494 . . . . . . . . . . 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 9973 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( ( I  + 
1 )  +  1 )  e.  NN )
196195, 80syl6eleq 2494 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( I  +  1 )  =/=  N  /\  ( N  e.  ( ZZ>=
`  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) ) )  -> 
( ( I  + 
1 )  +  1 )  e.  ( ZZ>= ` 
1 ) )
197 fzss1 11047 . . . . . . . . . . . . . . . . . . 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 3308 . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . 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 9195 . . . . . . . . . . . . . . . . . . . 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 11015 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( ( ( I  +  1 )  +  1 ) ... N )  ->  i  e.  ZZ )
205204zred 10331 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( ( ( I  +  1 )  +  1 ) ... N )  ->  i  e.  RR )
206205adantl 453 . . . . . . . . . . . . . . . . . . 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 9897 . . . . . . . . . . . . . . . . . . 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 11016 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( ( ( I  +  1 )  +  1 ) ... N )  ->  (
( I  +  1 )  +  1 )  <_  i )
209208adantl 453 . . . . . . . . . . . . . . . . . . 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 9186 . . . . . . . . . . . . . . . . . 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 9164 . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . 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 11430 . . . . . . . . . . . . . . 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 12452 . . . . . . . . . . . . . 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 11266 . . . . . . . . . . . . . . . 16  |-  ( ( ( I  +  1 )  +  1 ) ... N )  e. 
Fin
216215olci 381 . . . . . . . . . . . . . . 15  |-  ( ( ( ( I  + 
1 )  +  1 ) ... N ) 
C_  ( ZZ>= `  1
)  \/  ( ( ( I  +  1 )  +  1 ) ... N )  e. 
Fin )
217 sumz 12471 . . . . . . . . . . . . . . 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 8 . . . . . . . . . . . . . 14  |-  sum_ i  e.  ( ( ( I  +  1 )  +  1 ) ... N
) 0  =  0
219214, 218syl6eq 2452 . . . . . . . . . . . . 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 6056 . . . . . . . . . . . 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 9209 . . . . . . . . . . . 12  |-  ( 1  +  0 )  =  1
222220, 221syl6eq 2452 . . . . . . . . . . 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 2436 . . . . . . . . . 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 424 . . . . . . . . 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 2643 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( ( I  + 
1 ) ... N
) ( ( Q `
 i ) ^
2 )  =  1 )
226139, 225oveq12d 6058 . . . . . . 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 10049 . . . . . . 7  |-  ( 0  +  1 )  =  1
228226, 227syl6eq 2452 . . . . . 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 2436 . . . . 5  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( 2 ... N
) ( ( Q `
 i ) ^
2 )  =  1 )
230 simp1 957 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  3 )
)
231 2lt3 10099 . . . . . . . . . 10  |-  2  <  3
232159, 49, 231ltleii 9152 . . . . . . . . 9  |-  2  <_  3
233 2z 10268 . . . . . . . . . 10  |-  2  e.  ZZ
234233eluz1i 10451 . . . . . . . . 9  |-  ( 3  e.  ( ZZ>= `  2
)  <->  ( 3  e.  ZZ  /\  2  <_ 
3 ) )
2359, 232, 234mpbir2an 887 . . . . . . . 8  |-  3  e.  ( ZZ>= `  2 )
236 uztrn 10458 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  e.  ( ZZ>= `  2 )
)  ->  N  e.  ( ZZ>= `  2 )
)
237230, 235, 236sylancl 644 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  2 )
)
238 fveq2 5687 . . . . . . . 8  |-  ( i  =  2  ->  ( Q `  i )  =  ( Q ` 
2 ) )
239238oveq1d 6055 . . . . . . 7  |-  ( i  =  2  ->  (
( Q `  i
) ^ 2 )  =  ( ( Q `
 2 ) ^
2 ) )
240237, 93, 239fsum1p 12494 . . . . . 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 452 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  N  e.  ZZ )
242241zred 10331 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  N  e.  RR )
243 lttr 9108 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  3  e.  RR  /\  N  e.  RR )  ->  (
( 2  <  3  /\  3  <  N )  ->  2  <  N
) )
244159, 49, 243mp3an12 1269 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  RR  ->  (
( 2  <  3  /\  3  <  N )  ->  2  <  N
) )
245231, 244mpani 658 . . . . . . . . . . . . . . . 16  |-  ( N  e.  RR  ->  (
3  <  N  ->  2  <  N ) )
24650, 245syl 16 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  <  N  ->  2  <  N ) )
247246imp 419 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  2  <  N )
248 ltle 9119 . . . . . . . . . . . . . . 15  |-  ( ( 2  e.  RR  /\  N  e.  RR )  ->  ( 2  <  N  ->  2  <_  N )
)
249159, 248mpan 652 . . . . . . . . . . . . . 14  |-  ( N  e.  RR  ->  (
2  <  N  ->  2  <_  N ) )
250242, 247, 249sylc 58 . . . . . . . . . . . . 13  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  2  <_  N )
251250, 162jctil 524 . . . . . . . . . . . 12  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  (
1  <_  2  /\  2  <_  N ) )
252 1z 10267 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
253 elfz 11005 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  ZZ  /\  1  e.  ZZ  /\  N  e.  ZZ )  ->  (
2  e.  ( 1 ... N )  <->  ( 1  <_  2  /\  2  <_  N ) ) )
254233, 252, 253mp3an12 1269 . . . . . . . . . . . . 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 224 . . . . . . . . . . 11  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  2  e.  ( 1 ... N
) )
2572563adant3 977 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  2  e.  ( 1 ... N
) )
25899ltp1d 9897 . . . . . . . . . . . . . 14  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  I  <  ( I  +  1 ) )
259160, 99, 123, 164, 258lelttrd 9184 . . . . . . . . . . . . 13  |-  ( I  e.  ( 2 ... ( N  -  1 ) )  ->  2  <  ( I  +  1 ) )
2602593ad2ant3 980 . . . . . . . . . . . 12  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  2  <  ( I  +  1 ) )
261 ltne 9126 . . . . . . . . . . . 12  |-  ( ( 2  e.  RR  /\  2  <  ( I  + 
1 ) )  -> 
( I  +  1 )  =/=  2 )
262159, 260, 261sylancr 645 . . . . . . . . . . 11  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
I  +  1 )  =/=  2 )
263262necomd 2650 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  2  =/=  ( I  +  1 ) )
26414axlowdimlem12 25796 . . . . . . . . . 10  |-  ( ( 2  e.  ( 1 ... N )  /\  2  =/=  ( I  + 
1 ) )  -> 
( Q `  2
)  =  0 )
265257, 263, 264syl2anc 643 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( Q `  2 )  =  0 )
266265sq0id 11430 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
( Q `  2
) ^ 2 )  =  0 )
267266oveq1d 6055 . . . . . . 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 6050 . . . . . . . . 9  |-  ( 3 ... N )  =  ( ( 2  +  1 ) ... N
)
269268sumeq1i 12447 . . . . . . . 8  |-  sum_ i  e.  ( 3 ... N
) ( ( Q `
 i ) ^
2 )  =  sum_ i  e.  ( (
2  +  1 ) ... N ) ( ( Q `  i
) ^ 2 )
270269oveq2i 6051 . . . . . . 7  |-  ( 0  +  sum_ i  e.  ( 3 ... N ) ( ( Q `  i ) ^ 2 ) )  =  ( 0  +  sum_ i  e.  ( ( 2  +  1 ) ... N
) ( ( Q `
 i ) ^
2 ) )
271267, 270syl6eqr 2454 . . . . . 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 11267 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
3 ... N )  e. 
Fin )
2738, 80eleqtri 2476 . . . . . . . . . . . . 13  |-  3  e.  ( ZZ>= `  1 )
274 fzss1 11047 . . . . . . . . . . . . 13  |-  ( 3  e.  ( ZZ>= `  1
)  ->  ( 3 ... N )  C_  ( 1 ... N
) )
275273, 274ax-mp 8 . . . . . . . . . . . 12  |-  ( 3 ... N )  C_  ( 1 ... N
)
276275sseli 3304 . . . . . . . . . . 11  |-  ( i  e.  ( 3 ... N )  ->  i  e.  ( 1 ... N
) )
27786, 276, 90syl2an 464 . . . . . . . . . 10  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) )  /\  i  e.  ( 3 ... N ) )  ->  ( Q `  i )  e.  CC )
278277sqcld 11476 . . . . . . . . 9  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  I  e.  ( 2 ... ( N  - 
1 ) ) )  /\  i  e.  ( 3 ... N ) )  ->  ( ( Q `  i ) ^ 2 )  e.  CC )
2792783adantl2 1114 . . . . . . . 8  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  /\  i  e.  ( 3 ... N
) )  ->  (
( Q `  i
) ^ 2 )  e.  CC )
280272, 279fsumcl 12482 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( 3 ... N
) ( ( Q `
 i ) ^
2 )  e.  CC )
281280addid2d 9223 . . . . . 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 2441 . . . . 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 444 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  N  e.  ( ZZ>= `  3 )
)
28422axlowdimlem7 25791 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  P  e.  ( EE `  N ) )
285284ad2antrr 707 . . . . . . . . . . 11  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( 3 ... N ) )  ->  P  e.  ( EE `  N ) )
286276adantl 453 . . . . . . . . . . 11  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( 3 ... N ) )  ->  i  e.  ( 1 ... N ) )
287 fveecn 25745 . . . . . . . . . . 11  |-  ( ( P  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( P `  i )  e.  CC )
288285, 286, 287syl2anc 643 . . . . . . . . . 10  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( 3 ... N ) )  ->  ( P `  i )  e.  CC )
289288sqcld 11476 . . . . . . . . 9  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( 3 ... N ) )  ->  ( ( P `
 i ) ^
2 )  e.  CC )
29027, 141eqtri 2424 . . . . . . . . . 10  |-  ( -u
1 ^ 2 )  =  1
29125, 290syl6eq 2452 . . . . . . . . 9  |-  ( i  =  3  ->  (
( P `  i
) ^ 2 )  =  1 )
292283, 289, 291fsum1p 12494 . . . . . . . 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 10273 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 3  e.  ZZ  /\  1  e.  ZZ )  ->  ( 3  +  1 )  e.  ZZ )
2949, 252, 293mp2an 654 . . . . . . . . . . . . . . . . . . 19  |-  ( 3  +  1 )  e.  ZZ
295294zrei 10244 . . . . . . . . . . . . . . . . . 18  |-  ( 3  +  1 )  e.  RR
296 1lt3 10100 . . . . . . . . . . . . . . . . . . 19  |-  1  <  3
29749ltp1i 9870 . . . . . . . . . . . . . . . . . . 19  |-  3  <  ( 3  +  1 )
298157, 49, 295lttri 9155 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  <  3  /\  3  <  ( 3  +  1 ) )  ->  1  <  (
3  +  1 ) )
299296, 297, 298mp2an 654 . . . . . . . . . . . . . . . . . 18  |-  1  <  ( 3  +  1 )
300157, 295, 299ltleii 9152 . . . . . . . . . . . . . . . . 17  |-  1  <_  ( 3  +  1 )
301 eluz 10455 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  ZZ  /\  ( 3  +  1 )  e.  ZZ )  ->  ( ( 3  +  1 )  e.  ( ZZ>= `  1 )  <->  1  <_  ( 3  +  1 ) ) )
302252, 294, 301mp2an 654 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  +  1 )  e.  ( ZZ>= `  1
)  <->  1  <_  (
3  +  1 ) )
303300, 302mpbir 201 . . . . . . . . . . . . . . . 16  |-  ( 3  +  1 )  e.  ( ZZ>= `  1 )
304 fzss1 11047 . . . . . . . . . . . . . . . 16  |-  ( ( 3  +  1 )  e.  ( ZZ>= `  1
)  ->  ( (
3  +  1 ) ... N )  C_  ( 1 ... N
) )
305303, 304ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( ( 3  +  1 ) ... N )  C_  ( 1 ... N
)
306305sseli 3304 . . . . . . . . . . . . . 14  |-  ( i  e.  ( ( 3  +  1 ) ... N )  ->  i  e.  ( 1 ... N
) )
307306adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( (
3  +  1 ) ... N ) )  ->  i  e.  ( 1 ... N ) )
30849, 295ltnlei 9150 . . . . . . . . . . . . . . . . . . 19  |-  ( 3  <  ( 3  +  1 )  <->  -.  (
3  +  1 )  <_  3 )
309297, 308mpbi 200 . . . . . . . . . . . . . . . . . 18  |-  -.  (
3  +  1 )  <_  3
310309intnanr 882 . . . . . . . . . . . . . . . . 17  |-  -.  (
( 3  +  1 )  <_  3  /\  3  <_  N )
311 elfz 11005 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 3  e.  ZZ  /\  ( 3  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( 3  e.  ( ( 3  +  1 ) ... N )  <-> 
( ( 3  +  1 )  <_  3  /\  3  <_  N ) ) )
3129, 294, 311mp3an12 1269 . . . . . . . . . . . . . . . . . 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 295 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  -.  3  e.  ( (
3  +  1 ) ... N ) )
315 eleq1 2464 . . . . . . . . . . . . . . . . 17  |-  ( i  =  3  ->  (
i  e.  ( ( 3  +  1 ) ... N )  <->  3  e.  ( ( 3  +  1 ) ... N
) ) )
316315notbid 286 . . . . . . . . . . . . . . . 16  |-  ( i  =  3  ->  ( -.  i  e.  (
( 3  +  1 ) ... N )  <->  -.  3  e.  (
( 3  +  1 ) ... N ) ) )
317314, 316syl5ibrcom 214 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  (
i  =  3  ->  -.  i  e.  (
( 3  +  1 ) ... N ) ) )
318317necon2ad 2615 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  (
i  e.  ( ( 3  +  1 ) ... N )  -> 
i  =/=  3 ) )
319318imp 419 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( (
3  +  1 ) ... N ) )  ->  i  =/=  3
)
32022axlowdimlem9 25793 . . . . . . . . . . . . 13  |-  ( ( i  e.  ( 1 ... N )  /\  i  =/=  3 )  -> 
( P `  i
)  =  0 )
321307, 319, 320syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( (
3  +  1 ) ... N ) )  ->  ( P `  i )  =  0 )
322321sq0id 11430 . . . . . . . . . . 11  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  3  <  N )  /\  i  e.  ( (
3  +  1 ) ... N ) )  ->  ( ( P `
 i ) ^
2 )  =  0 )
323322sumeq2dv 12452 . . . . . . . . . 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 11266 . . . . . . . . . . . 12  |-  ( ( 3  +  1 ) ... N )  e. 
Fin
325324olci 381 . . . . . . . . . . 11  |-  ( ( ( 3  +  1 ) ... N ) 
C_  ( ZZ>= `  1
)  \/  ( ( 3  +  1 ) ... N )  e. 
Fin )
326 sumz 12471 . . . . . . . . . . 11  |-  ( ( ( ( 3  +  1 ) ... N
)  C_  ( ZZ>= ` 
1 )  \/  (
( 3  +  1 ) ... N )  e.  Fin )  ->  sum_ i  e.  ( ( 3  +  1 ) ... N ) 0  =  0 )
327325, 326ax-mp 8 . . . . . . . . . 10  |-  sum_ i  e.  ( ( 3  +  1 ) ... N
) 0  =  0
328323, 327syl6eq 2452 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  sum_ i  e.  ( ( 3  +  1 ) ... N
) ( ( P `
 i ) ^
2 )  =  0 )
329328oveq2d 6056 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  (
1  +  sum_ i  e.  ( ( 3  +  1 ) ... N
) ( ( P `
 i ) ^
2 ) )  =  ( 1  +  0 ) )
330292, 329eqtrd 2436 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  sum_ i  e.  ( 3 ... N
) ( ( P `
 i ) ^
2 )  =  ( 1  +  0 ) )
331330, 221syl6eq 2452 . . . . . 6  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N )  ->  sum_ i  e.  ( 3 ... N
) ( ( P `
 i ) ^
2 )  =  1 )
3323313adant3 977 . . . . 5  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  3  <  N  /\  I  e.  ( 2 ... ( N  -  1 ) ) )  ->  sum_ i  e.  ( 3 ... N
) ( ( P `
 i ) ^
2 )  =  1 )
333229, 282, 3323eqtr4rd 2447 . . . 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 1184 . . 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 424 . 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 2643 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 177    \/ wo 358    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721    =/= wne 2567    \ cdif 3277    u. cun 3278    i^i cin 3279    C_ wss 3280   (/)c0 3588   {csn 3774   <.cop 3777   class class class wbr 4172    X. cxp 4835   ` cfv 5413  (class class class)co 6040   Fincfn 7068   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947    + caddc 8949    < clt 9076    <_ cle 9077    - cmin 9247   -ucneg 9248   NNcn 9956   2c2 10005   3c3 10006   ZZcz 10238   ZZ>=cuz 10444   ...cfz 10999   ^cexp 11337   sum_csu 12434   EEcee 25731
This theorem is referenced by:  axlowdimlem17  25801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-fz 11000  df-fzo 11091  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-sum 12435  df-ee 25734
  Copyright terms: Public domain W3C validator