Metamath Proof Explorer

Theorem poimirlem23

Description: Lemma for poimir , two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimirlem23.1 
|- ( ph -> T : ( 1 ... N ) --> ( 0 ..^ K ) )
poimirlem23.2 
|- ( ph -> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
poimirlem23.3 
|- ( ph -> V e. ( 0 ... N ) )
Assertion poimirlem23 
|- ( ph -> ( E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 <-> -. ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimirlem23.1 
 |-  ( ph -> T : ( 1 ... N ) --> ( 0 ..^ K ) )
3 poimirlem23.2 
 |-  ( ph -> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
4 poimirlem23.3 
 |-  ( ph -> V e. ( 0 ... N ) )
5 ovex 
 |-  ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
6 5 csbex 
 |-  [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
7 6 rgenw 
 |-  A. y e. ( 0 ... ( N - 1 ) ) [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
8 eqid 
 |-  ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
9 fveq1 
 |-  ( p = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( p ` N ) = ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) )
10 9 neeq1d 
 |-  ( p = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( ( p ` N ) =/= 0 <-> ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) =/= 0 ) )
11 df-ne 
 |-  ( ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) =/= 0 <-> -. ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 )
12 10 11 bitrdi 
 |-  ( p = [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( ( p ` N ) =/= 0 <-> -. ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 ) )
13 8 12 rexrnmptw 
 |-  ( A. y e. ( 0 ... ( N - 1 ) ) [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V -> ( E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 <-> E. y e. ( 0 ... ( N - 1 ) ) -. ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 ) )
14 7 13 ax-mp 
 |-  ( E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 <-> E. y e. ( 0 ... ( N - 1 ) ) -. ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 )
15 rexnal 
 |-  ( E. y e. ( 0 ... ( N - 1 ) ) -. ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> -. A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 )
16 14 15 bitri 
 |-  ( E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 <-> -. A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 )
17 1 nnzd 
 |-  ( ph -> N e. ZZ )
18 elfzelz 
 |-  ( V e. ( 0 ... N ) -> V e. ZZ )
19 4 18 syl 
 |-  ( ph -> V e. ZZ )
20 zlem1lt 
 |-  ( ( N e. ZZ /\ V e. ZZ ) -> ( N <_ V <-> ( N - 1 ) < V ) )
21 17 19 20 syl2anc 
 |-  ( ph -> ( N <_ V <-> ( N - 1 ) < V ) )
22 elfzle2 
 |-  ( V e. ( 0 ... N ) -> V <_ N )
23 4 22 syl 
 |-  ( ph -> V <_ N )
24 19 zred 
 |-  ( ph -> V e. RR )
25 1 nnred 
 |-  ( ph -> N e. RR )
26 24 25 letri3d 
 |-  ( ph -> ( V = N <-> ( V <_ N /\ N <_ V ) ) )
27 26 biimprd 
 |-  ( ph -> ( ( V <_ N /\ N <_ V ) -> V = N ) )
28 23 27 mpand 
 |-  ( ph -> ( N <_ V -> V = N ) )
29 21 28 sylbird 
 |-  ( ph -> ( ( N - 1 ) < V -> V = N ) )
30 29 necon3ad 
 |-  ( ph -> ( V =/= N -> -. ( N - 1 ) < V ) )
31 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
32 1 31 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
33 nn0fz0 
 |-  ( ( N - 1 ) e. NN0 <-> ( N - 1 ) e. ( 0 ... ( N - 1 ) ) )
34 32 33 sylib 
 |-  ( ph -> ( N - 1 ) e. ( 0 ... ( N - 1 ) ) )
35 34 adantr 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> ( N - 1 ) e. ( 0 ... ( N - 1 ) ) )
36 iffalse 
 |-  ( -. ( N - 1 ) < V -> if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) = ( ( N - 1 ) + 1 ) )
37 1 nncnd 
 |-  ( ph -> N e. CC )
38 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
39 37 38 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
40 36 39 sylan9eqr 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) = N )
41 40 csbeq1d 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> [_ if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ N / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
42 oveq2 
 |-  ( j = N -> ( 1 ... j ) = ( 1 ... N ) )
43 42 imaeq2d 
 |-  ( j = N -> ( U " ( 1 ... j ) ) = ( U " ( 1 ... N ) ) )
44 43 xpeq1d 
 |-  ( j = N -> ( ( U " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... N ) ) X. { 1 } ) )
45 oveq1 
 |-  ( j = N -> ( j + 1 ) = ( N + 1 ) )
46 45 oveq1d 
 |-  ( j = N -> ( ( j + 1 ) ... N ) = ( ( N + 1 ) ... N ) )
47 46 imaeq2d 
 |-  ( j = N -> ( U " ( ( j + 1 ) ... N ) ) = ( U " ( ( N + 1 ) ... N ) ) )
48 47 xpeq1d 
 |-  ( j = N -> ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( U " ( ( N + 1 ) ... N ) ) X. { 0 } ) )
49 44 48 uneq12d 
 |-  ( j = N -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... N ) ) X. { 1 } ) u. ( ( U " ( ( N + 1 ) ... N ) ) X. { 0 } ) ) )
50 f1ofo 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U : ( 1 ... N ) -onto-> ( 1 ... N ) )
51 foima 
 |-  ( U : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( U " ( 1 ... N ) ) = ( 1 ... N ) )
52 3 50 51 3syl 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( 1 ... N ) )
53 52 xpeq1d 
 |-  ( ph -> ( ( U " ( 1 ... N ) ) X. { 1 } ) = ( ( 1 ... N ) X. { 1 } ) )
54 25 ltp1d 
 |-  ( ph -> N < ( N + 1 ) )
55 17 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
56 fzn 
 |-  ( ( ( N + 1 ) e. ZZ /\ N e. ZZ ) -> ( N < ( N + 1 ) <-> ( ( N + 1 ) ... N ) = (/) ) )
57 55 17 56 syl2anc 
 |-  ( ph -> ( N < ( N + 1 ) <-> ( ( N + 1 ) ... N ) = (/) ) )
58 54 57 mpbid 
 |-  ( ph -> ( ( N + 1 ) ... N ) = (/) )
59 58 imaeq2d 
 |-  ( ph -> ( U " ( ( N + 1 ) ... N ) ) = ( U " (/) ) )
60 59 xpeq1d 
 |-  ( ph -> ( ( U " ( ( N + 1 ) ... N ) ) X. { 0 } ) = ( ( U " (/) ) X. { 0 } ) )
61 ima0 
 |-  ( U " (/) ) = (/)
62 61 xpeq1i 
 |-  ( ( U " (/) ) X. { 0 } ) = ( (/) X. { 0 } )
63 0xp 
 |-  ( (/) X. { 0 } ) = (/)
64 62 63 eqtri 
 |-  ( ( U " (/) ) X. { 0 } ) = (/)
65 60 64 eqtrdi 
 |-  ( ph -> ( ( U " ( ( N + 1 ) ... N ) ) X. { 0 } ) = (/) )
66 53 65 uneq12d 
 |-  ( ph -> ( ( ( U " ( 1 ... N ) ) X. { 1 } ) u. ( ( U " ( ( N + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( 1 ... N ) X. { 1 } ) u. (/) ) )
67 un0 
 |-  ( ( ( 1 ... N ) X. { 1 } ) u. (/) ) = ( ( 1 ... N ) X. { 1 } )
68 66 67 eqtrdi 
 |-  ( ph -> ( ( ( U " ( 1 ... N ) ) X. { 1 } ) u. ( ( U " ( ( N + 1 ) ... N ) ) X. { 0 } ) ) = ( ( 1 ... N ) X. { 1 } ) )
69 49 68 sylan9eqr 
 |-  ( ( ph /\ j = N ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( 1 ... N ) X. { 1 } ) )
70 69 oveq2d 
 |-  ( ( ph /\ j = N ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( 1 ... N ) X. { 1 } ) ) )
71 1 70 csbied 
 |-  ( ph -> [_ N / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( 1 ... N ) X. { 1 } ) ) )
72 71 adantr 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> [_ N / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( 1 ... N ) X. { 1 } ) ) )
73 41 72 eqtrd 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> [_ if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( 1 ... N ) X. { 1 } ) ) )
74 73 fveq1d 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> ( [_ if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = ( ( T oF + ( ( 1 ... N ) X. { 1 } ) ) ` N ) )
75 elfzonn0 
 |-  ( j e. ( 0 ..^ K ) -> j e. NN0 )
76 nn0p1nn 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN )
77 75 76 syl 
 |-  ( j e. ( 0 ..^ K ) -> ( j + 1 ) e. NN )
78 elsni 
 |-  ( y e. { 1 } -> y = 1 )
79 78 oveq2d 
 |-  ( y e. { 1 } -> ( j + y ) = ( j + 1 ) )
80 79 eleq1d 
 |-  ( y e. { 1 } -> ( ( j + y ) e. NN <-> ( j + 1 ) e. NN ) )
81 77 80 syl5ibrcom 
 |-  ( j e. ( 0 ..^ K ) -> ( y e. { 1 } -> ( j + y ) e. NN ) )
82 81 imp 
 |-  ( ( j e. ( 0 ..^ K ) /\ y e. { 1 } ) -> ( j + y ) e. NN )
83 82 adantl 
 |-  ( ( ph /\ ( j e. ( 0 ..^ K ) /\ y e. { 1 } ) ) -> ( j + y ) e. NN )
84 1ex 
 |-  1 e. _V
85 84 fconst 
 |-  ( ( 1 ... N ) X. { 1 } ) : ( 1 ... N ) --> { 1 }
86 85 a1i 
 |-  ( ph -> ( ( 1 ... N ) X. { 1 } ) : ( 1 ... N ) --> { 1 } )
87 ovexd 
 |-  ( ph -> ( 1 ... N ) e. _V )
88 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
89 83 2 86 87 87 88 off 
 |-  ( ph -> ( T oF + ( ( 1 ... N ) X. { 1 } ) ) : ( 1 ... N ) --> NN )
90 elfz1end 
 |-  ( N e. NN <-> N e. ( 1 ... N ) )
91 1 90 sylib 
 |-  ( ph -> N e. ( 1 ... N ) )
92 89 91 ffvelrnd 
 |-  ( ph -> ( ( T oF + ( ( 1 ... N ) X. { 1 } ) ) ` N ) e. NN )
93 92 adantr 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> ( ( T oF + ( ( 1 ... N ) X. { 1 } ) ) ` N ) e. NN )
94 74 93 eqeltrd 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> ( [_ if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) e. NN )
95 94 nnne0d 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> ( [_ if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) =/= 0 )
96 breq1 
 |-  ( y = ( N - 1 ) -> ( y < V <-> ( N - 1 ) < V ) )
97 id 
 |-  ( y = ( N - 1 ) -> y = ( N - 1 ) )
98 oveq1 
 |-  ( y = ( N - 1 ) -> ( y + 1 ) = ( ( N - 1 ) + 1 ) )
99 96 97 98 ifbieq12d 
 |-  ( y = ( N - 1 ) -> if ( y < V , y , ( y + 1 ) ) = if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) )
100 99 csbeq1d 
 |-  ( y = ( N - 1 ) -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
101 100 fveq1d 
 |-  ( y = ( N - 1 ) -> ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = ( [_ if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) )
102 101 neeq1d 
 |-  ( y = ( N - 1 ) -> ( ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) =/= 0 <-> ( [_ if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) =/= 0 ) )
103 11 102 bitr3id 
 |-  ( y = ( N - 1 ) -> ( -. ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> ( [_ if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) =/= 0 ) )
104 103 rspcev 
 |-  ( ( ( N - 1 ) e. ( 0 ... ( N - 1 ) ) /\ ( [_ if ( ( N - 1 ) < V , ( N - 1 ) , ( ( N - 1 ) + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) =/= 0 ) -> E. y e. ( 0 ... ( N - 1 ) ) -. ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 )
105 35 95 104 syl2anc 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> E. y e. ( 0 ... ( N - 1 ) ) -. ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 )
106 105 15 sylib 
 |-  ( ( ph /\ -. ( N - 1 ) < V ) -> -. A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 )
107 106 ex 
 |-  ( ph -> ( -. ( N - 1 ) < V -> -. A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 ) )
108 30 107 syld 
 |-  ( ph -> ( V =/= N -> -. A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 ) )
109 108 necon4ad 
 |-  ( ph -> ( A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 -> V = N ) )
110 109 pm4.71rd 
 |-  ( ph -> ( A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> ( V = N /\ A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 ) ) )
111 32 nn0zd 
 |-  ( ph -> ( N - 1 ) e. ZZ )
112 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
113 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
114 111 112 113 3syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
115 39 114 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
116 fzss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
117 115 116 syl 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
118 117 sselda 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> j e. ( 0 ... N ) )
119 91 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> N e. ( 1 ... N ) )
120 2 ffnd 
 |-  ( ph -> T Fn ( 1 ... N ) )
121 120 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> T Fn ( 1 ... N ) )
122 84 fconst 
 |-  ( ( U " ( 1 ... j ) ) X. { 1 } ) : ( U " ( 1 ... j ) ) --> { 1 }
123 c0ex 
 |-  0 e. _V
124 123 fconst 
 |-  ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( U " ( ( j + 1 ) ... N ) ) --> { 0 }
125 122 124 pm3.2i 
 |-  ( ( ( U " ( 1 ... j ) ) X. { 1 } ) : ( U " ( 1 ... j ) ) --> { 1 } /\ ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( U " ( ( j + 1 ) ... N ) ) --> { 0 } )
126 dff1o3 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( U : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' U ) )
127 126 simprbi 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' U )
128 imain 
 |-  ( Fun `' U -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) )
129 3 127 128 3syl 
 |-  ( ph -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) )
130 elfzelz 
 |-  ( j e. ( 0 ... N ) -> j e. ZZ )
131 130 zred 
 |-  ( j e. ( 0 ... N ) -> j e. RR )
132 131 ltp1d 
 |-  ( j e. ( 0 ... N ) -> j < ( j + 1 ) )
133 fzdisj 
 |-  ( j < ( j + 1 ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
134 132 133 syl 
 |-  ( j e. ( 0 ... N ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
135 134 imaeq2d 
 |-  ( j e. ( 0 ... N ) -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( U " (/) ) )
136 135 61 eqtrdi 
 |-  ( j e. ( 0 ... N ) -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = (/) )
137 129 136 sylan9req 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) )
138 fun 
 |-  ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) : ( U " ( 1 ... j ) ) --> { 1 } /\ ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( U " ( ( j + 1 ) ... N ) ) --> { 0 } ) /\ ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
139 125 137 138 sylancr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
140 elfznn0 
 |-  ( j e. ( 0 ... N ) -> j e. NN0 )
141 140 76 syl 
 |-  ( j e. ( 0 ... N ) -> ( j + 1 ) e. NN )
142 nnuz 
 |-  NN = ( ZZ>= ` 1 )
143 141 142 eleqtrdi 
 |-  ( j e. ( 0 ... N ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
144 elfzuz3 
 |-  ( j e. ( 0 ... N ) -> N e. ( ZZ>= ` j ) )
145 fzsplit2 
 |-  ( ( ( j + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` j ) ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
146 143 144 145 syl2anc 
 |-  ( j e. ( 0 ... N ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
147 146 imaeq2d 
 |-  ( j e. ( 0 ... N ) -> ( U " ( 1 ... N ) ) = ( U " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) )
148 imaundi 
 |-  ( U " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) )
149 147 148 eqtr2di 
 |-  ( j e. ( 0 ... N ) -> ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) = ( U " ( 1 ... N ) ) )
150 149 52 sylan9eqr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
151 150 feq2d 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( U " ( 1 ... j ) ) u. ( U " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) <-> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) ) )
152 139 151 mpbid 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) )
153 152 ffnd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
154 ovexd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( 1 ... N ) e. _V )
155 eqidd 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ N e. ( 1 ... N ) ) -> ( T ` N ) = ( T ` N ) )
156 eqidd 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ N e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) )
157 121 153 154 154 88 155 156 ofval 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ N e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = ( ( T ` N ) + ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) ) )
158 119 157 mpdan 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = ( ( T ` N ) + ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) ) )
159 158 eqeq1d 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> ( ( T ` N ) + ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) ) = 0 ) )
160 2 91 ffvelrnd 
 |-  ( ph -> ( T ` N ) e. ( 0 ..^ K ) )
161 elfzonn0 
 |-  ( ( T ` N ) e. ( 0 ..^ K ) -> ( T ` N ) e. NN0 )
162 160 161 syl 
 |-  ( ph -> ( T ` N ) e. NN0 )
163 162 nn0red 
 |-  ( ph -> ( T ` N ) e. RR )
164 163 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( T ` N ) e. RR )
165 162 nn0ge0d 
 |-  ( ph -> 0 <_ ( T ` N ) )
166 165 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> 0 <_ ( T ` N ) )
167 1re 
 |-  1 e. RR
168 snssi 
 |-  ( 1 e. RR -> { 1 } C_ RR )
169 167 168 ax-mp 
 |-  { 1 } C_ RR
170 0re 
 |-  0 e. RR
171 snssi 
 |-  ( 0 e. RR -> { 0 } C_ RR )
172 170 171 ax-mp 
 |-  { 0 } C_ RR
173 169 172 unssi 
 |-  ( { 1 } u. { 0 } ) C_ RR
174 152 119 ffvelrnd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. ( { 1 } u. { 0 } ) )
175 173 174 sselid 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. RR )
176 elun 
 |-  ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. ( { 1 } u. { 0 } ) <-> ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. { 1 } \/ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. { 0 } ) )
177 0le1 
 |-  0 <_ 1
178 elsni 
 |-  ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. { 1 } -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 1 )
179 177 178 breqtrrid 
 |-  ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. { 1 } -> 0 <_ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) )
180 0le0 
 |-  0 <_ 0
181 elsni 
 |-  ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. { 0 } -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 )
182 180 181 breqtrrid 
 |-  ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. { 0 } -> 0 <_ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) )
183 179 182 jaoi 
 |-  ( ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. { 1 } \/ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. { 0 } ) -> 0 <_ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) )
184 176 183 sylbi 
 |-  ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. ( { 1 } u. { 0 } ) -> 0 <_ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) )
185 174 184 syl 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> 0 <_ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) )
186 add20 
 |-  ( ( ( ( T ` N ) e. RR /\ 0 <_ ( T ` N ) ) /\ ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) e. RR /\ 0 <_ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) ) ) -> ( ( ( T ` N ) + ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) ) = 0 <-> ( ( T ` N ) = 0 /\ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) ) )
187 164 166 175 185 186 syl22anc 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( T ` N ) + ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) ) = 0 <-> ( ( T ` N ) = 0 /\ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) ) )
188 159 187 bitrd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> ( ( T ` N ) = 0 /\ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) ) )
189 118 188 syldan 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> ( ( T ` N ) = 0 /\ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) ) )
190 189 ralbidva 
 |-  ( ph -> ( A. j e. ( 0 ... ( N - 1 ) ) ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> A. j e. ( 0 ... ( N - 1 ) ) ( ( T ` N ) = 0 /\ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) ) )
