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

Theorem poimirlem2 31906
Description: Lemma for poimir 31937- 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 5837 . . . . . . . . . . . . . . . . 17  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( U :
( 1 ... N
) -onto-> ( 1 ... N )  /\  Fun  `' U ) )
32simprbi 465 . . . . . . . . . . . . . . . 16  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  Fun  `' U
)
41, 3syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Fun  `' U )
5 imadif 5676 . . . . . . . . . . . . . . 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 11856 . . . . . . . . . . . . . . . . . . . 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 10632 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  N  e.  CC )
12 npcan1 10051 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
1413oveq2d 6321 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 1 ... (
( N  -  1 )  +  1 ) )  =  ( 1 ... N ) )
159, 14eleqtrd 2509 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( V  +  1 )  e.  ( 1 ... N ) )
16 fzsplit 11832 . . . . . . . . . . . . . . . . . 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 3582 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1 ... N )  \  {
( V  +  1 ) } )  =  ( ( ( 1 ... ( V  + 
1 ) )  u.  ( ( ( V  +  1 )  +  1 ) ... N
) )  \  {
( V  +  1 ) } ) )
19 difundir 3726 . . . . . . . . . . . . . . . . 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 11803 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( V  e.  ( 1 ... ( N  -  1 ) )  ->  V  e.  ( ZZ>= `  1 )
)
217, 20syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  V  e.  ( ZZ>= ` 
1 ) )
22 fzsuc 11850 . . . . . . . . . . . . . . . . . . . . 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 3582 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1 ... ( V  +  1 ) )  \  {
( V  +  1 ) } )  =  ( ( ( 1 ... V )  u. 
{ ( V  + 
1 ) } ) 
\  { ( V  +  1 ) } ) )
25 difun2 3877 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1 ... V
)  u.  { ( V  +  1 ) } )  \  {
( V  +  1 ) } )  =  ( ( 1 ... V )  \  {
( V  +  1 ) } )
26 elfzelz 11807 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( V  e.  ( 1 ... ( N  -  1 ) )  ->  V  e.  ZZ )
277, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  V  e.  ZZ )
2827zred 11047 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  V  e.  RR )
2928ltp1d 10544 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  V  <  ( V  +  1 ) )
3027peano2zd 11050 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( V  +  1 )  e.  ZZ )
3130zred 11047 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( V  +  1 )  e.  RR )
3228, 31ltnled 9789 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( V  <  ( V  +  1 )  <->  -.  ( V  +  1 )  <_  V )
)
3329, 32mpbid 213 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  ( V  + 
1 )  <_  V
)
34 elfzle2 11810 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( V  +  1 )  e.  ( 1 ... V )  ->  ( V  +  1 )  <_  V )
3533, 34nsyl 124 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  ( V  + 
1 )  e.  ( 1 ... V ) )
36 difsn 4134 . . . . . . . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( 1 ... V )  u. 
{ ( V  + 
1 ) } ) 
\  { ( V  +  1 ) } )  =  ( 1 ... V ) )
3924, 38eqtrd 2463 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1 ... ( V  +  1 ) )  \  {
( V  +  1 ) } )  =  ( 1 ... V
) )
4031ltp1d 10544 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( V  +  1 )  <  ( ( V  +  1 )  +  1 ) )
41 peano2re 9813 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( V  +  1 )  e.  RR  ->  (
( V  +  1 )  +  1 )  e.  RR )
4231, 41syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( V  + 
1 )  +  1 )  e.  RR )
4331, 42ltnled 9789 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( V  + 
1 )  <  (
( V  +  1 )  +  1 )  <->  -.  ( ( V  + 
1 )  +  1 )  <_  ( V  +  1 ) ) )
4440, 43mpbid 213 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  ( ( V  +  1 )  +  1 )  <_  ( V  +  1 ) )
45 elfzle1 11809 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( V  +  1 )  e.  ( ( ( V  +  1 )  +  1 ) ... N )  ->  (
( V  +  1 )  +  1 )  <_  ( V  + 
1 ) )
4644, 45nsyl 124 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  ( V  + 
1 )  e.  ( ( ( V  + 
1 )  +  1 ) ... N ) )
47 difsn 4134 . . . . . . . . . . . . . . . . . . 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 3621 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( 1 ... ( V  + 
1 ) )  \  { ( V  + 
1 ) } )  u.  ( ( ( ( V  +  1 )  +  1 ) ... N )  \  { ( V  + 
1 ) } ) )  =  ( ( 1 ... V )  u.  ( ( ( V  +  1 )  +  1 ) ... N ) ) )
5019, 49syl5eq 2475 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 1 ... ( V  + 
1 ) )  u.  ( ( ( V  +  1 )  +  1 ) ... N
) )  \  {
( V  +  1 ) } )  =  ( ( 1 ... V )  u.  (
( ( V  + 
1 )  +  1 ) ... N ) ) )
5118, 50eqtrd 2463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1 ... N )  \  {
( V  +  1 ) } )  =  ( ( 1 ... V )  u.  (
( ( V  + 
1 )  +  1 ) ... N ) ) )
5251imaeq2d 5187 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( U " (
( 1 ... N
)  \  { ( V  +  1 ) } ) )  =  ( U " (
( 1 ... V
)  u.  ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )
536, 52eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  \  ( U " { ( V  +  1 ) } ) )  =  ( U " ( ( 1 ... V )  u.  ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )
54 imaundi 5267 . . . . . . . . . . . . 13  |-  ( U
" ( ( 1 ... V )  u.  ( ( ( V  +  1 )  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... V
) )  u.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )
5553, 54syl6eq 2479 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  \  ( U " { ( V  +  1 ) } ) )  =  ( ( U " (
1 ... V ) )  u.  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) ) ) )
5655eleq2d 2492 . . . . . . . . . . 11  |-  ( ph  ->  ( n  e.  ( ( U " (
1 ... N ) ) 
\  ( U " { ( V  + 
1 ) } ) )  <->  n  e.  (
( U " (
1 ... V ) )  u.  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) ) ) ) )
57 eldif 3446 . . . . . . . . . . 11  |-  ( n  e.  ( ( U
" ( 1 ... N ) )  \ 
( U " {
( V  +  1 ) } ) )  <-> 
( n  e.  ( U " ( 1 ... N ) )  /\  -.  n  e.  ( U " {
( V  +  1 ) } ) ) )
58 elun 3606 . . . . . . . . . . 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 290 . . . . . . . . . 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 466 . . . . . . . . 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 5198 . . . . . . . . . . . . . . . 16  |-  ( U
" ( 1 ... V ) )  C_  ran  U
62 f1of 5831 . . . . . . . . . . . . . . . . . 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 5752 . . . . . . . . . . . . . . . . 17  |-  ( U : ( 1 ... N ) --> ( 1 ... N )  ->  ran  U  C_  ( 1 ... N ) )
6563, 64syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  U  C_  (
1 ... N ) )
6661, 65syl5ss 3475 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( U " (
1 ... V ) ) 
C_  ( 1 ... N ) )
6766sselda 3464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  n  e.  ( 1 ... N
) )
68 poimirlem2.2 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T : ( 1 ... N ) --> ZZ )
69 ffn 5746 . . . . . . . . . . . . . . . . . 18  |-  ( T : ( 1 ... N ) --> ZZ  ->  T  Fn  ( 1 ... N ) )
7068, 69syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  Fn  ( 1 ... N ) )
7170adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  T  Fn  ( 1 ... N
) )
72 1ex 9645 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  _V
73 fnconstg 5788 . . . . . . . . . . . . . . . . . . . . 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 9644 . . . . . . . . . . . . . . . . . . . . 21  |-  0  e.  _V
76 fnconstg 5788 . . . . . . . . . . . . . . . . . . . . 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 456 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( U " (
1 ... V ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... V ) )  /\  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } )  Fn  ( U " (
( V  +  1 ) ... N ) ) )
79 imain 5677 . . . . . . . . . . . . . . . . . . . . 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 11833 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( V  <  ( V  + 
1 )  ->  (
( 1 ... V
)  i^i  ( ( V  +  1 ) ... N ) )  =  (/) )
8229, 81syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1 ... V )  i^i  (
( V  +  1 ) ... N ) )  =  (/) )
8382imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
( 1 ... V
)  i^i  ( ( V  +  1 ) ... N ) ) )  =  ( U
" (/) ) )
84 ima0 5202 . . . . . . . . . . . . . . . . . . . . 21  |-  ( U
" (/) )  =  (/)
8583, 84syl6eq 2479 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... V
)  i^i  ( ( V  +  1 ) ... N ) ) )  =  (/) )
8680, 85eqtr3d 2465 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( U "
( 1 ... V
) )  i^i  ( U " ( ( V  +  1 ) ... N ) ) )  =  (/) )
87 fnun 5700 . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . 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 5267 . . . . . . . . . . . . . . . . . . . 20  |-  ( U
" ( ( 1 ... V )  u.  ( ( V  + 
1 ) ... N
) ) )  =  ( ( U "
( 1 ... V
) )  u.  ( U " ( ( V  +  1 ) ... N ) ) )
9010nnzd 11046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  N  e.  ZZ )
91 peano2zm 10987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
93 uzid 11180 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
9492, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1
) ) )
95 peano2uz 11219 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2508 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
98 fzss2 11845 . . . . . . . . . . . . . . . . . . . . . . . . 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 3465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  V  e.  ( 1 ... N ) )
101 fzsplit 11832 . . . . . . . . . . . . . . . . . . . . . . 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 5187 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
1 ... N ) )  =  ( U "
( ( 1 ... V )  u.  (
( V  +  1 ) ... N ) ) ) )
104 f1ofo 5838 . . . . . . . . . . . . . . . . . . . . . . 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 5815 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U : ( 1 ... N ) -onto-> ( 1 ... N )  -> 
( U " (
1 ... N ) )  =  ( 1 ... N ) )
107105, 106syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
1 ... N ) )  =  ( 1 ... N ) )
108103, 107eqtr3d 2465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... V
)  u.  ( ( V  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
10989, 108syl5eqr 2477 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( U "
( 1 ... V
) )  u.  ( U " ( ( V  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
110109fneq2d 5685 . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( 1 ... N ) )
112111adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( (
( U " (
1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  (
1 ... N ) )
113 fzfid 12192 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( 1 ... N )  e. 
Fin )
114 inidm 3671 . . . . . . . . . . . . . . . 16  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
115 eqidd 2423 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( U " (
1 ... V ) ) )  /\  n  e.  ( 1 ... N
) )  ->  ( T `  n )  =  ( T `  n ) )
116 fvun1 5952 . . . . . . . . . . . . . . . . . . . 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 1350 . . . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . . . 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 6135 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( U "
( 1 ... V
) )  ->  (
( ( U "
( 1 ... V
) )  X.  {
1 } ) `  n )  =  1 )
120119adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( (
( U " (
1 ... V ) )  X.  { 1 } ) `  n )  =  1 )
121118, 120eqtrd 2463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( (
( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  1 )
122121adantr 466 . . . . . . . . . . . . . . . 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 6554 . . . . . . . . . . . . . . 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 5788 . . . . . . . . . . . . . . . . . . . . 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 5788 . . . . . . . . . . . . . . . . . . . . 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 456 . . . . . . . . . . . . . . . . . . 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 5677 . . . . . . . . . . . . . . . . . . . . 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 11833 . . . . . . . . . . . . . . . . . . . . . . 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 5187 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
( 1 ... ( V  +  1 ) )  i^i  ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  ( U
" (/) ) )
134133, 84syl6eq 2479 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... ( V  +  1 ) )  i^i  ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  (/) )
135130, 134eqtr3d 2465 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( U "
( 1 ... ( V  +  1 ) ) )  i^i  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  (/) )
136 fnun 5700 . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . 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 5267 . . . . . . . . . . . . . . . . . . . 20  |-  ( U
" ( ( 1 ... ( V  + 
1 ) )  u.  ( ( ( V  +  1 )  +  1 ) ... N
) ) )  =  ( ( U "
( 1 ... ( V  +  1 ) ) )  u.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )
13917imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( U " (
1 ... N ) )  =  ( U "
( ( 1 ... ( V  +  1 ) )  u.  (
( ( V  + 
1 )  +  1 ) ... N ) ) ) )
140139, 107eqtr3d 2465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( U " (
( 1 ... ( V  +  1 ) )  u.  ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
141138, 140syl5eqr 2477 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( U "
( 1 ... ( V  +  1 ) ) )  u.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
142141fneq2d 5685 . . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( 1 ... N ) )
144143adantr 466 . . . . . . . . . . . . . . . 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 11180 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( V  e.  ZZ  ->  V  e.  ( ZZ>= `  V )
)
14627, 145syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  V  e.  ( ZZ>= `  V ) )
147 peano2uz 11219 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( V  e.  ( ZZ>= `  V
)  ->  ( V  +  1 )  e.  ( ZZ>= `  V )
)
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( V  +  1 )  e.  ( ZZ>= `  V ) )
149 fzss2 11845 . . . . . . . . . . . . . . . . . . . . 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 5223 . . . . . . . . . . . . . . . . . . . 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 3464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  n  e.  ( U " ( 1 ... ( V  + 
1 ) ) ) )
154 fvun1 5952 . . . . . . . . . . . . . . . . . . . . 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 1350 . . . . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . . . . 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 6135 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( U "
( 1 ... ( V  +  1 ) ) )  ->  (
( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } ) `  n )  =  1 )
158157adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... ( V  + 
1 ) ) ) )  ->  ( (
( U " (
1 ... ( V  + 
1 ) ) )  X.  { 1 } ) `  n )  =  1 )
159156, 158eqtrd 2463 . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( U " ( 1 ... V ) ) )  ->  ( (
( ( U "
( 1 ... ( V  +  1 ) ) )  X.  {
1 } )  u.  ( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  1 )
161160adantr 466 . . . . . . . . . . . . . . . 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 6554 . . . . . . . . . . . . . . 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 2466 . . . . . . . . . . . . . 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 672 . . . . . . . . . . . . 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 5198 . . . . . . . . . . . . . . . 16  |-  ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  C_  ran  U
166165, 65syl5ss 3475 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) )  C_  ( 1 ... N ) )
167166sselda 3464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  n  e.  ( 1 ... N
) )
16870adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  T  Fn  ( 1 ... N
) )
169111adantr 466 . . . . . . . . . . . . . . . 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 12192 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( 1 ... N )  e. 
Fin )
171 eqidd 2423 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )  /\  n  e.  ( 1 ... N
) )  ->  ( T `  n )  =  ( T `  n ) )
172 uzid 11180 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( V  +  1 )  e.  ZZ  ->  ( V  +  1 )  e.  ( ZZ>= `  ( V  +  1 ) ) )
17330, 172syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( V  +  1 )  e.  ( ZZ>= `  ( V  +  1
) ) )
174 peano2uz 11219 . . . . . . . . . . . . . . . . . . . . . 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 11844 . . . . . . . . . . . . . . . . . . . . 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 5223 . . . . . . . . . . . . . . . . . . . 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 3464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  n  e.  ( U " ( ( V  +  1 ) ... N ) ) )
181 fvun2 5953 . . . . . . . . . . . . . . . . . . . . 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 1350 . . . . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . . . . 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 6135 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( U "
( ( V  + 
1 ) ... N
) )  ->  (
( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) `  n )  =  0 )
185184adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  ( U " ( ( V  +  1 ) ... N ) ) )  ->  ( (
( U " (
( V  +  1 ) ... N ) )  X.  { 0 } ) `  n
)  =  0 )
186183, 185eqtrd 2463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( ( V  +  1 ) ... N ) ) )  ->  ( (
( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  0 )
187180, 186syldan 472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( (
( ( U "
( 1 ... V
) )  X.  {
1 } )  u.  ( ( U "
( ( V  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 n )  =  0 )
188187adantr 466 . . . . . . . . . . . . . . . 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 6554 . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . 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 5953 . . . . . . . . . . . . . . . . . . . 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 1350 . . . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . . . 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 6135 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  ->  (
( ( U "
( ( ( V  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) `  n )  =  0 )
195194adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  ( U " ( ( ( V  +  1 )  +  1 ) ... N ) ) )  ->  ( (
( U " (
( ( V  + 
1 )  +  1 ) ... N ) )  X.  { 0 } ) `  n
)  =  0 )
196193, 195eqtrd 2463 . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . 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 6554 . . . . . . . . . . . . . . 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 2466 . . . . . . . . . . . . . 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 672 . . . . . . . . . . . . 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 792 . . . . . . . . . . . 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 719 . . . . . . . . . . 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 466 . . . . . . . . . . . . . 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 3083 . . . . . . . . . . . . . . . . 17  |-  y  e. 
_V
206 ovex 6333 . . . . . . . . . . . . . . . . 17  |-  ( y  +  1 )  e. 
_V
207205, 206ifex 3979 . . . . . . . . . . . . . . . 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 4426 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( V  - 
1 )  ->  (
y  <  M  <->  ( V  -  1 )  < 
M ) )
210209adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  =  ( V  -  1
) )  ->  (
y  <  M  <->  ( V  -  1 )  < 
M ) )
211 simpr 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  =  ( V  -  1
) )  ->  y  =  ( V  - 
1 ) )
212 oveq1 6312 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( V  - 
1 )  ->  (
y  +  1 )  =  ( ( V  -  1 )  +  1 ) )
21327zcnd 11048 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  V  e.  CC )
214 npcan1 10051 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( V  e.  CC  ->  (
( V  -  1 )  +  1 )  =  V )
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( V  - 
1 )  +  1 )  =  V )
216212, 215sylan9eqr 2485 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  =  ( V  -  1
) )  ->  (
y  +  1 )  =  V )
217210, 211, 216ifbieq12d 3938 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  =  ( V  -  1
) )  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  =  if ( ( V  -  1 )  <  M , 
( V  -  1 ) ,  V ) )
218217adantlr 719 . . . . . . . . . . . . . . . . . . 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 3448 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  M  e.  ( 0 ... N ) )
221 elfzelz 11807 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  ( 0 ... N )  ->  M  e.  ZZ )
222220, 221syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  ZZ )
223 zltlem1 10996 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( M  e.  ZZ  /\  V  e.  ZZ )  ->  ( M  <  V  <->  M  <_  ( V  - 
1 ) ) )
224222, 27, 223syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( M  <  V  <->  M  <_  ( V  - 
1 ) ) )
225222zred 11047 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  e.  RR )
226 peano2zm 10987 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( V  e.  ZZ  ->  ( V  -  1 )  e.  ZZ )
22727, 226syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( V  -  1 )  e.  ZZ )
228227zred 11047 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( V  -  1 )  e.  RR )
229225, 228lenltd 9788 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( M  <_  ( V  -  1 )  <->  -.  ( V  -  1 )  <  M ) )
230224, 229bitrd 256 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( M  <  V  <->  -.  ( V  -  1 )  <  M ) )
231230biimpa 486 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  M  <  V )  ->  -.  ( V  -  1 )  <  M )
232231iffalsed 3922 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  M  <  V )  ->  if (
( V  -  1 )  <  M , 
( V  -  1 ) ,  V )  =  V )
233232adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  - 
1 ) )  ->  if ( ( V  - 
1 )  <  M ,  ( V  - 
1 ) ,  V
)  =  V )
234218, 233eqtrd 2463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  - 
1 ) )  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  =  V )
235234eqeq2d 2436 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  - 
1 ) )  -> 
( j  =  if ( y  <  M ,  y ,  ( y  +  1 ) )  <->  j  =  V ) )
236235biimpa 486 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  M  <  V )  /\  y  =  ( V  -  1 ) )  /\  j  =  if ( y  <  M ,  y ,  ( y  +  1 ) ) )  ->  j  =  V )
237 oveq2 6313 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  V  ->  (
1 ... j )  =  ( 1 ... V
) )
238237imaeq2d 5187 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  V  ->  ( U " ( 1 ... j ) )  =  ( U " (
1 ... V ) ) )
239238xpeq1d 4876 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  V  ->  (
( U " (
1 ... j ) )  X.  { 1 } )  =  ( ( U " ( 1 ... V ) )  X.  { 1 } ) )
240 oveq1 6312 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  V  ->  (
j  +  1 )  =  ( V  + 
1 ) )
241240oveq1d 6320 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  V  ->  (
( j  +  1 ) ... N )  =  ( ( V  +  1 ) ... N ) )
242241imaeq2d 5187 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  V  ->  ( U " ( ( j  +  1 ) ... N ) )  =  ( U " (
( V  +  1 ) ... N ) ) )
243242xpeq1d 4876 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  V  ->  (
( U " (
( j  +  1 ) ... N ) )  X.  { 0 } )  =  ( ( U " (
( V  +  1 ) ... N ) )  X.  { 0 } ) )
244239, 243uneq12d 3621 . . . . . . . . . . . . . . . . 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 6321 . . . . . . . . . . . . . . . 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 3422 . . . . . . . . . . . . . 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 11879 . . . . . . . . . . . . . . . . 17  |-  ( ( V  e.  ZZ  /\  N  e.  ZZ )  ->  ( V  e.  ( 1 ... N )  <-> 
( V  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) ) )
24927, 90, 248syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( V  e.  ( 1 ... N )  <-> 
( V  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) ) )
250100, 249mpbid 213 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( V  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) )
251250adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  M  <  V )  ->  ( V  -  1 )  e.  ( 0 ... ( N  -  1 ) ) )
252 ovex 6333 . . . . . . . . . . . . . . 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 5970 . . . . . . . . . . . . 13  |-  ( (
ph  /\  M  <  V )  ->  ( F `  ( V  -  1 ) )  =  ( T  oF  +  ( ( ( U
" ( 1 ... V ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( V  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
255254fveq1d 5883 . . . . . . . . . . . 12  |-  ( (
ph  /\  M  <  V )  ->  ( ( F `  ( V  -  1 ) ) `
 n )  =  ( ( T  oF  +  ( (
( U " (
1 ... V ) )  X.  { 1 } )  u.  ( ( U " ( ( V  +  1 ) ... N ) )  X.  { 0 } ) ) ) `  n ) )
256255adantr 466 . . . . . . . . . . 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 4426 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  V  ->  (
y  <  M  <->  V  <  M ) )
259 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  V  ->  y  =  V )
260 oveq1 6312 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  V  ->  (
y  +  1 )  =  ( V  + 
1 ) )
261258, 259, 260ifbieq12d 3938 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  V  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  =  if ( V  <  M ,  V ,  ( V  +  1 ) ) )
262 ltnsym 9739 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  e.  RR  /\  V  e.  RR )  ->  ( M  <  V  ->  -.  V  <  M
) )
263225, 28, 262syl2anc 665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( M  <  V  ->  -.  V  <  M
) )
264263imp 430 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  M  <  V )  ->  -.  V  <  M )
265264iffalsed 3922 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  M  <  V )  ->  if ( V  <  M ,  V ,  ( V  + 
1 ) )  =  ( V  +  1 ) )
266261, 265sylan9eqr 2485 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  V )  ->  if ( y  <  M ,  y ,  ( y  +  1 ) )  =  ( V  +  1 ) )
267266eqeq2d 2436 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  M  <  V )  /\  y  =  V )  ->  (
j  =  if ( y  <  M , 
y ,  ( y  +  1 ) )  <-> 
j  =  ( V  +  1 ) ) )
268267biimpa 486 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  M  <  V )  /\  y  =  V )  /\  j  =  if ( y  <  M ,  y ,  ( y  +  1 ) ) )  ->  j  =  ( V  + 
1 ) )
269 oveq2 6313 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( V  + 
1 )  ->  (
1 ... j )  =  ( 1 ... ( V  +  1 ) ) )
270269imaeq2d 5187 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  ( V  + 
1 )  ->  ( U " ( 1 ... j ) )  =  ( U " (
1 ... ( V  + 
1 ) ) ) )
271270xpeq1d 4876 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  ( V  + 
1 )  ->  (
( U " (
1 ... j ) )  X.  { 1 } )  =  ( ( U " ( 1 ... ( V  + 
1 ) ) )  X.  { 1 } ) )
272 oveq1 6312 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  ( V  + 
1 )  ->  (
j  +  1 )  =  ( ( V  +  1 )  +  1 ) )
273272oveq1d 6320 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( V  + 
1 )  ->  (
( j  +  1 ) ... N )  =  ( ( ( V  +  1 )  +  1 ) ... N ) )
274273imaeq2d 5187 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  ( V  + 
1 )  ->  ( U " ( ( j  +  1 ) ... N ) )  =  ( U " (
( ( V  + 
1 )  +  1 ) ... N ) ) )
275274xpeq1d 4876 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  ( V  + 
1 )  ->  (
( U " (
( j  +  1 ) ... N ) )  X.  { 0 } )  =  ( ( U " (
( ( V  + 
1 )  +  1 ) ... N ) )  X.  { 0 } ) )
276271, 275uneq12d 3621 . . . . . . . . . . . . . . . . 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 6321 . . . . . . . . . . . . . . . 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 3422 . . . . . . . . . . . . . 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 11209 . . . . . . . . . . . . . . . . 17  |-  1  e.  ( ZZ>= `  0 )
281 fzss1 11844 . . . . . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . . 15  |-  ( ph  ->  V  e.  ( 0 ... ( N  - 
1 ) ) )
284283adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  M  <  V )  ->  V  e.  ( 0 ... ( N  -  1 ) ) )
285 ovex 6333 . . . . . . . . . . . . . . 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 5970 . . . . . . . . . . . . 13  |-  ( (
ph  /\  M  <  V )  ->  ( F `  V )  =  ( T  oF  +  ( ( ( U
" ( 1 ... ( V  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
288287fveq1d 5883 . . . . . . . . . . . 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 466 . . . . . . . . . . 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 2473 . . . . . . . . . 10  |-  ( ( ( ph  /\  M  <  V )  /\  (
n  e.  ( U
" ( 1 ... V ) )  \/  n  e.  ( U
" ( ( ( V  +  1 )  +  1 ) ... N ) ) ) )  ->  ( ( F `  ( V  -  1 ) ) `
 n )  =  ( ( F `  V ) `  n
) )
291290ex 435 . . . . . . . . 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 218 . . . . . . . 8  |-  ( (
ph  /\  M  <  V )  ->  ( (
n  e.  ( U
" ( 1 ... N ) )  /\  -.  n  e.  ( U " { ( V  +  1 ) } ) )  ->  (
( F `  ( V  -  1 ) ) `  n )  =  ( ( F `
 V ) `  n ) ) )
293292expdimp 438 . . . . . . 7  |-  ( ( ( ph  /\  M  <  V )  /\  n  e.  ( U " (
1 ... N ) ) )  ->  ( -.  n  e.  ( U " { ( V  + 
1 ) } )  ->  ( ( F `
 ( V  - 
1 ) ) `  n )  =  ( ( F `  V
) `  n )
) )
294293necon1ad 2636 . . . . . 6  |-  ( ( ( ph  /\  M  <  V )  /\  n  e.  ( U " (
1 ... N ) ) )  ->  ( (
( F `  ( V  -  1 ) ) `  n )  =/=  ( ( F `
 V ) `  n )  ->  n  e.  ( U " {
( V  +  1 ) } ) ) )
295 elimasni 5214 . . . . . . . 8  |-  ( n  e.  ( U " { ( V  + 
1 ) } )  ->  ( V  + 
1 ) U n )
296 eqcom 2431 . . . . . . . . 9  |-  ( n  =  ( U `  ( V  +  1
) )  <->  ( U `  ( V  +  1 ) )  =  n )
297 f1ofn 5832 . . . . . . . . . . 11  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U  Fn  ( 1 ... N
) )
2981, 297syl 17 . . . . . . . . . 10  |-  ( ph  ->  U  Fn  ( 1 ... N ) )
299 fnbrfvb 5921 . . . . . . . . . 10  |-  ( ( U  Fn  ( 1 ... N )  /\  ( V  +  1
)  e.  ( 1 ... N ) )  ->  ( ( U `
 ( V  + 
1 ) )  =  n  <->  ( V  + 
1 ) U n ) )
300298, 15, 299syl2anc 665 . . . . . . . . 9  |-  ( ph  ->  ( ( U `  ( V  +  1
) )  =  n  <-> 
( V  +  1 ) U n ) )
301296, 300syl5bb 260 . . . . . . . 8  |-  ( ph  ->  ( n  =  ( U `  ( V  +  1 ) )  <-> 
( V  +  1 ) U n ) )
302295, 301syl5ibr 224 . . . . . . 7  |-  ( ph  ->  ( n  e.  ( U " { ( V  +  1 ) } )  ->  n  =  ( U `  ( V  +  1
) ) ) )
303302ad2antrr 730 . . . . . 6  |-  ( ( ( ph  /\  M  <  V )  /\  n  e.  ( U " (
1 ... N ) ) )  ->  ( n  e.  ( U " {
( V  +  1 ) } )  ->  n  =  ( U `  ( V  +  1 ) ) ) )
304294, 303syld 45 . . . . 5  |-  ( ( ( ph  /\  M  <  V )  /\  n  e.  ( U " (
1 ... N ) ) )  ->  ( (
( F `  ( V  -  1 ) ) `  n )  =/=  ( ( F `
 V ) `  n )  ->  n  =  ( U `  ( V  +  1
) ) ) )
305304ralrimiva 2836 . . . 4  |-  ( (
ph  /\  M  <  V )  ->  A. n  e.  ( U " (
1 ... N ) ) ( ( ( F `
 ( V  - 
1 ) ) `  n )  =/=  (
( F `  V
) `  n )  ->  n  =  ( U `
 ( V  + 
1 ) ) ) )
306 fvex 5891 . . . . 5  |-  ( U `
 ( V  + 
1 ) )  e. 
_V
307 eqeq2 2437 . . . . . . 7  |-  ( m  =  ( U `  ( V  +  1
) )  ->  (
n  =  m  <->  n  =  ( U `  ( V  +  1 ) ) ) )
308307imbi2d 317 . . . . . 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 2861 . . . . 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 3173 . . . 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 5676 . . . . . . . . . . . . . . 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 3582 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1 ... N )  \  { V } )  =  ( ( ( 1 ... V )  u.  (
( V  +  1 ) ... N ) )  \  { V } ) )
315 difundir 3726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1 ... V
)  u.  ( ( V  +  1 ) ... N ) ) 
\  { V }
)  =  ( ( ( 1 ... V
)  \  { V } )  u.  (
( ( V  + 
1 ) ... N
)  \  { V } ) )
316215, 21eqeltrd 2507 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( V  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 ) )
317 uzid 11180 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( V  -  1 )  e.  ZZ  ->  ( V  -  1 )  e.  ( ZZ>= `  ( V  -  1 ) ) )
318227, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( V  -  1 )  e.  ( ZZ>= `  ( V  -  1
) ) )
319 peano2uz 11219 . . . . . . . . . . . . . . . . . . . . . . . 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 2508 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  V  e.  ( ZZ>= `  ( V  -  1
) ) )
322 fzsplit2 11831 . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 1 ... V
)  =  ( ( 1 ... ( V  -  1 ) )  u.  ( ( ( V  -  1 )  +  1 ) ... V ) ) )
324215oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( V  -  1 )  +  1 ) ... V
)  =  ( V ... V ) )
325 fzsn 11847 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( V  e.  ZZ  ->  ( V ... V )  =  { V } )
32627, 325syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( V ... V
)  =  { V } )
327324, 326eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( V  -  1 )  +  1 ) ... V
)  =  { V } )
328327uneq2d 3620 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( 1 ... ( V  -  1 ) )  u.  (
( ( V  - 
1 )  +  1 ) ... V ) )  =  ( ( 1 ... ( V  -  1 ) )  u.  { V }
) )
329323, 328eqtrd 2463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1 ... V
)  =  ( ( 1 ... ( V  -  1 ) )  u.  { V }
) )
330329difeq1d 3582 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1 ... V )  \  { V } )  =  ( ( ( 1 ... ( V  -  1 ) )  u.  { V } )  \  { V } ) )
331 difun2 3877 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1 ... ( V  -  1 ) )  u.  { V } )  \  { V } )  =  ( ( 1 ... ( V  -  1 ) )  \  { V } )
33228ltm1d 10546 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( V  -  1 )  <  V )
333228, 28ltnled 9789 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( V  - 
1 )  <  V  <->  -.  V  <_  ( V  -  1 ) ) )
334332, 333mpbid 213 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  V  <_  ( V  -  1 ) )
335 elfzle2 11810 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( V  e.  ( 1 ... ( V  -  1 ) )  ->  V  <_  ( V  -  1 ) )
336334, 335nsyl 124 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  -.  V  e.  ( 1 ... ( V  -  1 ) ) )
337 difsn 4134 . . . . . . . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( 1 ... ( V  - 
1 ) )  u. 
{ V } ) 
\  { V }
)  =  ( 1 ... ( V  - 
1 ) ) )
340330, 339eqtrd 2463 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1 ... V )  \  { V } )  =  ( 1 ... ( V  -  1 ) ) )
341 elfzle1 11809 . . . . . . . . . . . . . . . . . . . 20  |-  ( V  e.  ( ( V  +  1 ) ... N )  ->  ( V  +  1 )  <_  V )
34233, 341nsyl 124 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  V  e.  ( ( V  +  1 ) ... N ) )
343 difsn 4134 . . . . . . . . . . . . . . . . . . 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 3621 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( 1 ... V )  \  { V } )  u.  ( ( ( V  +  1 ) ... N )  \  { V } ) )  =  ( ( 1 ... ( V  -  1 ) )  u.  (
( V  +  1 ) ... N ) ) )
346315, 345syl5eq 2475 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 1 ... V )  u.  ( ( V  + 
1 ) ... N
) )  \  { V } )  =  ( ( 1 ... ( V  -  1 ) )  u.  ( ( V  +  1 ) ... N ) ) )
347314, 346eqtrd 2463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1 ... N )  \  { V } )  =  ( ( 1 ... ( V  -  1 ) )  u.  ( ( V  +  1 ) ... N ) ) )
348347imaeq2d 5187 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( U " (
( 1 ... N
)  \  { V } ) )  =  ( U " (
( 1 ... ( V  -  1 ) )  u.  ( ( V  +  1 ) ... N ) ) ) )
349313, 348eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  \  ( U " { V }
) )  =  ( U " ( ( 1 ... ( V  -  1 ) )  u.  ( ( V  +  1 ) ... N ) ) ) )
350 imaundi 5267 . . . . . . . . . . . . 13  |-  ( U
" ( ( 1 ... ( V  - 
1 ) )  u.  ( ( V  + 
1 ) ... N
) ) )  =  ( ( U "
( 1 ... ( V  -  1 ) ) )  u.  ( U " ( ( V  +  1 ) ... N ) ) )
351349, 350syl6eq 2479 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( U "
( 1 ... N
) )  \  ( U " { V }
) )  =  ( ( U " (
1 ... ( V  - 
1 ) ) )  u.  ( U "
( ( V  + 
1 ) ... N
) ) ) )
352351eleq2d 2492 . . . . . . . . . . 11  |-  ( ph  ->  ( n  e.  ( ( U " (
1 ... N ) ) 
\  ( U " { V } ) )  <-> 
n  e.  ( ( U " ( 1