Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  signsvfn Structured version   Visualization version   GIF version

Theorem signsvfn 32974
Description: Number of changes in a word compared to a shorter word. (Contributed by Thierry Arnoux, 12-Oct-2018.)
Hypotheses
Ref Expression
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
Ref Expression
signsvfn (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = ((𝑉𝐹) + if((((𝑇𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0, 1, 0)))
Distinct variable groups:   𝑎,𝑏,   𝑓,𝑖,𝑛,𝐹   𝑓,𝐾,𝑖,𝑛   𝑓,𝑊,𝑖,𝑛   𝑖,𝑎,𝑗,𝑛,𝐹,𝑏   𝐾,𝑎,𝑏,𝑗,𝑓   𝑇,𝑎   𝑓,𝑏,𝑇,𝑗,𝑛
Allowed substitution hints:   (𝑓,𝑖,𝑗,𝑛)   𝑇(𝑖)   𝑉(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏)   𝑊(𝑗,𝑎,𝑏)

Proof of Theorem signsvfn
StepHypRef Expression
1 eldifi 4085 . . . . . 6 (𝐹 ∈ (Word ℝ ∖ {∅}) → 𝐹 ∈ Word ℝ)
2 s1cl 14419 . . . . . 6 (𝐾 ∈ ℝ → ⟨“𝐾”⟩ ∈ Word ℝ)
3 ccatcl 14391 . . . . . 6 ((𝐹 ∈ Word ℝ ∧ ⟨“𝐾”⟩ ∈ Word ℝ) → (𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ)
41, 2, 3syl2an 597 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ)
5 signsv.p . . . . . 6 = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
6 signsv.w . . . . . 6 𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}
7 signsv.t . . . . . 6 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))
8 signsv.v . . . . . 6 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))
95, 6, 7, 8signsvvfval 32970 . . . . 5 ((𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = Σ𝑗 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐾”⟩)))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0))
104, 9syl 17 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = Σ𝑗 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐾”⟩)))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0))
11 ccatlen 14392 . . . . . . . 8 ((𝐹 ∈ Word ℝ ∧ ⟨“𝐾”⟩ ∈ Word ℝ) → (♯‘(𝐹 ++ ⟨“𝐾”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐾”⟩)))
121, 2, 11syl2an 597 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (♯‘(𝐹 ++ ⟨“𝐾”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐾”⟩)))
13 s1len 14423 . . . . . . . 8 (♯‘⟨“𝐾”⟩) = 1
1413oveq2i 7361 . . . . . . 7 ((♯‘𝐹) + (♯‘⟨“𝐾”⟩)) = ((♯‘𝐹) + 1)
1512, 14eqtrdi 2794 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (♯‘(𝐹 ++ ⟨“𝐾”⟩)) = ((♯‘𝐹) + 1))
1615oveq2d 7366 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (1..^(♯‘(𝐹 ++ ⟨“𝐾”⟩))) = (1..^((♯‘𝐹) + 1)))
1716sumeq1d 15522 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^(♯‘(𝐹 ++ ⟨“𝐾”⟩)))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = Σ𝑗 ∈ (1..^((♯‘𝐹) + 1))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0))
18 eldifsn 4746 . . . . . . . 8 (𝐹 ∈ (Word ℝ ∖ {∅}) ↔ (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅))
19 lennncl 14351 . . . . . . . 8 ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ∈ ℕ)
2018, 19sylbi 216 . . . . . . 7 (𝐹 ∈ (Word ℝ ∖ {∅}) → (♯‘𝐹) ∈ ℕ)
21 nnuz 12736 . . . . . . 7 ℕ = (ℤ‘1)
2220, 21eleqtrdi 2849 . . . . . 6 (𝐹 ∈ (Word ℝ ∖ {∅}) → (♯‘𝐹) ∈ (ℤ‘1))
2322adantr 482 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (♯‘𝐹) ∈ (ℤ‘1))
24 1cnd 11084 . . . . . 6 ((((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1...(♯‘𝐹))) ∧ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1))) → 1 ∈ ℂ)
25 0cnd 11082 . . . . . 6 ((((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1...(♯‘𝐹))) ∧ ¬ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1))) → 0 ∈ ℂ)
2624, 25ifclda 4520 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1...(♯‘𝐹))) → if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) ∈ ℂ)
27 fveq2 6838 . . . . . . 7 (𝑗 = (♯‘𝐹) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) = ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)))
28 fvoveq1 7373 . . . . . . 7 (𝑗 = (♯‘𝐹) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)) = ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)))
2927, 28neeq12d 3004 . . . . . 6 (𝑗 = (♯‘𝐹) → (((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)) ↔ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1))))
3029ifbid 4508 . . . . 5 (𝑗 = (♯‘𝐹) → if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)), 1, 0))
3123, 26, 30fzosump1 15573 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^((♯‘𝐹) + 1))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = (Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)), 1, 0)))
3210, 17, 313eqtrd 2782 . . 3 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = (Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)), 1, 0)))
3332adantlr 714 . 2 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = (Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)), 1, 0)))
34 simpl 484 . . . . . . . . . . 11 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 𝐹 ∈ (Word ℝ ∖ {∅}))
3534eldifad 3921 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 𝐹 ∈ Word ℝ)
3635adantr 482 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → 𝐹 ∈ Word ℝ)
37 simplr 768 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → 𝐾 ∈ ℝ)
38 fzo0ss1 13532 . . . . . . . . . . 11 (1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹))
3938a1i 11 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹)))
4039sselda 3943 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → 𝑗 ∈ (0..^(♯‘𝐹)))
415, 6, 7, 8signstfvp 32963 . . . . . . . . 9 ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) = ((𝑇𝐹)‘𝑗))
4236, 37, 40, 41syl3anc 1372 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) = ((𝑇𝐹)‘𝑗))
43 elfzoel2 13501 . . . . . . . . . . . . 13 (𝑗 ∈ (1..^(♯‘𝐹)) → (♯‘𝐹) ∈ ℤ)
4443adantl 483 . . . . . . . . . . . 12 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → (♯‘𝐹) ∈ ℤ)
45 1nn0 12363 . . . . . . . . . . . 12 1 ∈ ℕ0
46 eluzmn 12704 . . . . . . . . . . . 12 (((♯‘𝐹) ∈ ℤ ∧ 1 ∈ ℕ0) → (♯‘𝐹) ∈ (ℤ‘((♯‘𝐹) − 1)))
4744, 45, 46sylancl 587 . . . . . . . . . . 11 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → (♯‘𝐹) ∈ (ℤ‘((♯‘𝐹) − 1)))
48 fzoss2 13530 . . . . . . . . . . 11 ((♯‘𝐹) ∈ (ℤ‘((♯‘𝐹) − 1)) → (0..^((♯‘𝐹) − 1)) ⊆ (0..^(♯‘𝐹)))
4947, 48syl 17 . . . . . . . . . 10 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → (0..^((♯‘𝐹) − 1)) ⊆ (0..^(♯‘𝐹)))
50 elfzo1elm1fzo0 13603 . . . . . . . . . . 11 (𝑗 ∈ (1..^(♯‘𝐹)) → (𝑗 − 1) ∈ (0..^((♯‘𝐹) − 1)))
5150adantl 483 . . . . . . . . . 10 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → (𝑗 − 1) ∈ (0..^((♯‘𝐹) − 1)))
5249, 51sseldd 3944 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → (𝑗 − 1) ∈ (0..^(♯‘𝐹)))
535, 6, 7, 8signstfvp 32963 . . . . . . . . 9 ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ (𝑗 − 1) ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)) = ((𝑇𝐹)‘(𝑗 − 1)))
5436, 37, 52, 53syl3anc 1372 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)) = ((𝑇𝐹)‘(𝑗 − 1)))
5542, 54neeq12d 3004 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → (((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)) ↔ ((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1))))
5655ifbid 4508 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(♯‘𝐹))) → if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = if(((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1)), 1, 0))
5756sumeq2dv 15524 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1)), 1, 0))
585, 6, 7, 8signsvvfval 32970 . . . . . 6 (𝐹 ∈ Word ℝ → (𝑉𝐹) = Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1)), 1, 0))
5935, 58syl 17 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑉𝐹) = Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1)), 1, 0))
6057, 59eqtr4d 2781 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = (𝑉𝐹))
6160adantlr 714 . . 3 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = (𝑉𝐹))
625, 6, 7, 8signstfvn 32961 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) = (((𝑇𝐹)‘((♯‘𝐹) − 1)) (sgn‘𝐾)))
6362adantlr 714 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) = (((𝑇𝐹)‘((♯‘𝐹) − 1)) (sgn‘𝐾)))
6435adantlr 714 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐹 ∈ Word ℝ)
65 simpr 486 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈ ℝ)
66 fzo0end 13594 . . . . . . . . 9 ((♯‘𝐹) ∈ ℕ → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
6720, 66syl 17 . . . . . . . 8 (𝐹 ∈ (Word ℝ ∖ {∅}) → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
6867ad2antrr 725 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
695, 6, 7, 8signstfvp 32963 . . . . . . 7 ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)) = ((𝑇𝐹)‘((♯‘𝐹) − 1)))
7064, 65, 68, 69syl3anc 1372 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)) = ((𝑇𝐹)‘((♯‘𝐹) − 1)))
7163, 70neeq12d 3004 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)) ↔ (((𝑇𝐹)‘((♯‘𝐹) − 1)) (sgn‘𝐾)) ≠ ((𝑇𝐹)‘((♯‘𝐹) − 1))))
725, 6, 7, 8signstfvcl 32965 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹))) → ((𝑇𝐹)‘((♯‘𝐹) − 1)) ∈ {-1, 1})
7368, 72syldan 592 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇𝐹)‘((♯‘𝐹) − 1)) ∈ {-1, 1})
74 rexr 11135 . . . . . . . 8 (𝐾 ∈ ℝ → 𝐾 ∈ ℝ*)
75 sgncl 32918 . . . . . . . 8 (𝐾 ∈ ℝ* → (sgn‘𝐾) ∈ {-1, 0, 1})
7674, 75syl 17 . . . . . . 7 (𝐾 ∈ ℝ → (sgn‘𝐾) ∈ {-1, 0, 1})
7776adantl 483 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (sgn‘𝐾) ∈ {-1, 0, 1})
785, 6signswch 32953 . . . . . 6 ((((𝑇𝐹)‘((♯‘𝐹) − 1)) ∈ {-1, 1} ∧ (sgn‘𝐾) ∈ {-1, 0, 1}) → ((((𝑇𝐹)‘((♯‘𝐹) − 1)) (sgn‘𝐾)) ≠ ((𝑇𝐹)‘((♯‘𝐹) − 1)) ↔ (((𝑇𝐹)‘((♯‘𝐹) − 1)) · (sgn‘𝐾)) < 0))
7973, 77, 78syl2anc 585 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇𝐹)‘((♯‘𝐹) − 1)) (sgn‘𝐾)) ≠ ((𝑇𝐹)‘((♯‘𝐹) − 1)) ↔ (((𝑇𝐹)‘((♯‘𝐹) − 1)) · (sgn‘𝐾)) < 0))
8065rexrd 11139 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈ ℝ*)
81 sgnsgn 32928 . . . . . . . . 9 (𝐾 ∈ ℝ* → (sgn‘(sgn‘𝐾)) = (sgn‘𝐾))
8280, 81syl 17 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (sgn‘(sgn‘𝐾)) = (sgn‘𝐾))
8382oveq2d 7366 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((sgn‘((𝑇𝐹)‘((♯‘𝐹) − 1))) · (sgn‘(sgn‘𝐾))) = ((sgn‘((𝑇𝐹)‘((♯‘𝐹) − 1))) · (sgn‘𝐾)))
8483breq1d 5114 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((sgn‘((𝑇𝐹)‘((♯‘𝐹) − 1))) · (sgn‘(sgn‘𝐾))) < 0 ↔ ((sgn‘((𝑇𝐹)‘((♯‘𝐹) − 1))) · (sgn‘𝐾)) < 0))
85 neg1rr 12202 . . . . . . . . 9 -1 ∈ ℝ
86 1re 11089 . . . . . . . . 9 1 ∈ ℝ
87 prssi 4780 . . . . . . . . 9 ((-1 ∈ ℝ ∧ 1 ∈ ℝ) → {-1, 1} ⊆ ℝ)
8885, 86, 87mp2an 691 . . . . . . . 8 {-1, 1} ⊆ ℝ
8988, 73sselid 3941 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇𝐹)‘((♯‘𝐹) − 1)) ∈ ℝ)
90 sgnclre 32919 . . . . . . . 8 (𝐾 ∈ ℝ → (sgn‘𝐾) ∈ ℝ)
9190adantl 483 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (sgn‘𝐾) ∈ ℝ)
92 sgnmulsgn 32929 . . . . . . 7 ((((𝑇𝐹)‘((♯‘𝐹) − 1)) ∈ ℝ ∧ (sgn‘𝐾) ∈ ℝ) → ((((𝑇𝐹)‘((♯‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔ ((sgn‘((𝑇𝐹)‘((♯‘𝐹) − 1))) · (sgn‘(sgn‘𝐾))) < 0))
9389, 91, 92syl2anc 585 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇𝐹)‘((♯‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔ ((sgn‘((𝑇𝐹)‘((♯‘𝐹) − 1))) · (sgn‘(sgn‘𝐾))) < 0))
94 sgnmulsgn 32929 . . . . . . 7 ((((𝑇𝐹)‘((♯‘𝐹) − 1)) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((((𝑇𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0 ↔ ((sgn‘((𝑇𝐹)‘((♯‘𝐹) − 1))) · (sgn‘𝐾)) < 0))
9589, 94sylancom 589 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0 ↔ ((sgn‘((𝑇𝐹)‘((♯‘𝐹) − 1))) · (sgn‘𝐾)) < 0))
9684, 93, 953bitr4d 311 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇𝐹)‘((♯‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔ (((𝑇𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0))
9771, 79, 963bitrd 305 . . . 4 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)) ↔ (((𝑇𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0))
9897ifbid 4508 . . 3 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)), 1, 0) = if((((𝑇𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0, 1, 0))
9961, 98oveq12d 7368 . 2 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((♯‘𝐹) − 1)), 1, 0)) = ((𝑉𝐹) + if((((𝑇𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0, 1, 0)))
10033, 99eqtrd 2778 1 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = ((𝑉𝐹) + if((((𝑇𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0, 1, 0)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wne 2942  cdif 3906  wss 3909  c0 4281  ifcif 4485  {csn 4585  {cpr 4587  {ctp 4589  cop 4591   class class class wbr 5104  cmpt 5187  cfv 6492  (class class class)co 7350  cmpo 7352  cc 10983  cr 10984  0cc0 10985  1c1 10986   + caddc 10988   · cmul 10990  *cxr 11122   < clt 11123  cmin 11319  -cneg 11320  cn 12087  0cn0 12347  cz 12433  cuz 12697  ...cfz 13354  ..^cfzo 13497  chash 14159  Word cword 14331   ++ cconcat 14387  ⟨“cs1 14412  sgncsgn 14906  Σcsu 15506  ndxcnx 17001  Basecbs 17019  +gcplusg 17069   Σg cgsu 17258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-inf2 9511  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-om 7794  df-1st 7912  df-2nd 7913  df-supp 8061  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-er 8582  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-sup 9312  df-oi 9380  df-card 9809  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-n0 12348  df-xnn0 12420  df-z 12434  df-uz 12698  df-rp 12846  df-fz 13355  df-fzo 13498  df-seq 13837  df-exp 13898  df-hash 14160  df-word 14332  df-lsw 14380  df-concat 14388  df-s1 14413  df-substr 14462  df-pfx 14492  df-sgn 14907  df-cj 14919  df-re 14920  df-im 14921  df-sqrt 15055  df-abs 15056  df-clim 15306  df-sum 15507  df-struct 16955  df-slot 16990  df-ndx 17002  df-base 17020  df-plusg 17082  df-0g 17259  df-gsum 17260  df-mgm 18433  df-sgrp 18482  df-mnd 18493  df-mulg 18808  df-cntz 19032
This theorem is referenced by:  signsvtp  32975  signsvtn  32976  signlem0  32979
  Copyright terms: Public domain W3C validator