Metamath Proof Explorer


Theorem signstcl

Description: Closure of the zero skipping sign word. (Contributed by Thierry Arnoux, 9-Oct-2018)

Ref Expression
Hypotheses signsv.p
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
signsv.w
|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
signsv.t
|- T = ( f e. Word RR |-> ( n e. ( 0 ..^ ( # ` f ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( f ` i ) ) ) ) ) )
signsv.v
|- V = ( f e. Word RR |-> sum_ j e. ( 1 ..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )
Assertion signstcl
|- ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 0 , 1 } )

Proof

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 } )