Metamath Proof Explorer

Theorem signstfval

Description: Value of the zero-skipping sign word. (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 signstfval ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → T ⁡ F ⁡ N = ∑ W i = 0 N sgn ⁡ F ⁡ i

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 1 2 3 4 signstfv ⊢ F ∈ Word ℝ → T ⁡ F = n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i
6 5 adantr ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → T ⁡ F = n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i
7 simpr ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F ∧ n = N → n = N
8 7 oveq2d ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F ∧ n = N → 0 … n = 0 … N
9 8 mpteq1d ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F ∧ n = N → i ∈ 0 … n ⟼ sgn ⁡ F ⁡ i = i ∈ 0 … N ⟼ sgn ⁡ F ⁡ i
10 9 oveq2d ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F ∧ n = N → ∑ W i = 0 n sgn ⁡ F ⁡ i = ∑ W i = 0 N sgn ⁡ F ⁡ i
11 simpr ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → N ∈ 0 ..^ F
12 ovexd ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → ∑ W i = 0 N sgn ⁡ F ⁡ i ∈ V
13 6 10 11 12 fvmptd ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → T ⁡ F ⁡ N = ∑ W i = 0 N sgn ⁡ F ⁡ i