signsvfn

Description: Number of changes in a word compared to a shorter word. (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	signsvfn	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to V (F ++ ⟨“ K ”⟩) = V (F) + if (T (F) (\|F\| - 1) K < 0, 1, 0)$

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		eldifi	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to F \in Word ℝ$
6		s1cl	$⊢ K \in ℝ \to ⟨“ K ”⟩ \in Word ℝ$
7		ccatcl	$⊢ (F \in Word ℝ \land ⟨“ K ”⟩ \in Word ℝ) \to F ++ ⟨“ K ”⟩ \in Word ℝ$
8	5 6 7	syl2an	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to F ++ ⟨“ K ”⟩ \in Word ℝ$
9	1 2 3 4	signsvvfval	$⊢ F ++ ⟨“ K ”⟩ \in Word ℝ \to V (F ++ ⟨“ K ”⟩) = \sum_{j \in (1 ..^\|F ++ ⟨“ K ”⟩\|)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0)$
10	8 9	syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to V (F ++ ⟨“ K ”⟩) = \sum_{j \in (1 ..^\|F ++ ⟨“ K ”⟩\|)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0)$
11		ccatlen	$⊢ (F \in Word ℝ \land ⟨“ K ”⟩ \in Word ℝ) \to \|F ++ ⟨“ K ”⟩\| = \|F\| + \|⟨“ K ”⟩\|$
12	5 6 11	syl2an	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \|F ++ ⟨“ K ”⟩\| = \|F\| + \|⟨“ K ”⟩\|$
13		s1len	$⊢ \|⟨“ K ”⟩\| = 1$
14	13	oveq2i	$⊢ \|F\| + \|⟨“ K ”⟩\| = \|F\| + 1$
15	12 14	eqtrdi	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \|F ++ ⟨“ K ”⟩\| = \|F\| + 1$
16	15	oveq2d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to (1 ..^\|F ++ ⟨“ K ”⟩\|) = (1 ..^\|F\| + 1)$
17	16	sumeq1d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \sum_{j \in (1 ..^\|F ++ ⟨“ K ”⟩\|)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) = \sum_{j \in (1 ..^\|F\| + 1)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0)$
18		eldifsn	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \leftrightarrow (F \in Word ℝ \land F \neq \emptyset)$
19		lennncl	$⊢ (F \in Word ℝ \land F \neq \emptyset) \to \|F\| \in ℕ$
20	18 19	sylbi	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to \|F\| \in ℕ$
21		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
22	20 21	eleqtrdi	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to \|F\| \in ℤ_{\geq 1}$
23	22	adantr	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \|F\| \in ℤ_{\geq 1}$
24		1cnd	$⊢ (((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 \dots \|F\|)) \land T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1)) \to 1 \in ℂ$
25		0cnd	$⊢ (((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 \dots \|F\|)) \land \neg T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1)) \to 0 \in ℂ$
26	24 25	ifclda	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 \dots \|F\|)) \to if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) \in ℂ$
27		fveq2	$⊢ j = \|F\| \to T (F ++ ⟨“ K ”⟩) (j) = T (F ++ ⟨“ K ”⟩) (\|F\|)$
28		fvoveq1	$⊢ j = \|F\| \to T (F ++ ⟨“ K ”⟩) (j - 1) = T (F ++ ⟨“ K ”⟩) (\|F\| - 1)$
29	27 28	neeq12d	$⊢ j = \|F\| \to (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1) \leftrightarrow T (F ++ ⟨“ K ”⟩) (\|F\|) \neq T (F ++ ⟨“ K ”⟩) (\|F\| - 1))$
30	29	ifbid	$⊢ j = \|F\| \to if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) = if (T (F ++ ⟨“ K ”⟩) (\|F\|) \neq T (F ++ ⟨“ K ”⟩) (\|F\| - 1), 1, 0)$
31	23 26 30	fzosump1	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \sum_{j \in (1 ..^\|F\| + 1)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) = \sum_{j \in (1 ..^\|F\|)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) + if (T (F ++ ⟨“ K ”⟩) (\|F\|) \neq T (F ++ ⟨“ K ”⟩) (\|F\| - 1), 1, 0)$
32	10 17 31	3eqtrd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to V (F ++ ⟨“ K ”⟩) = \sum_{j \in (1 ..^\|F\|)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) + if (T (F ++ ⟨“ K ”⟩) (\|F\|) \neq T (F ++ ⟨“ K ”⟩) (\|F\| - 1), 1, 0)$
33	32	adantlr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to V (F ++ ⟨“ K ”⟩) = \sum_{j \in (1 ..^\|F\|)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) + if (T (F ++ ⟨“ K ”⟩) (\|F\|) \neq T (F ++ ⟨“ K ”⟩) (\|F\| - 1), 1, 0)$
34		simpl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to F \in (Word ℝ ∖ \{\emptyset\})$
35	34	eldifad	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to F \in Word ℝ$
36	35	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to F \in Word ℝ$
37		simplr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to K \in ℝ$
38		fzo0ss1	$⊢ (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
39	38	a1i	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
40	39	sselda	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to j \in (0 ..^\|F\|)$
41	1 2 3 4	signstfvp	$⊢ (F \in Word ℝ \land K \in ℝ \land j \in (0 ..^\|F\|)) \to T (F ++ ⟨“ K ”⟩) (j) = T (F) (j)$
42	36 37 40 41	syl3anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to T (F ++ ⟨“ K ”⟩) (j) = T (F) (j)$
43		elfzoel2	$⊢ j \in (1 ..^\|F\|) \to \|F\| \in ℤ$
44	43	adantl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to \|F\| \in ℤ$
45		1nn0	$⊢ 1 \in ℕ_{0}$
46		eluzmn	$⊢ (\|F\| \in ℤ \land 1 \in ℕ_{0}) \to \|F\| \in ℤ_{\geq (\|F\| - 1)}$
47	44 45 46	sylancl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to \|F\| \in ℤ_{\geq (\|F\| - 1)}$
48		fzoss2	$⊢ \|F\| \in ℤ_{\geq (\|F\| - 1)} \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
49	47 48	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
50		elfzo1elm1fzo0	$⊢ j \in (1 ..^\|F\|) \to j - 1 \in (0 ..^\|F\| - 1)$
51	50	adantl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to j - 1 \in (0 ..^\|F\| - 1)$
52	49 51	sseldd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to j - 1 \in (0 ..^\|F\|)$
53	1 2 3 4	signstfvp	$⊢ (F \in Word ℝ \land K \in ℝ \land j - 1 \in (0 ..^\|F\|)) \to T (F ++ ⟨“ K ”⟩) (j - 1) = T (F) (j - 1)$
54	36 37 52 53	syl3anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to T (F ++ ⟨“ K ”⟩) (j - 1) = T (F) (j - 1)$
55	42 54	neeq12d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1) \leftrightarrow T (F) (j) \neq T (F) (j - 1))$
56	55	ifbid	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \land j \in (1 ..^\|F\|)) \to if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) = if (T (F) (j) \neq T (F) (j - 1), 1, 0)$
57	56	sumeq2dv	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \sum_{j \in (1 ..^\|F\|)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) = \sum_{j \in (1 ..^\|F\|)} if (T (F) (j) \neq T (F) (j - 1), 1, 0)$
58	1 2 3 4	signsvvfval	$⊢ F \in Word ℝ \to V (F) = \sum_{j \in (1 ..^\|F\|)} if (T (F) (j) \neq T (F) (j - 1), 1, 0)$
59	35 58	syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to V (F) = \sum_{j \in (1 ..^\|F\|)} if (T (F) (j) \neq T (F) (j - 1), 1, 0)$
60	57 59	eqtr4d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to \sum_{j \in (1 ..^\|F\|)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) = V (F)$
61	60	adantlr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to \sum_{j \in (1 ..^\|F\|)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) = V (F)$
62	1 2 3 4	signstfvn	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land K \in ℝ) \to T (F ++ ⟨“ K ”⟩) (\|F\|) = T (F) (\|F\| - 1) \underset{˙}{⨣} sgn (K)$
63	62	adantlr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to T (F ++ ⟨“ K ”⟩) (\|F\|) = T (F) (\|F\| - 1) \underset{˙}{⨣} sgn (K)$
64	35	adantlr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to F \in Word ℝ$
65		simpr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to K \in ℝ$
66		fzo0end	$⊢ \|F\| \in ℕ \to \|F\| - 1 \in (0 ..^\|F\|)$
67	20 66	syl	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to \|F\| - 1 \in (0 ..^\|F\|)$
68	67	ad2antrr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to \|F\| - 1 \in (0 ..^\|F\|)$
69	1 2 3 4	signstfvp	$⊢ (F \in Word ℝ \land K \in ℝ \land \|F\| - 1 \in (0 ..^\|F\|)) \to T (F ++ ⟨“ K ”⟩) (\|F\| - 1) = T (F) (\|F\| - 1)$
70	64 65 68 69	syl3anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to T (F ++ ⟨“ K ”⟩) (\|F\| - 1) = T (F) (\|F\| - 1)$
71	63 70	neeq12d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to (T (F ++ ⟨“ K ”⟩) (\|F\|) \neq T (F ++ ⟨“ K ”⟩) (\|F\| - 1) \leftrightarrow T (F) (\|F\| - 1) \underset{˙}{⨣} sgn (K) \neq T (F) (\|F\| - 1))$
72	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\}$
73	68 72	syldan	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to T (F) (\|F\| - 1) \in \{- 1, 1\}$
74		rexr	$⊢ K \in ℝ \to K \in ℝ^{*}$
75		sgncl	$⊢ K \in ℝ^{*} \to sgn (K) \in \{- 1, 0, 1\}$
76	74 75	syl	$⊢ K \in ℝ \to sgn (K) \in \{- 1, 0, 1\}$
77	76	adantl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to sgn (K) \in \{- 1, 0, 1\}$
78	1 2	signswch	$⊢ (T (F) (\|F\| - 1) \in \{- 1, 1\} \land sgn (K) \in \{- 1, 0, 1\}) \to (T (F) (\|F\| - 1) \underset{˙}{⨣} sgn (K) \neq T (F) (\|F\| - 1) \leftrightarrow T (F) (\|F\| - 1) sgn (K) < 0)$
79	73 77 78	syl2anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to (T (F) (\|F\| - 1) \underset{˙}{⨣} sgn (K) \neq T (F) (\|F\| - 1) \leftrightarrow T (F) (\|F\| - 1) sgn (K) < 0)$
80	65	rexrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to K \in ℝ^{*}$
81		sgnsgn	$⊢ K \in ℝ^{*} \to sgn (sgn (K)) = sgn (K)$
82	80 81	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to sgn (sgn (K)) = sgn (K)$
83	82	oveq2d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to sgn (T (F) (\|F\| - 1)) sgn (sgn (K)) = sgn (T (F) (\|F\| - 1)) sgn (K)$
84	83	breq1d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to (sgn (T (F) (\|F\| - 1)) sgn (sgn (K)) < 0 \leftrightarrow sgn (T (F) (\|F\| - 1)) sgn (K) < 0)$
85		neg1rr	$⊢ - 1 \in ℝ$
86		1re	$⊢ 1 \in ℝ$
87		prssi	$⊢ (- 1 \in ℝ \land 1 \in ℝ) \to \{- 1, 1\} \subseteq ℝ$
88	85 86 87	mp2an	$⊢ \{- 1, 1\} \subseteq ℝ$
89	88 73	sselid	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to T (F) (\|F\| - 1) \in ℝ$
90		sgnclre	$⊢ K \in ℝ \to sgn (K) \in ℝ$
91	90	adantl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to sgn (K) \in ℝ$
92		sgnmulsgn	$⊢ (T (F) (\|F\| - 1) \in ℝ \land sgn (K) \in ℝ) \to (T (F) (\|F\| - 1) sgn (K) < 0 \leftrightarrow sgn (T (F) (\|F\| - 1)) sgn (sgn (K)) < 0)$
93	89 91 92	syl2anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to (T (F) (\|F\| - 1) sgn (K) < 0 \leftrightarrow sgn (T (F) (\|F\| - 1)) sgn (sgn (K)) < 0)$
94		sgnmulsgn	$⊢ (T (F) (\|F\| - 1) \in ℝ \land K \in ℝ) \to (T (F) (\|F\| - 1) K < 0 \leftrightarrow sgn (T (F) (\|F\| - 1)) sgn (K) < 0)$
95	89 94	sylancom	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to (T (F) (\|F\| - 1) K < 0 \leftrightarrow sgn (T (F) (\|F\| - 1)) sgn (K) < 0)$
96	84 93 95	3bitr4d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to (T (F) (\|F\| - 1) sgn (K) < 0 \leftrightarrow T (F) (\|F\| - 1) K < 0)$
97	71 79 96	3bitrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to (T (F ++ ⟨“ K ”⟩) (\|F\|) \neq T (F ++ ⟨“ K ”⟩) (\|F\| - 1) \leftrightarrow T (F) (\|F\| - 1) K < 0)$
98	97	ifbid	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to if (T (F ++ ⟨“ K ”⟩) (\|F\|) \neq T (F ++ ⟨“ K ”⟩) (\|F\| - 1), 1, 0) = if (T (F) (\|F\| - 1) K < 0, 1, 0)$
99	61 98	oveq12d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to \sum_{j \in (1 ..^\|F\|)} if (T (F ++ ⟨“ K ”⟩) (j) \neq T (F ++ ⟨“ K ”⟩) (j - 1), 1, 0) + if (T (F ++ ⟨“ K ”⟩) (\|F\|) \neq T (F ++ ⟨“ K ”⟩) (\|F\| - 1), 1, 0) = V (F) + if (T (F) (\|F\| - 1) K < 0, 1, 0)$
100	33 99	eqtrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (0) \neq 0) \land K \in ℝ) \to V (F ++ ⟨“ K ”⟩) = V (F) + if (T (F) (\|F\| - 1) K < 0, 1, 0)$

Metamath Proof Explorer

Theorem signsvfn

Proof