# Metamath Proof Explorer

## Theorem 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
signsv.w
signsv.t ${⊢}{T}=\left({f}\in \mathrm{Word}ℝ⟼\left({n}\in \left(0..^\left|{f}\right|\right)⟼\underset{{i}=0}{\overset{{n}}{{\sum }_{{W}}}}\mathrm{sgn}\left({f}\left({i}\right)\right)\right)\right)$
signsv.v ${⊢}{V}=\left({f}\in \mathrm{Word}ℝ⟼\sum _{{j}\in \left(1..^\left|{f}\right|\right)}if\left({T}\left({f}\right)\left({j}\right)\ne {T}\left({f}\right)\left({j}-1\right),1,0\right)\right)$
signstfveq0.1 ${⊢}{N}=\left|{F}\right|$
Assertion signstfveq0 ${⊢}\left(\left({F}\in \left(\mathrm{Word}ℝ\setminus \left\{\varnothing \right\}\right)\wedge {F}\left(0\right)\ne 0\right)\wedge {F}\left({N}-1\right)=0\right)\to {T}\left({F}\right)\left({N}-1\right)={T}\left({F}\right)\left({N}-2\right)$

### Proof

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