Metamath Proof Explorer

Theorem signsvfpn

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
signsvf.b ⊢ B = E ⁡ N − 1
Assertion signsvfpn ⊢ φ ∧ 0 < B ⁢ A → 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 signsvf.b ⊢ B = E ⁡ N − 1
11 8 recnd ⊢ φ → A ∈ ℂ
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 11 24 mulcomd ⊢ φ → A ⁢ B = B ⁢ A
26 25 breq2d ⊢ φ → 0 < A ⁢ B ↔ 0 < B ⁢ A
27 10 22 eqeltrid ⊢ φ → B ∈ ℝ
28 sgnmulsgp ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ⁢ B ↔ 0 < sgn ⁡ A ⁢ sgn ⁡ B
29 8 27 28 syl2anc ⊢ φ → 0 < A ⁢ B ↔ 0 < sgn ⁡ A ⁢ sgn ⁡ B
30 26 29 bitr3d ⊢ φ → 0 < B ⁢ A ↔ 0 < sgn ⁡ A ⁢ sgn ⁡ B
31 30 biimpa ⊢ φ ∧ 0 < B ⁢ A → 0 < sgn ⁡ A ⁢ sgn ⁡ B
32 5 adantr ⊢ φ ∧ 0 < B ⁢ A → E ∈ Word ℝ ∖ ∅
33 24 adantr ⊢ φ ∧ 0 < B ⁢ A → B ∈ ℂ
34 11 adantr ⊢ φ ∧ 0 < B ⁢ A → A ∈ ℂ
35 simpr ⊢ φ ∧ 0 < B ⁢ A → 0 < B ⁢ A
36 35 gt0ne0d ⊢ φ ∧ 0 < B ⁢ A → B ⁢ A ≠ 0
37 33 34 36 mulne0bad ⊢ φ ∧ 0 < B ⁢ A → B ≠ 0
38 10 37 eqnetrrid ⊢ φ ∧ 0 < B ⁢ A → E ⁡ N − 1 ≠ 0
39 1 2 3 4 9 signsvtn0 ⊢ E ∈ Word ℝ ∖ ∅ ∧ E ⁡ N − 1 ≠ 0 → T ⁡ E ⁡ N − 1 = sgn ⁡ E ⁡ N − 1
40 10 fveq2i ⊢ sgn ⁡ B = sgn ⁡ E ⁡ N − 1
41 39 40 eqtr4di ⊢ E ∈ Word ℝ ∖ ∅ ∧ E ⁡ N − 1 ≠ 0 → T ⁡ E ⁡ N − 1 = sgn ⁡ B
42 32 38 41 syl2anc ⊢ φ ∧ 0 < B ⁢ A → T ⁡ E ⁡ N − 1 = sgn ⁡ B
43 42 fveq2d ⊢ φ ∧ 0 < B ⁢ A → sgn ⁡ T ⁡ E ⁡ N − 1 = sgn ⁡ sgn ⁡ B
44 27 adantr ⊢ φ ∧ 0 < B ⁢ A → B ∈ ℝ
45 44 rexrd ⊢ φ ∧ 0 < B ⁢ A → B ∈ ℝ *
46 sgnsgn ⊢ B ∈ ℝ * → sgn ⁡ sgn ⁡ B = sgn ⁡ B
47 45 46 syl ⊢ φ ∧ 0 < B ⁢ A → sgn ⁡ sgn ⁡ B = sgn ⁡ B
48 43 47 eqtrd ⊢ φ ∧ 0 < B ⁢ A → sgn ⁡ T ⁡ E ⁡ N − 1 = sgn ⁡ B
49 48 oveq2d ⊢ φ ∧ 0 < B ⁢ A → sgn ⁡ A ⁢ sgn ⁡ T ⁡ E ⁡ N − 1 = sgn ⁡ A ⁢ sgn ⁡ B
50 31 49 breqtrrd ⊢ φ ∧ 0 < B ⁢ A → 0 < sgn ⁡ A ⁢ sgn ⁡ T ⁡ E ⁡ N − 1
51 8 adantr ⊢ φ ∧ 0 < B ⁢ A → A ∈ ℝ
52 sgnclre ⊢ B ∈ ℝ → sgn ⁡ B ∈ ℝ
53 44 52 syl ⊢ φ ∧ 0 < B ⁢ A → sgn ⁡ B ∈ ℝ
54 42 53 eqeltrd ⊢ φ ∧ 0 < B ⁢ A → T ⁡ E ⁡ N − 1 ∈ ℝ
55 sgnmulsgp ⊢ A ∈ ℝ ∧ T ⁡ E ⁡ N − 1 ∈ ℝ → 0 < A ⁢ T ⁡ E ⁡ N − 1 ↔ 0 < sgn ⁡ A ⁢ sgn ⁡ T ⁡ E ⁡ N − 1
56 51 54 55 syl2anc ⊢ φ ∧ 0 < B ⁢ A → 0 < A ⁢ T ⁡ E ⁡ N − 1 ↔ 0 < sgn ⁡ A ⁢ sgn ⁡ T ⁡ E ⁡ N − 1
57 50 56 mpbird ⊢ φ ∧ 0 < B ⁢ A → 0 < A ⁢ T ⁡ E ⁡ N − 1
58 eqid ⊢ T ⁡ E ⁡ N − 1 = T ⁡ E ⁡ N − 1
59 1 2 3 4 5 6 7 8 9 58 signsvtp ⊢ φ ∧ 0 < A ⁢ T ⁡ E ⁡ N − 1 → V ⁡ F = V ⁡ E
60 57 59 syldan ⊢ φ ∧ 0 < B ⁢ A → V ⁡ F = V ⁡ E