Metamath Proof Explorer


Theorem signsvtp

Description: Adding a letter of the same sign as the highest coefficient does not change 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
signsvt.b B = T E N 1
Assertion signsvtp φ 0 < A B V F = V E

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 signsvt.b B = T E N 1
11 7 fveq2d φ V F = V E ++ ⟨“ A ”⟩
12 1 2 3 4 signsvfn E Word E 0 0 A V E ++ ⟨“ A ”⟩ = V E + if T E E 1 A < 0 1 0
13 5 6 8 12 syl21anc φ V E ++ ⟨“ A ”⟩ = V E + if T E E 1 A < 0 1 0
14 11 13 eqtrd φ V F = V E + if T E E 1 A < 0 1 0
15 14 adantr φ 0 < A B V F = V E + if T E E 1 A < 0 1 0
16 0red φ 0 < A B 0
17 5 adantr φ 0 < A B E Word
18 17 eldifad φ 0 < A B E Word
19 1 2 3 4 signstf E Word T E Word
20 wrdf T E Word T E : 0 ..^ T E
21 18 19 20 3syl φ 0 < A B T E : 0 ..^ T E
22 eldifsn E Word E Word E
23 5 22 sylib φ E Word E
24 23 adantr φ 0 < A B E Word E
25 lennncl E Word E E
26 fzo0end E E 1 0 ..^ E
27 24 25 26 3syl φ 0 < A B E 1 0 ..^ E
28 1 2 3 4 signstlen E Word T E = E
29 18 28 syl φ 0 < A B T E = E
30 29 oveq2d φ 0 < A B 0 ..^ T E = 0 ..^ E
31 27 30 eleqtrrd φ 0 < A B E 1 0 ..^ T E
32 21 31 ffvelrnd φ 0 < A B T E E 1
33 8 adantr φ 0 < A B A
34 32 33 remulcld φ 0 < A B T E E 1 A
35 simpr φ 0 < A B 0 < A B
36 9 oveq1i N 1 = E 1
37 36 fveq2i T E N 1 = T E E 1
38 10 37 eqtri B = T E E 1
39 38 32 eqeltrid φ 0 < A B B
40 39 recnd φ 0 < A B B
41 33 recnd φ 0 < A B A
42 40 41 mulcomd φ 0 < A B B A = A B
43 35 42 breqtrrd φ 0 < A B 0 < B A
44 38 oveq1i B A = T E E 1 A
45 43 44 breqtrdi φ 0 < A B 0 < T E E 1 A
46 16 34 45 ltnsymd φ 0 < A B ¬ T E E 1 A < 0
47 46 iffalsed φ 0 < A B if T E E 1 A < 0 1 0 = 0
48 47 oveq2d φ 0 < A B V E + if T E E 1 A < 0 1 0 = V E + 0
49 1 2 3 4 signsvvf V : Word 0
50 49 a1i φ 0 < A B V : Word 0
51 50 18 ffvelrnd φ 0 < A B V E 0
52 51 nn0cnd φ 0 < A B V E
53 52 addid1d φ 0 < A B V E + 0 = V E
54 15 48 53 3eqtrd φ 0 < A B V F = V E