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 ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
signsv.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
signsv.t ⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) )
signsv.v ⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
signsvf.e ⊢ ( 𝜑 → 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) )
signsvf.0 ⊢ ( 𝜑 → ( 𝐸 ‘ 0 ) ≠ 0 )
signsvf.f ⊢ ( 𝜑 → 𝐹 = ( 𝐸 ++ ⟨“ 𝐴 ”⟩ ) )
signsvf.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
signsvf.n ⊢ 𝑁 = ( ♯ ‘ 𝐸 )
signsvf.b ⊢ 𝐵 = ( 𝐸 ‘ ( 𝑁 − 1 ) )
Assertion signsvfpn ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( 𝑉 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 signsv.p ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
2 signsv.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
3 signsv.t ⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) )
4 signsv.v ⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
5 signsvf.e ⊢ ( 𝜑 → 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) )
6 signsvf.0 ⊢ ( 𝜑 → ( 𝐸 ‘ 0 ) ≠ 0 )
7 signsvf.f ⊢ ( 𝜑 → 𝐹 = ( 𝐸 ++ ⟨“ 𝐴 ”⟩ ) )
8 signsvf.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
9 signsvf.n ⊢ 𝑁 = ( ♯ ‘ 𝐸 )
10 signsvf.b ⊢ 𝐵 = ( 𝐸 ‘ ( 𝑁 − 1 ) )
11 8 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
12 5 eldifad ⊢ ( 𝜑 → 𝐸 ∈ Word ℝ )
13 wrdf ⊢ ( 𝐸 ∈ Word ℝ → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ ℝ )
14 12 13 syl ⊢ ( 𝜑 → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ ℝ )
15 9 oveq1i ⊢ ( 𝑁 − 1 ) = ( ( ♯ ‘ 𝐸 ) − 1 )
16 eldifsn ⊢ ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) )
17 5 16 sylib ⊢ ( 𝜑 → ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) )
18 lennncl ⊢ ( ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) → ( ♯ ‘ 𝐸 ) ∈ ℕ )
19 fzo0end ⊢ ( ( ♯ ‘ 𝐸 ) ∈ ℕ → ( ( ♯ ‘ 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
20 17 18 19 3syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
21 15 20 eqeltrid ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
22 14 21 ffvelcdmd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑁 − 1 ) ) ∈ ℝ )
23 22 recnd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑁 − 1 ) ) ∈ ℂ )
24 10 23 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
25 11 24 mulcomd ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
26 25 breq2d ⊢ ( 𝜑 → ( 0 < ( 𝐴 · 𝐵 ) ↔ 0 < ( 𝐵 · 𝐴 ) ) )
27 10 22 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
28 sgnmulsgp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < ( 𝐴 · 𝐵 ) ↔ 0 < ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) ) )
29 8 27 28 syl2anc ⊢ ( 𝜑 → ( 0 < ( 𝐴 · 𝐵 ) ↔ 0 < ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) ) )
30 26 29 bitr3d ⊢ ( 𝜑 → ( 0 < ( 𝐵 · 𝐴 ) ↔ 0 < ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) ) )
31 30 biimpa ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 0 < ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) )
32 5 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) )
33 24 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 𝐵 ∈ ℂ )
34 11 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 𝐴 ∈ ℂ )
35 simpr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 0 < ( 𝐵 · 𝐴 ) )
36 35 gt0ne0d ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( 𝐵 · 𝐴 ) ≠ 0 )
37 33 34 36 mulne0bad ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 𝐵 ≠ 0 )
38 10 37 eqnetrrid ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( 𝐸 ‘ ( 𝑁 − 1 ) ) ≠ 0 )
39 1 2 3 4 9 signsvtn0 ⊢ ( ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐸 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ ( 𝐸 ‘ ( 𝑁 − 1 ) ) ) )
40 10 fveq2i ⊢ ( sgn ‘ 𝐵 ) = ( sgn ‘ ( 𝐸 ‘ ( 𝑁 − 1 ) ) )
41 39 40 eqtr4di ⊢ ( ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐸 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ 𝐵 ) )
42 32 38 41 syl2anc ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ 𝐵 ) )
43 42 fveq2d ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) = ( sgn ‘ ( sgn ‘ 𝐵 ) ) )
44 27 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 𝐵 ∈ ℝ )
45 44 rexrd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 𝐵 ∈ ℝ* )
46 sgnsgn ⊢ ( 𝐵 ∈ ℝ* → ( sgn ‘ ( sgn ‘ 𝐵 ) ) = ( sgn ‘ 𝐵 ) )
47 45 46 syl ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( sgn ‘ ( sgn ‘ 𝐵 ) ) = ( sgn ‘ 𝐵 ) )
48 43 47 eqtrd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) = ( sgn ‘ 𝐵 ) )
49 48 oveq2d ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) = ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) )
50 31 49 breqtrrd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 0 < ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) )
51 8 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 𝐴 ∈ ℝ )
52 sgnclre ⊢ ( 𝐵 ∈ ℝ → ( sgn ‘ 𝐵 ) ∈ ℝ )
53 44 52 syl ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( sgn ‘ 𝐵 ) ∈ ℝ )
54 42 53 eqeltrd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ∈ ℝ )
55 sgnmulsgp ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ∈ ℝ ) → ( 0 < ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ↔ 0 < ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) ) )
56 51 54 55 syl2anc ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( 0 < ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ↔ 0 < ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) ) )
57 50 56 mpbird ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → 0 < ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) )
58 eqid ⊢ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) )
59 1 2 3 4 5 6 7 8 9 58 signsvtp ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) → ( 𝑉 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐸 ) )
60 57 59 syldan ⊢ ( ( 𝜑 ∧ 0 < ( 𝐵 · 𝐴 ) ) → ( 𝑉 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐸 ) )