Metamath Proof Explorer

Theorem signstfvn

Description: Zero-skipping sign in a word compared to a shorter 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 signstfvn 
|- ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) )

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 signswbase 
 |-  { -u 1 , 0 , 1 } = ( Base ` W )
6 1 2 signswmnd 
 |-  W e. Mnd
7 6 a1i 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> W e. Mnd )
8 eldifi 
 |-  ( F e. ( Word RR \ { (/) } ) -> F e. Word RR )
9 lencl 
 |-  ( F e. Word RR -> ( # ` F ) e. NN0 )
10 8 9 syl 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( # ` F ) e. NN0 )
11 eldifsn 
 |-  ( F e. ( Word RR \ { (/) } ) <-> ( F e. Word RR /\ F =/= (/) ) )
12 hasheq0 
 |-  ( F e. Word RR -> ( ( # ` F ) = 0 <-> F = (/) ) )
13 12 necon3bid 
 |-  ( F e. Word RR -> ( ( # ` F ) =/= 0 <-> F =/= (/) ) )
14 13 biimpar 
 |-  ( ( F e. Word RR /\ F =/= (/) ) -> ( # ` F ) =/= 0 )
15 11 14 sylbi 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( # ` F ) =/= 0 )
16 elnnne0 
 |-  ( ( # ` F ) e. NN <-> ( ( # ` F ) e. NN0 /\ ( # ` F ) =/= 0 ) )
17 10 15 16 sylanbrc 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( # ` F ) e. NN )
18 17 adantr 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( # ` F ) e. NN )
19 nnm1nn0 
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. NN0 )
20 18 19 syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( # ` F ) - 1 ) e. NN0 )
21 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
22 20 21 eleqtrdi 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( # ` F ) - 1 ) e. ( ZZ>= ` 0 ) )
23 ccatws1cl 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( F ++ <" K "> ) e. Word RR )
24 23 adantr 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( F ++ <" K "> ) e. Word RR )
25 wrdf 
 |-  ( ( F ++ <" K "> ) e. Word RR -> ( F ++ <" K "> ) : ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) --> RR )
26 24 25 syl 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( F ++ <" K "> ) : ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) --> RR )
27 9 nn0zd 
 |-  ( F e. Word RR -> ( # ` F ) e. ZZ )
28 fzoval 
 |-  ( ( # ` F ) e. ZZ -> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) )
29 27 28 syl 
 |-  ( F e. Word RR -> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) )
30 29 adantr 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) )
31 fzossfz 
 |-  ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
32 30 31 eqsstrrdi 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ... ( ( # ` F ) - 1 ) ) C_ ( 0 ... ( # ` F ) ) )
33 s1cl 
 |-  ( K e. RR -> <" K "> e. Word RR )
34 ccatlen 
 |-  ( ( F e. Word RR /\ <" K "> e. Word RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
35 33 34 sylan2 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
36 s1len 
 |-  ( # ` <" K "> ) = 1
37 36 oveq2i 
 |-  ( ( # ` F ) + ( # ` <" K "> ) ) = ( ( # ` F ) + 1 )
38 35 37 eqtrdi 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + 1 ) )
39 38 oveq2d 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
40 27 adantr 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` F ) e. ZZ )
41 40 peano2zd 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( ( # ` F ) + 1 ) e. ZZ )
42 fzoval 
 |-  ( ( ( # ` F ) + 1 ) e. ZZ -> ( 0 ..^ ( ( # ` F ) + 1 ) ) = ( 0 ... ( ( ( # ` F ) + 1 ) - 1 ) ) )
43 41 42 syl 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ..^ ( ( # ` F ) + 1 ) ) = ( 0 ... ( ( ( # ` F ) + 1 ) - 1 ) ) )
44 9 nn0cnd 
 |-  ( F e. Word RR -> ( # ` F ) e. CC )
45 1cnd 
 |-  ( F e. Word RR -> 1 e. CC )
46 44 45 pncand 
 |-  ( F e. Word RR -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) )
47 46 adantr 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) )
48 47 oveq2d 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ... ( ( ( # ` F ) + 1 ) - 1 ) ) = ( 0 ... ( # ` F ) ) )
49 39 43 48 3eqtrd 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) = ( 0 ... ( # ` F ) ) )
50 32 49 sseqtrrd 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ... ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) )
51 50 sselda 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> i e. ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) )
52 26 51 ffvelcdmd 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( ( F ++ <" K "> ) ` i ) e. RR )
53 8 52 sylanl1 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( ( F ++ <" K "> ) ` i ) e. RR )
54 53 rexrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( ( F ++ <" K "> ) ` i ) e. RR* )
55 sgncl 
 |-  ( ( ( F ++ <" K "> ) ` i ) e. RR* -> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) e. { -u 1 , 0 , 1 } )
56 54 55 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) e. { -u 1 , 0 , 1 } )
57 1 2 signswplusg 
 |-  .+^ = ( +g ` W )
58 rexr 
 |-  ( K e. RR -> K e. RR* )
59 sgncl 
 |-  ( K e. RR* -> ( sgn ` K ) e. { -u 1 , 0 , 1 } )
60 58 59 syl 
 |-  ( K e. RR -> ( sgn ` K ) e. { -u 1 , 0 , 1 } )
61 60 adantl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( sgn ` K ) e. { -u 1 , 0 , 1 } )
62 id 
 |-  ( i = ( ( ( # ` F ) - 1 ) + 1 ) -> i = ( ( ( # ` F ) - 1 ) + 1 ) )
63 44 45 npcand 
 |-  ( F e. Word RR -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
64 63 adantr 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
65 62 64 sylan9eqr 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> i = ( # ` F ) )
66 65 fveq2d 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> ( ( F ++ <" K "> ) ` i ) = ( ( F ++ <" K "> ) ` ( # ` F ) ) )
67 ccatws1ls 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( ( F ++ <" K "> ) ` ( # ` F ) ) = K )
68 67 adantr 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> ( ( F ++ <" K "> ) ` ( # ` F ) ) = K )
69 66 68 eqtrd 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> ( ( F ++ <" K "> ) ` i ) = K )
70 8 69 sylanl1 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> ( ( F ++ <" K "> ) ` i ) = K )
71 70 fveq2d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) = ( sgn ` K ) )
72 5 7 22 56 57 61 71 gsumnunsn 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( W gsum ( i e. ( 0 ... ( ( ( # ` F ) - 1 ) + 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) = ( ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) .+^ ( sgn ` K ) ) )
73 8 63 syl 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
74 73 adantr 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
75 74 oveq2d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( 0 ... ( ( ( # ` F ) - 1 ) + 1 ) ) = ( 0 ... ( # ` F ) ) )
76 75 mpteq1d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( i e. ( 0 ... ( ( ( # ` F ) - 1 ) + 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) = ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) )
77 76 oveq2d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( W gsum ( i e. ( 0 ... ( ( ( # ` F ) - 1 ) + 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) = ( W gsum ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) )
78 simpll 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> F e. Word RR )
79 33 ad2antlr 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> <" K "> e. Word RR )
80 30 eleq2d 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( i e. ( 0 ..^ ( # ` F ) ) <-> i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) )
81 80 biimpar 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> i e. ( 0 ..^ ( # ` F ) ) )
82 ccatval1 
 |-  ( ( F e. Word RR /\ <" K "> e. Word RR /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F ++ <" K "> ) ` i ) = ( F ` i ) )
83 78 79 81 82 syl3anc 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( ( F ++ <" K "> ) ` i ) = ( F ` i ) )
84 83 fveq2d 
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) = ( sgn ` ( F ` i ) ) )
85 84 mpteq2dva 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) = ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) )
86 8 85 sylan 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) = ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) )
87 86 oveq2d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) = ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) )
88 87 oveq1d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) .+^ ( sgn ` K ) ) = ( ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) .+^ ( sgn ` K ) ) )
89 72 77 88 3eqtr3d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( W gsum ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) = ( ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) .+^ ( sgn ` K ) ) )
90 eqid 
 |-  ( # ` F ) = ( # ` F )
91 90 olci 
 |-  ( ( # ` F ) e. ( 0 ..^ ( # ` F ) ) \/ ( # ` F ) = ( # ` F ) )
92 9 21 eleqtrdi 
 |-  ( F e. Word RR -> ( # ` F ) e. ( ZZ>= ` 0 ) )
93 fzosplitsni 
 |-  ( ( # ` F ) e. ( ZZ>= ` 0 ) -> ( ( # ` F ) e. ( 0 ..^ ( ( # ` F ) + 1 ) ) <-> ( ( # ` F ) e. ( 0 ..^ ( # ` F ) ) \/ ( # ` F ) = ( # ` F ) ) ) )
94 92 93 syl 
 |-  ( F e. Word RR -> ( ( # ` F ) e. ( 0 ..^ ( ( # ` F ) + 1 ) ) <-> ( ( # ` F ) e. ( 0 ..^ ( # ` F ) ) \/ ( # ` F ) = ( # ` F ) ) ) )
95 91 94 mpbiri 
 |-  ( F e. Word RR -> ( # ` F ) e. ( 0 ..^ ( ( # ` F ) + 1 ) ) )
96 95 adantr 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` F ) e. ( 0 ..^ ( ( # ` F ) + 1 ) ) )
97 96 39 eleqtrrd 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` F ) e. ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) )
98 1 2 3 4 signstfval 
 |-  ( ( ( F ++ <" K "> ) e. Word RR /\ ( # ` F ) e. ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( W gsum ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) )
99 23 97 98 syl2anc 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( W gsum ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) )
100 8 99 sylan 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( W gsum ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) )
101 fzo0end 
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
102 17 101 syl 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
103 1 2 3 4 signstfval 
 |-  ( ( F e. Word RR /\ ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) = ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) )
104 8 102 103 syl2anc 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) = ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) )
105 104 adantr 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) = ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) )
106 105 oveq1d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) = ( ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) .+^ ( sgn ` K ) ) )
107 89 100 106 3eqtr4d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) )