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