Metamath Proof Explorer

Theorem poimirlem31

Description: Lemma for poimir , assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 and poimirlem28 . Equation (2) of Kulpa p. 547. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimir.i 
|- I = ( ( 0 [,] 1 ) ^m ( 1 ... N ) )
poimir.r 
|- R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
poimir.1 
|- ( ph -> F e. ( ( R |`t I ) Cn R ) )
poimir.2 
|- ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> ( ( F ` z ) ` n ) <_ 0 )
poimirlem31.p 
|- P = ( ( 1st ` ( G ` k ) ) oF + ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
poimirlem31.3 
|- ( ph -> G : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
poimirlem31.4 
|- ( ( ph /\ k e. NN ) -> ran ( 1st ` ( G ` k ) ) C_ ( 0 ..^ k ) )
poimirlem31.5 
|- ( ( ph /\ ( k e. NN /\ i e. ( 0 ... N ) ) ) -> E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) )
Assertion poimirlem31 
|- ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) /\ r e. { <_ , `' <_ } ) ) -> E. j e. ( 0 ... N ) 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimir.i 
 |-  I = ( ( 0 [,] 1 ) ^m ( 1 ... N ) )
3 poimir.r 
 |-  R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
4 poimir.1 
 |-  ( ph -> F e. ( ( R |`t I ) Cn R ) )
5 poimir.2 
 |-  ( ( ph /\ ( n e. ( 1 ... N ) /\ z e. I /\ ( z ` n ) = 0 ) ) -> ( ( F ` z ) ` n ) <_ 0 )
6 poimirlem31.p 
 |-  P = ( ( 1st ` ( G ` k ) ) oF + ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
7 poimirlem31.3 
 |-  ( ph -> G : NN --> ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
8 poimirlem31.4 
 |-  ( ( ph /\ k e. NN ) -> ran ( 1st ` ( G ` k ) ) C_ ( 0 ..^ k ) )
9 poimirlem31.5 
 |-  ( ( ph /\ ( k e. NN /\ i e. ( 0 ... N ) ) ) -> E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) )
10 elpri 
 |-  ( r e. { <_ , `' <_ } -> ( r = <_ \/ r = `' <_ ) )
11 simprr 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> n e. ( 1 ... N ) )
12 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
13 12 sseli 
 |-  ( n e. ( 1 ... N ) -> n e. ( 0 ... N ) )
14 13 anim2i 
 |-  ( ( k e. NN /\ n e. ( 1 ... N ) ) -> ( k e. NN /\ n e. ( 0 ... N ) ) )
15 eleq1 
 |-  ( i = n -> ( i e. ( 0 ... N ) <-> n e. ( 0 ... N ) ) )
16 15 anbi2d 
 |-  ( i = n -> ( ( k e. NN /\ i e. ( 0 ... N ) ) <-> ( k e. NN /\ n e. ( 0 ... N ) ) ) )
17 16 anbi2d 
 |-  ( i = n -> ( ( ph /\ ( k e. NN /\ i e. ( 0 ... N ) ) ) <-> ( ph /\ ( k e. NN /\ n e. ( 0 ... N ) ) ) ) )
18 eqeq1 
 |-  ( i = n -> ( i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) <-> n = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) )
19 18 rexbidv 
 |-  ( i = n -> ( E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) <-> E. j e. ( 0 ... N ) n = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) )
20 17 19 imbi12d 
 |-  ( i = n -> ( ( ( ph /\ ( k e. NN /\ i e. ( 0 ... N ) ) ) -> E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) <-> ( ( ph /\ ( k e. NN /\ n e. ( 0 ... N ) ) ) -> E. j e. ( 0 ... N ) n = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) ) )
21 20 9 chvarvv 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 0 ... N ) ) ) -> E. j e. ( 0 ... N ) n = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) )
22 elfzle1 
 |-  ( n e. ( 1 ... N ) -> 1 <_ n )
23 1re 
 |-  1 e. RR
24 elfzelz 
 |-  ( n e. ( 1 ... N ) -> n e. ZZ )
25 24 zred 
 |-  ( n e. ( 1 ... N ) -> n e. RR )
26 lenlt 
 |-  ( ( 1 e. RR /\ n e. RR ) -> ( 1 <_ n <-> -. n < 1 ) )
27 23 25 26 sylancr 
 |-  ( n e. ( 1 ... N ) -> ( 1 <_ n <-> -. n < 1 ) )
28 22 27 mpbid 
 |-  ( n e. ( 1 ... N ) -> -. n < 1 )
29 elsni 
 |-  ( n e. { 0 } -> n = 0 )
30 0lt1 
 |-  0 < 1
31 29 30 eqbrtrdi 
 |-  ( n e. { 0 } -> n < 1 )
32 28 31 nsyl 
 |-  ( n e. ( 1 ... N ) -> -. n e. { 0 } )
33 ltso 
 |-  < Or RR
34 snfi 
 |-  { 0 } e. Fin
35 fzfi 
 |-  ( 1 ... N ) e. Fin
36 rabfi 
 |-  ( ( 1 ... N ) e. Fin -> { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } e. Fin )
37 35 36 ax-mp 
 |-  { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } e. Fin
38 unfi 
 |-  ( ( { 0 } e. Fin /\ { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } e. Fin ) -> ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) e. Fin )
39 34 37 38 mp2an 
 |-  ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) e. Fin
40 c0ex 
 |-  0 e. _V
41 40 snid 
 |-  0 e. { 0 }
42 elun1 
 |-  ( 0 e. { 0 } -> 0 e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) )
43 ne0i 
 |-  ( 0 e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) -> ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) =/= (/) )
44 41 42 43 mp2b 
 |-  ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) =/= (/)
45 0re 
 |-  0 e. RR
46 snssi 
 |-  ( 0 e. RR -> { 0 } C_ RR )
