Metamath Proof Explorer

Theorem signshwrd

Description: H , corresponding to the word F multiplied by ( x - C ) , is a word. (Contributed by Thierry Arnoux, 29-Sep-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 signshwrd ⊢ F ∈ Word ℝ ∧ C ∈ ℝ + → H ∈ Word ℝ

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 iswrdi ⊢ H : 0 ..^ F + 1 ⟶ ℝ → H ∈ Word ℝ
8 6 7 syl ⊢ F ∈ Word ℝ ∧ C ∈ ℝ + → H ∈ Word ℝ