Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem2 Structured version   Visualization version   Unicode version

Theorem poimirlem2 32006
Description: Lemma for poimir 32037- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimirlem2.1  |-  ( ph  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  M ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) )
poimirlem2.2  |-  ( ph  ->  T : ( 1 ... N ) --> ZZ )
poimirlem2.3  |-  ( ph  ->  U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
poimirlem2.4  |-  ( ph  ->  V  e.  ( 1 ... ( N  - 
1 ) ) )
poimirlem2.5  |-  ( ph  ->  M  e.  ( ( 0 ... N ) 
\  { V }
) )
Assertion
Ref Expression
poimirlem2  |-  ( ph  ->  E* n  e.  ( 1 ... N ) ( ( F `  ( V  -  1
) ) `  n
)  =/=  ( ( F `  V ) `
 n ) )
Distinct variable groups:    j, n, y, ph    j, F, n, y    j, M, n, y    j, N, n, y    T, j, n, y    U, j, n, y    j, V, n, y

Proof of Theorem poimirlem2
Dummy variable  m is distinct from all other variables.
StepHypRef Expression
1 poimirlem2.3 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
2 dff1o3 5834 . . . . . . . . . . . . . . . . 17  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( U :
( 1 ... N
) -onto-> ( 1 ... N )  /\  Fun  `' U ) )
32simprbi 471 . . . . . . . . . . . . . . . 16  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  Fun  `' U
)
41, 3syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Fun  `' U )
5 imadif 5668 . . . . . . . . . . . . . . 15  |-  ( Fun  `' U  ->  ( U
" ( ( 1 ... N )  \  { ( V  + 
1 ) } ) )  =  ( ( U " ( 1 ... N ) ) 
\  ( U " { ( V  + 
1 ) } ) ) )
64, 5syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( U " (
( 1 ... N
)  \  { ( V  +  1 ) } ) )  =  ( ( U "
( 1 ... N
) )  \  ( U " { ( V  +  1 ) } ) ) )
7 poimirlem2.4 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  V  e.  ( 1 ... ( N  - 
1 ) ) )
8 fzp1elp1 11875 . . . . . . . . . . . . . . . . . . . 20  |-  ( V  e.  ( 1 ... ( N  -  1 ) )  ->  ( V  +  1 )  e.  ( 1 ... ( ( N  - 
1 )  +  1 ) ) )
97, 8syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( V  +  1 )  e.  ( 1 ... ( ( N  -  1 )  +  1 ) ) )
10 poimir.0 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  N  e.  NN )
1110nncnd 10647 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  N  e.  CC )
12 npcan1 10065 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
1413oveq2d 6324 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 1 ... (
( N  -  1 )  +  1 ) )  =  ( 1 ... N ) )
159, 14eleqtrd 2551 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( V  +  1 )  e.  ( 1 ... N ) )
16 fzsplit 11851 . . . . . . . . . . . . . . . . . 18  |-  ( ( V  +  1 )  e.  ( 1 ... N )  ->  (
1 ... N )  =  ( ( 1 ... ( V  +  1 ) )  u.  (
( ( V  + 
1 )  +  1 ) ... N ) ) )
1715, 16syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1 ... N
)  =  ( ( 1 ... ( V  +  1 ) )  u.  ( ( ( V  +  1 )  +  1 ) ... N ) ) )
1817difeq1d 3539 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1 ... N )  \  {
( V  +  1 ) } )  =  ( ( ( 1 ... ( V  + 
1 ) )  u.  ( ( ( V  +  1 )  +  1 ) ... N
) )  \  {
( V  +  1 ) } ) )
19 difundir 3687 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1 ... ( V  +  1 ) )  u.  ( ( ( V  +  1 )  +  1 ) ... N ) ) 
\  { ( V  +  1 ) } )  =  ( ( ( 1 ... ( V  +  1 ) )  \  { ( V  +  1 ) } )  u.  (
( ( ( V  +  1 )  +  1 ) ... N
)  \  { ( V  +  1 ) } ) )
20 elfzuz 11822 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( V  e.  ( 1 ... ( N  -  1 ) )  ->  V  e.  ( ZZ>= `  1 )
)
217, 20syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  V  e.  ( ZZ>= ` 
1 ) )
22 fzsuc 11869 . . . . . . . . . . . . . . . . . . . . 21  |-  ( V  e.  ( ZZ>= `  1
)  ->  ( 1 ... ( V  + 
1 ) )  =  ( ( 1 ... V )  u.  {
( V  +  1 ) } ) )
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1 ... ( V  +  1 ) )  =  ( ( 1 ... V )  u.  { ( V  +  1 ) } ) )
2423difeq1d 3539 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1 ... ( V  +  1 ) )  \  {
( V  +  1 ) } )  =  ( ( ( 1 ... V )  u. 
{ ( V  + 
1 ) } ) 
\  { ( V  +  1 ) } ) )
25 difun2 3838 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1 ... V
)  u.  { ( V  +  1 ) } )  \  {
( V  +  1 ) } )  =  ( ( 1 ... V )  \  {
( V  +  1 ) } )
26 elfzelz 11826 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( V  e.  ( 1 ... ( N  -  1 ) )  ->  V  e.  ZZ )
277, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  V  e.  ZZ )
2827zred 11063 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  V  e.  RR )
2928ltp1d 10559 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  V  <  ( V  +  1 ) )
3027peano2zd 11066 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( V  +  1 )  e.  ZZ )
3130zred 11063 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( V  +  1 )  e.  RR )
3228, 31ltnled 9799 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( V  <  ( V  +  1 )  <->  -.  ( V  +  1 )  <_  V )
)
3329, 32mpbid 215 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  ( V  + 
1 )  <_  V
)
34 elfzle2 11829 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( V  +  1 )  e.  ( 1 ... V )  ->  ( V  +  1 )  <_  V )
3533, 34nsyl 125 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  ( V  + 
1 )  e.  ( 1 ... V ) )
36 difsn 4097 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( V  +  1 )  e.  ( 1 ... V )  -> 
( ( 1 ... V )  \  {
( V  +  1 ) } )  =  ( 1 ... V
) )
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( 1 ... V )  \  {
( V  +  1 ) } )  =  ( 1 ... V
) )
3825, 37syl5eq 2517 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( 1 ... V )  u. 
{ ( V  + 
1 ) } ) 
\  { ( V  +  1 ) } )  =  ( 1 ... V ) )
3924, 38eqtrd 2505 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1 ... ( V  +  1 ) )  \  {
( V  +  1 ) } )  =  ( 1 ... V
) )
4031ltp1d 10559 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( V  +  1 )  <  ( ( V  +  1 )  +  1 ) )
41 peano2re 9824 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( V  +  1 )  e.  RR  ->  (
( V  +  1 )  +  1 )  e.  RR )
4231, 41syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( V  + 
1 )  +  1 )  e.  RR )
4331, 42ltnled 9799 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( V  + 
1 )  <  (
( V  +  1 )  +  1 )  <->  -.  ( ( V  + 
1 )  +  1 )  <_  ( V  +  1 ) ) )
4440, 43mpbid 215 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  ( ( V  +  1 )  +  1 )  <_  ( V  +  1 ) )
45 elfzle1 11828 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( V  +  1 )  e.  ( ( ( V  +  1 )  +  1 ) ... N )  ->  (
( V  +  1 )  +  1 )  <_  ( V  + 
1 ) )
4644, 45nsyl 125 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  ( V  + 
1 )  e.  ( ( ( V  + 
1 )  +  1 ) ... N ) )
47 difsn 4097 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( V  +  1 )  e.  ( ( ( V  +  1 )  +  1 ) ... N )  -> 
( ( ( ( V  +  1 )  +  1 ) ... N )  \  {
( V  +  1 ) } )  =  ( ( ( V  +  1 )  +  1 ) ... N
) )
4846, 47syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( ( V  +  1 )  +  1 ) ... N )  \  {
( V  +  1 ) } )  =  ( ( ( V  +  1 )  +  1 ) ... N
) )
4939, 48uneq12d 3580 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( 1 ... ( V  + 
1 ) )  \  { ( V  + 
1 ) } )  u.  ( ( ( ( V  +  1 )  +  1 ) ... N )  \  { ( V  + 
1 ) } ) )  =  ( ( 1 ... V )  u.  ( ( ( V  +  1 )  +  1 ) ... N ) ) )
5019, 49syl5eq 2517 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 1 ... ( V  + 
1 ) )  u.  ( ( ( V  +  1 )  +  1 ) ... N
) )  \  {
( V  +  1 ) } )  =  ( ( 1 ... V )  u.  (
( ( V  + 
1 )  +  1 ) ... N ) ) )
5118, 50eqtrd 2505 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1 ... N )  \  {
( V  +  1 ) } )  =  ( ( 1 ... V )  u.  (
( ( V  + 
1 )  +  1 ) ... N ) ) )
5251imaeq2d 5174 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( U " (
( 1 ... N
)  \  { ( V  +  1 ) } ) )  =  ( U " (
( 1 ... V
)  u.  ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )
536, 52eqtr3d 2507 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  \  ( U " { ( V  +  1 ) } ) )  =  ( U " ( ( 1 ... V )  u.  ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )
54 imaundi 5254 . . . . . . . . . . . . 13  |-  ( U
" ( ( 1 ... V )  u.  ( ( ( V  +  1 )  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... V
) )  u.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )
5553, 54syl6eq 2521 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  \  ( U " { ( V  +  1 ) } ) )  =  ( ( U " (
1 ... V ) )  u.  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) ) ) )
5655eleq2d 2534 . . . . . . . . . . 11  |-  ( ph  ->  ( n  e.  ( ( U " (
1 ... N ) ) 
\  ( U " { ( V  + 
1 ) } ) )  <->  n  e.  (
( U " (
1 ... V ) )  u.  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) ) ) ) )
57 eldif 3400 . . . . . . . . . . 11  |-  ( n  e.  ( ( U
" ( 1 ... N ) )  \ 
( U " {
( V  +  1 ) } ) )  <-> 
( n  e.  ( U " ( 1 ... N ) )  /\  -.  n  e.  ( U " {
( V  +  1 ) } ) ) )
58 elun 3565 . . . . . . . . . . 11  |-  ( n  e.  ( ( U
" ( 1 ... V ) )  u.  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )  <->  ( n  e.  ( U " (
1 ... V ) )  \/  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )
5956, 57, 583bitr3g 295 . . . . . . . . . 10  |-  ( ph  ->  ( ( n  e.  ( U " (
1 ... N ) )  /\  -.  n  e.  ( U " {
( V  +  1 ) } ) )  <-> 
( n  e.  ( U " ( 1 ... V ) )  \/  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) ) ) )
6059adantr 472 . . . . . . . . 9  |-  ( (
ph  /\  M  <  V )  ->  ( (
n  e.  ( U
" ( 1 ... N ) )  /\  -.  n  e.  ( U " { ( V  +  1 ) } ) )  <->  ( n  e.  ( U " (
1 ... V ) )  \/  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) ) ) )
61 imassrn 5185 . . . . . . . . . . . . . . . 16  |-  ( U
" ( 1 ... V ) )  C_  ran  U
62 f1of 5828 . . . . . . . . . . . . . . . . . 18  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U :
( 1 ... N
) --> ( 1 ... N ) )
631, 62syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  U : ( 1 ... N ) --> ( 1 ... N ) )
64 frn 5747 . . . . . . . . . . . . . . . . 17  |-  ( U : ( 1 ... N ) --> ( 1 ... N )  ->  ran  U  C_  ( 1 ... N ) )
6563, 64syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  U  C_  (
1 ... N ) )
6661, 65syl5ss 3429 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( U " (
1 ... V ) ) 
C_  ( 1 ... N ) )
6766sselda 3418 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  n  e.  ( 1 ... N
) )
68 poimirlem2.2 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T : ( 1 ... N ) --> ZZ )
69 ffn 5739 . . . . . . . . . . . . . . . . . 18  |-  ( T : ( 1 ... N ) --> ZZ  ->  T  Fn  ( 1 ... N ) )
7068, 69syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  Fn  ( 1 ... N ) )
7170adantr 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  T  Fn  ( 1 ... N
) )
72 1ex 9656 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  _V
73 fnconstg 5784 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  e.  _V  ->  (
( U " (
1 ... V ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... V ) ) )
7472, 73ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U " ( 1 ... V ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... V ) )
75 c0ex 9655 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  _V
76 fnconstg 5784 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  _V  ->  (
( U " (
( V  +  1 ) ... N ) )  X.  { 0 } )  Fn  ( U " ( ( V  +  1 ) ... N ) ) )
7775, 76ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } )  Fn  ( U
" ( ( V  +  1 ) ... N ) )
7874, 77pm3.2i 462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( U " (
1 ... V ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... V ) )  /\  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } )  Fn  ( U " (
( V  +  1 ) ... N ) ) )
79 imain 5669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Fun  `' U  ->  ( U
" ( ( 1 ... V )  i^i  ( ( V  + 
1 ) ... N
) ) )  =  ( ( U "
( 1 ... V
) )  i^i  ( U " ( ( V  +  1 ) ... N ) ) ) )
804, 79syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... V
)  i^i  ( ( V  +  1 ) ... N ) ) )  =  ( ( U " ( 1 ... V ) )  i^i  ( U "
( ( V  + 
1 ) ... N
) ) ) )
81 fzdisj 11852 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( V  <  ( V  + 
1 )  ->  (
( 1 ... V
)  i^i  ( ( V  +  1 ) ... N ) )  =  (/) )
8229, 81syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1 ... V )  i^i  (
( V  +  1 ) ... N ) )  =  (/) )
8382imaeq2d 5174 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
( 1 ... V
)  i^i  ( ( V  +  1 ) ... N ) ) )  =  ( U
" (/) ) )
84 ima0 5189 . . . . . . . . . . . . . . . . . . . . 21  |-  ( U
" (/) )  =  (/)
8583, 84syl6eq 2521 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... V
)  i^i  ( ( V  +  1 ) ... N ) ) )  =  (/) )
8680, 85eqtr3d 2507 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( U "
( 1 ... V
) )  i^i  ( U " ( ( V  +  1 ) ... N ) ) )  =  (/) )
87 fnun 5692 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } )  Fn  ( U "
( 1 ... V
) )  /\  (
( U " (
( V  +  1 ) ... N ) )  X.  { 0 } )  Fn  ( U " ( ( V  +  1 ) ... N ) ) )  /\  ( ( U
" ( 1 ... V ) )  i^i  ( U " (
( V  +  1 ) ... N ) ) )  =  (/) )  ->  ( ( ( U " ( 1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
( U " (
1 ... V ) )  u.  ( U "
( ( V  + 
1 ) ... N
) ) ) )
8878, 86, 87sylancr 676 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( ( U " ( 1 ... V ) )  u.  ( U "
( ( V  + 
1 ) ... N
) ) ) )
89 imaundi 5254 . . . . . . . . . . . . . . . . . . . 20  |-  ( U
" ( ( 1 ... V )  u.  ( ( V  + 
1 ) ... N
) ) )  =  ( ( U "
( 1 ... V
) )  u.  ( U " ( ( V  +  1 ) ... N ) ) )
9010nnzd 11062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  N  e.  ZZ )
91 peano2zm 11004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
93 uzid 11197 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
9492, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1
) ) )
95 peano2uz 11235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
9694, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1
) ) )
9713, 96eqeltrrd 2550 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
98 fzss2 11864 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( 1 ... ( N  - 
1 ) )  C_  ( 1 ... N
) )
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 1 ... ( N  -  1 ) )  C_  ( 1 ... N ) )
10099, 7sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  V  e.  ( 1 ... N ) )
101 fzsplit 11851 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( V  e.  ( 1 ... N )  ->  (
1 ... N )  =  ( ( 1 ... V )  u.  (
( V  +  1 ) ... N ) ) )
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( 1 ... N
)  =  ( ( 1 ... V )  u.  ( ( V  +  1 ) ... N ) ) )
103102imaeq2d 5174 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
1 ... N ) )  =  ( U "
( ( 1 ... V )  u.  (
( V  +  1 ) ... N ) ) ) )
104 f1ofo 5835 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U :
( 1 ... N
) -onto-> ( 1 ... N ) )
1051, 104syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  U : ( 1 ... N ) -onto-> ( 1 ... N ) )
106 foima 5811 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U : ( 1 ... N ) -onto-> ( 1 ... N )  -> 
( U " (
1 ... N ) )  =  ( 1 ... N ) )
107105, 106syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
1 ... N ) )  =  ( 1 ... N ) )
108103, 107eqtr3d 2507 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... V
)  u.  ( ( V  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
10989, 108syl5eqr 2519 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( U "
( 1 ... V
) )  u.  ( U " ( ( V  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
110109fneq2d 5677 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( ( U " ( 1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
( U " (
1 ... V ) )  u.  ( U "
( ( V  + 
1 ) ... N
) ) )  <->  ( (
( U " (
1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
1 ... N ) ) )
11188, 110mpbid 215 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( 1 ... N ) )
112111adantr 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( (
( U " (
1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
1 ... N ) )
113 fzfid 12224 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( 1 ... N )  e. 
Fin )
114 inidm 3632 . . . . . . . . . . . . . . . 16  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
115 eqidd 2472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( U " (
1 ... V ) ) )  /\  n  e.  ( 1 ... N
) )  ->  ( T `  n )  =  ( T `  n ) )
116 fvun1 5951 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( U "
( 1 ... V
) )  X.  {
1 } )  Fn  ( U " (
1 ... V ) )  /\  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( U "
( ( V  + 
1 ) ... N
) )  /\  (
( ( U "
( 1 ... V
) )  i^i  ( U " ( ( V  +  1 ) ... N ) ) )  =  (/)  /\  n  e.  ( U " (
1 ... V ) ) ) )  ->  (
( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( U " ( 1 ... V ) )  X.  { 1 } ) `  n ) )
11774, 77, 116mp3an12 1380 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( U "
( 1 ... V
) )  i^i  ( U " ( ( V  +  1 ) ... N ) ) )  =  (/)  /\  n  e.  ( U " (
1 ... V ) ) )  ->  ( (
( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  ( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } ) `
 n ) )
11886, 117sylan 479 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( (
( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  ( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } ) `
 n ) )
11972fvconst2 6136 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( U "
( 1 ... V
) )  ->  (
( ( U "
( 1 ... V
) )  X.  {
1 } ) `  n )  =  1 )
120119adantl 473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( (
( U " (
1 ... V ) )  X.  { 1 } ) `  n )  =  1 )
121118, 120eqtrd 2505 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( (
( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  1 )
122121adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( U " (
1 ... V ) ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  n )  =  1 )
12371, 112, 113, 113, 114, 115, 122ofval 6559 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( U " (
1 ... V ) ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n )  =  ( ( T `  n
)  +  1 ) )
124 fnconstg 5784 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  e.  _V  ->  (
( U " (
1 ... ( V  + 
1 ) ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... ( V  +  1 ) ) ) )
12572, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... ( V  +  1 ) ) )
126 fnconstg 5784 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0  e.  _V  ->  (
( U " (
( ( V  + 
1 )  +  1 ) ... N ) )  X.  { 0 } )  Fn  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )
12775, 126ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } )  Fn  ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )
128125, 127pm3.2i 462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( U " (
1 ... ( V  + 
1 ) ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... ( V  +  1 ) ) )  /\  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } )  Fn  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )
129 imain 5669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Fun  `' U  ->  ( U
" ( ( 1 ... ( V  + 
1 ) )  i^i  ( ( ( V  +  1 )  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... ( V  +  1 ) ) )  i^i  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )
1304, 129syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... ( V  +  1 ) )  i^i  ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  ( ( U " ( 1 ... ( V  + 
1 ) ) )  i^i  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) ) ) )
131 fzdisj 11852 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( V  +  1 )  <  ( ( V  +  1 )  +  1 )  ->  (
( 1 ... ( V  +  1 ) )  i^i  ( ( ( V  +  1 )  +  1 ) ... N ) )  =  (/) )
13240, 131syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1 ... ( V  +  1 ) )  i^i  (
( ( V  + 
1 )  +  1 ) ... N ) )  =  (/) )
133132imaeq2d 5174 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
( 1 ... ( V  +  1 ) )  i^i  ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  ( U
" (/) ) )
134133, 84syl6eq 2521 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... ( V  +  1 ) )  i^i  ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  (/) )
135130, 134eqtr3d 2507 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( U "
( 1 ... ( V  +  1 ) ) )  i^i  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  (/) )
136 fnun 5692 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } )  Fn  ( U "
( 1 ... ( V  +  1 ) ) )  /\  (
( U " (
( ( V  + 
1 )  +  1 ) ... N ) )  X.  { 0 } )  Fn  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  /\  ( ( U
" ( 1 ... ( V  +  1 ) ) )  i^i  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )  =  (/) )  ->  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
( U " (
1 ... ( V  + 
1 ) ) )  u.  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) ) ) )
137128, 135, 136sylancr 676 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( ( U " ( 1 ... ( V  + 
1 ) ) )  u.  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) ) ) )
138 imaundi 5254 . . . . . . . . . . . . . . . . . . . 20  |-  ( U
" ( ( 1 ... ( V  + 
1 ) )  u.  ( ( ( V  +  1 )  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... ( V  +  1 ) ) )  u.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )
13917imaeq2d 5174 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
1 ... N ) )  =  ( U "
( ( 1 ... ( V  +  1 ) )  u.  (
( ( V  + 
1 )  +  1 ) ... N ) ) ) )
140139, 107eqtr3d 2507 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... ( V  +  1 ) )  u.  ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
141138, 140syl5eqr 2519 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( U "
( 1 ... ( V  +  1 ) ) )  u.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
142141fneq2d 5677 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
( U " (
1 ... ( V  + 
1 ) ) )  u.  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) ) )  <->  ( (
( U " (
1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
1 ... N ) ) )
143137, 142mpbid 215 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( 1 ... N ) )
144143adantr 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( (
( U " (
1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
1 ... N ) )
145 uzid 11197 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( V  e.  ZZ  ->  V  e.  ( ZZ>= `  V )
)
14627, 145syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  V  e.  ( ZZ>= `  V ) )
147 peano2uz 11235 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( V  e.  ( ZZ>= `  V
)  ->  ( V  +  1 )  e.  ( ZZ>= `  V )
)
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( V  +  1 )  e.  ( ZZ>= `  V ) )
149 fzss2 11864 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( V  +  1 )  e.  ( ZZ>= `  V
)  ->  ( 1 ... V )  C_  ( 1 ... ( V  +  1 ) ) )
150148, 149syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1 ... V
)  C_  ( 1 ... ( V  + 
1 ) ) )
151 imass2 5210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1 ... V ) 
C_  ( 1 ... ( V  +  1 ) )  ->  ( U " ( 1 ... V ) )  C_  ( U " ( 1 ... ( V  + 
1 ) ) ) )
152150, 151syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( U " (
1 ... V ) ) 
C_  ( U "
( 1 ... ( V  +  1 ) ) ) )
153152sselda 3418 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  n  e.  ( U " ( 1 ... ( V  + 
1 ) ) ) )
154 fvun1 5951 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  Fn  ( U " (
1 ... ( V  + 
1 ) ) )  /\  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  /\  (
( ( U "
( 1 ... ( V  +  1 ) ) )  i^i  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  (/)  /\  n  e.  ( U " (
1 ... ( V  + 
1 ) ) ) ) )  ->  (
( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } ) `  n ) )
155125, 127, 154mp3an12 1380 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( U "
( 1 ... ( V  +  1 ) ) )  i^i  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  (/)  /\  n  e.  ( U " (
1 ... ( V  + 
1 ) ) ) )  ->  ( (
( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  ( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } ) `
 n ) )
