signlem0

Description: Adding a zero as the highest coefficient does not change the parity of the sign changes. (Contributed by Thierry Arnoux, 12-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	signlem0	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to V (F ++ ⟨“ 0 ”⟩) = V (F)$

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		0re	$⊢ 0 \in ℝ$
6	1 2 3 4	signsvfn	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land 0 \in ℝ) \to V (F ++ ⟨“ 0 ”⟩) = V (F) + if (T (F) (\|F\| - 1) \cdot 0 < 0, 1, 0)$
7	5 6	mpan2	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to V (F ++ ⟨“ 0 ”⟩) = V (F) + if (T (F) (\|F\| - 1) \cdot 0 < 0, 1, 0)$
8	5	ltnri	$⊢ \neg 0 < 0$
9		neg1cn	$⊢ - 1 \in ℂ$
10		ax-1cn	$⊢ 1 \in ℂ$
11		prssi	$⊢ (- 1 \in ℂ \land 1 \in ℂ) \to \{- 1, 1\} \subseteq ℂ$
12	9 10 11	mp2an	$⊢ \{- 1, 1\} \subseteq ℂ$
13		simpl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to F \in (Word ℝ ∖ \{\emptyset\})$
14		eldifsn	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \leftrightarrow (F \in Word ℝ \land F \neq \emptyset)$
15	13 14	sylib	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to (F \in Word ℝ \land F \neq \emptyset)$
16		lennncl	$⊢ (F \in Word ℝ \land F \neq \emptyset) \to \|F\| \in ℕ$
17		fzo0end	$⊢ \|F\| \in ℕ \to \|F\| - 1 \in (0 ..^\|F\|)$
18	15 16 17	3syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to \|F\| - 1 \in (0 ..^\|F\|)$
19	1 2 3 4	signstfvcl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land \|F\| - 1 \in (0 ..^\|F\|)) \to T (F) (\|F\| - 1) \in \{- 1, 1\}$
20	18 19	mpdan	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to T (F) (\|F\| - 1) \in \{- 1, 1\}$
21	12 20	sselid	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to T (F) (\|F\| - 1) \in ℂ$
22	21	mul01d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to T (F) (\|F\| - 1) \cdot 0 = 0$
23	22	breq1d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to (T (F) (\|F\| - 1) \cdot 0 < 0 \leftrightarrow 0 < 0)$
24	8 23	mtbiri	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to \neg T (F) (\|F\| - 1) \cdot 0 < 0$
25	24	iffalsed	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to if (T (F) (\|F\| - 1) \cdot 0 < 0, 1, 0) = 0$
26	25	oveq2d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to V (F) + if (T (F) (\|F\| - 1) \cdot 0 < 0, 1, 0) = V (F) + 0$
27	1 2 3 4	signsvvf	$⊢ V : Word ℝ ⟶ ℕ_{0}$
28	27	a1i	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to V : Word ℝ ⟶ ℕ_{0}$
29	13	eldifad	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to F \in Word ℝ$
30	28 29	ffvelcdmd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to V (F) \in ℕ_{0}$
31	30	nn0cnd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to V (F) \in ℂ$
32	31	addridd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to V (F) + 0 = V (F)$
33	7 26 32	3eqtrd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \to V (F ++ ⟨“ 0 ”⟩) = V (F)$

Metamath Proof Explorer

Theorem signlem0

Proof