Metamath Proof Explorer

Theorem signsvtn

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 ⊢ 𝑁 = ( ♯ ‘ 𝐸 )
signsvt.b ⊢ 𝐵 = ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) )
Assertion signsvtn ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 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 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 9 oveq1i ⊢ ( 𝑁 − 1 ) = ( ( ♯ ‘ 𝐸 ) − 1 )
17 16 fveq2i ⊢ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) )
18 10 17 eqtri ⊢ 𝐵 = ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) )
19 18 oveq1i ⊢ ( 𝐵 · 𝐴 ) = ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 )
20 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) )
21 20 eldifad ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝐸 ∈ Word ℝ )
22 1 2 3 4 signstf ⊢ ( 𝐸 ∈ Word ℝ → ( 𝑇 ‘ 𝐸 ) ∈ Word ℝ )
23 wrdf ⊢ ( ( 𝑇 ‘ 𝐸 ) ∈ Word ℝ → ( 𝑇 ‘ 𝐸 ) : ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) ) ⟶ ℝ )
24 21 22 23 3syl ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝑇 ‘ 𝐸 ) : ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) ) ⟶ ℝ )
25 eldifsn ⊢ ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) )
26 5 25 sylib ⊢ ( 𝜑 → ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) )
28 lennncl ⊢ ( ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) → ( ♯ ‘ 𝐸 ) ∈ ℕ )
29 fzo0end ⊢ ( ( ♯ ‘ 𝐸 ) ∈ ℕ → ( ( ♯ ‘ 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
30 27 28 29 3syl ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ( ♯ ‘ 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
31 1 2 3 4 signstlen ⊢ ( 𝐸 ∈ Word ℝ → ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) = ( ♯ ‘ 𝐸 ) )
32 21 31 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) = ( ♯ ‘ 𝐸 ) )
33 32 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
34 30 33 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ( ♯ ‘ 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐸 ) ) ) )
35 24 34 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) ∈ ℝ )
36 18 35 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝐵 ∈ ℝ )
37 36 recnd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝐵 ∈ ℂ )
38 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝐴 ∈ ℝ )
39 38 recnd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝐴 ∈ ℂ )
40 37 39 mulcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
41 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝐴 · 𝐵 ) < 0 )
42 40 41 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝐵 · 𝐴 ) < 0 )
43 19 42 eqbrtrrid ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) < 0 )
44 43 iftrued ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → if ( ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) < 0 , 1 , 0 ) = 1 )
45 44 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ( 𝑉 ‘ 𝐸 ) + if ( ( ( ( 𝑇 ‘ 𝐸 ) ‘ ( ( ♯ ‘ 𝐸 ) − 1 ) ) · 𝐴 ) < 0 , 1 , 0 ) ) = ( ( 𝑉 ‘ 𝐸 ) + 1 ) )
46 15 45 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ( 𝑉 ‘ 𝐸 ) + 1 ) = ( 𝑉 ‘ 𝐹 ) )
47 1 2 3 4 signsvvf ⊢ 𝑉 : Word ℝ ⟶ ℕ0
48 47 a1i ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝑉 : Word ℝ ⟶ ℕ0 )
49 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝐹 = ( 𝐸 ++ ⟨“ 𝐴 ”⟩ ) )
50 38 s1cld ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ⟨“ 𝐴 ”⟩ ∈ Word ℝ )
51 ccatcl ⊢ ( ( 𝐸 ∈ Word ℝ ∧ ⟨“ 𝐴 ”⟩ ∈ Word ℝ ) → ( 𝐸 ++ ⟨“ 𝐴 ”⟩ ) ∈ Word ℝ )
52 21 50 51 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝐸 ++ ⟨“ 𝐴 ”⟩ ) ∈ Word ℝ )
53 49 52 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝐹 ∈ Word ℝ )
54 48 53 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝑉 ‘ 𝐹 ) ∈ ℕ0 )
55 54 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝑉 ‘ 𝐹 ) ∈ ℂ )
56 48 21 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝑉 ‘ 𝐸 ) ∈ ℕ0 )
57 56 nn0cnd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝑉 ‘ 𝐸 ) ∈ ℂ )
58 1cnd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 1 ∈ ℂ )
59 55 57 58 subaddd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ( ( 𝑉 ‘ 𝐹 ) − ( 𝑉 ‘ 𝐸 ) ) = 1 ↔ ( ( 𝑉 ‘ 𝐸 ) + 1 ) = ( 𝑉 ‘ 𝐹 ) ) )
60 46 59 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ( 𝑉 ‘ 𝐹 ) − ( 𝑉 ‘ 𝐸 ) ) = 1 )