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 ffvelrnd ( 𝜑 → ( 𝐸 ‘ ( 𝑁 − 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 < ( 𝐵 · 𝐴 ) ) → ( 𝑉𝐹 ) = ( 𝑉𝐸 ) )