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 ˙ = a 1 0 1 , b 1 0 1 if b = 0 a b
signsv.w W = Base ndx 1 0 1 + ndx ˙
signsv.t T = f Word n 0 ..^ f W i = 0 n sgn f i
signsv.v V = f Word j 1 ..^ f if T f j T f j 1 1 0
signstfveq0.1 N = F
Assertion signstfveq0 F Word F 0 0 F N 1 = 0 T F N 1 = T F N 2

Proof

Step Hyp Ref Expression
1 signsv.p ˙ = a 1 0 1 , b 1 0 1 if b = 0 a b
2 signsv.w W = Base ndx 1 0 1 + ndx ˙
3 signsv.t T = f Word n 0 ..^ f W i = 0 n sgn f i
4 signsv.v V = f Word j 1 ..^ f if T f j T f j 1 1 0
5 signstfveq0.1 N = F
6 simpll F Word F 0 0 F N 1 = 0 F Word
7 6 eldifad F Word F 0 0 F N 1 = 0 F Word
8 pfxcl F Word F prefix N 1 Word
9 7 8 syl F Word F 0 0 F N 1 = 0 F prefix N 1 Word
10 1nn0 1 0
11 10 a1i F Word F 0 0 F N 1 = 0 1 0
12 11 nn0red F Word F 0 0 F N 1 = 0 1
13 2re 2
14 13 a1i F Word F 0 0 F N 1 = 0 2
15 lencl F Word F 0
16 7 15 syl F Word F 0 0 F N 1 = 0 F 0
17 5 16 eqeltrid F Word F 0 0 F N 1 = 0 N 0
18 17 nn0red F Word F 0 0 F N 1 = 0 N
19 1le2 1 2
20 19 a1i F Word F 0 0 F N 1 = 0 1 2
21 1 2 3 4 5 signstfveq0a F Word F 0 0 F N 1 = 0 N 2
22 eluz2 N 2 2 N 2 N
23 21 22 sylib F Word F 0 0 F N 1 = 0 2 N 2 N
24 23 simp3d F Word F 0 0 F N 1 = 0 2 N
25 12 14 18 20 24 letrd F Word F 0 0 F N 1 = 0 1 N
26 fznn0 N 0 1 0 N 1 0 1 N
27 17 26 syl F Word F 0 0 F N 1 = 0 1 0 N 1 0 1 N
28 11 25 27 mpbir2and F Word F 0 0 F N 1 = 0 1 0 N
29 fznn0sub2 1 0 N N 1 0 N
30 28 29 syl F Word F 0 0 F N 1 = 0 N 1 0 N
31 5 oveq2i 0 N = 0 F
32 30 31 eleqtrdi F Word F 0 0 F N 1 = 0 N 1 0 F
33 pfxlen F Word N 1 0 F F prefix N 1 = N 1
34 7 32 33 syl2anc F Word F 0 0 F N 1 = 0 F prefix N 1 = N 1
35 uz2m1nn N 2 N 1
36 21 35 syl F Word F 0 0 F N 1 = 0 N 1
37 34 36 eqeltrd F Word F 0 0 F N 1 = 0 F prefix N 1
38 nnne0 F prefix N 1 F prefix N 1 0
39 fveq2 F prefix N 1 = F prefix N 1 =
40 hash0 = 0
41 39 40 eqtrdi F prefix N 1 = F prefix N 1 = 0
42 41 necon3i F prefix N 1 0 F prefix N 1
43 38 42 syl F prefix N 1 F prefix N 1
44 37 43 syl F Word F 0 0 F N 1 = 0 F prefix N 1
45 eldifsn F prefix N 1 Word F prefix N 1 Word F prefix N 1
46 9 44 45 sylanbrc F Word F 0 0 F N 1 = 0 F prefix N 1 Word
47 simpr F Word F 0 0 F N 1 = 0 F N 1 = 0
48 0re 0
49 47 48 eqeltrdi F Word F 0 0 F N 1 = 0 F N 1
50 1 2 3 4 signstfvn F prefix N 1 Word F N 1 T F prefix N 1 ++ ⟨“ F N 1 ”⟩ F prefix N 1 = T F prefix N 1 F prefix N 1 1 ˙ sgn F N 1
51 46 49 50 syl2anc F Word F 0 0 F N 1 = 0 T F prefix N 1 ++ ⟨“ F N 1 ”⟩ F prefix N 1 = T F prefix N 1 F prefix N 1 1 ˙ sgn F N 1
52 5 oveq1i N 1 = F 1
53 52 oveq2i F prefix N 1 = F prefix F 1
54 53 a1i F Word F 0 0 F N 1 = 0 F prefix N 1 = F prefix F 1
55 lsw F Word lastS F = F F 1
56 55 ad2antrr F Word F 0 0 F N 1 = 0 lastS F = F F 1
57 5 eqcomi F = N
58 57 oveq1i F 1 = N 1
59 58 fveq2i F F 1 = F N 1
60 56 59 eqtrdi F Word F 0 0 F N 1 = 0 lastS F = F N 1
61 60 s1eqd F Word F 0 0 F N 1 = 0 ⟨“ lastS F ”⟩ = ⟨“ F N 1 ”⟩
62 61 eqcomd F Word F 0 0 F N 1 = 0 ⟨“ F N 1 ”⟩ = ⟨“ lastS F ”⟩
63 54 62 oveq12d F Word F 0 0 F N 1 = 0 F prefix N 1 ++ ⟨“ F N 1 ”⟩ = F prefix F 1 ++ ⟨“ lastS F ”⟩
64 eldifsn F Word F Word F
65 6 64 sylib F Word F 0 0 F N 1 = 0 F Word F
66 pfxlswccat F Word F F prefix F 1 ++ ⟨“ lastS F ”⟩ = F
67 65 66 syl F Word F 0 0 F N 1 = 0 F prefix F 1 ++ ⟨“ lastS F ”⟩ = F
68 63 67 eqtrd F Word F 0 0 F N 1 = 0 F prefix N 1 ++ ⟨“ F N 1 ”⟩ = F
69 68 fveq2d F Word F 0 0 F N 1 = 0 T F prefix N 1 ++ ⟨“ F N 1 ”⟩ = T F
70 69 34 fveq12d F Word F 0 0 F N 1 = 0 T F prefix N 1 ++ ⟨“ F N 1 ”⟩ F prefix N 1 = T F N 1
71 17 nn0cnd F Word F 0 0 F N 1 = 0 N
72 1cnd F Word F 0 0 F N 1 = 0 1
73 71 72 72 subsub4d F Word F 0 0 F N 1 = 0 N - 1 - 1 = N 1 + 1
74 1p1e2 1 + 1 = 2
75 74 oveq2i N 1 + 1 = N 2
76 73 75 eqtrdi F Word F 0 0 F N 1 = 0 N - 1 - 1 = N 2
77 fzo0end N 1 N - 1 - 1 0 ..^ N 1
78 36 77 syl F Word F 0 0 F N 1 = 0 N - 1 - 1 0 ..^ N 1
79 76 78 eqeltrrd F Word F 0 0 F N 1 = 0 N 2 0 ..^ N 1
80 34 oveq2d F Word F 0 0 F N 1 = 0 0 ..^ F prefix N 1 = 0 ..^ N 1
81 79 80 eleqtrrd F Word F 0 0 F N 1 = 0 N 2 0 ..^ F prefix N 1
82 1 2 3 4 signstfvp F prefix N 1 Word F N 1 N 2 0 ..^ F prefix N 1 T F prefix N 1 ++ ⟨“ F N 1 ”⟩ N 2 = T F prefix N 1 N 2
83 9 49 81 82 syl3anc F Word F 0 0 F N 1 = 0 T F prefix N 1 ++ ⟨“ F N 1 ”⟩ N 2 = T F prefix N 1 N 2
84 68 eqcomd F Word F 0 0 F N 1 = 0 F = F prefix N 1 ++ ⟨“ F N 1 ”⟩
85 84 fveq2d F Word F 0 0 F N 1 = 0 T F = T F prefix N 1 ++ ⟨“ F N 1 ”⟩
86 85 fveq1d F Word F 0 0 F N 1 = 0 T F N 2 = T F prefix N 1 ++ ⟨“ F N 1 ”⟩ N 2
87 34 oveq1d F Word F 0 0 F N 1 = 0 F prefix N 1 1 = N - 1 - 1
88 87 73 eqtrd F Word F 0 0 F N 1 = 0 F prefix N 1 1 = N 1 + 1
89 88 75 eqtrdi F Word F 0 0 F N 1 = 0 F prefix N 1 1 = N 2
90 89 fveq2d F Word F 0 0 F N 1 = 0 T F prefix N 1 F prefix N 1 1 = T F prefix N 1 N 2
91 83 86 90 3eqtr4rd F Word F 0 0 F N 1 = 0 T F prefix N 1 F prefix N 1 1 = T F N 2
92 fveq2 F N 1 = 0 sgn F N 1 = sgn 0
93 sgn0 sgn 0 = 0
94 92 93 eqtrdi F N 1 = 0 sgn F N 1 = 0
95 94 adantl F Word F 0 0 F N 1 = 0 sgn F N 1 = 0
96 91 95 oveq12d F Word F 0 0 F N 1 = 0 T F prefix N 1 F prefix N 1 1 ˙ sgn F N 1 = T F N 2 ˙ 0
97 uznn0sub N 2 N 2 0
98 21 97 syl F Word F 0 0 F N 1 = 0 N 2 0
99 eluz2nn N 2 N
100 21 99 syl F Word F 0 0 F N 1 = 0 N
101 2rp 2 +
102 101 a1i F Word F 0 0 F N 1 = 0 2 +
103 18 102 ltsubrpd F Word F 0 0 F N 1 = 0 N 2 < N
104 elfzo0 N 2 0 ..^ N N 2 0 N N 2 < N
105 98 100 103 104 syl3anbrc F Word F 0 0 F N 1 = 0 N 2 0 ..^ N
106 5 oveq2i 0 ..^ N = 0 ..^ F
107 105 106 eleqtrdi F Word F 0 0 F N 1 = 0 N 2 0 ..^ F
108 1 2 3 4 signstcl F Word N 2 0 ..^ F T F N 2 1 0 1
109 7 107 108 syl2anc F Word F 0 0 F N 1 = 0 T F N 2 1 0 1
110 1 2 signswrid T F N 2 1 0 1 T F N 2 ˙ 0 = T F N 2
111 109 110 syl F Word F 0 0 F N 1 = 0 T F N 2 ˙ 0 = T F N 2
112 96 111 eqtrd F Word F 0 0 F N 1 = 0 T F prefix N 1 F prefix N 1 1 ˙ sgn F N 1 = T F N 2
113 51 70 112 3eqtr3d F Word F 0 0 F N 1 = 0 T F N 1 = T F N 2