Step |
Hyp |
Ref |
Expression |
1 |
|
signsv.p |
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) ) |
2 |
|
signsv.w |
|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. } |
3 |
|
signsv.t |
|- T = ( f e. Word RR |-> ( n e. ( 0 ..^ ( # ` f ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( f ` i ) ) ) ) ) ) |
4 |
|
signsv.v |
|- V = ( f e. Word RR |-> sum_ j e. ( 1 ..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) ) |
5 |
|
simpll |
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> F e. ( Word RR \ { (/) } ) ) |
6 |
5
|
eldifad |
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> F e. Word RR ) |
7 |
1 2 3 4
|
signstcl |
|- ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 0 , 1 } ) |
8 |
6 7
|
sylancom |
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 0 , 1 } ) |
9 |
1 2 3 4
|
signstfvneq0 |
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) =/= 0 ) |
10 |
|
eldifsn |
|- ( ( ( T ` F ) ` N ) e. ( { -u 1 , 0 , 1 } \ { 0 } ) <-> ( ( ( T ` F ) ` N ) e. { -u 1 , 0 , 1 } /\ ( ( T ` F ) ` N ) =/= 0 ) ) |
11 |
8 9 10
|
sylanbrc |
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. ( { -u 1 , 0 , 1 } \ { 0 } ) ) |
12 |
|
tpcomb |
|- { -u 1 , 0 , 1 } = { -u 1 , 1 , 0 } |
13 |
12
|
difeq1i |
|- ( { -u 1 , 0 , 1 } \ { 0 } ) = ( { -u 1 , 1 , 0 } \ { 0 } ) |
14 |
|
neg1ne0 |
|- -u 1 =/= 0 |
15 |
|
ax-1ne0 |
|- 1 =/= 0 |
16 |
|
diftpsn3 |
|- ( ( -u 1 =/= 0 /\ 1 =/= 0 ) -> ( { -u 1 , 1 , 0 } \ { 0 } ) = { -u 1 , 1 } ) |
17 |
14 15 16
|
mp2an |
|- ( { -u 1 , 1 , 0 } \ { 0 } ) = { -u 1 , 1 } |
18 |
13 17
|
eqtri |
|- ( { -u 1 , 0 , 1 } \ { 0 } ) = { -u 1 , 1 } |
19 |
11 18
|
eleqtrdi |
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 1 } ) |