Metamath Proof Explorer

Theorem signsvf0

Description: There is no change of sign in the empty 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 signsvf0 ⊢ V ⁡ ∅ = 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 wrd0 ⊢ ∅ ∈ Word ℝ
6 1 2 3 4 signsvvfval ⊢ ∅ ∈ Word ℝ → V ⁡ ∅ = ∑ j ∈ 1 ..^ ∅ if T ⁡ ∅ ⁡ j ≠ T ⁡ ∅ ⁡ j − 1 1 0
7 5 6 ax-mp ⊢ V ⁡ ∅ = ∑ j ∈ 1 ..^ ∅ if T ⁡ ∅ ⁡ j ≠ T ⁡ ∅ ⁡ j − 1 1 0
8 hash0 ⊢ ∅ = 0
9 8 oveq2i ⊢ 1 ..^ ∅ = 1 ..^ 0
10 0le1 ⊢ 0 ≤ 1
11 1z ⊢ 1 ∈ ℤ
12 0z ⊢ 0 ∈ ℤ
13 fzon ⊢ 1 ∈ ℤ ∧ 0 ∈ ℤ → 0 ≤ 1 ↔ 1 ..^ 0 = ∅
14 11 12 13 mp2an ⊢ 0 ≤ 1 ↔ 1 ..^ 0 = ∅
15 10 14 mpbi ⊢ 1 ..^ 0 = ∅
16 9 15 eqtri ⊢ 1 ..^ ∅ = ∅
17 16 sumeq1i ⊢ ∑ j ∈ 1 ..^ ∅ if T ⁡ ∅ ⁡ j ≠ T ⁡ ∅ ⁡ j − 1 1 0 = ∑ j ∈ ∅ if T ⁡ ∅ ⁡ j ≠ T ⁡ ∅ ⁡ j − 1 1 0
18 sum0 ⊢ ∑ j ∈ ∅ if T ⁡ ∅ ⁡ j ≠ T ⁡ ∅ ⁡ j − 1 1 0 = 0
19 7 17 18 3eqtri ⊢ V ⁡ ∅ = 0