191 190 adantr 
 |-  ( ( ph /\ V = N ) -> ( A. j e. ( 0 ... ( N - 1 ) ) ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> A. j e. ( 0 ... ( N - 1 ) ) ( ( T ` N ) = 0 /\ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) ) )
192 breq2 
 |-  ( V = N -> ( y < V <-> y < N ) )
193 192 ifbid 
 |-  ( V = N -> if ( y < V , y , ( y + 1 ) ) = if ( y < N , y , ( y + 1 ) ) )
194 elfzelz 
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> y e. ZZ )
195 194 zred 
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> y e. RR )
196 195 adantl 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y e. RR )
197 32 nn0red 
 |-  ( ph -> ( N - 1 ) e. RR )
198 197 adantr 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( N - 1 ) e. RR )
199 25 adantr 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. RR )
200 elfzle2 
 |-  ( y e. ( 0 ... ( N - 1 ) ) -> y <_ ( N - 1 ) )
201 200 adantl 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y <_ ( N - 1 ) )
202 25 ltm1d 
 |-  ( ph -> ( N - 1 ) < N )
203 202 adantr 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( N - 1 ) < N )
204 196 198 199 201 203 lelttrd 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y < N )
205 204 iftrued 
 |-  ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> if ( y < N , y , ( y + 1 ) ) = y )
206 193 205 sylan9eqr 
 |-  ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ V = N ) -> if ( y < V , y , ( y + 1 ) ) = y )
207 206 an32s 
 |-  ( ( ( ph /\ V = N ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> if ( y < V , y , ( y + 1 ) ) = y )
208 207 csbeq1d 
 |-  ( ( ( ph /\ V = N ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
209 208 fveq1d 
 |-  ( ( ( ph /\ V = N ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) )
210 209 eqeq1d 
 |-  ( ( ( ph /\ V = N ) /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 ) )
211 210 ralbidva 
 |-  ( ( ph /\ V = N ) -> ( A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> A. y e. ( 0 ... ( N - 1 ) ) ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 ) )
212 nfv 
 |-  F/ y ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0
213 nfcsb1v 
 |-  F/_ j [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
214 nfcv 
 |-  F/_ j N
215 213 214 nffv 
 |-  F/_ j ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N )
216 215 nfeq1 
 |-  F/ j ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0
217 csbeq1a 
 |-  ( j = y -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
218 217 fveq1d 
 |-  ( j = y -> ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) )
219 218 eqeq1d 
 |-  ( j = y -> ( ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 ) )
220 212 216 219 cbvralw 
 |-  ( A. j e. ( 0 ... ( N - 1 ) ) ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> A. y e. ( 0 ... ( N - 1 ) ) ( [_ y / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 )
221 211 220 bitr4di 
 |-  ( ( ph /\ V = N ) -> ( A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> A. j e. ( 0 ... ( N - 1 ) ) ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 ) )
222 ne0i 
 |-  ( ( N - 1 ) e. ( 0 ... ( N - 1 ) ) -> ( 0 ... ( N - 1 ) ) =/= (/) )
223 r19.3rzv 
 |-  ( ( 0 ... ( N - 1 ) ) =/= (/) -> ( ( T ` N ) = 0 <-> A. j e. ( 0 ... ( N - 1 ) ) ( T ` N ) = 0 ) )
224 34 222 223 3syl 
 |-  ( ph -> ( ( T ` N ) = 0 <-> A. j e. ( 0 ... ( N - 1 ) ) ( T ` N ) = 0 ) )
225 elfzelz 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> j e. ZZ )
226 225 zred 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> j e. RR )
227 226 ltp1d 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> j < ( j + 1 ) )
228 227 133 syl 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
229 228 imaeq2d 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( U " (/) ) )
230 229 61 eqtrdi 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> ( U " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = (/) )
231 129 230 sylan9req 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) )
232 231 adantlr 
 |-  ( ( ( ph /\ ( U ` N ) = N ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) )
233 simplr 
 |-  ( ( ( ph /\ ( U ` N ) = N ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( U ` N ) = N )
234 f1ofn 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U Fn ( 1 ... N ) )
235 3 234 syl 
 |-  ( ph -> U Fn ( 1 ... N ) )
236 235 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> U Fn ( 1 ... N ) )
237 elfznn0 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> j e. NN0 )
238 237 76 syl 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> ( j + 1 ) e. NN )
239 238 142 eleqtrdi 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
240 fzss1 
 |-  ( ( j + 1 ) e. ( ZZ>= ` 1 ) -> ( ( j + 1 ) ... N ) C_ ( 1 ... N ) )
241 239 240 syl 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> ( ( j + 1 ) ... N ) C_ ( 1 ... N ) )
242 241 adantl 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( j + 1 ) ... N ) C_ ( 1 ... N ) )
243 39 adantr 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )
244 elfzuz3 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` j ) )
245 eluzp1p1 
 |-  ( ( N - 1 ) e. ( ZZ>= ` j ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
246 244 245 syl 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
247 246 adantl 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( j + 1 ) ) )
248 243 247 eqeltrrd 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` ( j + 1 ) ) )
249 eluzfz2 
 |-  ( N e. ( ZZ>= ` ( j + 1 ) ) -> N e. ( ( j + 1 ) ... N ) )
250 248 249 syl 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ( j + 1 ) ... N ) )
251 fnfvima 
 |-  ( ( U Fn ( 1 ... N ) /\ ( ( j + 1 ) ... N ) C_ ( 1 ... N ) /\ N e. ( ( j + 1 ) ... N ) ) -> ( U ` N ) e. ( U " ( ( j + 1 ) ... N ) ) )
252 236 242 250 251 syl3anc 
 |-  ( ( ph /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( U ` N ) e. ( U " ( ( j + 1 ) ... N ) ) )
253 252 adantlr 
 |-  ( ( ( ph /\ ( U ` N ) = N ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( U ` N ) e. ( U " ( ( j + 1 ) ... N ) ) )
254 233 253 eqeltrrd 
 |-  ( ( ( ph /\ ( U ` N ) = N ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> N e. ( U " ( ( j + 1 ) ... N ) ) )
255 fnconstg 
 |-  ( 1 e. _V -> ( ( U " ( 1 ... j ) ) X. { 1 } ) Fn ( U " ( 1 ... j ) ) )
256 84 255 ax-mp 
 |-  ( ( U " ( 1 ... j ) ) X. { 1 } ) Fn ( U " ( 1 ... j ) )
257 fnconstg 
 |-  ( 0 e. _V -> ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( j + 1 ) ... N ) ) )
258 123 257 ax-mp 
 |-  ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( j + 1 ) ... N ) )
259 fvun2 
 |-  ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) Fn ( U " ( 1 ... j ) ) /\ ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( j + 1 ) ... N ) ) /\ ( ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) /\ N e. ( U " ( ( j + 1 ) ... N ) ) ) ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = ( ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ` N ) )
260 256 258 259 mp3an12 
 |-  ( ( ( ( U " ( 1 ... j ) ) i^i ( U " ( ( j + 1 ) ... N ) ) ) = (/) /\ N e. ( U " ( ( j + 1 ) ... N ) ) ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = ( ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ` N ) )
