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

Theorem signsvtp 27121
 Description: Adding a letter of the same sign as the highest coefficient does not change the sign. (Contributed by Thierry Arnoux, 12-Oct-2018.)
Hypotheses
Ref Expression
signsv.p
signsv.w
signsv.t Word ..^ g sgn
signsv.v Word ..^
signsvf.e Word
signsvf.0
signsvf.f concat
signsvf.a
signsvf.n
signsvt.b
Assertion
Ref Expression
signsvtp
Distinct variable groups:   ,,   ,,,   ,,,   ,,,,,,   ,,,,,,   ,,,,,
Allowed substitution hints:   (,,,,,)   (,,,,,)   (,,,)   ()   (,,)   (,,,,,)   (,,,,,)   (,,)

Proof of Theorem signsvtp
StepHypRef Expression
1 signsvf.f . . . . 5 concat
21fveq2d 5796 . . . 4 concat
3 signsvf.e . . . . 5 Word
4 signsvf.0 . . . . 5
5 signsvf.a . . . . 5
6 signsv.p . . . . . 6
7 signsv.w . . . . . 6
8 signsv.t . . . . . 6 Word ..^ g sgn
9 signsv.v . . . . . 6 Word ..^
106, 7, 8, 9signsvfn 27120 . . . . 5 Word concat
113, 4, 5, 10syl21anc 1218 . . . 4 concat
122, 11eqtrd 2492 . . 3
14 0re 9490 . . . . . 6
1514a1i 11 . . . . 5
163adantr 465 . . . . . . . . 9 Word
1716eldifad 3441 . . . . . . . 8 Word
186, 7, 8, 9signstf 27104 . . . . . . . 8 Word Word
19 wrdf 12351 . . . . . . . 8 Word ..^
2017, 18, 193syl 20 . . . . . . 7 ..^
21 eldifsn 4101 . . . . . . . . . . . 12 Word Word
223, 21sylib 196 . . . . . . . . . . 11 Word
2322adantr 465 . . . . . . . . . 10 Word
24 lennncl 12361 . . . . . . . . . 10 Word
2523, 24syl 16 . . . . . . . . 9
26 fzo0end 11729 . . . . . . . . 9 ..^
2725, 26syl 16 . . . . . . . 8 ..^
286, 7, 8, 9signstlen 27105 . . . . . . . . . 10 Word
2917, 28syl 16 . . . . . . . . 9
3029oveq2d 6209 . . . . . . . 8 ..^ ..^
3127, 30eleqtrrd 2542 . . . . . . 7 ..^
3220, 31ffvelrnd 5946 . . . . . 6
335adantr 465 . . . . . 6
3432, 33remulcld 9518 . . . . 5
35 simpr 461 . . . . . . 7
36 signsvt.b . . . . . . . . . . 11
37 signsvf.n . . . . . . . . . . . . 13
3837oveq1i 6203 . . . . . . . . . . . 12
3938fveq2i 5795 . . . . . . . . . . 11
4036, 39eqtri 2480 . . . . . . . . . 10
4140, 32syl5eqel 2543 . . . . . . . . 9
4241recnd 9516 . . . . . . . 8
4333recnd 9516 . . . . . . . 8
4442, 43mulcomd 9511 . . . . . . 7
4535, 44breqtrrd 4419 . . . . . 6
4640oveq1i 6203 . . . . . 6
4745, 46syl6breq 4432 . . . . 5
4815, 34, 47ltnsymd 9627 . . . 4
49 iffalse 3900 . . . 4
5048, 49syl 16 . . 3
5150oveq2d 6209 . 2
526, 7, 8, 9signsvvf 27117 . . . . . 6 Word
5352a1i 11 . . . . 5 Word
5453, 17ffvelrnd 5946 . . . 4
5554nn0cnd 10742 . . 3