47 45 46 ax-mp 
 |-  { 0 } C_ RR
48 ssrab2 
 |-  { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } C_ ( 1 ... N )
49 24 ssriv 
 |-  ( 1 ... N ) C_ ZZ
50 zssre 
 |-  ZZ C_ RR
51 49 50 sstri 
 |-  ( 1 ... N ) C_ RR
52 48 51 sstri 
 |-  { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } C_ RR
53 47 52 unssi 
 |-  ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) C_ RR
54 39 44 53 3pm3.2i 
 |-  ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) e. Fin /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) =/= (/) /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) C_ RR )
55 fisupcl 
 |-  ( ( < Or RR /\ ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) e. Fin /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) =/= (/) /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) C_ RR ) ) -> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) )
56 33 54 55 mp2an 
 |-  sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } )
57 eleq1 
 |-  ( n = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( n e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) <-> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) ) )
58 56 57 mpbiri 
 |-  ( n = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> n e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) )
59 elun 
 |-  ( n e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) <-> ( n e. { 0 } \/ n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) )
60 58 59 sylib 
 |-  ( n = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( n e. { 0 } \/ n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) )
61 oveq2 
 |-  ( a = n -> ( 1 ... a ) = ( 1 ... n ) )
62 61 raleqdv 
 |-  ( a = n -> ( A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) <-> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
63 62 elrab 
 |-  ( n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } <-> ( n e. ( 1 ... N ) /\ A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
64 elfzuz 
 |-  ( n e. ( 1 ... N ) -> n e. ( ZZ>= ` 1 ) )
65 eluzfz2 
 |-  ( n e. ( ZZ>= ` 1 ) -> n e. ( 1 ... n ) )
66 64 65 syl 
 |-  ( n e. ( 1 ... N ) -> n e. ( 1 ... n ) )
67 simpl 
 |-  ( ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) -> 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) )
68 67 ralimi 
 |-  ( A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) -> A. b e. ( 1 ... n ) 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) )
69 fveq2 
 |-  ( b = n -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) = ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )
70 69 breq2d 
 |-  ( b = n -> ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) <-> 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
71 70 rspcva 
 |-  ( ( n e. ( 1 ... n ) /\ A. b e. ( 1 ... n ) 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) ) -> 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )
72 66 68 71 syl2an 
 |-  ( ( n e. ( 1 ... N ) /\ A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )
73 63 72 sylbi 
 |-  ( n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } -> 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )
74 73 orim2i 
 |-  ( ( n e. { 0 } \/ n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) -> ( n e. { 0 } \/ 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
75 60 74 syl 
 |-  ( n = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( n e. { 0 } \/ 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
76 orel1 
 |-  ( -. n e. { 0 } -> ( ( n e. { 0 } \/ 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) -> 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
77 32 75 76 syl2im 
 |-  ( n e. ( 1 ... N ) -> ( n = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
78 77 reximdv 
 |-  ( n e. ( 1 ... N ) -> ( E. j e. ( 0 ... N ) n = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> E. j e. ( 0 ... N ) 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
79 21 78 syl5 
 |-  ( n e. ( 1 ... N ) -> ( ( ph /\ ( k e. NN /\ n e. ( 0 ... N ) ) ) -> E. j e. ( 0 ... N ) 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
80 14 79 sylan2i 
 |-  ( n e. ( 1 ... N ) -> ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> E. j e. ( 0 ... N ) 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
81 11 80 mpcom 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> E. j e. ( 0 ... N ) 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )
82 breq 
 |-  ( r = <_ -> ( 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <-> 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
83 82 rexbidv 
 |-  ( r = <_ -> ( E. j e. ( 0 ... N ) 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <-> E. j e. ( 0 ... N ) 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
84 81 83 syl5ibrcom 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> ( r = <_ -> E. j e. ( 0 ... N ) 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
85 1 nnzd 
 |-  ( ph -> N e. ZZ )
86 elfzm1b 
 |-  ( ( n e. ZZ /\ N e. ZZ ) -> ( n e. ( 1 ... N ) <-> ( n - 1 ) e. ( 0 ... ( N - 1 ) ) ) )
87 24 85 86 syl2anr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n e. ( 1 ... N ) <-> ( n - 1 ) e. ( 0 ... ( N - 1 ) ) ) )
88 87 biimpd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n e. ( 1 ... N ) -> ( n - 1 ) e. ( 0 ... ( N - 1 ) ) ) )
89 88 ex 
 |-  ( ph -> ( n e. ( 1 ... N ) -> ( n e. ( 1 ... N ) -> ( n - 1 ) e. ( 0 ... ( N - 1 ) ) ) ) )
90 89 pm2.43d 
 |-  ( ph -> ( n e. ( 1 ... N ) -> ( n - 1 ) e. ( 0 ... ( N - 1 ) ) ) )
91 1 nncnd 
 |-  ( ph -> N e. CC )
92 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
93 91 92 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
94 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
95 1 94 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
96 95 nn0zd 
 |-  ( ph -> ( N - 1 ) e. ZZ )
97 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
98 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
99 96 97 98 3syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
100 93 99 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
101 fzss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
102 100 101 syl 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
103 102 sseld 
 |-  ( ph -> ( ( n - 1 ) e. ( 0 ... ( N - 1 ) ) -> ( n - 1 ) e. ( 0 ... N ) ) )
104 90 103 syld 
 |-  ( ph -> ( n e. ( 1 ... N ) -> ( n - 1 ) e. ( 0 ... N ) ) )
105 104 anim2d 
 |-  ( ph -> ( ( k e. NN /\ n e. ( 1 ... N ) ) -> ( k e. NN /\ ( n - 1 ) e. ( 0 ... N ) ) ) )
106 105 imp 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> ( k e. NN /\ ( n - 1 ) e. ( 0 ... N ) ) )
107 ovex 
 |-  ( n - 1 ) e. _V
108 eleq1 
 |-  ( i = ( n - 1 ) -> ( i e. ( 0 ... N ) <-> ( n - 1 ) e. ( 0 ... N ) ) )
109 108 anbi2d 
 |-  ( i = ( n - 1 ) -> ( ( k e. NN /\ i e. ( 0 ... N ) ) <-> ( k e. NN /\ ( n - 1 ) e. ( 0 ... N ) ) ) )
110 109 anbi2d 
 |-  ( i = ( n - 1 ) -> ( ( ph /\ ( k e. NN /\ i e. ( 0 ... N ) ) ) <-> ( ph /\ ( k e. NN /\ ( n - 1 ) e. ( 0 ... N ) ) ) ) )
111 eqeq1 
 |-  ( i = ( n - 1 ) -> ( i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) <-> ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) )
112 111 rexbidv 
 |-  ( i = ( n - 1 ) -> ( E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) <-> E. j e. ( 0 ... N ) ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) )
113 110 112 imbi12d 
 |-  ( i = ( n - 1 ) -> ( ( ( ph /\ ( k e. NN /\ i e. ( 0 ... N ) ) ) -> E. j e. ( 0 ... N ) i = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) <-> ( ( ph /\ ( k e. NN /\ ( n - 1 ) e. ( 0 ... N ) ) ) -> E. j e. ( 0 ... N ) ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) ) )
114 107 113 9 vtocl 
 |-  ( ( ph /\ ( k e. NN /\ ( n - 1 ) e. ( 0 ... N ) ) ) -> E. j e. ( 0 ... N ) ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) )
115 106 114 syldan 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> E. j e. ( 0 ... N ) ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) )
116 eleq1 
 |-  ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) <-> sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) ) )
117 56 116 mpbiri 
 |-  ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) )
118 elun 
 |-  ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) <-> ( ( n - 1 ) e. { 0 } \/ ( n - 1 ) e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) )