261 232 254 260 syl2anc 
 |-  ( ( ( ph /\ ( U ` N ) = N ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = ( ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ` N ) )
262 123 fvconst2 
 |-  ( N e. ( U " ( ( j + 1 ) ... N ) ) -> ( ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ` N ) = 0 )
263 254 262 syl 
 |-  ( ( ( ph /\ ( U ` N ) = N ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ` N ) = 0 )
264 261 263 eqtrd 
 |-  ( ( ( ph /\ ( U ` N ) = N ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 )
265 264 ralrimiva 
 |-  ( ( ph /\ ( U ` N ) = N ) -> A. j e. ( 0 ... ( N - 1 ) ) ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 )
266 265 ex 
 |-  ( ph -> ( ( U ` N ) = N -> A. j e. ( 0 ... ( N - 1 ) ) ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) )
267 34 adantr 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> ( N - 1 ) e. ( 0 ... ( N - 1 ) ) )
268 ax-1ne0 
 |-  1 =/= 0
269 imain 
 |-  ( Fun `' U -> ( U " ( ( 1 ... ( N - 1 ) ) i^i ( ( ( N - 1 ) + 1 ) ... N ) ) ) = ( ( U " ( 1 ... ( N - 1 ) ) ) i^i ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) ) )
270 3 127 269 3syl 
 |-  ( ph -> ( U " ( ( 1 ... ( N - 1 ) ) i^i ( ( ( N - 1 ) + 1 ) ... N ) ) ) = ( ( U " ( 1 ... ( N - 1 ) ) ) i^i ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) ) )
271 202 39 breqtrrd 
 |-  ( ph -> ( N - 1 ) < ( ( N - 1 ) + 1 ) )
272 fzdisj 
 |-  ( ( N - 1 ) < ( ( N - 1 ) + 1 ) -> ( ( 1 ... ( N - 1 ) ) i^i ( ( ( N - 1 ) + 1 ) ... N ) ) = (/) )
273 271 272 syl 
 |-  ( ph -> ( ( 1 ... ( N - 1 ) ) i^i ( ( ( N - 1 ) + 1 ) ... N ) ) = (/) )
274 273 imaeq2d 
 |-  ( ph -> ( U " ( ( 1 ... ( N - 1 ) ) i^i ( ( ( N - 1 ) + 1 ) ... N ) ) ) = ( U " (/) ) )
275 274 61 eqtrdi 
 |-  ( ph -> ( U " ( ( 1 ... ( N - 1 ) ) i^i ( ( ( N - 1 ) + 1 ) ... N ) ) ) = (/) )
276 270 275 eqtr3d 
 |-  ( ph -> ( ( U " ( 1 ... ( N - 1 ) ) ) i^i ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) ) = (/) )
277 276 adantr 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> ( ( U " ( 1 ... ( N - 1 ) ) ) i^i ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) ) = (/) )
278 91 adantr 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> N e. ( 1 ... N ) )
279 elimasni 
 |-  ( N e. ( U " { N } ) -> N U N )
280 fnbrfvb 
 |-  ( ( U Fn ( 1 ... N ) /\ N e. ( 1 ... N ) ) -> ( ( U ` N ) = N <-> N U N ) )
281 235 91 280 syl2anc 
 |-  ( ph -> ( ( U ` N ) = N <-> N U N ) )
282 279 281 syl5ibr 
 |-  ( ph -> ( N e. ( U " { N } ) -> ( U ` N ) = N ) )
283 282 necon3ad 
 |-  ( ph -> ( ( U ` N ) =/= N -> -. N e. ( U " { N } ) ) )
284 283 imp 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> -. N e. ( U " { N } ) )
285 278 284 eldifd 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> N e. ( ( 1 ... N ) \ ( U " { N } ) ) )
286 imadif 
 |-  ( Fun `' U -> ( U " ( ( 1 ... N ) \ { N } ) ) = ( ( U " ( 1 ... N ) ) \ ( U " { N } ) ) )
287 3 127 286 3syl 
 |-  ( ph -> ( U " ( ( 1 ... N ) \ { N } ) ) = ( ( U " ( 1 ... N ) ) \ ( U " { N } ) ) )
288 difun2 
 |-  ( ( ( 1 ... ( N - 1 ) ) u. { N } ) \ { N } ) = ( ( 1 ... ( N - 1 ) ) \ { N } )
289 elun 
 |-  ( j e. ( ( 1 ... ( N - 1 ) ) u. { N } ) <-> ( j e. ( 1 ... ( N - 1 ) ) \/ j e. { N } ) )
290 velsn 
 |-  ( j e. { N } <-> j = N )
291 290 orbi2i 
 |-  ( ( j e. ( 1 ... ( N - 1 ) ) \/ j e. { N } ) <-> ( j e. ( 1 ... ( N - 1 ) ) \/ j = N ) )
292 289 291 bitri 
 |-  ( j e. ( ( 1 ... ( N - 1 ) ) u. { N } ) <-> ( j e. ( 1 ... ( N - 1 ) ) \/ j = N ) )
293 1 142 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
294 fzm1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( j e. ( 1 ... N ) <-> ( j e. ( 1 ... ( N - 1 ) ) \/ j = N ) ) )
295 293 294 syl 
 |-  ( ph -> ( j e. ( 1 ... N ) <-> ( j e. ( 1 ... ( N - 1 ) ) \/ j = N ) ) )
296 292 295 bitr4id 
 |-  ( ph -> ( j e. ( ( 1 ... ( N - 1 ) ) u. { N } ) <-> j e. ( 1 ... N ) ) )
297 296 eqrdv 
 |-  ( ph -> ( ( 1 ... ( N - 1 ) ) u. { N } ) = ( 1 ... N ) )
298 297 difeq1d 
 |-  ( ph -> ( ( ( 1 ... ( N - 1 ) ) u. { N } ) \ { N } ) = ( ( 1 ... N ) \ { N } ) )
299 197 25 ltnled 
 |-  ( ph -> ( ( N - 1 ) < N <-> -. N <_ ( N - 1 ) ) )
300 202 299 mpbid 
 |-  ( ph -> -. N <_ ( N - 1 ) )
301 elfzle2 
 |-  ( N e. ( 1 ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
302 300 301 nsyl 
 |-  ( ph -> -. N e. ( 1 ... ( N - 1 ) ) )
303 difsn 
 |-  ( -. N e. ( 1 ... ( N - 1 ) ) -> ( ( 1 ... ( N - 1 ) ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
304 302 303 syl 
 |-  ( ph -> ( ( 1 ... ( N - 1 ) ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
305 288 298 304 3eqtr3a 
 |-  ( ph -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
306 305 imaeq2d 
 |-  ( ph -> ( U " ( ( 1 ... N ) \ { N } ) ) = ( U " ( 1 ... ( N - 1 ) ) ) )
307 52 difeq1d 
 |-  ( ph -> ( ( U " ( 1 ... N ) ) \ ( U " { N } ) ) = ( ( 1 ... N ) \ ( U " { N } ) ) )
308 287 306 307 3eqtr3rd 
 |-  ( ph -> ( ( 1 ... N ) \ ( U " { N } ) ) = ( U " ( 1 ... ( N - 1 ) ) ) )
309 308 adantr 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> ( ( 1 ... N ) \ ( U " { N } ) ) = ( U " ( 1 ... ( N - 1 ) ) ) )
310 285 309 eleqtrd 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> N e. ( U " ( 1 ... ( N - 1 ) ) ) )
311 fnconstg 
 |-  ( 1 e. _V -> ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( N - 1 ) ) ) )
312 84 311 ax-mp 
 |-  ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( N - 1 ) ) )
313 fnconstg 
 |-  ( 0 e. _V -> ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) )
314 123 313 ax-mp 
 |-  ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( N - 1 ) + 1 ) ... N ) )
315 fvun1 
 |-  ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( N - 1 ) ) ) /\ ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) /\ ( ( ( U " ( 1 ... ( N - 1 ) ) ) i^i ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) ) = (/) /\ N e. ( U " ( 1 ... ( N - 1 ) ) ) ) ) -> ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) ` N ) )
316 312 314 315 mp3an12 
 |-  ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) i^i ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) ) = (/) /\ N e. ( U " ( 1 ... ( N - 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) ` N ) )
317 277 310 316 syl2anc 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) ` N ) )
318 84 fvconst2 
 |-  ( N e. ( U " ( 1 ... ( N - 1 ) ) ) -> ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) ` N ) = 1 )
319 310 318 syl 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) ` N ) = 1 )
320 317 319 eqtrd 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 1 )
321 320 neeq1d 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> ( ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` N ) =/= 0 <-> 1 =/= 0 ) )
322 268 321 mpbiri 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` N ) =/= 0 )
323 df-ne 
 |-  ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) =/= 0 <-> -. ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 )
324 oveq2 
 |-  ( j = ( N - 1 ) -> ( 1 ... j ) = ( 1 ... ( N - 1 ) ) )
325 324 imaeq2d 
 |-  ( j = ( N - 1 ) -> ( U " ( 1 ... j ) ) = ( U " ( 1 ... ( N - 1 ) ) ) )
326 325 xpeq1d 
 |-  ( j = ( N - 1 ) -> ( ( U " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) )
327 oveq1 
 |-  ( j = ( N - 1 ) -> ( j + 1 ) = ( ( N - 1 ) + 1 ) )
328 327 oveq1d 
 |-  ( j = ( N - 1 ) -> ( ( j + 1 ) ... N ) = ( ( ( N - 1 ) + 1 ) ... N ) )
329 328 imaeq2d 
 |-  ( j = ( N - 1 ) -> ( U " ( ( j + 1 ) ... N ) ) = ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) )
330 329 xpeq1d 
 |-  ( j = ( N - 1 ) -> ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) )
331 326 330 uneq12d 
 |-  ( j = ( N - 1 ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
332 331 fveq1d 
 |-  ( j = ( N - 1 ) -> ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` N ) )
333 332 neeq1d 
 |-  ( j = ( N - 1 ) -> ( ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) =/= 0 <-> ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` N ) =/= 0 ) )
334 323 333 bitr3id 
 |-  ( j = ( N - 1 ) -> ( -. ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 <-> ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` N ) =/= 0 ) )
335 334 rspcev 
 |-  ( ( ( N - 1 ) e. ( 0 ... ( N - 1 ) ) /\ ( ( ( ( U " ( 1 ... ( N - 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( N - 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` N ) =/= 0 ) -> E. j e. ( 0 ... ( N - 1 ) ) -. ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 )
336 267 322 335 syl2anc 
 |-  ( ( ph /\ ( U ` N ) =/= N ) -> E. j e. ( 0 ... ( N - 1 ) ) -. ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 )
337 336 ex 
 |-  ( ph -> ( ( U ` N ) =/= N -> E. j e. ( 0 ... ( N - 1 ) ) -. ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) )
338 rexnal 
 |-  ( E. j e. ( 0 ... ( N - 1 ) ) -. ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 <-> -. A. j e. ( 0 ... ( N - 1 ) ) ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 )
339 337 338 syl6ib 
 |-  ( ph -> ( ( U ` N ) =/= N -> -. A. j e. ( 0 ... ( N - 1 ) ) ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) )
340 339 necon4ad 
 |-  ( ph -> ( A. j e. ( 0 ... ( N - 1 ) ) ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 -> ( U ` N ) = N ) )
341 266 340 impbid 
 |-  ( ph -> ( ( U ` N ) = N <-> A. j e. ( 0 ... ( N - 1 ) ) ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) )
342 224 341 anbi12d 
 |-  ( ph -> ( ( ( T ` N ) = 0 /\ ( U ` N ) = N ) <-> ( A. j e. ( 0 ... ( N - 1 ) ) ( T ` N ) = 0 /\ A. j e. ( 0 ... ( N - 1 ) ) ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) ) )
343 r19.26 
 |-  ( A. j e. ( 0 ... ( N - 1 ) ) ( ( T ` N ) = 0 /\ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) <-> ( A. j e. ( 0 ... ( N - 1 ) ) ( T ` N ) = 0 /\ A. j e. ( 0 ... ( N - 1 ) ) ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) )
344 342 343 bitr4di 
 |-  ( ph -> ( ( ( T ` N ) = 0 /\ ( U ` N ) = N ) <-> A. j e. ( 0 ... ( N - 1 ) ) ( ( T ` N ) = 0 /\ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) ) )
345 344 adantr 
 |-  ( ( ph /\ V = N ) -> ( ( ( T ` N ) = 0 /\ ( U ` N ) = N ) <-> A. j e. ( 0 ... ( N - 1 ) ) ( ( T ` N ) = 0 /\ ( ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ` N ) = 0 ) ) )
346 191 221 345 3bitr4d 
 |-  ( ( ph /\ V = N ) -> ( A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) )
347 346 pm5.32da 
 |-  ( ph -> ( ( V = N /\ A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 ) <-> ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) )
348 110 347 bitrd 
 |-  ( ph -> ( A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) )
349 348 notbid 
 |-  ( ph -> ( -. A. y e. ( 0 ... ( N - 1 ) ) ( [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ` N ) = 0 <-> -. ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) )
350 16 349 syl5bb 
 |-  ( ph -> ( E. p e. ran ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < V , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ( p ` N ) =/= 0 <-> -. ( V = N /\ ( ( T ` N ) = 0 /\ ( U ` N ) = N ) ) ) )