Metamath Proof Explorer

Theorem signstfveq0

Description: In case the last letter is zero, the zero skipping sign is the same as the previous letter. (Contributed by Thierry Arnoux, 11-Oct-2018) (Proof shortened by AV, 4-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 ) )
signstfveq0.1 
|- N = ( # ` F )
Assertion signstfveq0 
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( ( T ` F ) ` ( N - 2 ) ) )

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 signstfveq0.1 
 |-  N = ( # ` F )
6 simpll 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> F e. ( Word RR \ { (/) } ) )
7 6 eldifad 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> F e. Word RR )
8 pfxcl 
 |-  ( F e. Word RR -> ( F prefix ( N - 1 ) ) e. Word RR )
9 7 8 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F prefix ( N - 1 ) ) e. Word RR )
10 1nn0 
 |-  1 e. NN0
11 10 a1i 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> 1 e. NN0 )
12 11 nn0red 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> 1 e. RR )
13 2re 
 |-  2 e. RR
14 13 a1i 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> 2 e. RR )
15 lencl 
 |-  ( F e. Word RR -> ( # ` F ) e. NN0 )
16 7 15 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( # ` F ) e. NN0 )
17 5 16 eqeltrid 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N e. NN0 )
18 17 nn0red 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N e. RR )
19 1le2 
 |-  1 <_ 2
20 19 a1i 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> 1 <_ 2 )
21 1 2 3 4 5 signstfveq0a 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N e. ( ZZ>= ` 2 ) )
22 eluz2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) )
23 21 22 sylib 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) )
24 23 simp3d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> 2 <_ N )
25 12 14 18 20 24 letrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> 1 <_ N )
26 fznn0 
 |-  ( N e. NN0 -> ( 1 e. ( 0 ... N ) <-> ( 1 e. NN0 /\ 1 <_ N ) ) )
27 17 26 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( 1 e. ( 0 ... N ) <-> ( 1 e. NN0 /\ 1 <_ N ) ) )
28 11 25 27 mpbir2and 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> 1 e. ( 0 ... N ) )
29 fznn0sub2 
 |-  ( 1 e. ( 0 ... N ) -> ( N - 1 ) e. ( 0 ... N ) )
30 28 29 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( N - 1 ) e. ( 0 ... N ) )
31 5 oveq2i 
 |-  ( 0 ... N ) = ( 0 ... ( # ` F ) )