119 107 elsn 
 |-  ( ( n - 1 ) e. { 0 } <-> ( n - 1 ) = 0 )
120 oveq2 
 |-  ( a = ( n - 1 ) -> ( 1 ... a ) = ( 1 ... ( n - 1 ) ) )
121 120 raleqdv 
 |-  ( a = ( n - 1 ) -> ( A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) <-> A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
122 121 elrab 
 |-  ( ( n - 1 ) e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } <-> ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
123 119 122 orbi12i 
 |-  ( ( ( n - 1 ) e. { 0 } \/ ( n - 1 ) e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) <-> ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) )
124 118 123 bitri 
 |-  ( ( n - 1 ) e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) <-> ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) )
125 117 124 sylib 
 |-  ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) )
126 125 a1i 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) ) )
127 ltm1 
 |-  ( n e. RR -> ( n - 1 ) < n )
128 peano2rem 
 |-  ( n e. RR -> ( n - 1 ) e. RR )
129 ltnle 
 |-  ( ( ( n - 1 ) e. RR /\ n e. RR ) -> ( ( n - 1 ) < n <-> -. n <_ ( n - 1 ) ) )
130 128 129 mpancom 
 |-  ( n e. RR -> ( ( n - 1 ) < n <-> -. n <_ ( n - 1 ) ) )
131 127 130 mpbid 
 |-  ( n e. RR -> -. n <_ ( n - 1 ) )
132 25 131 syl 
 |-  ( n e. ( 1 ... N ) -> -. n <_ ( n - 1 ) )
133 breq2 
 |-  ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( n <_ ( n - 1 ) <-> n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) )
134 133 notbid 
 |-  ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( -. n <_ ( n - 1 ) <-> -. n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) )
135 132 134 syl5ibcom 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> -. n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) ) )
136 elun2 
 |-  ( n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } -> n e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) )
137 fimaxre2 
 |-  ( ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) C_ RR /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) e. Fin ) -> E. x e. RR A. y e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) y <_ x )
138 53 39 137 mp2an 
 |-  E. x e. RR A. y e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) y <_ x
139 53 44 138 3pm3.2i 
 |-  ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) C_ RR /\ ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) =/= (/) /\ E. x e. RR A. y e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) y <_ x )
140 139 suprubii 
 |-  ( n e. ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) -> n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) )
141 136 140 syl 
 |-  ( n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } -> n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) )
142 141 con3i 
 |-  ( -. n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> -. n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } )
