Metamath Proof Explorer


Theorem signsvfnn

Description: Adding a letter of a different sign as the highest coefficient changes the sign. (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
signsvf.e φ E Word
signsvf.0 φ E 0 0
signsvf.f φ F = E ++ ⟨“ A ”⟩
signsvf.a φ A
signsvf.n N = E
signsvf.b B = E N 1
Assertion signsvfnn φ B A < 0 V F V E = 1

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 signsvf.e φ E Word
6 signsvf.0 φ E 0 0
7 signsvf.f φ F = E ++ ⟨“ A ”⟩
8 signsvf.a φ A
9 signsvf.n N = E
10 signsvf.b B = E N 1
11 5 adantr φ B A < 0 E Word
12 5 eldifad φ E Word
13 wrdf E Word E : 0 ..^ E
14 12 13 syl φ E : 0 ..^ E
15 9 oveq1i N 1 = E 1
16 eldifsn E Word E Word E
17 5 16 sylib φ E Word E
18 lennncl E Word E E
19 fzo0end E E 1 0 ..^ E
20 17 18 19 3syl φ E 1 0 ..^ E
21 15 20 eqeltrid φ N 1 0 ..^ E
22 14 21 ffvelrnd φ E N 1
23 22 recnd φ E N 1
24 10 23 eqeltrid φ B
25 24 adantr φ B A < 0 B
26 8 recnd φ A
27 26 adantr φ B A < 0 A
28 simpr φ B A < 0 B A < 0
29 28 lt0ne0d φ B A < 0 B A 0
30 25 27 29 mulne0bad φ B A < 0 B 0
31 10 30 eqnetrrid φ B A < 0 E N 1 0
32 1 2 3 4 9 signsvtn0 E Word E N 1 0 T E N 1 = sgn E N 1
33 10 fveq2i sgn B = sgn E N 1
34 32 33 eqtr4di E Word E N 1 0 T E N 1 = sgn B
35 11 31 34 syl2anc φ B A < 0 T E N 1 = sgn B
36 35 fveq2d φ B A < 0 sgn T E N 1 = sgn sgn B
37 10 22 eqeltrid φ B
38 37 adantr φ B A < 0 B
39 38 rexrd φ B A < 0 B *
40 sgnsgn B * sgn sgn B = sgn B
41 39 40 syl φ B A < 0 sgn sgn B = sgn B
42 36 41 eqtrd φ B A < 0 sgn T E N 1 = sgn B
43 42 oveq2d φ B A < 0 sgn A sgn T E N 1 = sgn A sgn B
44 26 24 mulcomd φ A B = B A
45 44 breq1d φ A B < 0 B A < 0
46 sgnmulsgn A B A B < 0 sgn A sgn B < 0
47 8 37 46 syl2anc φ A B < 0 sgn A sgn B < 0
48 45 47 bitr3d φ B A < 0 sgn A sgn B < 0
49 48 biimpa φ B A < 0 sgn A sgn B < 0
50 43 49 eqbrtrd φ B A < 0 sgn A sgn T E N 1 < 0
51 8 adantr φ B A < 0 A
52 sgnclre B sgn B
53 38 52 syl φ B A < 0 sgn B
54 35 53 eqeltrd φ B A < 0 T E N 1
55 sgnmulsgn A T E N 1 A T E N 1 < 0 sgn A sgn T E N 1 < 0
56 51 54 55 syl2anc φ B A < 0 A T E N 1 < 0 sgn A sgn T E N 1 < 0
57 50 56 mpbird φ B A < 0 A T E N 1 < 0
58 eqid T E N 1 = T E N 1
59 1 2 3 4 5 6 7 8 9 58 signsvtn φ A T E N 1 < 0 V F V E = 1
60 57 59 syldan φ B A < 0 V F V E = 1