signstfveq0a

	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))$
	signstfveq0.1	$⊢ N = \|F\|$
Assertion	signstfveq0a	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \in ℤ_{\geq 2}$

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		signstfveq0.1	$⊢ N = \|F\|$
6		simpll	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F \in (Word ℝ ∖ \{\emptyset\})$
7	6	eldifad	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F \in Word ℝ$
8		lencl	$⊢ F \in Word ℝ \to \|F\| \in ℕ_{0}$
9	5 8	eqeltrid	$⊢ F \in Word ℝ \to N \in ℕ_{0}$
10	7 9	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \in ℕ_{0}$
11		eldifsn	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \leftrightarrow (F \in Word ℝ \land F \neq \emptyset)$
12	6 11	sylib	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to (F \in Word ℝ \land F \neq \emptyset)$
13		hasheq0	$⊢ F \in Word ℝ \to (\|F\| = 0 \leftrightarrow F = \emptyset)$
14	13	necon3bid	$⊢ F \in Word ℝ \to (\|F\| \neq 0 \leftrightarrow F \neq \emptyset)$
15	14	biimpar	$⊢ (F \in Word ℝ \land F \neq \emptyset) \to \|F\| \neq 0$
16	5	neeq1i	$⊢ N \neq 0 \leftrightarrow \|F\| \neq 0$
17	15 16	sylibr	$⊢ (F \in Word ℝ \land F \neq \emptyset) \to N \neq 0$
18	12 17	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \neq 0$
19		elnnne0	$⊢ N \in ℕ \leftrightarrow (N \in ℕ_{0} \land N \neq 0)$
20	10 18 19	sylanbrc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \in ℕ$
21		simplr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F (0) \neq 0$
22		simpr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F (N - 1) = 0$
23	21 22	neeqtrrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F (0) \neq F (N - 1)$
24	23	necomd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F (N - 1) \neq F (0)$
25		oveq1	$⊢ N = 1 \to N - 1 = 1 - 1$
26		1m1e0	$⊢ 1 - 1 = 0$
27	25 26	eqtrdi	$⊢ N = 1 \to N - 1 = 0$
28	27	fveq2d	$⊢ N = 1 \to F (N - 1) = F (0)$
29	28	necon3i	$⊢ F (N - 1) \neq F (0) \to N \neq 1$
30	24 29	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \neq 1$
31		eluz2b3	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land N \neq 1)$
32	20 30 31	sylanbrc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \in ℤ_{\geq 2}$

Metamath Proof Explorer

Theorem signstfveq0a

Proof