143 ianor 
 |-  ( -. ( n e. ( 1 ... N ) /\ A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) <-> ( -. n e. ( 1 ... N ) \/ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
144 143 63 xchnxbir 
 |-  ( -. n e. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } <-> ( -. n e. ( 1 ... N ) \/ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
145 142 144 sylib 
 |-  ( -. n <_ sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( -. n e. ( 1 ... N ) \/ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
146 135 145 syl6 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( -. n e. ( 1 ... N ) \/ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) )
147 pm2.63 
 |-  ( ( n e. ( 1 ... N ) \/ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> ( ( -. n e. ( 1 ... N ) \/ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
148 147 orcs 
 |-  ( n e. ( 1 ... N ) -> ( ( -. n e. ( 1 ... N ) \/ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
149 146 148 syld 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
150 126 149 jcad 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) /\ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) )
151 andir 
 |-  ( ( ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) /\ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) <-> ( ( ( n - 1 ) = 0 /\ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) \/ ( ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) /\ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) )
152 24 zcnd 
 |-  ( n e. ( 1 ... N ) -> n e. CC )
153 ax-1cn 
 |-  1 e. CC
154 0cn 
 |-  0 e. CC
155 subadd 
 |-  ( ( n e. CC /\ 1 e. CC /\ 0 e. CC ) -> ( ( n - 1 ) = 0 <-> ( 1 + 0 ) = n ) )
156 153 154 155 mp3an23 
 |-  ( n e. CC -> ( ( n - 1 ) = 0 <-> ( 1 + 0 ) = n ) )
157 152 156 syl 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) = 0 <-> ( 1 + 0 ) = n ) )
158 157 biimpa 
 |-  ( ( n e. ( 1 ... N ) /\ ( n - 1 ) = 0 ) -> ( 1 + 0 ) = n )
159 1p0e1 
 |-  ( 1 + 0 ) = 1
160 158 159 eqtr3di 
 |-  ( ( n e. ( 1 ... N ) /\ ( n - 1 ) = 0 ) -> n = 1 )
161 1z 
 |-  1 e. ZZ
162 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
163 161 162 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
164 oveq2 
 |-  ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
165 sneq 
 |-  ( n = 1 -> { n } = { 1 } )
166 163 164 165 3eqtr4a 
 |-  ( n = 1 -> ( 1 ... n ) = { n } )
167 166 raleqdv 
 |-  ( n = 1 -> ( A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) <-> A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
168 167 notbid 
 |-  ( n = 1 -> ( -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) <-> -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
169 168 biimpd 
 |-  ( n = 1 -> ( -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) -> -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
170 160 169 syl 
 |-  ( ( n e. ( 1 ... N ) /\ ( n - 1 ) = 0 ) -> ( -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) -> -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
171 170 expimpd 
 |-  ( n e. ( 1 ... N ) -> ( ( ( n - 1 ) = 0 /\ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
172 ralun 
 |-  ( ( A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) /\ A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> A. b e. ( ( 1 ... ( n - 1 ) ) u. { n } ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) )
173 npcan1 
 |-  ( n e. CC -> ( ( n - 1 ) + 1 ) = n )
174 152 173 syl 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) + 1 ) = n )
175 174 64 eqeltrd 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
176 peano2zm 
 |-  ( n e. ZZ -> ( n - 1 ) e. ZZ )
177 uzid 
 |-  ( ( n - 1 ) e. ZZ -> ( n - 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
178 peano2uz 
 |-  ( ( n - 1 ) e. ( ZZ>= ` ( n - 1 ) ) -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
179 24 176 177 178 4syl 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) + 1 ) e. ( ZZ>= ` ( n - 1 ) ) )
180 174 179 eqeltrrd 
 |-  ( n e. ( 1 ... N ) -> n e. ( ZZ>= ` ( n - 1 ) ) )
181 fzsplit2 
 |-  ( ( ( ( n - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` ( n - 1 ) ) ) -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) )
182 175 180 181 syl2anc 
 |-  ( n e. ( 1 ... N ) -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) )
183 174 oveq1d 
 |-  ( n e. ( 1 ... N ) -> ( ( ( n - 1 ) + 1 ) ... n ) = ( n ... n ) )
184 fzsn 
 |-  ( n e. ZZ -> ( n ... n ) = { n } )
185 24 184 syl 
 |-  ( n e. ( 1 ... N ) -> ( n ... n ) = { n } )
186 183 185 eqtrd 
 |-  ( n e. ( 1 ... N ) -> ( ( ( n - 1 ) + 1 ) ... n ) = { n } )
187 186 uneq2d 
 |-  ( n e. ( 1 ... N ) -> ( ( 1 ... ( n - 1 ) ) u. ( ( ( n - 1 ) + 1 ) ... n ) ) = ( ( 1 ... ( n - 1 ) ) u. { n } ) )
188 182 187 eqtrd 
 |-  ( n e. ( 1 ... N ) -> ( 1 ... n ) = ( ( 1 ... ( n - 1 ) ) u. { n } ) )
189 188 raleqdv 
 |-  ( n e. ( 1 ... N ) -> ( A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) <-> A. b e. ( ( 1 ... ( n - 1 ) ) u. { n } ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
190 172 189 syl5ibr 
 |-  ( n e. ( 1 ... N ) -> ( ( A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) /\ A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
191 190 expdimp 
 |-  ( ( n e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> ( A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) -> A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
192 191 con3d 
 |-  ( ( n e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> ( -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) -> -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
193 192 adantrl 
 |-  ( ( n e. ( 1 ... N ) /\ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) -> ( -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) -> -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
194 193 expimpd 
 |-  ( n e. ( 1 ... N ) -> ( ( ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) /\ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
195 171 194 jaod 
 |-  ( n e. ( 1 ... N ) -> ( ( ( ( n - 1 ) = 0 /\ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) \/ ( ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) /\ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) -> -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
196 151 195 syl5bi 
 |-  ( n e. ( 1 ... N ) -> ( ( ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) /\ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) )
197 fveq2 
 |-  ( b = n -> ( P ` b ) = ( P ` n ) )
198 197 neeq1d 
 |-  ( b = n -> ( ( P ` b ) =/= 0 <-> ( P ` n ) =/= 0 ) )
199 70 198 anbi12d 
 |-  ( b = n -> ( ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) <-> ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) /\ ( P ` n ) =/= 0 ) ) )
200 199 ralsng 
 |-  ( n e. ( 1 ... N ) -> ( A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) <-> ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) /\ ( P ` n ) =/= 0 ) ) )
201 200 notbid 
 |-  ( n e. ( 1 ... N ) -> ( -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) <-> -. ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) /\ ( P ` n ) =/= 0 ) ) )
202 ianor 
 |-  ( -. ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) /\ ( P ` n ) =/= 0 ) <-> ( -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) \/ -. ( P ` n ) =/= 0 ) )
203 nne 
 |-  ( -. ( P ` n ) =/= 0 <-> ( P ` n ) = 0 )
204 203 orbi2i 
 |-  ( ( -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) \/ -. ( P ` n ) =/= 0 ) <-> ( -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) \/ ( P ` n ) = 0 ) )
205 202 204 bitri 
 |-  ( -. ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) /\ ( P ` n ) =/= 0 ) <-> ( -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) \/ ( P ` n ) = 0 ) )
206 201 205 bitrdi 
 |-  ( n e. ( 1 ... N ) -> ( -. A. b e. { n } ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) <-> ( -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) \/ ( P ` n ) = 0 ) ) )
207 196 206 sylibd 
 |-  ( n e. ( 1 ... N ) -> ( ( ( ( n - 1 ) = 0 \/ ( ( n - 1 ) e. ( 1 ... N ) /\ A. b e. ( 1 ... ( n - 1 ) ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) ) /\ -. A. b e. ( 1 ... n ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) ) -> ( -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) \/ ( P ` n ) = 0 ) ) )
208 150 207 syld 
 |-  ( n e. ( 1 ... N ) -> ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) \/ ( P ` n ) = 0 ) ) )
209 208 ad2antlr 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) \/ ( P ` n ) = 0 ) ) )
210 retop 
 |-  ( topGen ` ran (,) ) e. Top
211 210 fconst6 
 |-  ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top
212 pttop 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) : ( 1 ... N ) --> Top ) -> ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) e. Top )
213 35 211 212 mp2an 
 |-  ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ) e. Top
214 3 213 eqeltri 
 |-  R e. Top
215 reex 
 |-  RR e. _V
216 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
217 mapss 
 |-  ( ( RR e. _V /\ ( 0 [,] 1 ) C_ RR ) -> ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) ) )
218 215 216 217 mp2an 
 |-  ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) C_ ( RR ^m ( 1 ... N ) )
219 2 218 eqsstri 
 |-  I C_ ( RR ^m ( 1 ... N ) )
220 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
221 3 220 ptuniconst 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( topGen ` ran (,) ) e. Top ) -> ( RR ^m ( 1 ... N ) ) = U. R )
222 35 210 221 mp2an 
 |-  ( RR ^m ( 1 ... N ) ) = U. R
223 222 restuni 
 |-  ( ( R e. Top /\ I C_ ( RR ^m ( 1 ... N ) ) ) -> I = U. ( R |`t I ) )
224 214 219 223 mp2an 
 |-  I = U. ( R |`t I )
225 224 222 cnf 
 |-  ( F e. ( ( R |`t I ) Cn R ) -> F : I --> ( RR ^m ( 1 ... N ) ) )
