Metamath Proof Explorer

Theorem signsvtn0

Description: If the last letter is nonzero, then this is the zero-skipping sign. (Contributed by Thierry Arnoux, 8-Oct-2018) (Proof shortened by AV, 3-Nov-2022)

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 ) )
signsvtn0.1 
|- N = ( # ` F )
Assertion signsvtn0 
|- ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( sgn ` ( F ` ( N - 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 signsvtn0.1 
 |-  N = ( # ` F )
6 eldifsn 
 |-  ( F e. ( Word RR \ { (/) } ) <-> ( F e. Word RR /\ F =/= (/) ) )
7 6 biimpi 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( F e. Word RR /\ F =/= (/) ) )
8 7 adantr 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F e. Word RR /\ F =/= (/) ) )
9 8 simpld 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F e. Word RR )
10 9 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> F e. Word RR )
11 wrdf 
 |-  ( F e. Word RR -> F : ( 0 ..^ ( # ` F ) ) --> RR )
12 10 11 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> F : ( 0 ..^ ( # ` F ) ) --> RR )
13 lennncl 
 |-  ( ( F e. Word RR /\ F =/= (/) ) -> ( # ` F ) e. NN )
14 8 13 syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( # ` F ) e. NN )
15 14 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( # ` F ) e. NN )
16 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` F ) ) <-> ( # ` F ) e. NN )
17 15 16 sylibr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> 0 e. ( 0 ..^ ( # ` F ) ) )
18 12 17 ffvelrnd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( F ` 0 ) e. RR )
19 1 2 3 4 signstf0 
 |-  ( ( F ` 0 ) e. RR -> ( T ` <" ( F ` 0 ) "> ) = <" ( sgn ` ( F ` 0 ) ) "> )
20 18 19 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( T ` <" ( F ` 0 ) "> ) = <" ( sgn ` ( F ` 0 ) ) "> )
21 simpr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> N = 1 )
22 5 21 eqtr3id 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( # ` F ) = 1 )
23 eqs1 
 |-  ( ( F e. Word RR /\ ( # ` F ) = 1 ) -> F = <" ( F ` 0 ) "> )
24 10 22 23 syl2anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> F = <" ( F ` 0 ) "> )
25 24 fveq2d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( T ` F ) = ( T ` <" ( F ` 0 ) "> ) )
26 oveq1 
 |-  ( N = 1 -> ( N - 1 ) = ( 1 - 1 ) )
27 1m1e0 
 |-  ( 1 - 1 ) = 0
28 26 27 eqtrdi 
 |-  ( N = 1 -> ( N - 1 ) = 0 )
29 28 fveq2d 
 |-  ( N = 1 -> ( F ` ( N - 1 ) ) = ( F ` 0 ) )
30 29 fveq2d 
 |-  ( N = 1 -> ( sgn ` ( F ` ( N - 1 ) ) ) = ( sgn ` ( F ` 0 ) ) )
31 30 s1eqd 
 |-  ( N = 1 -> <" ( sgn ` ( F ` ( N - 1 ) ) ) "> = <" ( sgn ` ( F ` 0 ) ) "> )
32 21 31 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> <" ( sgn ` ( F ` ( N - 1 ) ) ) "> = <" ( sgn ` ( F ` 0 ) ) "> )
33 20 25 32 3eqtr4d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( T ` F ) = <" ( sgn ` ( F ` ( N - 1 ) ) ) "> )
34 21 28 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( N - 1 ) = 0 )
35 33 34 fveq12d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( <" ( sgn ` ( F ` ( N - 1 ) ) ) "> ` 0 ) )
36 9 11 syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F : ( 0 ..^ ( # ` F ) ) --> RR )
37 5 oveq1i 
 |-  ( N - 1 ) = ( ( # ` F ) - 1 )
38 fzo0end 
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
39 8 13 38 3syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
40 37 39 eqeltrid 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( N - 1 ) e. ( 0 ..^ ( # ` F ) ) )
41 36 40 ffvelrnd 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F ` ( N - 1 ) ) e. RR )
42 41 rexrd 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F ` ( N - 1 ) ) e. RR* )
43 sgncl 
 |-  ( ( F ` ( N - 1 ) ) e. RR* -> ( sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } )
44 42 43 syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } )
45 44 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } )
46 s1fv 
 |-  ( ( sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } -> ( <" ( sgn ` ( F ` ( N - 1 ) ) ) "> ` 0 ) = ( sgn ` ( F ` ( N - 1 ) ) ) )
47 45 46 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( <" ( sgn ` ( F ` ( N - 1 ) ) ) "> ` 0 ) = ( sgn ` ( F ` ( N - 1 ) ) ) )
48 35 47 eqtrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N = 1 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( sgn ` ( F ` ( N - 1 ) ) ) )
49 fzossfz 
 |-  ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
50 49 39 sselid 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( # ` F ) - 1 ) e. ( 0 ... ( # ` F ) ) )
51 pfxres 
 |-  ( ( F e. Word RR /\ ( ( # ` F ) - 1 ) e. ( 0 ... ( # ` F ) ) ) -> ( F prefix ( ( # ` F ) - 1 ) ) = ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) )
52 9 50 51 syl2anc 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F prefix ( ( # ` F ) - 1 ) ) = ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) )
53 52 oveq1d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( F prefix ( ( # ` F ) - 1 ) ) ++ <" ( lastS ` F ) "> ) = ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ++ <" ( lastS ` F ) "> ) )
54 pfxlswccat 
 |-  ( ( F e. Word RR /\ F =/= (/) ) -> ( ( F prefix ( ( # ` F ) - 1 ) ) ++ <" ( lastS ` F ) "> ) = F )
55 54 eqcomd 
 |-  ( ( F e. Word RR /\ F =/= (/) ) -> F = ( ( F prefix ( ( # ` F ) - 1 ) ) ++ <" ( lastS ` F ) "> ) )
56 8 55 syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F = ( ( F prefix ( ( # ` F ) - 1 ) ) ++ <" ( lastS ` F ) "> ) )
57 37 oveq2i 
 |-  ( 0 ..^ ( N - 1 ) ) = ( 0 ..^ ( ( # ` F ) - 1 ) )
58 57 a1i 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( 0 ..^ ( N - 1 ) ) = ( 0 ..^ ( ( # ` F ) - 1 ) ) )
59 58 reseq2d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F |` ( 0 ..^ ( N - 1 ) ) ) = ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) )
60 37 a1i 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( N - 1 ) = ( ( # ` F ) - 1 ) )
61 60 fveq2d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F ` ( N - 1 ) ) = ( F ` ( ( # ` F ) - 1 ) ) )
62 lsw 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( lastS ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
63 62 adantr 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( lastS ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
64 61 63 eqtr4d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F ` ( N - 1 ) ) = ( lastS ` F ) )
65 64 s1eqd 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> <" ( F ` ( N - 1 ) ) "> = <" ( lastS ` F ) "> )
66 59 65 oveq12d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( F |` ( 0 ..^ ( N - 1 ) ) ) ++ <" ( F ` ( N - 1 ) ) "> ) = ( ( F |` ( 0 ..^ ( ( # ` F ) - 1 ) ) ) ++ <" ( lastS ` F ) "> ) )
67 53 56 66 3eqtr4d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F = ( ( F |` ( 0 ..^ ( N - 1 ) ) ) ++ <" ( F ` ( N - 1 ) ) "> ) )
68 67 fveq2d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( T ` F ) = ( T ` ( ( F |` ( 0 ..^ ( N - 1 ) ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) )
69 ffn 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> RR -> F Fn ( 0 ..^ ( # ` F ) ) )
70 9 11 69 3syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F Fn ( 0 ..^ ( # ` F ) ) )
71 5 a1i 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> N = ( # ` F ) )
72 71 oveq2d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) ) )
73 72 fneq2d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F Fn ( 0 ..^ N ) <-> F Fn ( 0 ..^ ( # ` F ) ) ) )
74 70 73 mpbird 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> F Fn ( 0 ..^ N ) )
75 5 14 eqeltrid 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> N e. NN )
76 75 nnnn0d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> N e. NN0 )
77 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
78 fzossrbm1 
 |-  ( N e. ZZ -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
79 76 77 78 3syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
80 fnssres 
 |-  ( ( F Fn ( 0 ..^ N ) /\ ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) ) -> ( F |` ( 0 ..^ ( N - 1 ) ) ) Fn ( 0 ..^ ( N - 1 ) ) )
81 74 79 80 syl2anc 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F |` ( 0 ..^ ( N - 1 ) ) ) Fn ( 0 ..^ ( N - 1 ) ) )
82 hashfn 
 |-  ( ( F |` ( 0 ..^ ( N - 1 ) ) ) Fn ( 0 ..^ ( N - 1 ) ) -> ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) = ( # ` ( 0 ..^ ( N - 1 ) ) ) )
83 81 82 syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) = ( # ` ( 0 ..^ ( N - 1 ) ) ) )
84 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
85 hashfzo0 
 |-  ( ( N - 1 ) e. NN0 -> ( # ` ( 0 ..^ ( N - 1 ) ) ) = ( N - 1 ) )
86 75 84 85 3syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( # ` ( 0 ..^ ( N - 1 ) ) ) = ( N - 1 ) )
87 83 86 eqtrd 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) = ( N - 1 ) )
88 87 eqcomd 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( N - 1 ) = ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) )
89 68 88 fveq12d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( ( T ` ( ( F |` ( 0 ..^ ( N - 1 ) ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ) )
90 89 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( ( T ` ( ( F |` ( 0 ..^ ( N - 1 ) ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ) )
91 52 59 eqtr4d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F prefix ( ( # ` F ) - 1 ) ) = ( F |` ( 0 ..^ ( N - 1 ) ) ) )
92 pfxcl 
 |-  ( F e. Word RR -> ( F prefix ( ( # ` F ) - 1 ) ) e. Word RR )
93 9 92 syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F prefix ( ( # ` F ) - 1 ) ) e. Word RR )
94 91 93 eqeltrrd 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F |` ( 0 ..^ ( N - 1 ) ) ) e. Word RR )
95 94 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( F |` ( 0 ..^ ( N - 1 ) ) ) e. Word RR )
96 87 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) = ( N - 1 ) )
97 75 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> N e. NN )
98 97 nncnd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> N e. CC )
99 1cnd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> 1 e. CC )
100 simpr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> N =/= 1 )
101 98 99 100 subne0d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( N - 1 ) =/= 0 )
102 96 101 eqnetrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) =/= 0 )
103 fveq2 
 |-  ( ( F |` ( 0 ..^ ( N - 1 ) ) ) = (/) -> ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) = ( # ` (/) ) )
104 hash0 
 |-  ( # ` (/) ) = 0
105 103 104 eqtrdi 
 |-  ( ( F |` ( 0 ..^ ( N - 1 ) ) ) = (/) -> ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) = 0 )
106 105 necon3i 
 |-  ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) =/= 0 -> ( F |` ( 0 ..^ ( N - 1 ) ) ) =/= (/) )
107 102 106 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( F |` ( 0 ..^ ( N - 1 ) ) ) =/= (/) )
108 95 107 jca 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( F |` ( 0 ..^ ( N - 1 ) ) ) e. Word RR /\ ( F |` ( 0 ..^ ( N - 1 ) ) ) =/= (/) ) )
109 eldifsn 
 |-  ( ( F |` ( 0 ..^ ( N - 1 ) ) ) e. ( Word RR \ { (/) } ) <-> ( ( F |` ( 0 ..^ ( N - 1 ) ) ) e. Word RR /\ ( F |` ( 0 ..^ ( N - 1 ) ) ) =/= (/) ) )
110 108 109 sylibr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( F |` ( 0 ..^ ( N - 1 ) ) ) e. ( Word RR \ { (/) } ) )
111 41 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( F ` ( N - 1 ) ) e. RR )
112 1 2 3 4 signstfvn 
 |-  ( ( ( F |` ( 0 ..^ ( N - 1 ) ) ) e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) e. RR ) -> ( ( T ` ( ( F |` ( 0 ..^ ( N - 1 ) ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ) = ( ( ( T ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) - 1 ) ) .+^ ( sgn ` ( F ` ( N - 1 ) ) ) ) )
113 110 111 112 syl2anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( T ` ( ( F |` ( 0 ..^ ( N - 1 ) ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ) = ( ( ( T ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) - 1 ) ) .+^ ( sgn ` ( F ` ( N - 1 ) ) ) ) )
114 lennncl 
 |-  ( ( ( F |` ( 0 ..^ ( N - 1 ) ) ) e. Word RR /\ ( F |` ( 0 ..^ ( N - 1 ) ) ) =/= (/) ) -> ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) e. NN )
115 fzo0end 
 |-  ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) e. NN -> ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) - 1 ) e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ) )
116 108 114 115 3syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) - 1 ) e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ) )
117 1 2 3 4 signstcl 
 |-  ( ( ( F |` ( 0 ..^ ( N - 1 ) ) ) e. Word RR /\ ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) - 1 ) e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ) ) -> ( ( T ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) - 1 ) ) e. { -u 1 , 0 , 1 } )
118 95 116 117 syl2anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( T ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) - 1 ) ) e. { -u 1 , 0 , 1 } )
119 44 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } )
120 simpr 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( F ` ( N - 1 ) ) =/= 0 )
121 sgn0bi 
 |-  ( ( F ` ( N - 1 ) ) e. RR* -> ( ( sgn ` ( F ` ( N - 1 ) ) ) = 0 <-> ( F ` ( N - 1 ) ) = 0 ) )
122 121 necon3bid 
 |-  ( ( F ` ( N - 1 ) ) e. RR* -> ( ( sgn ` ( F ` ( N - 1 ) ) ) =/= 0 <-> ( F ` ( N - 1 ) ) =/= 0 ) )
123 122 biimpar 
 |-  ( ( ( F ` ( N - 1 ) ) e. RR* /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( sgn ` ( F ` ( N - 1 ) ) ) =/= 0 )
124 42 120 123 syl2anc 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( sgn ` ( F ` ( N - 1 ) ) ) =/= 0 )
125 124 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( sgn ` ( F ` ( N - 1 ) ) ) =/= 0 )
126 1 2 signswlid 
 |-  ( ( ( ( ( T ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) - 1 ) ) e. { -u 1 , 0 , 1 } /\ ( sgn ` ( F ` ( N - 1 ) ) ) e. { -u 1 , 0 , 1 } ) /\ ( sgn ` ( F ` ( N - 1 ) ) ) =/= 0 ) -> ( ( ( T ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) - 1 ) ) .+^ ( sgn ` ( F ` ( N - 1 ) ) ) ) = ( sgn ` ( F ` ( N - 1 ) ) ) )
127 118 119 125 126 syl21anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( ( T ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) ` ( ( # ` ( F |` ( 0 ..^ ( N - 1 ) ) ) ) - 1 ) ) .+^ ( sgn ` ( F ` ( N - 1 ) ) ) ) = ( sgn ` ( F ` ( N - 1 ) ) ) )
128 90 113 127 3eqtrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) /\ N =/= 1 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( sgn ` ( F ` ( N - 1 ) ) ) )
129 48 128 pm2.61dane 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( sgn ` ( F ` ( N - 1 ) ) ) )