156135, 155sylan 479 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... ( V  + 
1 ) ) ) )  ->  ( (
( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  ( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } ) `
 n ) )
15772fvconst2 6136 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( U "
( 1 ... ( V  +  1 ) ) )  ->  (
( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } ) `  n )  =  1 )
158157adantl 473 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... ( V  + 
1 ) ) ) )  ->  ( (
( U " (
1 ... ( V  + 
1 ) ) )  X.  { 1 } ) `  n )  =  1 )
159156, 158eqtrd 2505 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... ( V  + 
1 ) ) ) )  ->  ( (
( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  1 )
160153, 159syldan 478 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( (
( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  1 )
161160adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( U " (
1 ... V ) ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  n )  =  1 )
16271, 144, 113, 113, 114, 115, 161ofval 6559 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( U " (
1 ... V ) ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n )  =  ( ( T `  n
)  +  1 ) )
163123, 162eqtr4d 2508 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( U " (
1 ... V ) ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n )  =  ( ( T  oF  +  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n ) )
16467, 163mpdan 681 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( ( T  oF  +  ( ( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) ) `  n )  =  ( ( T  oF  +  ( ( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) ) `  n ) )
165 imassrn 5185 . . . . . . . . . . . . . . . 16  |-  ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  C_  ran  U
166165, 65syl5ss 3429 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) )  C_  ( 1 ... N ) )
167166sselda 3418 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  n  e.  ( 1 ... N
) )
16870adantr 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  T  Fn  ( 1 ... N
) )
169111adantr 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( (
( U " (
1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
1 ... N ) )
170 fzfid 12224 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( 1 ... N )  e. 
Fin )
171 eqidd 2472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )  /\  n  e.  ( 1 ... N
) )  ->  ( T `  n )  =  ( T `  n ) )
172 uzid 11197 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( V  +  1 )  e.  ZZ  ->  ( V  +  1 )  e.  ( ZZ>= `  ( V  +  1 ) ) )
17330, 172syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( V  +  1 )  e.  ( ZZ>= `  ( V  +  1
) ) )
174 peano2uz 11235 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( V  +  1 )  e.  ( ZZ>= `  ( V  +  1 ) )  ->  ( ( V  +  1 )  +  1 )  e.  ( ZZ>= `  ( V  +  1 ) ) )
175173, 174syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( V  + 
1 )  +  1 )  e.  ( ZZ>= `  ( V  +  1
) ) )
176 fzss1 11863 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( V  +  1 )  +  1 )  e.  ( ZZ>= `  ( V  +  1 ) )  ->  ( (
( V  +  1 )  +  1 ) ... N )  C_  ( ( V  + 
1 ) ... N
) )
177175, 176syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( V  +  1 )  +  1 ) ... N
)  C_  ( ( V  +  1 ) ... N ) )
178 imass2 5210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( V  + 
1 )  +  1 ) ... N ) 
C_  ( ( V  +  1 ) ... N )  ->  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  C_  ( U " ( ( V  +  1 ) ... N ) ) )
179177, 178syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) )  C_  ( U " ( ( V  + 
1 ) ... N
) ) )
180179sselda 3418 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  n  e.  ( U " ( ( V  +  1 ) ... N ) ) )
181 fvun2 5952 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( U "
( 1 ... V
) )  X.  {
1 } )  Fn  ( U " (
1 ... V ) )  /\  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( U "
( ( V  + 
1 ) ... N
) )  /\  (
( ( U "
( 1 ... V
) )  i^i  ( U " ( ( V  +  1 ) ... N ) ) )  =  (/)  /\  n  e.  ( U " (
( V  +  1 ) ... N ) ) ) )  -> 
( ( ( ( U " ( 1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) `  n
)  =  ( ( ( U " (
( V  +  1 ) ... N ) )  X.  { 0 } ) `  n
) )
18274, 77, 181mp3an12 1380 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( U "
( 1 ... V
) )  i^i  ( U " ( ( V  +  1 ) ... N ) ) )  =  (/)  /\  n  e.  ( U " (
( V  +  1 ) ... N ) ) )  ->  (
( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) `  n ) )
18386, 182sylan 479 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  ( U " ( ( V  +  1 ) ... N ) ) )  ->  ( (
( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  ( ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } ) `
 n ) )
18475fvconst2 6136 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( U "
( ( V  + 
1 ) ... N
) )  ->  (
( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) `  n )  =  0 )
185184adantl 473 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  ( U " ( ( V  +  1 ) ... N ) ) )  ->  ( (
( U " (
( V  +  1 ) ... N ) )  X.  { 0 } ) `  n
)  =  0 )
186183, 185eqtrd 2505 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( ( V  +  1 ) ... N ) ) )  ->  ( (
( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  0 )
187180, 186syldan 478 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( (
( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  0 )
188187adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  n )  =  0 )
189168, 169, 170, 170, 114, 171, 188ofval 6559 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n )  =  ( ( T `  n
)  +  0 ) )
190143adantr 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( (
( U " (
1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
1 ... N ) )
191 fvun2 5952 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  Fn  ( U " (
1 ... ( V  + 
1 ) ) )  /\  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  /\  (
( ( U "
( 1 ... ( V  +  1 ) ) )  i^i  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  (/)  /\  n  e.  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) ) )  -> 
( ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) `  n
)  =  ( ( ( U " (
( ( V  + 
1 )  +  1 ) ... N ) )  X.  { 0 } ) `  n
) )
192125, 127, 191mp3an12 1380 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( U "
( 1 ... ( V  +  1 ) ) )  i^i  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  (/)  /\  n  e.  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )  ->  (
( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) `  n ) )
193135, 192sylan 479 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( (
( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  ( ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) `
 n ) )