226 4 225 syl 
 |-  ( ph -> F : I --> ( RR ^m ( 1 ... N ) ) )
227 226 ad2antrr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> F : I --> ( RR ^m ( 1 ... N ) ) )
228 simplr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> k e. NN )
229 elfzelz 
 |-  ( x e. ( 0 ... k ) -> x e. ZZ )
230 229 zred 
 |-  ( x e. ( 0 ... k ) -> x e. RR )
231 230 adantr 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> x e. RR )
232 nnre 
 |-  ( k e. NN -> k e. RR )
233 232 adantl 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> k e. RR )
234 nnne0 
 |-  ( k e. NN -> k =/= 0 )
235 234 adantl 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> k =/= 0 )
236 231 233 235 redivcld 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> ( x / k ) e. RR )
237 elfzle1 
 |-  ( x e. ( 0 ... k ) -> 0 <_ x )
238 230 237 jca 
 |-  ( x e. ( 0 ... k ) -> ( x e. RR /\ 0 <_ x ) )
239 nnrp 
 |-  ( k e. NN -> k e. RR+ )
240 239 rpregt0d 
 |-  ( k e. NN -> ( k e. RR /\ 0 < k ) )
241 divge0 
 |-  ( ( ( x e. RR /\ 0 <_ x ) /\ ( k e. RR /\ 0 < k ) ) -> 0 <_ ( x / k ) )
242 238 240 241 syl2an 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> 0 <_ ( x / k ) )
243 elfzle2 
 |-  ( x e. ( 0 ... k ) -> x <_ k )
244 243 adantr 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> x <_ k )
245 1red 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> 1 e. RR )
246 239 adantl 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> k e. RR+ )
247 231 245 246 ledivmuld 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> ( ( x / k ) <_ 1 <-> x <_ ( k x. 1 ) ) )
248 nncn 
 |-  ( k e. NN -> k e. CC )
249 248 mulid1d 
 |-  ( k e. NN -> ( k x. 1 ) = k )
250 249 breq2d 
 |-  ( k e. NN -> ( x <_ ( k x. 1 ) <-> x <_ k ) )
251 250 adantl 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> ( x <_ ( k x. 1 ) <-> x <_ k ) )
252 247 251 bitrd 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> ( ( x / k ) <_ 1 <-> x <_ k ) )
253 244 252 mpbird 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> ( x / k ) <_ 1 )
254 elicc01 
 |-  ( ( x / k ) e. ( 0 [,] 1 ) <-> ( ( x / k ) e. RR /\ 0 <_ ( x / k ) /\ ( x / k ) <_ 1 ) )
255 236 242 253 254 syl3anbrc 
 |-  ( ( x e. ( 0 ... k ) /\ k e. NN ) -> ( x / k ) e. ( 0 [,] 1 ) )
256 255 ancoms 
 |-  ( ( k e. NN /\ x e. ( 0 ... k ) ) -> ( x / k ) e. ( 0 [,] 1 ) )
257 elsni 
 |-  ( y e. { k } -> y = k )
258 257 oveq2d 
 |-  ( y e. { k } -> ( x / y ) = ( x / k ) )
259 258 eleq1d 
 |-  ( y e. { k } -> ( ( x / y ) e. ( 0 [,] 1 ) <-> ( x / k ) e. ( 0 [,] 1 ) ) )
260 256 259 syl5ibrcom 
 |-  ( ( k e. NN /\ x e. ( 0 ... k ) ) -> ( y e. { k } -> ( x / y ) e. ( 0 [,] 1 ) ) )
