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 ffvelrnd ( 𝜑 → ( 𝐸 ‘ ( 𝑁 − 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 )