Metamath Proof Explorer


Theorem signshlen

Description: Length of H , corresponding to the word F multiplied by ( x - C ) . (Contributed by Thierry Arnoux, 14-Oct-2018)

Ref Expression
Hypotheses signsv.p ˙ = a 1 0 1 , b 1 0 1 if b = 0 a b
signsv.w W = Base ndx 1 0 1 + ndx ˙
signsv.t T = f Word n 0 ..^ f W i = 0 n sgn f i
signsv.v V = f Word j 1 ..^ f if T f j T f j 1 1 0
signs.h H = ⟨“ 0 ”⟩ ++ F f F ++ ⟨“ 0 ”⟩ fc × C
Assertion signshlen F Word C + H = F + 1

Proof

Step Hyp Ref Expression
1 signsv.p ˙ = a 1 0 1 , b 1 0 1 if b = 0 a b
2 signsv.w W = Base ndx 1 0 1 + ndx ˙
3 signsv.t T = f Word n 0 ..^ f W i = 0 n sgn f i
4 signsv.v V = f Word j 1 ..^ f if T f j T f j 1 1 0
5 signs.h H = ⟨“ 0 ”⟩ ++ F f F ++ ⟨“ 0 ”⟩ fc × C
6 1 2 3 4 5 signshf F Word C + H : 0 ..^ F + 1
7 ffn H : 0 ..^ F + 1 H Fn 0 ..^ F + 1
8 hashfn H Fn 0 ..^ F + 1 H = 0 ..^ F + 1
9 6 7 8 3syl F Word C + H = 0 ..^ F + 1
10 lencl F Word F 0
11 10 adantr F Word C + F 0
12 1nn0 1 0
13 12 a1i F Word C + 1 0
14 11 13 nn0addcld F Word C + F + 1 0
15 hashfzo0 F + 1 0 0 ..^ F + 1 = F + 1
16 14 15 syl F Word C + 0 ..^ F + 1 = F + 1
17 9 16 eqtrd F Word C + H = F + 1