261 260 impr 
 |-  ( ( k e. NN /\ ( x e. ( 0 ... k ) /\ y e. { k } ) ) -> ( x / y ) e. ( 0 [,] 1 ) )
262 228 261 sylan 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ ( x e. ( 0 ... k ) /\ y e. { k } ) ) -> ( x / y ) e. ( 0 [,] 1 ) )
263 elun 
 |-  ( y e. ( { 1 } u. { 0 } ) <-> ( y e. { 1 } \/ y e. { 0 } ) )
264 fzofzp1 
 |-  ( x e. ( 0 ..^ k ) -> ( x + 1 ) e. ( 0 ... k ) )
265 elsni 
 |-  ( y e. { 1 } -> y = 1 )
266 265 oveq2d 
 |-  ( y e. { 1 } -> ( x + y ) = ( x + 1 ) )
267 266 eleq1d 
 |-  ( y e. { 1 } -> ( ( x + y ) e. ( 0 ... k ) <-> ( x + 1 ) e. ( 0 ... k ) ) )
268 264 267 syl5ibrcom 
 |-  ( x e. ( 0 ..^ k ) -> ( y e. { 1 } -> ( x + y ) e. ( 0 ... k ) ) )
269 elfzonn0 
 |-  ( x e. ( 0 ..^ k ) -> x e. NN0 )
270 269 nn0cnd 
 |-  ( x e. ( 0 ..^ k ) -> x e. CC )
271 270 addid1d 
 |-  ( x e. ( 0 ..^ k ) -> ( x + 0 ) = x )
272 elfzofz 
 |-  ( x e. ( 0 ..^ k ) -> x e. ( 0 ... k ) )
273 271 272 eqeltrd 
 |-  ( x e. ( 0 ..^ k ) -> ( x + 0 ) e. ( 0 ... k ) )
274 elsni 
 |-  ( y e. { 0 } -> y = 0 )
275 274 oveq2d 
 |-  ( y e. { 0 } -> ( x + y ) = ( x + 0 ) )
276 275 eleq1d 
 |-  ( y e. { 0 } -> ( ( x + y ) e. ( 0 ... k ) <-> ( x + 0 ) e. ( 0 ... k ) ) )
277 273 276 syl5ibrcom 
 |-  ( x e. ( 0 ..^ k ) -> ( y e. { 0 } -> ( x + y ) e. ( 0 ... k ) ) )
278 268 277 jaod 
 |-  ( x e. ( 0 ..^ k ) -> ( ( y e. { 1 } \/ y e. { 0 } ) -> ( x + y ) e. ( 0 ... k ) ) )
279 263 278 syl5bi 
 |-  ( x e. ( 0 ..^ k ) -> ( y e. ( { 1 } u. { 0 } ) -> ( x + y ) e. ( 0 ... k ) ) )
280 279 imp 
 |-  ( ( x e. ( 0 ..^ k ) /\ y e. ( { 1 } u. { 0 } ) ) -> ( x + y ) e. ( 0 ... k ) )
281 280 adantl 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ ( x e. ( 0 ..^ k ) /\ y e. ( { 1 } u. { 0 } ) ) ) -> ( x + y ) e. ( 0 ... k ) )
282 7 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
283 xp1st 
 |-  ( ( G ` k ) e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` ( G ` k ) ) e. ( NN0 ^m ( 1 ... N ) ) )
284 elmapfn 
 |-  ( ( 1st ` ( G ` k ) ) e. ( NN0 ^m ( 1 ... N ) ) -> ( 1st ` ( G ` k ) ) Fn ( 1 ... N ) )
285 282 283 284 3syl 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( G ` k ) ) Fn ( 1 ... N ) )
286 df-f 
 |-  ( ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> ( 0 ..^ k ) <-> ( ( 1st ` ( G ` k ) ) Fn ( 1 ... N ) /\ ran ( 1st ` ( G ` k ) ) C_ ( 0 ..^ k ) ) )
287 285 8 286 sylanbrc 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> ( 0 ..^ k ) )
288 287 adantr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( 1st ` ( G ` k ) ) : ( 1 ... N ) --> ( 0 ..^ k ) )
289 1ex 
 |-  1 e. _V
290 289 fconst 
 |-  ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) : ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) --> { 1 }
291 40 fconst 
 |-  ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) --> { 0 }
292 290 291 pm3.2i 
 |-  ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) : ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) --> { 1 } /\ ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) --> { 0 } )
