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 |
1 2 3 4
|
signstfval |
|- ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) = ( W gsum ( i e. ( 0 ... N ) |-> ( sgn ` ( F ` i ) ) ) ) ) |
6 |
1 2
|
signswbase |
|- { -u 1 , 0 , 1 } = ( Base ` W ) |
7 |
1 2
|
signswmnd |
|- W e. Mnd |
8 |
7
|
a1i |
|- ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> W e. Mnd ) |
9 |
|
fzo0ssnn0 |
|- ( 0 ..^ ( # ` F ) ) C_ NN0 |
10 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
11 |
9 10
|
sseqtri |
|- ( 0 ..^ ( # ` F ) ) C_ ( ZZ>= ` 0 ) |
12 |
11
|
a1i |
|- ( F e. Word RR -> ( 0 ..^ ( # ` F ) ) C_ ( ZZ>= ` 0 ) ) |
13 |
12
|
sselda |
|- ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> N e. ( ZZ>= ` 0 ) ) |
14 |
|
wrdf |
|- ( F e. Word RR -> F : ( 0 ..^ ( # ` F ) ) --> RR ) |
15 |
14
|
ad2antrr |
|- ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... N ) ) -> F : ( 0 ..^ ( # ` F ) ) --> RR ) |
16 |
|
fzssfzo |
|- ( N e. ( 0 ..^ ( # ` F ) ) -> ( 0 ... N ) C_ ( 0 ..^ ( # ` F ) ) ) |
17 |
16
|
adantl |
|- ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( 0 ... N ) C_ ( 0 ..^ ( # ` F ) ) ) |
18 |
17
|
sselda |
|- ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... N ) ) -> i e. ( 0 ..^ ( # ` F ) ) ) |
19 |
15 18
|
ffvelrnd |
|- ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... N ) ) -> ( F ` i ) e. RR ) |
20 |
19
|
rexrd |
|- ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... N ) ) -> ( F ` i ) e. RR* ) |
21 |
|
sgncl |
|- ( ( F ` i ) e. RR* -> ( sgn ` ( F ` i ) ) e. { -u 1 , 0 , 1 } ) |
22 |
20 21
|
syl |
|- ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... N ) ) -> ( sgn ` ( F ` i ) ) e. { -u 1 , 0 , 1 } ) |
23 |
6 8 13 22
|
gsumncl |
|- ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( W gsum ( i e. ( 0 ... N ) |-> ( sgn ` ( F ` i ) ) ) ) e. { -u 1 , 0 , 1 } ) |
24 |
5 23
|
eqeltrd |
|- ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 0 , 1 } ) |