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