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 ) ) )