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 sseldi
 |-  ( ( 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 ) ) ) )