293 xp2nd 
 |-  ( ( G ` k ) e. ( ( NN0 ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( G ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
294 282 293 syl 
 |-  ( ( ph /\ k e. NN ) -> ( 2nd ` ( G ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
295 fvex 
 |-  ( 2nd ` ( G ` k ) ) e. _V
296 f1oeq1 
 |-  ( f = ( 2nd ` ( G ` k ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
297 295 296 elab 
 |-  ( ( 2nd ` ( G ` k ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
298 294 297 sylib 
 |-  ( ( ph /\ k e. NN ) -> ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
299 dff1o3 
 |-  ( ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( G ` k ) ) ) )
300 299 simprbi 
 |-  ( ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( G ` k ) ) )
301 imain 
 |-  ( Fun `' ( 2nd ` ( G ` k ) ) -> ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) i^i ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) ) )
302 298 300 301 3syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) i^i ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) ) )
303 elfznn0 
 |-  ( j e. ( 0 ... N ) -> j e. NN0 )
304 303 nn0red 
 |-  ( j e. ( 0 ... N ) -> j e. RR )
305 304 ltp1d 
 |-  ( j e. ( 0 ... N ) -> j < ( j + 1 ) )
306 fzdisj 
 |-  ( j < ( j + 1 ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
307 305 306 syl 
 |-  ( j e. ( 0 ... N ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
308 307 imaeq2d 
 |-  ( j e. ( 0 ... N ) -> ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( 2nd ` ( G ` k ) ) " (/) ) )
309 ima0 
 |-  ( ( 2nd ` ( G ` k ) ) " (/) ) = (/)
310 308 309 eqtrdi 
 |-  ( j e. ( 0 ... N ) -> ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = (/) )
311 302 310 sylan9req 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) i^i ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) ) = (/) )
312 fun 
 |-  ( ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) : ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) --> { 1 } /\ ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) --> { 0 } ) /\ ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) i^i ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) ) = (/) ) -> ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) u. ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
313 292 311 312 sylancr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) u. ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
314 imaundi 
 |-  ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) u. ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) )
315 nn0p1nn 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN )
316 303 315 syl 
 |-  ( j e. ( 0 ... N ) -> ( j + 1 ) e. NN )
317 nnuz 
 |-  NN = ( ZZ>= ` 1 )
318 316 317 eleqtrdi 
 |-  ( j e. ( 0 ... N ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
319 elfzuz3 
 |-  ( j e. ( 0 ... N ) -> N e. ( ZZ>= ` j ) )
320 fzsplit2 
 |-  ( ( ( j + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` j ) ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
321 318 319 320 syl2anc 
 |-  ( j e. ( 0 ... N ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
322 321 imaeq2d 
 |-  ( j e. ( 0 ... N ) -> ( ( 2nd ` ( G ` k ) ) " ( 1 ... N ) ) = ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) )
323 f1ofo 
 |-  ( ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
324 foima 
 |-  ( ( 2nd ` ( G ` k ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( G ` k ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
325 298 323 324 3syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2nd ` ( G ` k ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
326 322 325 sylan9req 
 |-  ( ( j e. ( 0 ... N ) /\ ( ph /\ k e. NN ) ) -> ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
327 326 ancoms 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( 2nd ` ( G ` k ) ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
328 314 327 eqtr3id 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) u. ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
329 328 feq2d 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) u. ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) <-> ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) ) )
330 313 329 mpbid 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) )
331 fzfid 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( 1 ... N ) e. Fin )
332 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
333 281 288 330 331 331 332 off 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( 1st ` ( G ` k ) ) oF + ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... k ) )
334 6 feq1i 
 |-  ( P : ( 1 ... N ) --> ( 0 ... k ) <-> ( ( 1st ` ( G ` k ) ) oF + ( ( ( ( 2nd ` ( G ` k ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( G ` k ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... k ) )
335 333 334 sylibr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> P : ( 1 ... N ) --> ( 0 ... k ) )
336 vex 
 |-  k e. _V
337 336 fconst 
 |-  ( ( 1 ... N ) X. { k } ) : ( 1 ... N ) --> { k }
338 337 a1i 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( 1 ... N ) X. { k } ) : ( 1 ... N ) --> { k } )
339 262 335 338 331 331 332 off 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( P oF / ( ( 1 ... N ) X. { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
340 2 eleq2i 
 |-  ( ( P oF / ( ( 1 ... N ) X. { k } ) ) e. I <-> ( P oF / ( ( 1 ... N ) X. { k } ) ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) )
341 ovex 
 |-  ( 0 [,] 1 ) e. _V
342 ovex 
 |-  ( 1 ... N ) e. _V
343 341 342 elmap 
 |-  ( ( P oF / ( ( 1 ... N ) X. { k } ) ) e. ( ( 0 [,] 1 ) ^m ( 1 ... N ) ) <-> ( P oF / ( ( 1 ... N ) X. { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
344 340 343 bitri 
 |-  ( ( P oF / ( ( 1 ... N ) X. { k } ) ) e. I <-> ( P oF / ( ( 1 ... N ) X. { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1 ) )
345 339 344 sylibr 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( P oF / ( ( 1 ... N ) X. { k } ) ) e. I )
346 227 345 ffvelrnd 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) e. ( RR ^m ( 1 ... N ) ) )
347 elmapi 
 |-  ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) e. ( RR ^m ( 1 ... N ) ) -> ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) : ( 1 ... N ) --> RR )
348 346 347 syl 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) : ( 1 ... N ) --> RR )
349 348 ffvelrnda 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) e. RR )
350 349 an32s 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) e. RR )
351 0red 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> 0 e. RR )
352 350 351 ltnled 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) < 0 <-> -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
353 ltle 
 |-  ( ( ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) e. RR /\ 0 e. RR ) -> ( ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) < 0 -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
354 350 45 353 sylancl 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) < 0 -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
355 352 354 sylbird 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
356 248 234 div0d 
 |-  ( k e. NN -> ( 0 / k ) = 0 )
357 oveq1 
 |-  ( ( P ` n ) = 0 -> ( ( P ` n ) / k ) = ( 0 / k ) )
358 357 eqeq1d 
 |-  ( ( P ` n ) = 0 -> ( ( ( P ` n ) / k ) = 0 <-> ( 0 / k ) = 0 ) )
359 356 358 syl5ibrcom 
 |-  ( k e. NN -> ( ( P ` n ) = 0 -> ( ( P ` n ) / k ) = 0 ) )
360 359 ad3antlr 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( P ` n ) = 0 -> ( ( P ` n ) / k ) = 0 ) )
361 335 ffnd 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> P Fn ( 1 ... N ) )
362 fnconstg 
 |-  ( k e. _V -> ( ( 1 ... N ) X. { k } ) Fn ( 1 ... N ) )
363 336 362 mp1i 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) -> ( ( 1 ... N ) X. { k } ) Fn ( 1 ... N ) )
364 eqidd 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( P ` n ) = ( P ` n ) )
365 336 fvconst2 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { k } ) ` n ) = k )
366 365 adantl 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1 ... N ) X. { k } ) ` n ) = k )
367 361 363 331 331 332 364 366 ofval 
 |-  ( ( ( ( ph /\ k e. NN ) /\ j e. ( 0 ... N ) ) /\ n e. ( 1 ... N ) ) -> ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = ( ( P ` n ) / k ) )
368 367 an32s 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = ( ( P ` n ) / k ) )
369 368 eqeq1d 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 0 <-> ( ( P ` n ) / k ) = 0 ) )
370 360 369 sylibrd 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( P ` n ) = 0 -> ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 0 ) )
371 simplll 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ph )
372 simplr 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> n e. ( 1 ... N ) )
373 345 adantlr 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( P oF / ( ( 1 ... N ) X. { k } ) ) e. I )
374 ovex 
 |-  ( P oF / ( ( 1 ... N ) X. { k } ) ) e. _V
