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 ⊢ ⨣ = ( 𝑎 ∈ { - 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 ) )
signstfveq0.1 ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
Assertion signstfveq0 ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 1 ) ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) )

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 signstfveq0.1 ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
6 simpll ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) )
7 6 eldifad ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 𝐹 ∈ Word ℝ )
8 pfxcl ⊢ ( 𝐹 ∈ Word ℝ → ( 𝐹 prefix ( 𝑁 − 1 ) ) ∈ Word ℝ )
9 7 8 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝐹 prefix ( 𝑁 − 1 ) ) ∈ Word ℝ )
10 1nn0 ⊢ 1 ∈ ℕ0
11 10 a1i ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 1 ∈ ℕ0 )
12 11 nn0red ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 1 ∈ ℝ )
13 2re ⊢ 2 ∈ ℝ
14 13 a1i ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 2 ∈ ℝ )
15 lencl ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
16 7 15 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
17 5 16 eqeltrid ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 𝑁 ∈ ℕ0 )
18 17 nn0red ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 𝑁 ∈ ℝ )
19 1le2 ⊢ 1 ≤ 2
20 19 a1i ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 1 ≤ 2 )
21 1 2 3 4 5 signstfveq0a ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
22 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
23 21 22 sylib ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
24 23 simp3d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 2 ≤ 𝑁 )
25 12 14 18 20 24 letrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 1 ≤ 𝑁 )
26 fznn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ∈ ( 0 ... 𝑁 ) ↔ ( 1 ∈ ℕ0 ∧ 1 ≤ 𝑁 ) ) )
27 17 26 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 1 ∈ ( 0 ... 𝑁 ) ↔ ( 1 ∈ ℕ0 ∧ 1 ≤ 𝑁 ) ) )
28 11 25 27 mpbir2and ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 1 ∈ ( 0 ... 𝑁 ) )
29 fznn0sub2 ⊢ ( 1 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 1 ) ∈ ( 0 ... 𝑁 ) )
30 28 29 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑁 − 1 ) ∈ ( 0 ... 𝑁 ) )
31 5 oveq2i ⊢ ( 0 ... 𝑁 ) = ( 0 ... ( ♯ ‘ 𝐹 ) )
32 30 31 eleqtrdi ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑁 − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
33 pfxlen ⊢ ( ( 𝐹 ∈ Word ℝ ∧ ( 𝑁 − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) = ( 𝑁 − 1 ) )
34 7 32 33 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) = ( 𝑁 − 1 ) )
35 uz2m1nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ )
36 21 35 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑁 − 1 ) ∈ ℕ )
37 34 36 eqeltrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ∈ ℕ )
38 nnne0 ⊢ ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ∈ ℕ → ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ≠ 0 )
39 fveq2 ⊢ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) = ∅ → ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) = ( ♯ ‘ ∅ ) )
40 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
41 39 40 eqtrdi ⊢ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) = ∅ → ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) = 0 )
42 41 necon3i ⊢ ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ≠ 0 → ( 𝐹 prefix ( 𝑁 − 1 ) ) ≠ ∅ )
43 38 42 syl ⊢ ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ∈ ℕ → ( 𝐹 prefix ( 𝑁 − 1 ) ) ≠ ∅ )
44 37 43 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝐹 prefix ( 𝑁 − 1 ) ) ≠ ∅ )
45 eldifsn ⊢ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ∈ Word ℝ ∧ ( 𝐹 prefix ( 𝑁 − 1 ) ) ≠ ∅ ) )
46 9 44 45 sylanbrc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝐹 prefix ( 𝑁 − 1 ) ) ∈ ( Word ℝ ∖ { ∅ } ) )
47 simpr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 )
48 0re ⊢ 0 ∈ ℝ
49 47 48 eqeltrdi ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ )
50 1 2 3 4 signstfvn ⊢ ( ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ ) → ( ( 𝑇 ‘ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) ‘ ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ) = ( ( ( 𝑇 ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) − 1 ) ) ⨣ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ) )
51 46 49 50 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑇 ‘ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) ‘ ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ) = ( ( ( 𝑇 ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) − 1 ) ) ⨣ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ) )
52 5 oveq1i ⊢ ( 𝑁 − 1 ) = ( ( ♯ ‘ 𝐹 ) − 1 )
53 52 oveq2i ⊢ ( 𝐹 prefix ( 𝑁 − 1 ) ) = ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) )
54 53 a1i ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝐹 prefix ( 𝑁 − 1 ) ) = ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
55 lsw ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) → ( lastS ‘ 𝐹 ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
56 55 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( lastS ‘ 𝐹 ) = ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
57 5 eqcomi ⊢ ( ♯ ‘ 𝐹 ) = 𝑁
58 57 oveq1i ⊢ ( ( ♯ ‘ 𝐹 ) − 1 ) = ( 𝑁 − 1 )
59 58 fveq2i ⊢ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) = ( 𝐹 ‘ ( 𝑁 − 1 ) )
60 56 59 eqtrdi ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( lastS ‘ 𝐹 ) = ( 𝐹 ‘ ( 𝑁 − 1 ) ) )
61 60 s1eqd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ⟨“ ( lastS ‘ 𝐹 ) ”⟩ = ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ )
62 61 eqcomd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ = ⟨“ ( lastS ‘ 𝐹 ) ”⟩ )
63 54 62 oveq12d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) = ( ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝐹 ) ”⟩ ) )
64 eldifsn ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) )
65 6 64 sylib ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) )
66 pfxlswccat ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) → ( ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝐹 ) ”⟩ ) = 𝐹 )
67 65 66 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝐹 prefix ( ( ♯ ‘ 𝐹 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝐹 ) ”⟩ ) = 𝐹 )
68 63 67 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) = 𝐹 )
69 68 fveq2d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑇 ‘ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) = ( 𝑇 ‘ 𝐹 ) )
70 69 34 fveq12d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑇 ‘ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) ‘ ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 1 ) ) )
71 17 nn0cnd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 𝑁 ∈ ℂ )
72 1cnd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 1 ∈ ℂ )
73 71 72 72 subsub4d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − ( 1 + 1 ) ) )
74 1p1e2 ⊢ ( 1 + 1 ) = 2
75 74 oveq2i ⊢ ( 𝑁 − ( 1 + 1 ) ) = ( 𝑁 − 2 )
76 73 75 eqtrdi ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − 2 ) )
77 fzo0end ⊢ ( ( 𝑁 − 1 ) ∈ ℕ → ( ( 𝑁 − 1 ) − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
78 36 77 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑁 − 1 ) − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
79 76 78 eqeltrrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
80 34 oveq2d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ) = ( 0 ..^ ( 𝑁 − 1 ) ) )
81 79 80 eleqtrrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ) )
82 1 2 3 4 signstfvp ⊢ ( ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ∈ Word ℝ ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ∈ ℝ ∧ ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ) ) → ( ( 𝑇 ‘ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) ‘ ( 𝑁 − 2 ) ) = ( ( 𝑇 ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ‘ ( 𝑁 − 2 ) ) )
83 9 49 81 82 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑇 ‘ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) ‘ ( 𝑁 − 2 ) ) = ( ( 𝑇 ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ‘ ( 𝑁 − 2 ) ) )
84 68 eqcomd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 𝐹 = ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) )
85 84 fveq2d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑇 ‘ 𝐹 ) = ( 𝑇 ‘ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) )
86 85 fveq1d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) = ( ( 𝑇 ‘ ( ( 𝐹 prefix ( 𝑁 − 1 ) ) ++ ⟨“ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ”⟩ ) ) ‘ ( 𝑁 − 2 ) ) )
87 34 oveq1d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) − 1 ) = ( ( 𝑁 − 1 ) − 1 ) )
88 87 73 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) − 1 ) = ( 𝑁 − ( 1 + 1 ) ) )
89 88 75 eqtrdi ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) − 1 ) = ( 𝑁 − 2 ) )
90 89 fveq2d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑇 ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) − 1 ) ) = ( ( 𝑇 ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ‘ ( 𝑁 − 2 ) ) )
91 83 86 90 3eqtr4rd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑇 ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) − 1 ) ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) )
92 fveq2 ⊢ ( ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) = ( sgn ‘ 0 ) )
93 sgn0 ⊢ ( sgn ‘ 0 ) = 0
94 92 93 eqtrdi ⊢ ( ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) = 0 )
95 94 adantl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) = 0 )
96 91 95 oveq12d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( ( 𝑇 ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) − 1 ) ) ⨣ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ) = ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) ⨣ 0 ) )
97 uznn0sub ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 2 ) ∈ ℕ0 )
98 21 97 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑁 − 2 ) ∈ ℕ0 )
99 eluz2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
100 21 99 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 𝑁 ∈ ℕ )
101 2rp ⊢ 2 ∈ ℝ+
102 101 a1i ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → 2 ∈ ℝ+ )
103 18 102 ltsubrpd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑁 − 2 ) < 𝑁 )
104 elfzo0 ⊢ ( ( 𝑁 − 2 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( ( 𝑁 − 2 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ( 𝑁 − 2 ) < 𝑁 ) )
105 98 100 103 104 syl3anbrc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ 𝑁 ) )
106 5 oveq2i ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) )
107 105 106 eleqtrdi ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
108 1 2 3 4 signstcl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) ∈ { - 1 , 0 , 1 } )
109 7 107 108 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) ∈ { - 1 , 0 , 1 } )
110 1 2 signswrid ⊢ ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) ∈ { - 1 , 0 , 1 } → ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) ⨣ 0 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) )
111 109 110 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) ⨣ 0 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) )
112 96 111 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( ( 𝑇 ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 prefix ( 𝑁 − 1 ) ) ) − 1 ) ) ⨣ ( sgn ‘ ( 𝐹 ‘ ( 𝑁 − 1 ) ) ) ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) )
113 51 70 112 3eqtr3d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( 𝐹 ‘ ( 𝑁 − 1 ) ) = 0 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 1 ) ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑁 − 2 ) ) )