Metamath Proof Explorer

Theorem signsvvf

Description: V is a function. (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 signsvvf ⊢ V : Word ℝ ⟶ ℕ 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 fzofi ⊢ 1 ..^ f ∈ Fin
6 5 a1i ⊢ f ∈ Word ℝ → 1 ..^ f ∈ Fin
7 1nn0 ⊢ 1 ∈ ℕ 0
8 7 a1i ⊢ f ∈ Word ℝ ∧ j ∈ 1 ..^ f ∧ T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 → 1 ∈ ℕ 0
9 0nn0 ⊢ 0 ∈ ℕ 0
10 9 a1i ⊢ f ∈ Word ℝ ∧ j ∈ 1 ..^ f ∧ ¬ T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 → 0 ∈ ℕ 0
11 8 10 ifclda ⊢ f ∈ Word ℝ ∧ j ∈ 1 ..^ f → if T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 1 0 ∈ ℕ 0
12 6 11 fsumnn0cl ⊢ f ∈ Word ℝ → ∑ j ∈ 1 ..^ f if T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 1 0 ∈ ℕ 0
13 4 12 fmpti ⊢ V : Word ℝ ⟶ ℕ 0