signstfvn

Description: Zero-skipping sign in a word compared to a shorter 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	signstfvn	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to T (F ++ ⟨“ K ”⟩) (\|F\|) = T (F) (\|F\| - 1) \underset{˙}{⨣} sgn (K)$

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	signswbase	$⊢ \{- 1, 0, 1\} = {Base}_{W}$
6	1 2	signswmnd	$⊢ W \in Mnd$
7	6	a1i	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to W \in Mnd$
8		eldifi	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to F \in Word ℝ$
9		lencl	$⊢ F \in Word ℝ \to \|F\| \in ℕ_{0}$
10	8 9	syl	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to \|F\| \in ℕ_{0}$
11		eldifsn	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \leftrightarrow (F \in Word ℝ \land F \neq \emptyset)$
12		hasheq0	$⊢ F \in Word ℝ \to (\|F\| = 0 \leftrightarrow F = \emptyset)$
13	12	necon3bid	$⊢ F \in Word ℝ \to (\|F\| \neq 0 \leftrightarrow F \neq \emptyset)$
14	13	biimpar	$⊢ (F \in Word ℝ \land F \neq \emptyset) \to \|F\| \neq 0$
15	11 14	sylbi	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to \|F\| \neq 0$
16		elnnne0	$⊢ \|F\| \in ℕ \leftrightarrow (\|F\| \in ℕ_{0} \land \|F\| \neq 0)$
17	10 15 16	sylanbrc	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to \|F\| \in ℕ$
18	17	adantr	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \|F\| \in ℕ$
19		nnm1nn0	$⊢ \|F\| \in ℕ \to \|F\| - 1 \in ℕ_{0}$
20	18 19	syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \|F\| - 1 \in ℕ_{0}$
21		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
22	20 21	eleqtrdi	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \|F\| - 1 \in ℤ_{\geq 0}$
23		ccatws1cl	$⊢ (F \in Word ℝ \land K \in ℝ) \to F ++ ⟨“ K ”⟩ \in Word ℝ$
24	23	adantr	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to F ++ ⟨“ K ”⟩ \in Word ℝ$
25		wrdf	$⊢ F ++ ⟨“ K ”⟩ \in Word ℝ \to (F ++ ⟨“ K ”⟩) : (0 ..^\|F ++ ⟨“ K ”⟩\|) ⟶ ℝ$
26	24 25	syl	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to (F ++ ⟨“ K ”⟩) : (0 ..^\|F ++ ⟨“ K ”⟩\|) ⟶ ℝ$
27	9	nn0zd	$⊢ F \in Word ℝ \to \|F\| \in ℤ$
28		fzoval	$⊢ \|F\| \in ℤ \to (0 ..^\|F\|) = (0 \dots \|F\| - 1)$
29	27 28	syl	$⊢ F \in Word ℝ \to (0 ..^\|F\|) = (0 \dots \|F\| - 1)$
30	29	adantr	$⊢ (F \in Word ℝ \land K \in ℝ) \to (0 ..^\|F\|) = (0 \dots \|F\| - 1)$
31		fzossfz	$⊢ (0 ..^\|F\|) \subseteq (0 \dots \|F\|)$
32	30 31	eqsstrrdi	$⊢ (F \in Word ℝ \land K \in ℝ) \to (0 \dots \|F\| - 1) \subseteq (0 \dots \|F\|)$
33		s1cl	$⊢ K \in ℝ \to ⟨“ K ”⟩ \in Word ℝ$
34		ccatlen	$⊢ (F \in Word ℝ \land ⟨“ K ”⟩ \in Word ℝ) \to \|F ++ ⟨“ K ”⟩\| = \|F\| + \|⟨“ K ”⟩\|$
35	33 34	sylan2	$⊢ (F \in Word ℝ \land K \in ℝ) \to \|F ++ ⟨“ K ”⟩\| = \|F\| + \|⟨“ K ”⟩\|$
36		s1len	$⊢ \|⟨“ K ”⟩\| = 1$
37	36	oveq2i	$⊢ \|F\| + \|⟨“ K ”⟩\| = \|F\| + 1$
38	35 37	eqtrdi	$⊢ (F \in Word ℝ \land K \in ℝ) \to \|F ++ ⟨“ K ”⟩\| = \|F\| + 1$
39	38	oveq2d	$⊢ (F \in Word ℝ \land K \in ℝ) \to (0 ..^\|F ++ ⟨“ K ”⟩\|) = (0 ..^\|F\| + 1)$
40	27	adantr	$⊢ (F \in Word ℝ \land K \in ℝ) \to \|F\| \in ℤ$
41	40	peano2zd	$⊢ (F \in Word ℝ \land K \in ℝ) \to \|F\| + 1 \in ℤ$
42		fzoval	$⊢ \|F\| + 1 \in ℤ \to (0 ..^\|F\| + 1) = (0 \dots \|F\| + 1 - 1)$
43	41 42	syl	$⊢ (F \in Word ℝ \land K \in ℝ) \to (0 ..^\|F\| + 1) = (0 \dots \|F\| + 1 - 1)$
44	9	nn0cnd	$⊢ F \in Word ℝ \to \|F\| \in ℂ$
45		1cnd	$⊢ F \in Word ℝ \to 1 \in ℂ$
46	44 45	pncand	$⊢ F \in Word ℝ \to \|F\| + 1 - 1 = \|F\|$
47	46	adantr	$⊢ (F \in Word ℝ \land K \in ℝ) \to \|F\| + 1 - 1 = \|F\|$
48	47	oveq2d	$⊢ (F \in Word ℝ \land K \in ℝ) \to (0 \dots \|F\| + 1 - 1) = (0 \dots \|F\|)$
49	39 43 48	3eqtrd	$⊢ (F \in Word ℝ \land K \in ℝ) \to (0 ..^\|F ++ ⟨“ K ”⟩\|) = (0 \dots \|F\|)$
50	32 49	sseqtrrd	$⊢ (F \in Word ℝ \land K \in ℝ) \to (0 \dots \|F\| - 1) \subseteq (0 ..^\|F ++ ⟨“ K ”⟩\|)$
51	50	sselda	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to i \in (0 ..^\|F ++ ⟨“ K ”⟩\|)$
52	26 51	ffvelcdmd	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to (F ++ ⟨“ K ”⟩) (i) \in ℝ$
53	8 52	sylanl1	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to (F ++ ⟨“ K ”⟩) (i) \in ℝ$
54	53	rexrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to (F ++ ⟨“ K ”⟩) (i) \in ℝ^{*}$
55		sgncl	$⊢ (F ++ ⟨“ K ”⟩) (i) \in ℝ^{*} \to sgn ((F ++ ⟨“ K ”⟩) (i)) \in \{- 1, 0, 1\}$
56	54 55	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to sgn ((F ++ ⟨“ K ”⟩) (i)) \in \{- 1, 0, 1\}$
57	1 2	signswplusg	$⊢ \underset{˙}{⨣} = +_{W}$
58		rexr	$⊢ K \in ℝ \to K \in ℝ^{*}$
59		sgncl	$⊢ K \in ℝ^{*} \to sgn (K) \in \{- 1, 0, 1\}$
60	58 59	syl	$⊢ K \in ℝ \to sgn (K) \in \{- 1, 0, 1\}$
61	60	adantl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to sgn (K) \in \{- 1, 0, 1\}$
62		id	$⊢ i = \|F\| - 1 + 1 \to i = \|F\| - 1 + 1$
63	44 45	npcand	$⊢ F \in Word ℝ \to \|F\| - 1 + 1 = \|F\|$
64	63	adantr	$⊢ (F \in Word ℝ \land K \in ℝ) \to \|F\| - 1 + 1 = \|F\|$
65	62 64	sylan9eqr	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i = \|F\| - 1 + 1) \to i = \|F\|$
66	65	fveq2d	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i = \|F\| - 1 + 1) \to (F ++ ⟨“ K ”⟩) (i) = (F ++ ⟨“ K ”⟩) (\|F\|)$
67		ccatws1ls	$⊢ (F \in Word ℝ \land K \in ℝ) \to (F ++ ⟨“ K ”⟩) (\|F\|) = K$
68	67	adantr	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i = \|F\| - 1 + 1) \to (F ++ ⟨“ K ”⟩) (\|F\|) = K$
69	66 68	eqtrd	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i = \|F\| - 1 + 1) \to (F ++ ⟨“ K ”⟩) (i) = K$
70	8 69	sylanl1	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land i = \|F\| - 1 + 1) \to (F ++ ⟨“ K ”⟩) (i) = K$
71	70	fveq2d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land i = \|F\| - 1 + 1) \to sgn ((F ++ ⟨“ K ”⟩) (i)) = sgn (K)$
72	5 7 22 56 57 61 71	gsumnunsn	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to {\sum_{W}}_{i = 0}^{\|F\| - 1 + 1} sgn ((F ++ ⟨“ K ”⟩) (i)) = ({\sum_{W}}_{i = 0}^{\|F\| - 1}, sgn ((F ++ ⟨“ K ”⟩) (i))) \underset{˙}{⨣} sgn (K)$
73	8 63	syl	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to \|F\| - 1 + 1 = \|F\|$
74	73	adantr	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \|F\| - 1 + 1 = \|F\|$
75	74	oveq2d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to (0 \dots \|F\| - 1 + 1) = (0 \dots \|F\|)$
76	75	mpteq1d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to (i \in (0 \dots \|F\| - 1 + 1) ⟼ sgn ((F ++ ⟨“ K ”⟩) (i))) = (i \in (0 \dots \|F\|) ⟼ sgn ((F ++ ⟨“ K ”⟩) (i)))$
77	76	oveq2d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to {\sum_{W}}_{i = 0}^{\|F\| - 1 + 1} sgn ((F ++ ⟨“ K ”⟩) (i)) = {\sum_{W}}_{i = 0}^{\|F\|} sgn ((F ++ ⟨“ K ”⟩) (i))$
78		simpll	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to F \in Word ℝ$
79	33	ad2antlr	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to ⟨“ K ”⟩ \in Word ℝ$
80	30	eleq2d	$⊢ (F \in Word ℝ \land K \in ℝ) \to (i \in (0 ..^\|F\|) \leftrightarrow i \in (0 \dots \|F\| - 1))$
81	80	biimpar	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to i \in (0 ..^\|F\|)$
82		ccatval1	$⊢ (F \in Word ℝ \land ⟨“ K ”⟩ \in Word ℝ \land i \in (0 ..^\|F\|)) \to (F ++ ⟨“ K ”⟩) (i) = F (i)$
83	78 79 81 82	syl3anc	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to (F ++ ⟨“ K ”⟩) (i) = F (i)$
84	83	fveq2d	$⊢ ((F \in Word ℝ \land K \in ℝ) \land i \in (0 \dots \|F\| - 1)) \to sgn ((F ++ ⟨“ K ”⟩) (i)) = sgn (F (i))$
85	84	mpteq2dva	$⊢ (F \in Word ℝ \land K \in ℝ) \to (i \in (0 \dots \|F\| - 1) ⟼ sgn ((F ++ ⟨“ K ”⟩) (i))) = (i \in (0 \dots \|F\| - 1) ⟼ sgn (F (i)))$
86	8 85	sylan	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to (i \in (0 \dots \|F\| - 1) ⟼ sgn ((F ++ ⟨“ K ”⟩) (i))) = (i \in (0 \dots \|F\| - 1) ⟼ sgn (F (i)))$
87	86	oveq2d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to {\sum_{W}}_{i = 0}^{\|F\| - 1} sgn ((F ++ ⟨“ K ”⟩) (i)) = {\sum_{W}}_{i = 0}^{\|F\| - 1} sgn (F (i))$
88	87	oveq1d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to ({\sum_{W}}_{i = 0}^{\|F\| - 1}, sgn ((F ++ ⟨“ K ”⟩) (i))) \underset{˙}{⨣} sgn (K) = ({\sum_{W}}_{i = 0}^{\|F\| - 1}, sgn (F (i))) \underset{˙}{⨣} sgn (K)$
89	72 77 88	3eqtr3d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to {\sum_{W}}_{i = 0}^{\|F\|} sgn ((F ++ ⟨“ K ”⟩) (i)) = ({\sum_{W}}_{i = 0}^{\|F\| - 1}, sgn (F (i))) \underset{˙}{⨣} sgn (K)$
90		eqid	$⊢ \|F\| = \|F\|$
91	90	olci	$⊢ (\|F\| \in (0 ..^\|F\|) \lor \|F\| = \|F\|)$
92	9 21	eleqtrdi	$⊢ F \in Word ℝ \to \|F\| \in ℤ_{\geq 0}$
93		fzosplitsni	$⊢ \|F\| \in ℤ_{\geq 0} \to (\|F\| \in (0 ..^\|F\| + 1) \leftrightarrow (\|F\| \in (0 ..^\|F\|) \lor \|F\| = \|F\|))$
94	92 93	syl	$⊢ F \in Word ℝ \to (\|F\| \in (0 ..^\|F\| + 1) \leftrightarrow (\|F\| \in (0 ..^\|F\|) \lor \|F\| = \|F\|))$
95	91 94	mpbiri	$⊢ F \in Word ℝ \to \|F\| \in (0 ..^\|F\| + 1)$
96	95	adantr	$⊢ (F \in Word ℝ \land K \in ℝ) \to \|F\| \in (0 ..^\|F\| + 1)$
97	96 39	eleqtrrd	$⊢ (F \in Word ℝ \land K \in ℝ) \to \|F\| \in (0 ..^\|F ++ ⟨“ K ”⟩\|)$
98	1 2 3 4	signstfval	$⊢ (F ++ ⟨“ K ”⟩ \in Word ℝ \land \|F\| \in (0 ..^\|F ++ ⟨“ K ”⟩\|)) \to T (F ++ ⟨“ K ”⟩) (\|F\|) = {\sum_{W}}_{i = 0}^{\|F\|} sgn ((F ++ ⟨“ K ”⟩) (i))$
99	23 97 98	syl2anc	$⊢ (F \in Word ℝ \land K \in ℝ) \to T (F ++ ⟨“ K ”⟩) (\|F\|) = {\sum_{W}}_{i = 0}^{\|F\|} sgn ((F ++ ⟨“ K ”⟩) (i))$
100	8 99	sylan	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to T (F ++ ⟨“ K ”⟩) (\|F\|) = {\sum_{W}}_{i = 0}^{\|F\|} sgn ((F ++ ⟨“ K ”⟩) (i))$
101		fzo0end	$⊢ \|F\| \in ℕ \to \|F\| - 1 \in (0 ..^\|F\|)$
102	17 101	syl	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to \|F\| - 1 \in (0 ..^\|F\|)$
103	1 2 3 4	signstfval	$⊢ (F \in Word ℝ \land \|F\| - 1 \in (0 ..^\|F\|)) \to T (F) (\|F\| - 1) = {\sum_{W}}_{i = 0}^{\|F\| - 1} sgn (F (i))$
104	8 102 103	syl2anc	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to T (F) (\|F\| - 1) = {\sum_{W}}_{i = 0}^{\|F\| - 1} sgn (F (i))$
105	104	adantr	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to T (F) (\|F\| - 1) = {\sum_{W}}_{i = 0}^{\|F\| - 1} sgn (F (i))$
106	105	oveq1d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to T (F) (\|F\| - 1) \underset{˙}{⨣} sgn (K) = ({\sum_{W}}_{i = 0}^{\|F\| - 1}, sgn (F (i))) \underset{˙}{⨣} sgn (K)$
107	89 100 106	3eqtr4d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to T (F ++ ⟨“ K ”⟩) (\|F\|) = T (F) (\|F\| - 1) \underset{˙}{⨣} sgn (K)$

Metamath Proof Explorer

Theorem signstfvn

Proof