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