signshnz

Description: H is not the empty word. (Contributed by Thierry Arnoux, 14-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))$
	signs.h	$⊢ H = (⟨“ 0 ”⟩ ++ F) -_{f} ((F ++ ⟨“ 0 ”⟩) \circ_{fc} \times C)$
Assertion	signshnz	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to H \neq \emptyset$

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		signs.h	$⊢ H = (⟨“ 0 ”⟩ ++ F) -_{f} ((F ++ ⟨“ 0 ”⟩) \circ_{fc} \times C)$
6	1 2 3 4 5	signshlen	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|H\| = \|F\| + 1$
7		lencl	$⊢ F \in Word ℝ \to \|F\| \in ℕ_{0}$
8	7	adantr	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|F\| \in ℕ_{0}$
9		nn0p1nn	$⊢ \|F\| \in ℕ_{0} \to \|F\| + 1 \in ℕ$
10	8 9	syl	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|F\| + 1 \in ℕ$
11	6 10	eqeltrd	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|H\| \in ℕ$
12	11	nnne0d	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|H\| \neq 0$
13	1 2 3 4 5	signshwrd	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to H \in Word ℝ$
14		hasheq0	$⊢ H \in Word ℝ \to (\|H\| = 0 \leftrightarrow H = \emptyset)$
15	13 14	syl	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to (\|H\| = 0 \leftrightarrow H = \emptyset)$
16	15	necon3bid	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to (\|H\| \neq 0 \leftrightarrow H \neq \emptyset)$
17	12 16	mpbid	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to H \neq \emptyset$

Metamath Proof Explorer