signsvtn0

Description: If the last letter is nonzero, then this is the zero-skipping sign. (Contributed by Thierry Arnoux, 8-Oct-2018) (Proof shortened by AV, 3-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))$
	signsvtn0.1	$⊢ N = \|F\|$
Assertion	signsvtn0	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to T (F) (N - 1) = sgn (F (N - 1))$

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		signsvtn0.1	$⊢ N = \|F\|$
6		eldifsn	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \leftrightarrow (F \in Word ℝ \land F \neq \emptyset)$
7	6	birani	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to (F \in Word ℝ \land F \neq \emptyset)$
8	7	simpld	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F \in Word ℝ$
9	8	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to F \in Word ℝ$
10		wrdf	$⊢ F \in Word ℝ \to F : (0 ..^\|F\|) ⟶ ℝ$
11	9 10	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to F : (0 ..^\|F\|) ⟶ ℝ$
12		lennncl	$⊢ (F \in Word ℝ \land F \neq \emptyset) \to \|F\| \in ℕ$
13	7 12	syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to \|F\| \in ℕ$
14	13	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to \|F\| \in ℕ$
15		lbfzo0	$⊢ 0 \in (0 ..^\|F\|) \leftrightarrow \|F\| \in ℕ$
16	14 15	sylibr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to 0 \in (0 ..^\|F\|)$
17	11 16	ffvelcdmd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to F (0) \in ℝ$
18	1 2 3 4	signstf0	$⊢ F (0) \in ℝ \to T (⟨“ F (0) ”⟩) = ⟨“ sgn (F (0)) ”⟩$
19	17 18	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to T (⟨“ F (0) ”⟩) = ⟨“ sgn (F (0)) ”⟩$
20		simpr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to N = 1$
21	5 20	eqtr3id	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to \|F\| = 1$
22		eqs1	$⊢ (F \in Word ℝ \land \|F\| = 1) \to F = ⟨“ F (0) ”⟩$
23	9 21 22	syl2anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to F = ⟨“ F (0) ”⟩$
24	23	fveq2d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to T (F) = T (⟨“ 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	fveq2d	$⊢ N = 1 \to sgn (F (N - 1)) = sgn (F (0))$
30	29	s1eqd	$⊢ N = 1 \to ⟨“ sgn (F (N - 1)) ”⟩ = ⟨“ sgn (F (0)) ”⟩$
31	20 30	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to ⟨“ sgn (F (N - 1)) ”⟩ = ⟨“ sgn (F (0)) ”⟩$
32	19 24 31	3eqtr4d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to T (F) = ⟨“ sgn (F (N - 1)) ”⟩$
33	20 27	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to N - 1 = 0$
34	32 33	fveq12d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to T (F) (N - 1) = ⟨“ sgn (F (N - 1)) ”⟩ (0)$
35	8 10	syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F : (0 ..^\|F\|) ⟶ ℝ$
36	5	oveq1i	$⊢ N - 1 = \|F\| - 1$
37		fzo0end	$⊢ \|F\| \in ℕ \to \|F\| - 1 \in (0 ..^\|F\|)$
38	7 12 37	3syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to \|F\| - 1 \in (0 ..^\|F\|)$
39	36 38	eqeltrid	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to N - 1 \in (0 ..^\|F\|)$
40	35 39	ffvelcdmd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F (N - 1) \in ℝ$
41	40	rexrd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F (N - 1) \in ℝ^{*}$
42		sgncl	$⊢ F (N - 1) \in ℝ^{*} \to sgn (F (N - 1)) \in \{- 1, 0, 1\}$
43	41 42	syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to sgn (F (N - 1)) \in \{- 1, 0, 1\}$
44	43	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to sgn (F (N - 1)) \in \{- 1, 0, 1\}$
45		s1fv	$⊢ sgn (F (N - 1)) \in \{- 1, 0, 1\} \to ⟨“ sgn (F (N - 1)) ”⟩ (0) = sgn (F (N - 1))$
46	44 45	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to ⟨“ sgn (F (N - 1)) ”⟩ (0) = sgn (F (N - 1))$
47	34 46	eqtrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N = 1) \to T (F) (N - 1) = sgn (F (N - 1))$
48		fzossfz	$⊢ (0 ..^\|F\|) \subseteq (0 \dots \|F\|)$
49	48 38	sselid	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to \|F\| - 1 \in (0 \dots \|F\|)$
50		pfxres	$⊢ (F \in Word ℝ \land \|F\| - 1 \in (0 \dots \|F\|)) \to F prefix (\|F\| - 1) = {F ↾}_{(0 ..^\|F\| - 1)}$
51	8 49 50	syl2anc	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F prefix (\|F\| - 1) = {F ↾}_{(0 ..^\|F\| - 1)}$
52	51	oveq1d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to (F prefix (\|F\| - 1)) ++ ⟨“ lastS (F) ”⟩ = ({F ↾}_{(0 ..^\|F\| - 1)}) ++ ⟨“ lastS (F) ”⟩$
53		pfxlswccat	$⊢ (F \in Word ℝ \land F \neq \emptyset) \to (F prefix (\|F\| - 1)) ++ ⟨“ lastS (F) ”⟩ = F$
54	53	eqcomd	$⊢ (F \in Word ℝ \land F \neq \emptyset) \to F = (F prefix (\|F\| - 1)) ++ ⟨“ lastS (F) ”⟩$
55	7 54	syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F = (F prefix (\|F\| - 1)) ++ ⟨“ lastS (F) ”⟩$
56	36	oveq2i	$⊢ (0 ..^N - 1) = (0 ..^\|F\| - 1)$
57	56	a1i	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to (0 ..^N - 1) = (0 ..^\|F\| - 1)$
58	57	reseq2d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to {F ↾}_{(0 ..^N - 1)} = {F ↾}_{(0 ..^\|F\| - 1)}$
59	36	a1i	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to N - 1 = \|F\| - 1$
60	59	fveq2d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F (N - 1) = F (\|F\| - 1)$
61		lsw	$⊢ F \in (Word ℝ ∖ \{\emptyset\}) \to lastS (F) = F (\|F\| - 1)$
62	61	adantr	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to lastS (F) = F (\|F\| - 1)$
63	60 62	eqtr4d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F (N - 1) = lastS (F)$
64	63	s1eqd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to ⟨“ F (N - 1) ”⟩ = ⟨“ lastS (F) ”⟩$
65	58 64	oveq12d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to ({F ↾}_{(0 ..^N - 1)}) ++ ⟨“ F (N - 1) ”⟩ = ({F ↾}_{(0 ..^\|F\| - 1)}) ++ ⟨“ lastS (F) ”⟩$
66	52 55 65	3eqtr4d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F = ({F ↾}_{(0 ..^N - 1)}) ++ ⟨“ F (N - 1) ”⟩$
67	66	fveq2d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to T (F) = T (({F ↾}_{(0 ..^N - 1)}) ++ ⟨“ F (N - 1) ”⟩)$
68		ffn	$⊢ F : (0 ..^\|F\|) ⟶ ℝ \to F Fn (0 ..^\|F\|)$
69	8 10 68	3syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F Fn (0 ..^\|F\|)$
70	5	a1i	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to N = \|F\|$
71	70	oveq2d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to (0 ..^N) = (0 ..^\|F\|)$
72	71	fneq2d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to (F Fn (0 ..^N) \leftrightarrow F Fn (0 ..^\|F\|))$
73	69 72	mpbird	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F Fn (0 ..^N)$
74	5 13	eqeltrid	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to N \in ℕ$
75	74	nnnn0d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to N \in ℕ_{0}$
76		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
77		fzossrbm1	$⊢ N \in ℤ \to (0 ..^N - 1) \subseteq (0 ..^N)$
78	75 76 77	3syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to (0 ..^N - 1) \subseteq (0 ..^N)$
79		fnssres	$⊢ (F Fn (0 ..^N) \land (0 ..^N - 1) \subseteq (0 ..^N)) \to ({F ↾}_{(0 ..^N - 1)}) Fn (0 ..^N - 1)$
80	73 78 79	syl2anc	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to ({F ↾}_{(0 ..^N - 1)}) Fn (0 ..^N - 1)$
81		hashfn	$⊢ ({F ↾}_{(0 ..^N - 1)}) Fn (0 ..^N - 1) \to \|{F ↾}_{(0 ..^N - 1)}\| = \|(0 ..^N - 1)\|$
82	80 81	syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to \|{F ↾}_{(0 ..^N - 1)}\| = \|(0 ..^N - 1)\|$
83		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
84		hashfzo0	$⊢ N - 1 \in ℕ_{0} \to \|(0 ..^N - 1)\| = N - 1$
85	74 83 84	3syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to \|(0 ..^N - 1)\| = N - 1$
86	82 85	eqtrd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to \|{F ↾}_{(0 ..^N - 1)}\| = N - 1$
87	86	eqcomd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to N - 1 = \|{F ↾}_{(0 ..^N - 1)}\|$
88	67 87	fveq12d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to T (F) (N - 1) = T (({F ↾}_{(0 ..^N - 1)}) ++ ⟨“ F (N - 1) ”⟩) (\|{F ↾}_{(0 ..^N - 1)}\|)$
89	88	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to T (F) (N - 1) = T (({F ↾}_{(0 ..^N - 1)}) ++ ⟨“ F (N - 1) ”⟩) (\|{F ↾}_{(0 ..^N - 1)}\|)$
90	51 58	eqtr4d	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F prefix (\|F\| - 1) = {F ↾}_{(0 ..^N - 1)}$
91		pfxcl	$⊢ F \in Word ℝ \to F prefix (\|F\| - 1) \in Word ℝ$
92	8 91	syl	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F prefix (\|F\| - 1) \in Word ℝ$
93	90 92	eqeltrrd	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to {F ↾}_{(0 ..^N - 1)} \in Word ℝ$
94	93	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to {F ↾}_{(0 ..^N - 1)} \in Word ℝ$
95	86	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to \|{F ↾}_{(0 ..^N - 1)}\| = N - 1$
96	74	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to N \in ℕ$
97	96	nncnd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to N \in ℂ$
98		1cnd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to 1 \in ℂ$
99		simpr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to N \neq 1$
100	97 98 99	subne0d	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to N - 1 \neq 0$
101	95 100	eqnetrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to \|{F ↾}_{(0 ..^N - 1)}\| \neq 0$
102		fveq2	$⊢ {F ↾}_{(0 ..^N - 1)} = \emptyset \to \|{F ↾}_{(0 ..^N - 1)}\| = \|\emptyset\|$
103		hash0	$⊢ \|\emptyset\| = 0$
104	102 103	eqtrdi	$⊢ {F ↾}_{(0 ..^N - 1)} = \emptyset \to \|{F ↾}_{(0 ..^N - 1)}\| = 0$
105	104	necon3i	$⊢ \|{F ↾}_{(0 ..^N - 1)}\| \neq 0 \to {F ↾}_{(0 ..^N - 1)} \neq \emptyset$
106	101 105	syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to {F ↾}_{(0 ..^N - 1)} \neq \emptyset$
107	94 106	jca	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to ({F ↾}_{(0 ..^N - 1)} \in Word ℝ \land {F ↾}_{(0 ..^N - 1)} \neq \emptyset)$
108		eldifsn	$⊢ {F ↾}_{(0 ..^N - 1)} \in (Word ℝ ∖ \{\emptyset\}) \leftrightarrow ({F ↾}_{(0 ..^N - 1)} \in Word ℝ \land {F ↾}_{(0 ..^N - 1)} \neq \emptyset)$
109	107 108	sylibr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to {F ↾}_{(0 ..^N - 1)} \in (Word ℝ ∖ \{\emptyset\})$
110	40	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to F (N - 1) \in ℝ$
111	1 2 3 4	signstfvn	$⊢ ({F ↾}_{(0 ..^N - 1)} \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \in ℝ) \to T (({F ↾}_{(0 ..^N - 1)}) ++ ⟨“ F (N - 1) ”⟩) (\|{F ↾}_{(0 ..^N - 1)}\|) = T ({F ↾}_{(0 ..^N - 1)}) (\|{F ↾}_{(0 ..^N - 1)}\| - 1) \underset{˙}{⨣} sgn (F (N - 1))$
112	109 110 111	syl2anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to T (({F ↾}_{(0 ..^N - 1)}) ++ ⟨“ F (N - 1) ”⟩) (\|{F ↾}_{(0 ..^N - 1)}\|) = T ({F ↾}_{(0 ..^N - 1)}) (\|{F ↾}_{(0 ..^N - 1)}\| - 1) \underset{˙}{⨣} sgn (F (N - 1))$
113		lennncl	$⊢ ({F ↾}_{(0 ..^N - 1)} \in Word ℝ \land {F ↾}_{(0 ..^N - 1)} \neq \emptyset) \to \|{F ↾}_{(0 ..^N - 1)}\| \in ℕ$
114		fzo0end	$⊢ \|{F ↾}_{(0 ..^N - 1)}\| \in ℕ \to \|{F ↾}_{(0 ..^N - 1)}\| - 1 \in (0 ..^\|{F ↾}_{(0 ..^N - 1)}\|)$
115	107 113 114	3syl	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to \|{F ↾}_{(0 ..^N - 1)}\| - 1 \in (0 ..^\|{F ↾}_{(0 ..^N - 1)}\|)$
116	1 2 3 4	signstcl	$⊢ ({F ↾}_{(0 ..^N - 1)} \in Word ℝ \land \|{F ↾}_{(0 ..^N - 1)}\| - 1 \in (0 ..^\|{F ↾}_{(0 ..^N - 1)}\|)) \to T ({F ↾}_{(0 ..^N - 1)}) (\|{F ↾}_{(0 ..^N - 1)}\| - 1) \in \{- 1, 0, 1\}$
117	94 115 116	syl2anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to T ({F ↾}_{(0 ..^N - 1)}) (\|{F ↾}_{(0 ..^N - 1)}\| - 1) \in \{- 1, 0, 1\}$
118	43	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to sgn (F (N - 1)) \in \{- 1, 0, 1\}$
119		simpr	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to F (N - 1) \neq 0$
120		sgn0bi	$⊢ F (N - 1) \in ℝ^{*} \to (sgn (F (N - 1)) = 0 \leftrightarrow F (N - 1) = 0)$
121	120	necon3bid	$⊢ F (N - 1) \in ℝ^{*} \to (sgn (F (N - 1)) \neq 0 \leftrightarrow F (N - 1) \neq 0)$
122	121	biimpar	$⊢ (F (N - 1) \in ℝ^{*} \land F (N - 1) \neq 0) \to sgn (F (N - 1)) \neq 0$
123	41 119 122	syl2anc	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to sgn (F (N - 1)) \neq 0$
124	123	adantr	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to sgn (F (N - 1)) \neq 0$
125	1 2	signswlid	$⊢ ((T ({F ↾}_{(0 ..^N - 1)}) (\|{F ↾}_{(0 ..^N - 1)}\| - 1) \in \{- 1, 0, 1\} \land sgn (F (N - 1)) \in \{- 1, 0, 1\}) \land sgn (F (N - 1)) \neq 0) \to T ({F ↾}_{(0 ..^N - 1)}) (\|{F ↾}_{(0 ..^N - 1)}\| - 1) \underset{˙}{⨣} sgn (F (N - 1)) = sgn (F (N - 1))$
126	117 118 124 125	syl21anc	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to T ({F ↾}_{(0 ..^N - 1)}) (\|{F ↾}_{(0 ..^N - 1)}\| - 1) \underset{˙}{⨣} sgn (F (N - 1)) = sgn (F (N - 1))$
127	89 112 126	3eqtrd	$⊢ ((F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \land N \neq 1) \to T (F) (N - 1) = sgn (F (N - 1))$
128	47 127	pm2.61dane	$⊢ (F \in (Word ℝ ∖ \{\emptyset\}) \land F (N - 1) \neq 0) \to T (F) (N - 1) = sgn (F (N - 1))$

Metamath Proof Explorer

Theorem signsvtn0

Proof