signstf

Description: The zero skipping sign word is a word. (Contributed by Thierry Arnoux, 8-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	signstf	$⊢ F \in Word ℝ \to T (F) \in Word ℝ$

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	signstfv	$⊢ F \in Word ℝ \to T (F) = (n \in (0 ..^\|F\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (F (i)))$
6		neg1rr	$⊢ - 1 \in ℝ$
7		0re	$⊢ 0 \in ℝ$
8		1re	$⊢ 1 \in ℝ$
9		tpssi	$⊢ (- 1 \in ℝ \land 0 \in ℝ \land 1 \in ℝ) \to \{- 1, 0, 1\} \subseteq ℝ$
10	6 7 8 9	mp3an	$⊢ \{- 1, 0, 1\} \subseteq ℝ$
11	1 2	signswbase	$⊢ \{- 1, 0, 1\} = {Base}_{W}$
12	1 2	signswmnd	$⊢ W \in Mnd$
13	12	a1i	$⊢ (F \in Word ℝ \land n \in (0 ..^\|F\|)) \to W \in Mnd$
14		fzo0ssnn0	$⊢ (0 ..^\|F\|) \subseteq ℕ_{0}$
15		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
16	14 15	sseqtri	$⊢ (0 ..^\|F\|) \subseteq ℤ_{\geq 0}$
17	16	a1i	$⊢ F \in Word ℝ \to (0 ..^\|F\|) \subseteq ℤ_{\geq 0}$
18	17	sselda	$⊢ (F \in Word ℝ \land n \in (0 ..^\|F\|)) \to n \in ℤ_{\geq 0}$
19		wrdf	$⊢ F \in Word ℝ \to F : (0 ..^\|F\|) ⟶ ℝ$
20	19	ad2antrr	$⊢ ((F \in Word ℝ \land n \in (0 ..^\|F\|)) \land i \in (0 \dots n)) \to F : (0 ..^\|F\|) ⟶ ℝ$
21		fzssfzo	$⊢ n \in (0 ..^\|F\|) \to (0 \dots n) \subseteq (0 ..^\|F\|)$
22	21	adantl	$⊢ (F \in Word ℝ \land n \in (0 ..^\|F\|)) \to (0 \dots n) \subseteq (0 ..^\|F\|)$
23	22	sselda	$⊢ ((F \in Word ℝ \land n \in (0 ..^\|F\|)) \land i \in (0 \dots n)) \to i \in (0 ..^\|F\|)$
24	20 23	ffvelrnd	$⊢ ((F \in Word ℝ \land n \in (0 ..^\|F\|)) \land i \in (0 \dots n)) \to F (i) \in ℝ$
25	24	rexrd	$⊢ ((F \in Word ℝ \land n \in (0 ..^\|F\|)) \land i \in (0 \dots n)) \to F (i) \in ℝ^{*}$
26		sgncl	$⊢ F (i) \in ℝ^{*} \to sgn (F (i)) \in \{- 1, 0, 1\}$
27	25 26	syl	$⊢ ((F \in Word ℝ \land n \in (0 ..^\|F\|)) \land i \in (0 \dots n)) \to sgn (F (i)) \in \{- 1, 0, 1\}$
28	11 13 18 27	gsumncl	$⊢ (F \in Word ℝ \land n \in (0 ..^\|F\|)) \to {\sum_{W}}_{i = 0}^{n} sgn (F (i)) \in \{- 1, 0, 1\}$
29	10 28	sselid	$⊢ (F \in Word ℝ \land n \in (0 ..^\|F\|)) \to {\sum_{W}}_{i = 0}^{n} sgn (F (i)) \in ℝ$
30	5 29	fmpt3d	$⊢ F \in Word ℝ \to T (F) : (0 ..^\|F\|) ⟶ ℝ$
31		iswrdi	$⊢ T (F) : (0 ..^\|F\|) ⟶ ℝ \to T (F) \in Word ℝ$
32	30 31	syl	$⊢ F \in Word ℝ \to T (F) \in Word ℝ$

Metamath Proof Explorer

Theorem signstf

Proof