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 ⊢ ⨣ = ( 𝑎 ∈ { - 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 ⊢ 𝑁 = ( ♯ ‘ 𝐸 )
signsvt.b ⊢ 𝐵 = ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) )
Assertion signsvtp ( ( 𝜑 ∧ 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 signsvt.b ⊢ 𝐵 = ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) )
11 7 fveq2d ⊢ ( 𝜑 → ( 𝑉 ‘ 𝐹 ) = ( 𝑉 ‘ ( 𝐸 ++ ⟨“ 𝐴 ”⟩ ) ) )
12 1 2 3 4 signsvfn ⊢ ( ( ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐸 ‘ 0 ) ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → ( 𝑉 ‘ ( 𝐸 ++ ⟨“ 𝐴 ”⟩ ) ) = ( ( 𝑉 ‘ 𝐸 ) + if ( ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) < 0 , 1 , 0 ) ) )
13 5 6 8 12 syl21anc ⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐸 ++ ⟨“ 𝐴 ”⟩ ) ) = ( ( 𝑉 ‘ 𝐸 ) + if ( ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) < 0 , 1 , 0 ) ) )
14 11 13 eqtrd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝐹 ) = ( ( 𝑉 ‘ 𝐸 ) + if ( ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) < 0 , 1 , 0 ) ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝑉 ‘ 𝐹 ) = ( ( 𝑉 ‘ 𝐸 ) + if ( ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) < 0 , 1 , 0 ) ) )
16 0red ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 0 ∈ ℝ )
17 5 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) )
18 17 eldifad ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐸 ∈ Word ℝ )
19 1 2 3 4 signstf ⊢ ( 𝐸 ∈ Word ℝ → ( 𝑇 ‘ 𝐸 ) ∈ Word ℝ )
20 wrdf ⊢ ( ( 𝑇 ‘ 𝐸 ) ∈ Word ℝ → ( 𝑇 ‘ 𝐸 ) : ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) ) ⟶ ℝ )
21 18 19 20 3syl ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝑇 ‘ 𝐸 ) : ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) ) ⟶ ℝ )
22 eldifsn ⊢ ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) )
23 5 22 sylib ⊢ ( 𝜑 → ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) )
25 lennncl ⊢ ( ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) → ( ♯ ‘ 𝐸 ) ∈ ℕ )
26 fzo0end ⊢ ( ( ♯ ‘ 𝐸 ) ∈ ℕ → ( ( ♯ ‘ 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
27 24 25 26 3syl ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( ( ♯ ‘ 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
28 1 2 3 4 signstlen ⊢ ( 𝐸 ∈ Word ℝ → ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) = ( ♯ ‘ 𝐸 ) )
29 18 28 syl ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) = ( ♯ ‘ 𝐸 ) )
30 29 oveq2d ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
31 27 30 eleqtrrd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( ( ♯ ‘ 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) ) )
32 21 31 ffvelcdmd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) ∈ ℝ )
33 8 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐴 ∈ ℝ )
34 32 33 remulcld ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) ∈ ℝ )
35 simpr ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 0 < ( 𝐴 · 𝐵 ) )
36 9 oveq1i ⊢ ( 𝑁 − 1 ) = ( ( ♯ ‘ 𝐸 ) − 1 )
37 36 fveq2i ⊢ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) )
38 10 37 eqtri ⊢ 𝐵 = ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) )
39 38 32 eqeltrid ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐵 ∈ ℝ )
40 39 recnd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐵 ∈ ℂ )
41 33 recnd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝐴 ∈ ℂ )
42 40 41 mulcomd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
43 35 42 breqtrrd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 0 < ( 𝐵 · 𝐴 ) )
44 38 oveq1i ⊢ ( 𝐵 · 𝐴 ) = ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 )
45 43 44 breqtrdi ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 0 < ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) )
46 16 34 45 ltnsymd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ¬ ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) < 0 )
47 46 iffalsed ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → if ( ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) < 0 , 1 , 0 ) = 0 )
48 47 oveq2d ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( ( 𝑉 ‘ 𝐸 ) + if ( ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) < 0 , 1 , 0 ) ) = ( ( 𝑉 ‘ 𝐸 ) + 0 ) )
49 1 2 3 4 signsvvf ⊢ 𝑉 : Word ℝ ⟶ ℕ0
50 49 a1i ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → 𝑉 : Word ℝ ⟶ ℕ0 )
51 50 18 ffvelcdmd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝑉 ‘ 𝐸 ) ∈ ℕ0 )
52 51 nn0cnd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝑉 ‘ 𝐸 ) ∈ ℂ )
53 52 addridd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( ( 𝑉 ‘ 𝐸 ) + 0 ) = ( 𝑉 ‘ 𝐸 ) )
54 15 48 53 3eqtrd ⊢ ( ( 𝜑 ∧ 0 < ( 𝐴 · 𝐵 ) ) → ( 𝑉 ‘ 𝐹 ) = ( 𝑉 ‘ 𝐸 ) )