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 ffvelrnd ( ( ( 𝐹 ∈ ( 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 ffvelrnd ( ( 𝐹 ∈ ( 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 ) ) ) )