Metamath Proof Explorer

Theorem signlem0

Description: Adding a zero as the highest coefficient does not change the parity of the sign changes. (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 ) )
Assertion signlem0 ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( 𝑉 ‘ ( 𝐹 ++ ⟨“ 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 0re ⊢ 0 ∈ ℝ
6 1 2 3 4 signsvfn ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 0 ∈ ℝ ) → ( 𝑉 ‘ ( 𝐹 ++ ⟨“ 0 ”⟩ ) ) = ( ( 𝑉 ‘ 𝐹 ) + if ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 0 ) < 0 , 1 , 0 ) ) )
7 5 6 mpan2 ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( 𝑉 ‘ ( 𝐹 ++ ⟨“ 0 ”⟩ ) ) = ( ( 𝑉 ‘ 𝐹 ) + if ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 0 ) < 0 , 1 , 0 ) ) )
8 5 ltnri ⊢ ¬ 0 < 0
9 neg1cn ⊢ - 1 ∈ ℂ
10 ax-1cn ⊢ 1 ∈ ℂ
11 prssi ⊢ ( ( - 1 ∈ ℂ ∧ 1 ∈ ℂ ) → { - 1 , 1 } ⊆ ℂ )
12 9 10 11 mp2an ⊢ { - 1 , 1 } ⊆ ℂ
13 simpl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) )
14 eldifsn ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) )
15 13 14 sylib ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) )
16 lennncl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
17 fzo0end ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
18 15 16 17 3syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
19 1 2 3 4 signstfvcl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ { - 1 , 1 } )
20 18 19 mpdan ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ { - 1 , 1 } )
21 12 20 sselid ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ ℂ )
22 21 mul01d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 0 ) = 0 )
23 22 breq1d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 0 ) < 0 ↔ 0 < 0 ) )
24 8 23 mtbiri ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ¬ ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 0 ) < 0 )
25 24 iffalsed ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → if ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 0 ) < 0 , 1 , 0 ) = 0 )
26 25 oveq2d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( ( 𝑉 ‘ 𝐹 ) + if ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 0 ) < 0 , 1 , 0 ) ) = ( ( 𝑉 ‘ 𝐹 ) + 0 ) )
27 1 2 3 4 signsvvf ⊢ 𝑉 : Word ℝ ⟶ ℕ0
28 27 a1i ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → 𝑉 : Word ℝ ⟶ ℕ0 )
29 13 eldifad ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → 𝐹 ∈ Word ℝ )
30 28 29 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( 𝑉 ‘ 𝐹 ) ∈ ℕ0 )
31 30 nn0cnd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( 𝑉 ‘ 𝐹 ) ∈ ℂ )
32 31 addridd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( ( 𝑉 ‘ 𝐹 ) + 0 ) = ( 𝑉 ‘ 𝐹 ) )
33 7 26 32 3eqtrd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ( 𝑉 ‘ ( 𝐹 ++ ⟨“ 0 ”⟩ ) ) = ( 𝑉 ‘ 𝐹 ) )