signstcl

Description: Closure of the zero skipping sign word. (Contributed by Thierry Arnoux, 9-Oct-2018)

	Ref	Expression
Hypotheses	signsv.p	$⊢ \underset{˙}{⨣} = (a \in \{- 1, 0, 1\}, b \in \{- 1, 0, 1\} ⟼ if (b = 0, a, b))$
	signsv.w	$⊢ W = \{⟨{Base}_{ndx}, \{- 1, 0, 1\}⟩, ⟨+_{ndx}, \underset{˙}{⨣}⟩\}$
	signsv.t	$⊢ T = (f \in Word ℝ ⟼ (n \in (0 ..^\|f\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (f (i))))$
	signsv.v	$⊢ V = (f \in Word ℝ ⟼ \sum_{j \in (1 ..^\|f\|)} if (T (f) (j) \neq T (f) (j - 1), 1, 0))$
Assertion	signstcl	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F) (N) \in \{- 1, 0, 1\}$

Proof

Step	Hyp	Ref	Expression
1		signsv.p	$⊢ \underset{˙}{⨣} = (a \in \{- 1, 0, 1\}, b \in \{- 1, 0, 1\} ⟼ if (b = 0, a, b))$
2		signsv.w	$⊢ W = \{⟨{Base}_{ndx}, \{- 1, 0, 1\}⟩, ⟨+_{ndx}, \underset{˙}{⨣}⟩\}$
3		signsv.t	$⊢ T = (f \in Word ℝ ⟼ (n \in (0 ..^\|f\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (f (i))))$
4		signsv.v	$⊢ V = (f \in Word ℝ ⟼ \sum_{j \in (1 ..^\|f\|)} if (T (f) (j) \neq T (f) (j - 1), 1, 0))$
5	1 2 3 4	signstfval	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F) (N) = {\sum_{W}}_{i = 0}^{N} sgn (F (i))$
6	1 2	signswbase	$⊢ \{- 1, 0, 1\} = {Base}_{W}$
7	1 2	signswmnd	$⊢ W \in Mnd$
8	7	a1i	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to W \in Mnd$
9		fzo0ssnn0	$⊢ (0 ..^\|F\|) \subseteq ℕ_{0}$
10		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
11	9 10	sseqtri	$⊢ (0 ..^\|F\|) \subseteq ℤ_{\geq 0}$
12	11	a1i	$⊢ F \in Word ℝ \to (0 ..^\|F\|) \subseteq ℤ_{\geq 0}$
13	12	sselda	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to N \in ℤ_{\geq 0}$
14		wrdf	$⊢ F \in Word ℝ \to F : (0 ..^\|F\|) ⟶ ℝ$
15	14	ad2antrr	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land i \in (0 \dots N)) \to F : (0 ..^\|F\|) ⟶ ℝ$
16		fzssfzo	$⊢ N \in (0 ..^\|F\|) \to (0 \dots N) \subseteq (0 ..^\|F\|)$
17	16	adantl	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to (0 \dots N) \subseteq (0 ..^\|F\|)$
18	17	sselda	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land i \in (0 \dots N)) \to i \in (0 ..^\|F\|)$
19	15 18	ffvelcdmd	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land i \in (0 \dots N)) \to F (i) \in ℝ$
20	19	rexrd	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land i \in (0 \dots N)) \to F (i) \in ℝ^{*}$
21		sgncl	$⊢ F (i) \in ℝ^{*} \to sgn (F (i)) \in \{- 1, 0, 1\}$
22	20 21	syl	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land i \in (0 \dots N)) \to sgn (F (i)) \in \{- 1, 0, 1\}$
23	6 8 13 22	gsumncl	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to {\sum_{W}}_{i = 0}^{N} sgn (F (i)) \in \{- 1, 0, 1\}$
24	5 23	eqeltrd	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F) (N) \in \{- 1, 0, 1\}$

Metamath Proof Explorer

Theorem signstcl

Proof