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