Metamath Proof Explorer

Theorem signstf

Description: The zero skipping sign word is a word. (Contributed by Thierry Arnoux, 8-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 signstf 
|- ( F e. Word RR -> ( T ` F ) e. Word RR )

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 signstfv 
 |-  ( F e. Word RR -> ( T ` F ) = ( n e. ( 0 ..^ ( # ` F ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( F ` i ) ) ) ) ) )
6 neg1rr 
 |-  -u 1 e. RR
7 0re 
 |-  0 e. RR
8 1re 
 |-  1 e. RR
9 tpssi 
 |-  ( ( -u 1 e. RR /\ 0 e. RR /\ 1 e. RR ) -> { -u 1 , 0 , 1 } C_ RR )
10 6 7 8 9 mp3an 
 |-  { -u 1 , 0 , 1 } C_ RR
11 1 2 signswbase 
 |-  { -u 1 , 0 , 1 } = ( Base ` W )
12 1 2 signswmnd 
 |-  W e. Mnd
13 12 a1i 
 |-  ( ( F e. Word RR /\ n e. ( 0 ..^ ( # ` F ) ) ) -> W e. Mnd )
14 fzo0ssnn0 
 |-  ( 0 ..^ ( # ` F ) ) C_ NN0
15 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
16 14 15 sseqtri 
 |-  ( 0 ..^ ( # ` F ) ) C_ ( ZZ>= ` 0 )
17 16 a1i 
 |-  ( F e. Word RR -> ( 0 ..^ ( # ` F ) ) C_ ( ZZ>= ` 0 ) )
18 17 sselda 
 |-  ( ( F e. Word RR /\ n e. ( 0 ..^ ( # ` F ) ) ) -> n e. ( ZZ>= ` 0 ) )
19 wrdf 
 |-  ( F e. Word RR -> F : ( 0 ..^ ( # ` F ) ) --> RR )
20 19 ad2antrr 
 |-  ( ( ( F e. Word RR /\ n e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... n ) ) -> F : ( 0 ..^ ( # ` F ) ) --> RR )
21 fzssfzo 
 |-  ( n e. ( 0 ..^ ( # ` F ) ) -> ( 0 ... n ) C_ ( 0 ..^ ( # ` F ) ) )
22 21 adantl 
 |-  ( ( F e. Word RR /\ n e. ( 0 ..^ ( # ` F ) ) ) -> ( 0 ... n ) C_ ( 0 ..^ ( # ` F ) ) )
23 22 sselda 
 |-  ( ( ( F e. Word RR /\ n e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... n ) ) -> i e. ( 0 ..^ ( # ` F ) ) )
24 20 23 ffvelrnd 
 |-  ( ( ( F e. Word RR /\ n e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... n ) ) -> ( F ` i ) e. RR )
25 24 rexrd 
 |-  ( ( ( F e. Word RR /\ n e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... n ) ) -> ( F ` i ) e. RR* )
26 sgncl 
 |-  ( ( F ` i ) e. RR* -> ( sgn ` ( F ` i ) ) e. { -u 1 , 0 , 1 } )
27 25 26 syl 
 |-  ( ( ( F e. Word RR /\ n e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... n ) ) -> ( sgn ` ( F ` i ) ) e. { -u 1 , 0 , 1 } )
28 11 13 18 27 gsumncl 
 |-  ( ( F e. Word RR /\ n e. ( 0 ..^ ( # ` F ) ) ) -> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( F ` i ) ) ) ) e. { -u 1 , 0 , 1 } )
29 10 28 sselid 
 |-  ( ( F e. Word RR /\ n e. ( 0 ..^ ( # ` F ) ) ) -> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( F ` i ) ) ) ) e. RR )
30 5 29 fmpt3d 
 |-  ( F e. Word RR -> ( T ` F ) : ( 0 ..^ ( # ` F ) ) --> RR )
31 iswrdi 
 |-  ( ( T ` F ) : ( 0 ..^ ( # ` F ) ) --> RR -> ( T ` F ) e. Word RR )
32 30 31 syl 
 |-  ( F e. Word RR -> ( T ` F ) e. Word RR )