19475fvconst2 6136 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  ->  (
( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) `  n )  =  0 )
195194adantl 473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( (
( U " (
( ( V  + 
1 )  +  1 ) ... N ) )  X.  { 0 } ) `  n
)  =  0 )
196193, 195eqtrd 2505 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( (
( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  0 )
197196adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  n )  =  0 )
198168, 190, 170, 170, 114, 171, 197ofval 6559 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n )  =  ( ( T `  n
)  +  0 ) )
199189, 198eqtr4d 2508 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )  /\  n  e.  ( 1 ... N
) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n )  =  ( ( T  oF  +  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n ) )
200167, 199mpdan 681 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( ( T  oF  +  ( ( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) ) `  n )  =  ( ( T  oF  +  ( ( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) ) `  n ) )
201164, 200jaodan 802 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  ( U " (
1 ... V ) )  \/  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n )  =  ( ( T  oF  +  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n ) )
202201adantlr 729 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  V )  /\  (
n  e.  ( U
" ( 1 ... V ) )  \/  n  e.  ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )  ->  ( ( T  oF  +  ( ( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) ) `  n )  =  ( ( T  oF  +  ( ( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) ) `  n ) )
203 poimirlem2.1 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  M ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) )
204203adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  M  <  V )  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  M ,  y ,  ( y  +  1 ) )  / 
j ]_ ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) )
205 vex 3034 . . . . . . . . . . . . . . . . 17  |-  y  e. 
_V
206 ovex 6336 . . . . . . . . . . . . . . . . 17  |-  ( y  +  1 )  e. 
_V
207205, 206ifex 3940 . . . . . . . . . . . . . . . 16  |-  if ( y  <  M , 
y ,  ( y  +  1 ) )  e.  _V
208207a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  - 
1 ) )  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  e.  _V )
209 breq1 4398 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( V  - 
1 )  ->  (
y  <  M  <->  ( V  -  1 )  < 
M ) )
210209adantl 473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  =  ( V  -  1
) )  ->  (
y  <  M  <->  ( V  -  1 )  < 
M ) )
211 simpr 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  =  ( V  -  1
) )  ->  y  =  ( V  - 
1 ) )
212 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( V  - 
1 )  ->  (
y  +  1 )  =  ( ( V  -  1 )  +  1 ) )
21327zcnd 11064 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  V  e.  CC )
214 npcan1 10065 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( V  e.  CC  ->  (
( V  -  1 )  +  1 )  =  V )
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( V  - 
1 )  +  1 )  =  V )
216212, 215sylan9eqr 2527 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  =  ( V  -  1
) )  ->  (
y  +  1 )  =  V )
217210, 211, 216ifbieq12d 3899 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  =  ( V  -  1
) )  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  =  if ( ( V  -  1 )  <  M , 
( V  -  1 ) ,  V ) )
218217adantlr 729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  - 
1 ) )  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  =  if ( ( V  -  1 )  <  M , 
( V  -  1 ) ,  V ) )
219 poimirlem2.5 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  M  e.  ( ( 0 ... N ) 
\  { V }
) )
220219eldifad 3402 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  M  e.  ( 0 ... N ) )
221 elfzelz 11826 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  ( 0 ... N )  ->  M  e.  ZZ )
222220, 221syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  ZZ )
223 zltlem1 11013 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( M  e.  ZZ  /\  V  e.  ZZ )  ->  ( M  <  V  <->  M  <_  ( V  - 
1 ) ) )
224222, 27, 223syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( M  <  V  <->  M  <_  ( V  - 
1 ) ) )
225222zred 11063 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  RR )
226 peano2zm 11004 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( V  e.  ZZ  ->  ( V  -  1 )  e.  ZZ )
22727, 226syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( V  -  1 )  e.  ZZ )
228227zred 11063 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( V  -  1 )  e.  RR )
229225, 228lenltd 9798 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( M  <_  ( V  -  1 )  <->  -.  ( V  -  1 )  <  M ) )
230224, 229bitrd 261 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( M  <  V  <->  -.  ( V  -  1 )  <  M ) )
231230biimpa 492 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  M  <  V )  ->  -.  ( V  -  1 )  <  M )
232231iffalsed 3883 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  M  <  V )  ->  if (
( V  -  1 )  <  M , 
( V  -  1 ) ,  V )  =  V )
233232adantr 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  - 
1 ) )  ->  if ( ( V  - 
1 )  <  M ,  ( V  - 
1 ) ,  V
)  =  V )
234218, 233eqtrd 2505 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  - 
1 ) )  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  =  V )
235234eqeq2d 2481 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  - 
1 ) )  -> 
( j  =  if ( y  <  M ,  y ,  ( y  +  1 ) )  <->  j  =  V ) )
236235biimpa 492 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  -  1 ) )  /\  j  =  if ( y  <  M ,  y ,  ( y  +  1 ) ) )  ->  j  =  V )
237 oveq2 6316 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  V  ->  (
1 ... j )  =  ( 1 ... V
) )
238237imaeq2d 5174 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  V  ->  ( U " ( 1 ... j ) )  =  ( U " (
1 ... V ) ) )
239238xpeq1d 4862 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  V  ->  (
( U " (
1 ... j ) )  X.  { 1 } )  =  ( ( U " ( 1 ... V ) )  X.  { 1 } ) )
240 oveq1 6315 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  V  ->  (
j  +  1 )  =  ( V  + 
1 ) )
241240oveq1d 6323 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  V  ->  (
( j  +  1 ) ... N )  =  ( ( V  +  1 ) ... N ) )
242241imaeq2d 5174 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  V  ->  ( U " ( ( j  +  1 ) ... N ) )  =  ( U " (
( V  +  1 ) ... N ) ) )
243242xpeq1d 4862 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  V  ->  (
( U " (
( j  +  1 ) ... N ) )  X.  { 0 } )  =  ( ( U " (
( V  +  1 ) ... N ) )  X.  { 0 } ) )
244239, 243uneq12d 3580 . . . . . . . . . . . . . . . . 17  |-  ( j  =  V  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )  =  ( ( ( U " ( 1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) )
245244oveq2d 6324 . . . . . . . . . . . . . . . 16  |-  ( j  =  V  ->  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  ( T  oF  +  ( ( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) ) )
246236, 245syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  -  1 ) )  /\  j  =  if ( y  <  M ,  y ,  ( y  +  1 ) ) )  ->  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  ( T  oF  +  ( ( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) ) )
247208, 246csbied 3376 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  - 
1 ) )  ->  [_ if ( y  < 
M ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  =  ( T  oF  +  ( ( ( U " ( 1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
248 elfzm1b 11898 . . . . . . . . . . . . . . . . 17  |-  ( ( V  e.  ZZ  /\  N  e.  ZZ )  ->  ( V  e.  ( 1 ... N )  <-> 
( V  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) ) )
24927, 90, 248syl2anc 673 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( V  e.  ( 1 ... N )  <-> 
( V  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) ) )
250100, 249mpbid 215 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( V  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) )
251250adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  M  <  V )  ->  ( V  -  1 )  e.  ( 0 ... ( N  -  1 ) ) )
252 ovex 6336 . . . . . . . . . . . . . . 15  |-  ( T  oF  +  ( ( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V
253252a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  M  <  V )  ->  ( T  oF  +  (
( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V )
254204, 247, 251, 253fvmptd 5969 . . . . . . . . . . . . 13  |-  ( (
ph  /\  M  <  V )  ->  ( F `  ( V  -  1 ) )  =  ( T  oF  +  ( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
255254fveq1d 5881 . . . . . . . . . . . 12  |-  ( (
ph  /\  M  <  V )  ->  ( ( F `  ( V  -  1 ) ) `
 n )  =  ( ( T  oF  +  ( (
( U " (
1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n ) )
256255adantr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  V )  /\  (
n  e.  ( U
" ( 1 ... V ) )  \/  n  e.  ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )  ->  ( ( F `  ( V  -  1 ) ) `
 n )  =  ( ( T  oF  +  ( (
( U " (
1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n ) )
257207a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  V )  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  e.  _V )
258 breq1 4398 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  V  ->  (
y  <  M  <->  V  <  M ) )
259 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  V  ->  y  =  V )
260 oveq1 6315 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  V  ->  (
y  +  1 )  =  ( V  + 
1 ) )
261258, 259, 260ifbieq12d 3899 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  V  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  =  if ( V  <  M ,  V ,  ( V  +  1 ) ) )
262 ltnsym 9750 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  e.  RR  /\  V  e.  RR )  ->  ( M  <  V  ->  -.  V  <  M
) )
263225, 28, 262syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( M  <  V  ->  -.  V  <  M
) )
264263imp 436 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  M  <  V )  ->  -.  V  <  M )
265264iffalsed 3883 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  M  <  V )  ->  if ( V  <  M ,  V ,  ( V  + 
1 ) )  =  ( V  +  1 ) )
266261, 265sylan9eqr 2527 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  V )  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  =  ( V  +  1 ) )
267266eqeq2d 2481 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  V )  ->  (
j  =  if ( y  <  M , 
y ,  ( y  +  1 ) )  <-> 
j  =  ( V  +  1 ) ) )
268267biimpa 492 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  M  <  V )  /\  y  =  V )  /\  j  =  if ( y  <  M ,  y ,  ( y  +  1 ) ) )  ->  j  =  ( V  + 
1 ) )
269 oveq2 6316 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( V  + 
1 )  ->  (
1 ... j )  =  ( 1 ... ( V  +  1 ) ) )
270269imaeq2d 5174 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  ( V  + 
1 )  ->  ( U " ( 1 ... j ) )  =  ( U " (
1 ... ( V  + 
1 ) ) ) )
271270xpeq1d 4862 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  ( V  + 
1 )  ->  (
( U " (
1 ... j ) )  X.  { 1 } )  =  ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } ) )
272 oveq1 6315 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  ( V  + 
1 )  ->  (
j  +  1 )  =  ( ( V  +  1 )  +  1 ) )
273272oveq1d 6323 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( V  + 
1 )  ->  (
( j  +  1 ) ... N )  =  ( ( ( V  +  1 )  +  1 ) ... N ) )
274273imaeq2d 5174 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  ( V  + 
1 )  ->  ( U " ( ( j  +  1 ) ... N ) )  =  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )
275274xpeq1d 4862 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  ( V  + 
1 )  ->  (
( U " (
( j  +  1 ) ... N ) )  X.  { 0 } )  =  ( ( U " (
( ( V  + 
1 )  +  1 ) ... N ) )  X.  { 0 } ) )
276271, 275uneq12d 3580 . . . . . . . . . . . . . . . . 17  |-  ( j  =  ( V  + 
1 )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )  =  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) )
277276oveq2d 6324 . . . . . . . . . . . . . . . 16  |-  ( j  =  ( V  + 
1 )  ->  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  ( T  oF  +  ( ( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) ) )
278268, 277syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  M  <  V )  /\  y  =  V )  /\  j  =  if ( y  <  M ,  y ,  ( y  +  1 ) ) )  ->  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  ( T  oF  +  ( ( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) ) )
279257, 278csbied 3376 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  V )  ->  [_ if ( y  <  M ,  y ,  ( y  +  1 ) )  /  j ]_ ( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  =  ( T  oF  +  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
280 1eluzge0 11226 . . . . . . . . . . . . . . . . 17  |-  1  e.  ( ZZ>= `  0 )
281 fzss1 11863 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... ( N  - 
1 ) )  C_  ( 0 ... ( N  -  1 ) ) )
282280, 281ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( 1 ... ( N  - 
1 ) )  C_  ( 0 ... ( N  -  1 ) )
283282, 7sseldi 3416 . . . . . . . . . . . . . . 15  |-  ( ph  ->  V  e.  ( 0 ... ( N  - 
1 ) ) )
284283adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  M  <  V )  ->  V  e.  ( 0 ... ( N  -  1 ) ) )
285 ovex 6336 . . . . . . . . . . . . . . 15  |-  ( T  oF  +  ( ( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V
286285a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  M  <  V )  ->  ( T  oF  +  (
( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V )
287204, 279, 284, 286fvmptd 5969 . . . . . . . . . . . . 13  |-  ( (
ph  /\  M  <  V )  ->  ( F `  V )  =  ( T  oF  +  ( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
288287fveq1d 5881 . . . . . . . . . . . 12  |-  ( (
ph  /\  M  <  V )  ->  ( ( F `  V ) `  n )  =  ( ( T  oF  +  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n ) )
289288adantr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  M  <  V )  /\  (
n  e.  ( U
" ( 1 ... V ) )  \/  n  e.  ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )  ->  ( ( F `  V ) `  n )  =  ( ( T  oF  +  ( ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } )  u.  ( ( U " ( ( ( V  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n ) )
290202, 256, 2893eqtr4d 2515 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  V )  /\  (
n  e.  ( U
" ( 1 ... V ) )  \/  n  e.  ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )  ->  ( ( F `  ( V  -  1 ) ) `
 n )  =  ( ( F `  V ) `  n
) )
291290ex 441 . . . . . . . . 9  |-  ( (
ph  /\  M  <  V )  ->  ( (
n  e.  ( U
" ( 1 ... V ) )  \/  n  e.  ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( ( F `
 ( V  - 
1 ) ) `  n )  =  ( ( F `  V
) `  n )
) )
29260, 291sylbid 223 . . . . . . . 8  |-  ( (
ph  /\  M  <  V )  ->  ( (
n  e.  ( U
" ( 1 ... N ) )  /\  -.  n  e.  ( U " { ( V  +  1 ) } ) )  ->  (
( F `  ( V  -  1 ) ) `  n )  =  ( ( F `
 V ) `  n ) ) )
293292expdimp 444 . . . . . . 7  |-  ( ( ( ph  /\  M  <  V )  /\  n  e.  ( U " (
1 ... N ) ) )  ->  ( -.  n  e.  ( U " { ( V  + 
1 ) } )  ->  ( ( F `
 ( V  - 
1 ) ) `  n )  =  ( ( F `  V
) `  n )
) )
294293necon1ad 2660 . . . . . 6  |-  ( ( ( ph  /\  M  <  V )  /\  n  e.  ( U " (
1 ... N ) ) )  ->  ( (
( F `  ( V  -  1 ) ) `  n )  =/=  ( ( F `
 V ) `  n )  ->  n  e.  ( U " {
( V  +  1 ) } ) ) )
295 elimasni 5201 . . . . . . . 8  |-  ( n  e.  ( U " { ( V  + 
1 ) } )  ->  ( V  + 
1 ) U n )
296 eqcom 2478 . . . . . . . . 9  |-  ( n  =  ( U `  ( V  +  1
) )  <->  ( U `  ( V  +  1 ) )  =  n )
297 f1ofn 5829 . . . . . . . . . . 11  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U  Fn  ( 1 ... N
) )
2981, 297syl 17 . . . . . . . . . 10  |-  ( ph  ->  U  Fn  ( 1 ... N ) )
299 fnbrfvb 5919 . . . . . . . . . 10  |-  ( ( U  Fn  ( 1 ... N )  /\  ( V  +  1
)  e.  ( 1 ... N ) )  ->  ( ( U `
 ( V  + 
1 ) )  =  n  <->  ( V  + 
1 ) U n ) )
300298, 15, 299syl2anc 673 . . . . . . . . 9  |-  ( ph  ->  ( ( U `  ( V  +  1
) )  =  n  <-> 
( V  +  1 ) U n ) )
301296, 300syl5bb 265 . . . . . . . 8  |-  ( ph  ->  ( n  =  ( U `  ( V  +  1 ) )  <-> 
( V  +  1 ) U n ) )
302295, 301syl5ibr 229 . . . . . . 7  |-  ( ph  ->  ( n  e.  ( U " { ( V  +  1 ) } )  ->  n  =  ( U `  ( V  +  1
) ) ) )
303302ad2antrr 740 . . . . . 6  |-  ( ( ( ph  /\  M  <  V )  /\  n  e.  ( U " (
1 ... N ) ) )  ->  ( n  e.  ( U " {
( V  +  1 ) } )  ->  n  =  ( U `  ( V  +  1 ) ) ) )
304294, 303syld 44 . . . . 5  |-  ( ( ( ph  /\  M  <  V )  /\  n  e.  ( U " (
1 ... N ) ) )  ->  ( (
( F `  ( V  -  1 ) ) `  n )  =/=  ( ( F `
 V ) `  n )  ->  n  =  ( U `  ( V  +  1
) ) ) )
305304ralrimiva 2809 . . . 4  |-  ( (
ph  /\  M  <  V )  ->  A. n  e.  ( U " (
1 ... N ) ) ( ( ( F `
 ( V  - 
1 ) ) `  n )  =/=  (
( F `  V
) `  n )  ->  n  =  ( U `
 ( V  + 
1 ) ) ) )
306 fvex 5889 . . . . 5  |-  ( U `
 ( V  + 
1 ) )  e. 
_V
307 eqeq2 2482 . . . . . . 7  |-  ( m  =  ( U `  ( V  +  1
) )  ->  (
n  =  m  <->  n  =  ( U `  ( V  +  1 ) ) ) )
308307imbi2d 323 . . . . . 6  |-  ( m  =  ( U `  ( V  +  1
) )  ->  (
( ( ( F `
 ( V  - 
1 ) ) `  n )  =/=  (
( F `  V
) `  n )  ->  n  =  m )  <-> 
( ( ( F `
 ( V  - 
1 ) ) `  n )  =/=  (
( F `  V
) `  n )  ->  n  =  ( U `
 ( V  + 
1 ) ) ) ) )
309308ralbidv 2829 . . . . 5  |-  ( m  =  ( U `  ( V  +  1
) )  ->  ( A. n  e.  ( U " ( 1 ... N ) ) ( ( ( F `  ( V  -  1
) ) `  n
)  =/=  ( ( F `  V ) `
 n )  ->  n  =  m )  <->  A. n  e.  ( U
" ( 1 ... N ) ) ( ( ( F `  ( V  -  1
) ) `  n
)  =/=  ( ( F `  V ) `
 n )  ->  n  =  ( U `  ( V  +  1 ) ) ) ) )
