Metamath Proof Explorer

Theorem signsvf1

Description: In a single-letter word, which represents a constant polynomial, there is no change of sign. (Contributed by Thierry Arnoux, 8-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
Assertion signsvf1 ⊢ K ∈ ℝ → V ⁡ ⟨“ K ”⟩ = 0

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 s1cl ⊢ K ∈ ℝ → ⟨“ K ”⟩ ∈ Word ℝ
6 1 2 3 4 signsvvfval ⊢ ⟨“ K ”⟩ ∈ Word ℝ → V ⁡ ⟨“ K ”⟩ = ∑ j ∈ 1 ..^ ⟨“ K ”⟩ if T ⁡ ⟨“ K ”⟩ ⁡ j ≠ T ⁡ ⟨“ K ”⟩ ⁡ j − 1 1 0
7 5 6 syl ⊢ K ∈ ℝ → V ⁡ ⟨“ K ”⟩ = ∑ j ∈ 1 ..^ ⟨“ K ”⟩ if T ⁡ ⟨“ K ”⟩ ⁡ j ≠ T ⁡ ⟨“ K ”⟩ ⁡ j − 1 1 0
8 s1len ⊢ ⟨“ K ”⟩ = 1
9 8 oveq2i ⊢ 1 ..^ ⟨“ K ”⟩ = 1 ..^ 1
10 fzo0 ⊢ 1 ..^ 1 = ∅
11 9 10 eqtri ⊢ 1 ..^ ⟨“ K ”⟩ = ∅
12 11 sumeq1i ⊢ ∑ j ∈ 1 ..^ ⟨“ K ”⟩ if T ⁡ ⟨“ K ”⟩ ⁡ j ≠ T ⁡ ⟨“ K ”⟩ ⁡ j − 1 1 0 = ∑ j ∈ ∅ if T ⁡ ⟨“ K ”⟩ ⁡ j ≠ T ⁡ ⟨“ K ”⟩ ⁡ j − 1 1 0
13 sum0 ⊢ ∑ j ∈ ∅ if T ⁡ ⟨“ K ”⟩ ⁡ j ≠ T ⁡ ⟨“ K ”⟩ ⁡ j − 1 1 0 = 0
14 12 13 eqtri ⊢ ∑ j ∈ 1 ..^ ⟨“ K ”⟩ if T ⁡ ⟨“ K ”⟩ ⁡ j ≠ T ⁡ ⟨“ K ”⟩ ⁡ j − 1 1 0 = 0
15 7 14 eqtrdi ⊢ K ∈ ℝ → V ⁡ ⟨“ K ”⟩ = 0