Metamath Proof Explorer

Theorem signstcl

Description: Closure of the zero skipping sign word. (Contributed by Thierry Arnoux, 9-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 signstcl ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → T ⁡ F ⁡ N ∈ − 1 0 1

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 signstfval ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → T ⁡ F ⁡ N = ∑ W i = 0 N sgn ⁡ F ⁡ i
6 1 2 signswbase ⊢ − 1 0 1 = Base W
7 1 2 signswmnd ⊢ W ∈ Mnd
8 7 a1i ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → W ∈ Mnd
9 fzo0ssnn0 ⊢ 0 ..^ F ⊆ ℕ 0
10 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
11 9 10 sseqtri ⊢ 0 ..^ F ⊆ ℤ ≥ 0
12 11 a1i ⊢ F ∈ Word ℝ → 0 ..^ F ⊆ ℤ ≥ 0
13 12 sselda ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → N ∈ ℤ ≥ 0
14 wrdf ⊢ F ∈ Word ℝ → F : 0 ..^ F ⟶ ℝ
15 14 ad2antrr ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F ∧ i ∈ 0 … N → F : 0 ..^ F ⟶ ℝ
16 fzssfzo ⊢ N ∈ 0 ..^ F → 0 … N ⊆ 0 ..^ F
17 16 adantl ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → 0 … N ⊆ 0 ..^ F
18 17 sselda ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F ∧ i ∈ 0 … N → i ∈ 0 ..^ F
19 15 18 ffvelrnd ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F ∧ i ∈ 0 … N → F ⁡ i ∈ ℝ
20 19 rexrd ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F ∧ i ∈ 0 … N → F ⁡ i ∈ ℝ *
21 sgncl ⊢ F ⁡ i ∈ ℝ * → sgn ⁡ F ⁡ i ∈ − 1 0 1
22 20 21 syl ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F ∧ i ∈ 0 … N → sgn ⁡ F ⁡ i ∈ − 1 0 1
23 6 8 13 22 gsumncl ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → ∑ W i = 0 N sgn ⁡ F ⁡ i ∈ − 1 0 1
24 5 23 eqeltrd ⊢ F ∈ Word ℝ ∧ N ∈ 0 ..^ F → T ⁡ F ⁡ N ∈ − 1 0 1