310306, 309spcev 3127 . . . 4  |-  ( A. n  e.  ( U " ( 1 ... N
) ) ( ( ( F `  ( V  -  1 ) ) `  n )  =/=  ( ( F `
 V ) `  n )  ->  n  =  ( U `  ( V  +  1
) ) )  ->  E. m A. n  e.  ( U " (
1 ... N ) ) ( ( ( F `
 ( V  - 
1 ) ) `  n )  =/=  (
( F `  V
) `  n )  ->  n  =  m ) )
311305, 310syl 17 . . 3  |-  ( (
ph  /\  M  <  V )  ->  E. m A. n  e.  ( U " ( 1 ... N ) ) ( ( ( F `  ( V  -  1
) ) `  n
)  =/=  ( ( F `  V ) `
 n )  ->  n  =  m )
)
312 imadif 5668 . . . . . . . . . . . . . . 15  |-  ( Fun  `' U  ->  ( U
" ( ( 1 ... N )  \  { V } ) )  =  ( ( U
" ( 1 ... N ) )  \ 
( U " { V } ) ) )
3134, 312syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( U " (
( 1 ... N
)  \  { V } ) )  =  ( ( U "
( 1 ... N
) )  \  ( U " { V }
) ) )
314102difeq1d 3539 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1 ... N )  \  { V } )  =  ( ( ( 1 ... V )  u.  (
( V  +  1 ) ... N ) )  \  { V } ) )
315 difundir 3687 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1 ... V
)  u.  ( ( V  +  1 ) ... N ) ) 
\  { V }
)  =  ( ( ( 1 ... V
)  \  { V } )  u.  (
( ( V  + 
1 ) ... N
)  \  { V } ) )
316215, 21eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( V  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 ) )
317 uzid 11197 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( V  -  1 )  e.  ZZ  ->  ( V  -  1 )  e.  ( ZZ>= `  ( V  -  1 ) ) )
318227, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( V  -  1 )  e.  ( ZZ>= `  ( V  -  1
) ) )
319 peano2uz 11235 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( V  -  1 )  e.  ( ZZ>= `  ( V  -  1 ) )  ->  ( ( V  -  1 )  +  1 )  e.  ( ZZ>= `  ( V  -  1 ) ) )
320318, 319syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( V  - 
1 )  +  1 )  e.  ( ZZ>= `  ( V  -  1
) ) )
321215, 320eqeltrrd 2550 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  V  e.  ( ZZ>= `  ( V  -  1
) ) )
322 fzsplit2 11850 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( V  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 )  /\  V  e.  ( ZZ>= `  ( V  -  1 ) ) )  ->  ( 1 ... V )  =  ( ( 1 ... ( V  -  1 ) )  u.  (
( ( V  - 
1 )  +  1 ) ... V ) ) )
323316, 321, 322syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 1 ... V
)  =  ( ( 1 ... ( V  -  1 ) )  u.  ( ( ( V  -  1 )  +  1 ) ... V ) ) )
324215oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( V  -  1 )  +  1 ) ... V
)  =  ( V ... V ) )
325 fzsn 11866 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( V  e.  ZZ  ->  ( V ... V )  =  { V } )
32627, 325syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( V ... V
)  =  { V } )
327324, 326eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( V  -  1 )  +  1 ) ... V
)  =  { V } )
328327uneq2d 3579 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( 1 ... ( V  -  1 ) )  u.  (
( ( V  - 
1 )  +  1 ) ... V ) )  =  ( ( 1 ... ( V  -  1 ) )  u.  { V }
) )
329323, 328eqtrd 2505 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1 ... V
)  =  ( ( 1 ... ( V  -  1 ) )  u.  { V }
) )
330329difeq1d 3539 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1 ... V )  \  { V } )  =  ( ( ( 1 ... ( V  -  1 ) )  u.  { V } )  \  { V } ) )
331 difun2 3838 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1 ... ( V  -  1 ) )  u.  { V } )  \  { V } )  =  ( ( 1 ... ( V  -  1 ) )  \  { V } )
33228ltm1d 10561 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( V  -  1 )  <  V )
333228, 28ltnled 9799 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( V  - 
1 )  <  V  <->  -.  V  <_  ( V  -  1 ) ) )
334332, 333mpbid 215 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  V  <_  ( V  -  1 ) )
335 elfzle2 11829 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( V  e.  ( 1 ... ( V  -  1 ) )  ->  V  <_  ( V  -  1 ) )
336334, 335nsyl 125 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  V  e.  ( 1 ... ( V  -  1 ) ) )
337 difsn 4097 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  V  e.  ( 1 ... ( V  - 
1 ) )  -> 
( ( 1 ... ( V  -  1 ) )  \  { V } )  =  ( 1 ... ( V  -  1 ) ) )
338336, 337syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( 1 ... ( V  -  1 ) )  \  { V } )  =  ( 1 ... ( V  -  1 ) ) )
339331, 338syl5eq 2517 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( 1 ... ( V  - 
1 ) )  u. 
{ V } ) 
\  { V }
)  =  ( 1 ... ( V  - 
1 ) ) )
340330, 339eqtrd 2505 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1 ... V )  \  { V } )  =  ( 1 ... ( V  -  1 ) ) )
341 elfzle1 11828 . . . . . . . . . . . . . . . . . . . 20  |-  ( V  e.  ( ( V  +  1 ) ... N )  ->  ( V  +  1 )  <_  V )
34233, 341nsyl 125 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  V  e.  ( ( V  +  1 ) ... N ) )
343 difsn 4097 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  V  e.  ( ( V  +  1 ) ... N )  -> 
( ( ( V  +  1 ) ... N )  \  { V } )  =  ( ( V  +  1 ) ... N ) )
344342, 343syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( V  +  1 ) ... N )  \  { V } )  =  ( ( V  +  1 ) ... N ) )
345340, 344uneq12d 3580 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( 1 ... V )  \  { V } )  u.  ( ( ( V  +  1 ) ... N )  \  { V } ) )  =  ( ( 1 ... ( V  -  1 ) )  u.  (
( V  +  1 ) ... N ) ) )
346315, 345syl5eq 2517 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 1 ... V )  u.  ( ( V  + 
1 ) ... N
) )  \  { V } )  =  ( ( 1 ... ( V  -  1 ) )  u.  ( ( V  +  1 ) ... N ) ) )
347314, 346eqtrd 2505 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1 ... N )  \  { V } )  =  ( ( 1 ... ( V  -  1 ) )  u.  ( ( V  +  1 ) ... N ) ) )
348347imaeq2d 5174 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( U " (
( 1 ... N
)  \  { V } ) )  =  ( U " (
( 1 ... ( V  -  1 ) )  u.  ( ( V  +  1 ) ... N ) ) ) )
349313, 348eqtr3d 2507 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  \  ( U " { V }
) )  =  ( U " ( ( 1 ... ( V  -  1 ) )  u.  ( ( V  +  1 ) ... N ) ) ) )
350 imaundi 5254 . . . . . . . . . . . . 13  |-  ( U
" ( ( 1 ... ( V  - 
1 ) )  u.  ( ( V  + 
1 ) ... N
) ) )  =  ( ( U "
( 1 ... ( V  -  1 ) ) )  u.  ( U " ( ( V  +  1 ) ... N ) ) )
351349, 350syl6eq 2521 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  \  ( U " { V }
) )  =  ( ( U " (
1 ... ( V  - 
1 ) ) )  u.  ( U "
( ( V  + 
1 ) ... N
) ) ) )
352351eleq2d 2534 . . . . . . . . . . 11  |-  ( ph  ->  ( n  e.  ( ( U " (
1 ... N ) ) 
\  ( U " { V } ) )  <-> 
n  e.  ( ( U