375 eleq1 
 |-  ( z = ( P oF / ( ( 1 ... N ) X. { k } ) ) -> ( z e. I <-> ( P oF / ( ( 1 ... N ) X. { k } ) ) e. I ) )
376 fveq1 
 |-  ( z = ( P oF / ( ( 1 ... N ) X. { k } ) ) -> ( z ` n ) = ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) )
377 376 eqeq1d 
 |-  ( z = ( P oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( z ` n ) = 0 <-> ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 0 ) )
378 fveq2 
 |-  ( z = ( P oF / ( ( 1 ... N ) X. { k } ) ) -> ( F ` z ) = ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) )
379 378 fveq1d 
 |-  ( z = ( P oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( F ` z ) ` n ) = ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )
380 379 breq1d 
 |-  ( z = ( P oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( ( F ` z ) ` n ) <_ 0 <-> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
381 377 380 imbi12d 
 |-  ( z = ( P oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( ( z ` n ) = 0 -> ( ( F ` z ) ` n ) <_ 0 ) <-> ( ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 0 -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) ) )
382 375 381 imbi12d 
 |-  ( z = ( P oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( z e. I -> ( ( z ` n ) = 0 -> ( ( F ` z ) ` n ) <_ 0 ) ) <-> ( ( P oF / ( ( 1 ... N ) X. { k } ) ) e. I -> ( ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 0 -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) ) ) )
383 382 imbi2d 
 |-  ( z = ( P oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( n e. ( 1 ... N ) -> ( z e. I -> ( ( z ` n ) = 0 -> ( ( F ` z ) ` n ) <_ 0 ) ) ) <-> ( n e. ( 1 ... N ) -> ( ( P oF / ( ( 1 ... N ) X. { k } ) ) e. I -> ( ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 0 -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) ) ) ) )
384 383 imbi2d 
 |-  ( z = ( P oF / ( ( 1 ... N ) X. { k } ) ) -> ( ( ph -> ( n e. ( 1 ... N ) -> ( z e. I -> ( ( z ` n ) = 0 -> ( ( F ` z ) ` n ) <_ 0 ) ) ) ) <-> ( ph -> ( n e. ( 1 ... N ) -> ( ( P oF / ( ( 1 ... N ) X. { k } ) ) e. I -> ( ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 0 -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) ) ) ) ) )
385 5 3exp2 
 |-  ( ph -> ( n e. ( 1 ... N ) -> ( z e. I -> ( ( z ` n ) = 0 -> ( ( F ` z ) ` n ) <_ 0 ) ) ) )
386 374 384 385 vtocl 
 |-  ( ph -> ( n e. ( 1 ... N ) -> ( ( P oF / ( ( 1 ... N ) X. { k } ) ) e. I -> ( ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 0 -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) ) ) )
387 371 372 373 386 syl3c 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( ( P oF / ( ( 1 ... N ) X. { k } ) ) ` n ) = 0 -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
388 370 387 syld 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( P ` n ) = 0 -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
389 355 388 jaod 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( -. 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) \/ ( P ` n ) = 0 ) -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
390 209 389 syld 
 |-  ( ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) /\ j e. ( 0 ... N ) ) -> ( ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
391 390 reximdva 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... N ) ) -> ( E. j e. ( 0 ... N ) ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> E. j e. ( 0 ... N ) ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
392 391 anasss 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> ( E. j e. ( 0 ... N ) ( n - 1 ) = sup ( ( { 0 } u. { a e. ( 1 ... N ) | A. b e. ( 1 ... a ) ( 0 <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` b ) /\ ( P ` b ) =/= 0 ) } ) , RR , < ) -> E. j e. ( 0 ... N ) ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
393 115 392 mpd 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> E. j e. ( 0 ... N ) ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 )
394 breq 
 |-  ( r = `' <_ -> ( 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <-> 0 `' <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
395 fvex 
 |-  ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) e. _V
396 40 395 brcnv 
 |-  ( 0 `' <_ ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <-> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 )
397 394 396 bitrdi 
 |-  ( r = `' <_ -> ( 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <-> ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
398 397 rexbidv 
 |-  ( r = `' <_ -> ( E. j e. ( 0 ... N ) 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <-> E. j e. ( 0 ... N ) ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) <_ 0 ) )
399 393 398 syl5ibrcom 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> ( r = `' <_ -> E. j e. ( 0 ... N ) 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
400 84 399 jaod 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> ( ( r = <_ \/ r = `' <_ ) -> E. j e. ( 0 ... N ) 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
401 10 400 syl5 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) ) ) -> ( r e. { <_ , `' <_ } -> E. j e. ( 0 ... N ) 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) )
402 401 exp32 
 |-  ( ph -> ( k e. NN -> ( n e. ( 1 ... N ) -> ( r e. { <_ , `' <_ } -> E. j e. ( 0 ... N ) 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) ) ) ) )
403 402 3imp2 
 |-  ( ( ph /\ ( k e. NN /\ n e. ( 1 ... N ) /\ r e. { <_ , `' <_ } ) ) -> E. j e. ( 0 ... N ) 0 r ( ( F ` ( P oF / ( ( 1 ... N ) X. { k } ) ) ) ` n ) )