32 30 31 eleqtrdi 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( N - 1 ) e. ( 0 ... ( # ` F ) ) )
33 pfxlen 
 |-  ( ( F e. Word RR /\ ( N - 1 ) e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F prefix ( N - 1 ) ) ) = ( N - 1 ) )
34 7 32 33 syl2anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( # ` ( F prefix ( N - 1 ) ) ) = ( N - 1 ) )
35 uz2m1nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
36 21 35 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( N - 1 ) e. NN )
37 34 36 eqeltrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( # ` ( F prefix ( N - 1 ) ) ) e. NN )
38 nnne0 
 |-  ( ( # ` ( F prefix ( N - 1 ) ) ) e. NN -> ( # ` ( F prefix ( N - 1 ) ) ) =/= 0 )
39 fveq2 
 |-  ( ( F prefix ( N - 1 ) ) = (/) -> ( # ` ( F prefix ( N - 1 ) ) ) = ( # ` (/) ) )
40 hash0 
 |-  ( # ` (/) ) = 0
41 39 40 eqtrdi 
 |-  ( ( F prefix ( N - 1 ) ) = (/) -> ( # ` ( F prefix ( N - 1 ) ) ) = 0 )
42 41 necon3i 
 |-  ( ( # ` ( F prefix ( N - 1 ) ) ) =/= 0 -> ( F prefix ( N - 1 ) ) =/= (/) )
43 38 42 syl 
 |-  ( ( # ` ( F prefix ( N - 1 ) ) ) e. NN -> ( F prefix ( N - 1 ) ) =/= (/) )
44 37 43 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F prefix ( N - 1 ) ) =/= (/) )
45 eldifsn 
 |-  ( ( F prefix ( N - 1 ) ) e. ( Word RR \ { (/) } ) <-> ( ( F prefix ( N - 1 ) ) e. Word RR /\ ( F prefix ( N - 1 ) ) =/= (/) ) )
46 9 44 45 sylanbrc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F prefix ( N - 1 ) ) e. ( Word RR \ { (/) } ) )
47 simpr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F ` ( N - 1 ) ) = 0 )
48 0re 
 |-  0 e. RR
49 47 48 eqeltrdi 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F ` ( N - 1 ) ) e. RR )
50 1 2 3 4 signstfvn 
 |-  ( ( ( F prefix ( N - 1 ) ) e. ( Word RR \ { (/) } ) /\ ( F ` ( N - 1 ) ) e. RR ) -> ( ( T ` ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F prefix ( N - 1 ) ) ) ) = ( ( ( T ` ( F prefix ( N - 1 ) ) ) ` ( ( # ` ( F prefix ( N - 1 ) ) ) - 1 ) ) .+^ ( sgn ` ( F ` ( N - 1 ) ) ) ) )
51 46 49 50 syl2anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( T ` ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F prefix ( N - 1 ) ) ) ) = ( ( ( T ` ( F prefix ( N - 1 ) ) ) ` ( ( # ` ( F prefix ( N - 1 ) ) ) - 1 ) ) .+^ ( sgn ` ( F ` ( N - 1 ) ) ) ) )
52 5 oveq1i 
 |-  ( N - 1 ) = ( ( # ` F ) - 1 )
53 52 oveq2i 
 |-  ( F prefix ( N - 1 ) ) = ( F prefix ( ( # ` F ) - 1 ) )
54 53 a1i 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F prefix ( N - 1 ) ) = ( F prefix ( ( # ` F ) - 1 ) ) )
55 lsw 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( lastS ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
56 55 ad2antrr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( lastS ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
57 5 eqcomi 
 |-  ( # ` F ) = N
58 57 oveq1i 
 |-  ( ( # ` F ) - 1 ) = ( N - 1 )
59 58 fveq2i 
 |-  ( F ` ( ( # ` F ) - 1 ) ) = ( F ` ( N - 1 ) )
60 56 59 eqtrdi 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( lastS ` F ) = ( F ` ( N - 1 ) ) )
61 60 s1eqd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> <" ( lastS ` F ) "> = <" ( F ` ( N - 1 ) ) "> )
62 61 eqcomd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> <" ( F ` ( N - 1 ) ) "> = <" ( lastS ` F ) "> )
63 54 62 oveq12d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) = ( ( F prefix ( ( # ` F ) - 1 ) ) ++ <" ( lastS ` F ) "> ) )
64 eldifsn 
 |-  ( F e. ( Word RR \ { (/) } ) <-> ( F e. Word RR /\ F =/= (/) ) )
65 6 64 sylib 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( F e. Word RR /\ F =/= (/) ) )
66 pfxlswccat 
 |-  ( ( F e. Word RR /\ F =/= (/) ) -> ( ( F prefix ( ( # ` F ) - 1 ) ) ++ <" ( lastS ` F ) "> ) = F )
67 65 66 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( F prefix ( ( # ` F ) - 1 ) ) ++ <" ( lastS ` F ) "> ) = F )
68 63 67 eqtrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) = F )
69 68 fveq2d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( T ` ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) = ( T ` F ) )
70 69 34 fveq12d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( T ` ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) ` ( # ` ( F prefix ( N - 1 ) ) ) ) = ( ( T ` F ) ` ( N - 1 ) ) )
71 17 nn0cnd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N e. CC )
72 1cnd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> 1 e. CC )
73 71 72 72 subsub4d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( N - 1 ) - 1 ) = ( N - ( 1 + 1 ) ) )
74 1p1e2 
 |-  ( 1 + 1 ) = 2
75 74 oveq2i 
 |-  ( N - ( 1 + 1 ) ) = ( N - 2 )
76 73 75 eqtrdi 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( N - 1 ) - 1 ) = ( N - 2 ) )
77 fzo0end 
 |-  ( ( N - 1 ) e. NN -> ( ( N - 1 ) - 1 ) e. ( 0 ..^ ( N - 1 ) ) )
78 36 77 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( N - 1 ) - 1 ) e. ( 0 ..^ ( N - 1 ) ) )
79 76 78 eqeltrrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( N - 2 ) e. ( 0 ..^ ( N - 1 ) ) )
80 34 oveq2d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( 0 ..^ ( # ` ( F prefix ( N - 1 ) ) ) ) = ( 0 ..^ ( N - 1 ) ) )
81 79 80 eleqtrrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( N - 2 ) e. ( 0 ..^ ( # ` ( F prefix ( N - 1 ) ) ) ) )
82 1 2 3 4 signstfvp 
 |-  ( ( ( F prefix ( N - 1 ) ) e. Word RR /\ ( F ` ( N - 1 ) ) e. RR /\ ( N - 2 ) e. ( 0 ..^ ( # ` ( F prefix ( N - 1 ) ) ) ) ) -> ( ( T ` ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) ` ( N - 2 ) ) = ( ( T ` ( F prefix ( N - 1 ) ) ) ` ( N - 2 ) ) )
83 9 49 81 82 syl3anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( T ` ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) ` ( N - 2 ) ) = ( ( T ` ( F prefix ( N - 1 ) ) ) ` ( N - 2 ) ) )
84 68 eqcomd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> F = ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) )
85 84 fveq2d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( T ` F ) = ( T ` ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) )
86 85 fveq1d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( T ` F ) ` ( N - 2 ) ) = ( ( T ` ( ( F prefix ( N - 1 ) ) ++ <" ( F ` ( N - 1 ) ) "> ) ) ` ( N - 2 ) ) )
87 34 oveq1d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( # ` ( F prefix ( N - 1 ) ) ) - 1 ) = ( ( N - 1 ) - 1 ) )
88 87 73 eqtrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( # ` ( F prefix ( N - 1 ) ) ) - 1 ) = ( N - ( 1 + 1 ) ) )
89 88 75 eqtrdi 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( # ` ( F prefix ( N - 1 ) ) ) - 1 ) = ( N - 2 ) )
90 89 fveq2d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( T ` ( F prefix ( N - 1 ) ) ) ` ( ( # ` ( F prefix ( N - 1 ) ) ) - 1 ) ) = ( ( T ` ( F prefix ( N - 1 ) ) ) ` ( N - 2 ) ) )
91 83 86 90 3eqtr4rd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( T ` ( F prefix ( N - 1 ) ) ) ` ( ( # ` ( F prefix ( N - 1 ) ) ) - 1 ) ) = ( ( T ` F ) ` ( N - 2 ) ) )
92 fveq2 
 |-  ( ( F ` ( N - 1 ) ) = 0 -> ( sgn ` ( F ` ( N - 1 ) ) ) = ( sgn ` 0 ) )
93 sgn0 
 |-  ( sgn ` 0 ) = 0
94 92 93 eqtrdi 
 |-  ( ( F ` ( N - 1 ) ) = 0 -> ( sgn ` ( F ` ( N - 1 ) ) ) = 0 )
95 94 adantl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( sgn ` ( F ` ( N - 1 ) ) ) = 0 )
96 91 95 oveq12d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( ( T ` ( F prefix ( N - 1 ) ) ) ` ( ( # ` ( F prefix ( N - 1 ) ) ) - 1 ) ) .+^ ( sgn ` ( F ` ( N - 1 ) ) ) ) = ( ( ( T ` F ) ` ( N - 2 ) ) .+^ 0 ) )
97 uznn0sub 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. NN0 )
98 21 97 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( N - 2 ) e. NN0 )
99 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
100 21 99 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> N e. NN )
101 2rp 
 |-  2 e. RR+
102 101 a1i 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> 2 e. RR+ )
103 18 102 ltsubrpd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( N - 2 ) < N )
104 elfzo0 
 |-  ( ( N - 2 ) e. ( 0 ..^ N ) <-> ( ( N - 2 ) e. NN0 /\ N e. NN /\ ( N - 2 ) < N ) )
105 98 100 103 104 syl3anbrc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( N - 2 ) e. ( 0 ..^ N ) )
106 5 oveq2i 
 |-  ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) )
107 105 106 eleqtrdi 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( N - 2 ) e. ( 0 ..^ ( # ` F ) ) )
108 1 2 3 4 signstcl 
 |-  ( ( F e. Word RR /\ ( N - 2 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` ( N - 2 ) ) e. { -u 1 , 0 , 1 } )
109 7 107 108 syl2anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( T ` F ) ` ( N - 2 ) ) e. { -u 1 , 0 , 1 } )
110 1 2 signswrid 
 |-  ( ( ( T ` F ) ` ( N - 2 ) ) e. { -u 1 , 0 , 1 } -> ( ( ( T ` F ) ` ( N - 2 ) ) .+^ 0 ) = ( ( T ` F ) ` ( N - 2 ) ) )
111 109 110 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( ( T ` F ) ` ( N - 2 ) ) .+^ 0 ) = ( ( T ` F ) ` ( N - 2 ) ) )
112 96 111 eqtrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( ( T ` ( F prefix ( N - 1 ) ) ) ` ( ( # ` ( F prefix ( N - 1 ) ) ) - 1 ) ) .+^ ( sgn ` ( F ` ( N - 1 ) ) ) ) = ( ( T ` F ) ` ( N - 2 ) ) )
113 51 70 112 3eqtr3d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( F ` ( N - 1 ) ) = 0 ) -> ( ( T ` F ) ` ( N - 1 ) ) = ( ( T ` F ) ` ( N - 2 ) ) )