signstfveq0

Description: In case the last letter is zero, the zero skipping sign is the same as the previous letter. (Contributed by Thierry Arnoux, 11-Oct-2018) (Proof shortened by AV, 4-Nov-2022)

	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	signstfveq0	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T (F) (N - 1) = T (F) (N - 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		pfxcl	$⊢ F \in Word ℝ \to F prefix (N - 1) \in Word ℝ$
9	7 8	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F prefix (N - 1) \in Word ℝ$
10		1nn0	$⊢ 1 \in ℕ_{0}$
11	10	a1i	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to 1 \in ℕ_{0}$
12	11	nn0red	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to 1 \in ℝ$
13		2re	$⊢ 2 \in ℝ$
14	13	a1i	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to 2 \in ℝ$
15		lencl	$⊢ F \in Word ℝ \to \|F\| \in ℕ_{0}$
16	7 15	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to \|F\| \in ℕ_{0}$
17	5 16	eqeltrid	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \in ℕ_{0}$
18	17	nn0red	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \in ℝ$
19		1le2	$⊢ 1 \leq 2$
20	19	a1i	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to 1 \leq 2$
21	1 2 3 4 5	signstfveq0a	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \in ℤ_{\geq 2}$
22		eluz2	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land N \in ℤ \land 2 \leq N)$
23	21 22	sylib	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to (2 \in ℤ \land N \in ℤ \land 2 \leq N)$
24	23	simp3d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to 2 \leq N$
25	12 14 18 20 24	letrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to 1 \leq N$
26		fznn0	$⊢ N \in ℕ_{0} \to (1 \in (0 \dots N) \leftrightarrow (1 \in ℕ_{0} \land 1 \leq N))$
27	17 26	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to (1 \in (0 \dots N) \leftrightarrow (1 \in ℕ_{0} \land 1 \leq N))$
28	11 25 27	mpbir2and	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to 1 \in (0 \dots N)$
29		fznn0sub2	$⊢ 1 \in (0 \dots N) \to N - 1 \in (0 \dots N)$
30	28 29	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 1 \in (0 \dots N)$
31	5	oveq2i	$⊢ (0 \dots N) = (0 \dots \|F\|)$
32	30 31	eleqtrdi	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 1 \in (0 \dots \|F\|)$
33		pfxlen	$⊢ (F \in Word ℝ \land N - 1 \in (0 \dots \|F\|)) \to \|F prefix (N - 1)\| = N - 1$
34	7 32 33	syl2anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to \|F prefix (N - 1)\| = N - 1$
35		uz2m1nn	$⊢ N \in ℤ_{\geq 2} \to N - 1 \in ℕ$
36	21 35	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 1 \in ℕ$
37	34 36	eqeltrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to \|F prefix (N - 1)\| \in ℕ$
38		nnne0	$⊢ \|F prefix (N - 1)\| \in ℕ \to \|F prefix (N - 1)\| \neq 0$
39		fveq2	$⊢ F prefix (N - 1) = \emptyset \to \|F prefix (N - 1)\| = \|\emptyset\|$
40		hash0	$⊢ \|\emptyset\| = 0$
41	39 40	syl6eq	$⊢ F prefix (N - 1) = \emptyset \to \|F prefix (N - 1)\| = 0$
42	41	necon3i	$⊢ \|F prefix (N - 1)\| \neq 0 \to F prefix (N - 1) \neq \emptyset$
43	38 42	syl	$⊢ \|F prefix (N - 1)\| \in ℕ \to F prefix (N - 1) \neq \emptyset$
44	37 43	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F prefix (N - 1) \neq \emptyset$
45		eldifsn	$⊢ F prefix (N - 1) \in (Word ℝ ∖ \{\emptyset\}) \leftrightarrow (F prefix (N - 1) \in Word ℝ \land F prefix (N - 1) \neq \emptyset)$
46	9 44 45	sylanbrc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F prefix (N - 1) \in (Word ℝ ∖ \{\emptyset\})$
47		simpr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F (N - 1) = 0$
48		0re	$⊢ 0 \in ℝ$
49	47 48	eqeltrdi	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F (N - 1) \in ℝ$
50	1 2 3 4	signstfvn	$⊢ (F prefix (N - 1) \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \in ℝ) \to T ((F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩) (\|F prefix (N - 1)\|) = T (F prefix (N - 1)) (\|F prefix (N - 1)\| - 1) \underset{˙}{⨣} sgn (F (N - 1))$
51	46 49 50	syl2anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T ((F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩) (\|F prefix (N - 1)\|) = T (F prefix (N - 1)) (\|F prefix (N - 1)\| - 1) \underset{˙}{⨣} sgn (F (N - 1))$
52	5	oveq1i	$⊢ N - 1 = \|F\| - 1$
53	52	oveq2i	$⊢ F prefix (N - 1) = F prefix (\|F\| - 1)$
54	53	a1i	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F prefix (N - 1) = F prefix (\|F\| - 1)$
55		lsw	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to lastS (F) = F (\|F\| - 1)$
56	55	ad2antrr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to lastS (F) = F (\|F\| - 1)$
57	5	eqcomi	$⊢ \|F\| = N$
58	57	oveq1i	$⊢ \|F\| - 1 = N - 1$
59	58	fveq2i	$⊢ F (\|F\| - 1) = F (N - 1)$
60	56 59	syl6eq	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to lastS (F) = F (N - 1)$
61	60	s1eqd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to ⟨“ lastS (F) ”⟩ = ⟨“ F (N - 1) ”⟩$
62	61	eqcomd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to ⟨“ F (N - 1) ”⟩ = ⟨“ lastS (F) ”⟩$
63	54 62	oveq12d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to (F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩ = (F prefix (\|F\| - 1)) ++ ⟨“ lastS (F) ”⟩$
64		eldifsn	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \leftrightarrow (F \in Word ℝ \land F \neq \emptyset)$
65	6 64	sylib	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to (F \in Word ℝ \land F \neq \emptyset)$
66		pfxlswccat	$⊢ (F \in Word ℝ \land F \neq \emptyset) \to (F prefix (\|F\| - 1)) ++ ⟨“ lastS (F) ”⟩ = F$
67	65 66	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to (F prefix (\|F\| - 1)) ++ ⟨“ lastS (F) ”⟩ = F$
68	63 67	eqtrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to (F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩ = F$
69	68	fveq2d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T ((F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩) = T (F)$
70	69 34	fveq12d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T ((F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩) (\|F prefix (N - 1)\|) = T (F) (N - 1)$
71	17	nn0cnd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \in ℂ$
72		1cnd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to 1 \in ℂ$
73	71 72 72	subsub4d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 1 - 1 = N - (1 + 1)$
74		1p1e2	$⊢ 1 + 1 = 2$
75	74	oveq2i	$⊢ N - (1 + 1) = N - 2$
76	73 75	syl6eq	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 1 - 1 = N - 2$
77		fzo0end	$⊢ N - 1 \in ℕ \to N - 1 - 1 \in (0 ..^N - 1)$
78	36 77	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 1 - 1 \in (0 ..^N - 1)$
79	76 78	eqeltrrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 2 \in (0 ..^N - 1)$
80	34	oveq2d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to (0 ..^\|F prefix (N - 1)\|) = (0 ..^N - 1)$
81	79 80	eleqtrrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 2 \in (0 ..^\|F prefix (N - 1)\|)$
82	1 2 3 4	signstfvp	$⊢ (F prefix (N - 1) \in Word ℝ \land F (N - 1) \in ℝ \land N - 2 \in (0 ..^\|F prefix (N - 1)\|)) \to T ((F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩) (N - 2) = T (F prefix (N - 1)) (N - 2)$
83	9 49 81 82	syl3anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T ((F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩) (N - 2) = T (F prefix (N - 1)) (N - 2)$
84	68	eqcomd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to F = (F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩$
85	84	fveq2d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T (F) = T ((F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩)$
86	85	fveq1d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T (F) (N - 2) = T ((F prefix (N - 1)) ++ ⟨“ F (N - 1) ”⟩) (N - 2)$
87	34	oveq1d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to \|F prefix (N - 1)\| - 1 = N - 1 - 1$
88	87 73	eqtrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to \|F prefix (N - 1)\| - 1 = N - (1 + 1)$
89	88 75	syl6eq	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to \|F prefix (N - 1)\| - 1 = N - 2$
90	89	fveq2d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T (F prefix (N - 1)) (\|F prefix (N - 1)\| - 1) = T (F prefix (N - 1)) (N - 2)$
91	83 86 90	3eqtr4rd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T (F prefix (N - 1)) (\|F prefix (N - 1)\| - 1) = T (F) (N - 2)$
92		fveq2	$⊢ F (N - 1) = 0 \to sgn (F (N - 1)) = sgn (0)$
93		sgn0	$⊢ sgn (0) = 0$
94	92 93	syl6eq	$⊢ F (N - 1) = 0 \to sgn (F (N - 1)) = 0$
95	94	adantl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to sgn (F (N - 1)) = 0$
96	91 95	oveq12d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T (F prefix (N - 1)) (\|F prefix (N - 1)\| - 1) \underset{˙}{⨣} sgn (F (N - 1)) = T (F) (N - 2) \underset{˙}{⨣} 0$
97		uznn0sub	$⊢ N \in ℤ_{\geq 2} \to N - 2 \in ℕ_{0}$
98	21 97	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 2 \in ℕ_{0}$
99		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
100	21 99	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N \in ℕ$
101		2rp	$⊢ 2 \in ℝ^{+}$
102	101	a1i	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to 2 \in ℝ^{+}$
103	18 102	ltsubrpd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 2 < N$
104		elfzo0	$⊢ N - 2 \in (0 ..^N) \leftrightarrow (N - 2 \in ℕ_{0} \land N \in ℕ \land N - 2 < N)$
105	98 100 103 104	syl3anbrc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 2 \in (0 ..^N)$
106	5	oveq2i	$⊢ (0 ..^N) = (0 ..^\|F\|)$
107	105 106	eleqtrdi	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to N - 2 \in (0 ..^\|F\|)$
108	1 2 3 4	signstcl	$⊢ (F \in Word ℝ \land N - 2 \in (0 ..^\|F\|)) \to T (F) (N - 2) \in \{- 1, 0, 1\}$
109	7 107 108	syl2anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T (F) (N - 2) \in \{- 1, 0, 1\}$
110	1 2	signswrid	$⊢ T (F) (N - 2) \in \{- 1, 0, 1\} \to T (F) (N - 2) \underset{˙}{⨣} 0 = T (F) (N - 2)$
111	109 110	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T (F) (N - 2) \underset{˙}{⨣} 0 = T (F) (N - 2)$
112	96 111	eqtrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T (F prefix (N - 1)) (\|F prefix (N - 1)\| - 1) \underset{˙}{⨣} sgn (F (N - 1)) = T (F) (N - 2)$
113	51 70 112	3eqtr3d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land F (N - 1) = 0) \to T (F) (N - 1) = T (F) (N - 2)$

Metamath Proof Explorer

Theorem signstfveq0

Proof