Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  signlem0 Structured version   Unicode version

Theorem signlem0 27119
 Description: Adding a zero as the highest coefficient does not change the parity of the sign changes. (Contributed by Thierry Arnoux, 12-Oct-2018.)
Hypotheses
Ref Expression
signsv.p
signsv.w
signsv.t Word ..^ g sgn
signsv.v Word ..^
Assertion
Ref Expression
signlem0 Word concat
Distinct variable groups:   ,,   ,,,   ,,,   ,,,,,,   ,   ,,,,
Allowed substitution hints:   (,,,)   ()   (,,,,,)   (,,)

Proof of Theorem signlem0
StepHypRef Expression
1 0re 9484 . . . 4
21a1i 11 . . 3 Word
3 signsv.p . . . 4
4 signsv.w . . . 4
5 signsv.t . . . 4 Word ..^ g sgn
6 signsv.v . . . 4 Word ..^
73, 4, 5, 6signsvfn 27114 . . 3 Word concat
82, 7mpdan 668 . 2 Word concat
91ltnri 9581 . . . . 5
10 neg1cn 10523 . . . . . . . . 9
11 ax-1cn 9438 . . . . . . . . 9
12 prssi 4124 . . . . . . . . 9
1310, 11, 12mp2an 672 . . . . . . . 8
14 simpl 457 . . . . . . . . 9 Word Word
15 simpr 461 . . . . . . . . 9 Word
16 eldifsn 4095 . . . . . . . . . . . 12 Word Word
1714, 16sylib 196 . . . . . . . . . . 11 Word Word
18 lennncl 12349 . . . . . . . . . . 11 Word
1917, 18syl 16 . . . . . . . . . 10 Word
20 fzo0end 11717 . . . . . . . . . 10 ..^
2119, 20syl 16 . . . . . . . . 9 Word ..^
223, 4, 5, 6signstfvcl 27105 . . . . . . . . 9 Word ..^
2314, 15, 21, 22syl21anc 1218 . . . . . . . 8 Word
2413, 23sseldi 3449 . . . . . . 7 Word
2524mul01d 9666 . . . . . 6 Word
2625breq1d 4397 . . . . 5 Word
279, 26mtbiri 303 . . . 4 Word
28 iffalse 3894 . . . 4
2927, 28syl 16 . . 3 Word
3029oveq2d 6203 . 2 Word
313, 4, 5, 6signsvvf 27111 . . . . . 6 Word
3231a1i 11 . . . . 5 Word Word
3314eldifad 3435 . . . . 5 Word Word
3432, 33ffvelrnd 5940 . . . 4 Word
3534nn0cnd 10736 . . 3 Word