Metamath Proof Explorer

Theorem signsvfnn

Description: Adding a letter of a different sign as the highest coefficient changes 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 signsvfnn ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( 𝑉 ‘ 𝐹 ) − ( 𝑉 ‘ 𝐸 ) ) = 1 )

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 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) )
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 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐵 ∈ ℂ )
26 8 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
27 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐴 ∈ ℂ )
28 simpr ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( 𝐵 · 𝐴 ) < 0 )
29 28 lt0ne0d ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( 𝐵 · 𝐴 ) ≠ 0 )
30 25 27 29 mulne0bad ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐵 ≠ 0 )
31 10 30 eqnetrrid ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( 𝐸 ‘ ( 𝑁 − 1 ) ) ≠ 0 )
32 1 2 3 4 9 signsvtn0 ⊢ ( ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐸 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ ( 𝐸 ‘ ( 𝑁 − 1 ) ) ) )
33 10 fveq2i ⊢ ( sgn ‘ 𝐵 ) = ( sgn ‘ ( 𝐸 ‘ ( 𝑁 − 1 ) ) )
34 32 33 eqtr4di ⊢ ( ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐸 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ 𝐵 ) )
35 11 31 34 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ 𝐵 ) )
36 35 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) = ( sgn ‘ ( sgn ‘ 𝐵 ) ) )
37 10 22 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐵 ∈ ℝ )
39 38 rexrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐵 ∈ ℝ* )
40 sgnsgn ⊢ ( 𝐵 ∈ ℝ* → ( sgn ‘ ( sgn ‘ 𝐵 ) ) = ( sgn ‘ 𝐵 ) )
41 39 40 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( sgn ‘ ( sgn ‘ 𝐵 ) ) = ( sgn ‘ 𝐵 ) )
42 36 41 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) = ( sgn ‘ 𝐵 ) )
43 42 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) = ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) )
44 26 24 mulcomd ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
45 44 breq1d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 ↔ ( 𝐵 · 𝐴 ) < 0 ) )
46 sgnmulsgn ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 ) )
47 8 37 46 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 ) )
48 45 47 bitr3d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐴 ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 ) )
49 48 biimpa ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 )
50 43 49 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) < 0 )
51 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐴 ∈ ℝ )
52 sgnclre ⊢ ( 𝐵 ∈ ℝ → ( sgn ‘ 𝐵 ) ∈ ℝ )
53 38 52 syl ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( sgn ‘ 𝐵 ) ∈ ℝ )
54 35 53 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ∈ ℝ )
55 sgnmulsgn ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ∈ ℝ ) → ( ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) < 0 ) )
56 51 54 55 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) < 0 ) )
57 50 56 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) < 0 )
58 eqid ⊢ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) )
59 1 2 3 4 5 6 7 8 9 58 signsvtn ⊢ ( ( 𝜑 ∧ ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) < 0 ) → ( ( 𝑉 ‘ 𝐹 ) − ( 𝑉 ‘ 𝐸 ) ) = 1 )
60 57 59 syldan ⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( 𝑉 ‘ 𝐹 ) − ( 𝑉 ‘ 𝐸 ) ) = 1 )