Metamath Proof Explorer


Theorem signlem0

Description: Adding a zero as the highest coefficient does not change the parity of the sign changes. (Contributed by Thierry Arnoux, 12-Oct-2018)

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
Assertion signlem0 F Word F 0 0 V F ++ ⟨“ 0 ”⟩ = V F

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 0re 0
6 1 2 3 4 signsvfn F Word F 0 0 0 V F ++ ⟨“ 0 ”⟩ = V F + if T F F 1 0 < 0 1 0
7 5 6 mpan2 F Word F 0 0 V F ++ ⟨“ 0 ”⟩ = V F + if T F F 1 0 < 0 1 0
8 5 ltnri ¬ 0 < 0
9 neg1cn 1
10 ax-1cn 1
11 prssi 1 1 1 1
12 9 10 11 mp2an 1 1
13 simpl F Word F 0 0 F Word
14 eldifsn F Word F Word F
15 13 14 sylib F Word F 0 0 F Word F
16 lennncl F Word F F
17 fzo0end F F 1 0 ..^ F
18 15 16 17 3syl F Word F 0 0 F 1 0 ..^ F
19 1 2 3 4 signstfvcl F Word F 0 0 F 1 0 ..^ F T F F 1 1 1
20 18 19 mpdan F Word F 0 0 T F F 1 1 1
21 12 20 sselid F Word F 0 0 T F F 1
22 21 mul01d F Word F 0 0 T F F 1 0 = 0
23 22 breq1d F Word F 0 0 T F F 1 0 < 0 0 < 0
24 8 23 mtbiri F Word F 0 0 ¬ T F F 1 0 < 0
25 24 iffalsed F Word F 0 0 if T F F 1 0 < 0 1 0 = 0
26 25 oveq2d F Word F 0 0 V F + if T F F 1 0 < 0 1 0 = V F + 0
27 1 2 3 4 signsvvf V : Word 0
28 27 a1i F Word F 0 0 V : Word 0
29 13 eldifad F Word F 0 0 F Word
30 28 29 ffvelrnd F Word F 0 0 V F 0
31 30 nn0cnd F Word F 0 0 V F
32 31 addid1d F Word F 0 0 V F + 0 = V F
33 7 26 32 3eqtrd F Word F 0 0 V F ++ ⟨“ 0 ”⟩ = V F