Metamath Proof Explorer

Theorem 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 ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
signsv.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
signsv.t ⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) )
signsv.v ⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
signsvtn0.1 ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
Assertion signsvtn0 ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 signsv.p ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
2 signsv.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
3 signsv.t ⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) )
4 signsv.v ⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
5 signsvtn0.1 ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
6 eldifsn ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) )
7 6 birani ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) )
8 7 simpld ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → 𝐹 ∈ Word ℝ )
9 8 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → 𝐹 ∈ Word ℝ )
10 wrdf ⊢ ( 𝐹 ∈ Word ℝ → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ℝ )
11 9 10 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ℝ )
12 lennncl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
13 7 12 syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
14 13 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
15 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ )
16 14 15 sylibr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
17 11 16 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( 𝐹 ‘ 0 ) ∈ ℝ )
18 1 2 3 4 signstf0 ⊢ ( ( 𝐹 ‘ 0 ) ∈ ℝ → ( 𝑇 ‘ ⟨“ ( 𝐹 ‘ 0 ) ”⟩ ) = ⟨“ ( sgn ‘ ( 𝐹 ‘ 0 ) ) ”⟩ )
19 17 18 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( 𝑇 ‘ ⟨“ ( 𝐹 ‘ 0 ) ”⟩ ) = ⟨“ ( sgn ‘ ( 𝐹 ‘ 0 ) ) ”⟩ )
20 simpr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → 𝑁 = 1 )
21 5 20 eqtr3id ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( ♯ ‘ 𝐹 ) = 1 )
22 eqs1 ⊢ ( ( 𝐹 ∈ Word ℝ ∧ ( ♯ ‘ 𝐹 ) = 1 ) → 𝐹 = ⟨“ ( 𝐹 ‘ 0 ) ”⟩ )
23 9 21 22 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → 𝐹 = ⟨“ ( 𝐹 ‘ 0 ) ”⟩ )
24 23 fveq2d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( 𝑇 ‘ 𝐹 ) = ( 𝑇 ‘ ⟨“ ( 𝐹 ‘ 0 ) ”⟩ ) )
25 oveq1 ⊢ ( 𝑁 = 1 → ( 𝑁 − 1 ) = ( 1 − 1 ) )
26 1m1e0 ⊢ ( 1 − 1 ) = 0
27 25 26 eqtrdi ⊢ ( 𝑁 = 1 → ( 𝑁 − 1 ) = 0 )
28 27 fveq2d ⊢ ( 𝑁 = 1 → ( 𝐹 ‘ ( 𝑁 − 1 ) ) = ( 𝐹 ‘ 0 ) )
29 28 fveq2d ⊢ ( 𝑁 = 1 → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) = ( sgn ‘ ( 𝐹 ‘ 0 ) ) )
30 29 s1eqd ⊢ ( 𝑁 = 1 → ⟨“ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ”⟩ = ⟨“ ( sgn ‘ ( 𝐹 ‘ 0 ) ) ”⟩ )
31 20 30 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ⟨“ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ”⟩ = ⟨“ ( sgn ‘ ( 𝐹 ‘ 0 ) ) ”⟩ )
32 19 24 31 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( 𝑇 ‘ 𝐹 ) = ⟨“ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ”⟩ )
33 20 27 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( 𝑁 − 1 ) = 0 )
34 32 33 fveq12d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 1 ) ) = ( ⟨“ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ”⟩ ‘ 0 ) )
35 8 10 syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ℝ )
36 5 oveq1i ⊢ ( 𝑁 − 1 ) = ( ( ♯ ‘ 𝐹 ) − 1 )
37 fzo0end ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
38 7 12 37 3syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
39 36 38 eqeltrid ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
40 35 39 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ )
41 40 rexrd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ* )
42 sgncl ⊢ ( ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ* → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ∈ { - 1 , 0 , 1 } )
43 41 42 syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ∈ { - 1 , 0 , 1 } )
44 43 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ∈ { - 1 , 0 , 1 } )
45 s1fv ⊢ ( ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ∈ { - 1 , 0 , 1 } → ( ⟨“ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ”⟩ ‘ 0 ) = ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) )
46 44 45 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( ⟨“ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ”⟩ ‘ 0 ) = ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) )
47 34 46 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 = 1 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) )
48 fzossfz ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
49 48 38 sselid ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
50 pfxres ⊢ ( ( 𝐹 ∈ Word ℝ ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) = ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
51 8 49 50 syl2anc ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) = ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
52 51 oveq1d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝐹 ) ”⟩ ) = ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ++ ⟨“ ( lastS ‘ 𝐹 ) ”⟩ ) )
53 pfxlswccat ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) → ( ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝐹 ) ”⟩ ) = 𝐹 )
54 53 eqcomd ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) → 𝐹 = ( ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝐹 ) ”⟩ ) )
55 7 54 syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → 𝐹 = ( ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝐹 ) ”⟩ ) )
56 36 oveq2i ⊢ ( 0 ..^ ( 𝑁 − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) )
57 56 a1i ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 0 ..^ ( 𝑁 − 1 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
58 57 reseq2d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) = ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
59 36 a1i ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝑁 − 1 ) = ( ( ♯ ‘ 𝐹 ) − 1 ) )
60 59 fveq2d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 ‘ ( 𝑁 − 1 ) ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
61 lsw ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) → ( lastS ‘ 𝐹 ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
62 61 adantr ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( lastS ‘ 𝐹 ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
63 60 62 eqtr4d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 ‘ ( 𝑁 − 1 ) ) = ( lastS ‘ 𝐹 ) )
64 63 s1eqd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ = ⟨“ ( lastS ‘ 𝐹 ) ”⟩ )
65 58 64 oveq12d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) = ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ++ ⟨“ ( lastS ‘ 𝐹 ) ”⟩ ) )
66 52 55 65 3eqtr4d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) )
67 66 fveq2d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝑇 ‘ 𝐹 ) = ( 𝑇 ‘ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) )
68 ffn ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ℝ → 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
69 8 10 68 3syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
70 5 a1i ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → 𝑁 = ( ♯ ‘ 𝐹 ) )
71 70 oveq2d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
72 71 fneq2d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 Fn ( 0 ..^ 𝑁 ) ↔ 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
73 69 72 mpbird ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → 𝐹 Fn ( 0 ..^ 𝑁 ) )
74 5 13 eqeltrid ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → 𝑁 ∈ ℕ )
75 74 nnnn0d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → 𝑁 ∈ ℕ0 )
76 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
77 fzossrbm1 ⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
78 75 76 77 3syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
79 fnssres ⊢ ( ( 𝐹 Fn ( 0 ..^ 𝑁 ) ∧ ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) Fn ( 0 ..^ ( 𝑁 − 1 ) ) )
80 73 78 79 syl2anc ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) Fn ( 0 ..^ ( 𝑁 − 1 ) ) )
81 hashfn ⊢ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) Fn ( 0 ..^ ( 𝑁 − 1 ) ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) = ( ♯ ‘ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
82 80 81 syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) = ( ♯ ‘ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
83 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
84 hashfzo0 ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( 𝑁 − 1 ) ) ) = ( 𝑁 − 1 ) )
85 74 83 84 3syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ♯ ‘ ( 0 ..^ ( 𝑁 − 1 ) ) ) = ( 𝑁 − 1 ) )
86 82 85 eqtrd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) = ( 𝑁 − 1 ) )
87 86 eqcomd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝑁 − 1 ) = ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) )
88 67 87 fveq12d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 1 ) ) = ( ( 𝑇 ‘ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) ‘ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ) )
89 88 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 1 ) ) = ( ( 𝑇 ‘ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) ‘ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ) )
90 51 58 eqtr4d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) = ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
91 pfxcl ⊢ ( 𝐹 ∈ Word ℝ → ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ Word ℝ )
92 8 91 syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ Word ℝ )
93 90 92 eqeltrrd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ∈ Word ℝ )
94 93 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ∈ Word ℝ )
95 86 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) = ( 𝑁 − 1 ) )
96 74 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → 𝑁 ∈ ℕ )
97 96 nncnd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → 𝑁 ∈ ℂ )
98 1cnd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → 1 ∈ ℂ )
99 simpr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → 𝑁 ≠ 1 )
100 97 98 99 subne0d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( 𝑁 − 1 ) ≠ 0 )
101 95 100 eqnetrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ≠ 0 )
102 fveq2 ⊢ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) = ∅ → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) = ( ♯ ‘ ∅ ) )
103 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
104 102 103 eqtrdi ⊢ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) = ∅ → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) = 0 )
105 104 necon3i ⊢ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ≠ 0 → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ≠ ∅ )
106 101 105 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ≠ ∅ )
107 94 106 jca ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ∈ Word ℝ ∧ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ≠ ∅ ) )
108 eldifsn ⊢ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ∈ Word ℝ ∧ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ≠ ∅ ) )
109 107 108 sylibr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ∈ ( Word ℝ ∖ { ∅ } ) )
110 40 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ )
111 1 2 3 4 signstfvn ⊢ ( ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ ) → ( ( 𝑇 ‘ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) ‘ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ) = ( ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) − 1 ) ) ⨣ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ) )
112 109 110 111 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( ( 𝑇 ‘ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) ‘ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ) = ( ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) − 1 ) ) ⨣ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ) )
113 lennncl ⊢ ( ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ∈ Word ℝ ∧ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ≠ ∅ ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ∈ ℕ )
114 fzo0end ⊢ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ∈ ℕ → ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ) )
115 107 113 114 3syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ) )
116 1 2 3 4 signstcl ⊢ ( ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ∈ Word ℝ ∧ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) − 1 ) ) ∈ { - 1 , 0 , 1 } )
117 94 115 116 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) − 1 ) ) ∈ { - 1 , 0 , 1 } )
118 43 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ∈ { - 1 , 0 , 1 } )
119 simpr ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 )
120 sgn0bi ⊢ ( ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ* → ( ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) = 0 ↔ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) )
121 120 necon3bid ⊢ ( ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ* → ( ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ≠ 0 ↔ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) )
122 121 biimpar ⊢ ( ( ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ* ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ≠ 0 )
123 41 119 122 syl2anc ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ≠ 0 )
124 123 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ≠ 0 )
125 1 2 signswlid ⊢ ( ( ( ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) − 1 ) ) ∈ { - 1 , 0 , 1 } ∧ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ∈ { - 1 , 0 , 1 } ) ∧ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ≠ 0 ) → ( ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) − 1 ) ) ⨣ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ) = ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) )
126 117 118 124 125 syl21anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 − 1 ) ) ) ) − 1 ) ) ⨣ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ) = ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) )
127 89 112 126 3eqtrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ 𝑁 ≠ 1 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) )
128 47 127 pm2.61dane ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) )