Proof of Theorem signsvfn
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eldifi 4131 | . . . . . 6
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → 𝐹 ∈
Word ℝ) | 
| 2 |  | s1cl 14640 | . . . . . 6
⊢ (𝐾 ∈ ℝ →
〈“𝐾”〉
∈ Word ℝ) | 
| 3 |  | ccatcl 14612 | . . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ) | 
| 4 | 1, 2, 3 | syl2an 596 | . . . . 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)) | 
| 9 | 5, 6, 7, 8 | signsvvfval 34593 | . . . . 5
⊢ ((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ → (𝑉‘(𝐹 ++ 〈“𝐾”〉)) = Σ𝑗 ∈ (1..^(♯‘(𝐹 ++ 〈“𝐾”〉)))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0)) | 
| 10 | 4, 9 | syl 17 | . . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑉‘(𝐹 ++ 〈“𝐾”〉)) = Σ𝑗 ∈ (1..^(♯‘(𝐹 ++ 〈“𝐾”〉)))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0)) | 
| 11 |  | ccatlen 14613 | . . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (♯‘(𝐹 ++ 〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) | 
| 12 | 1, 2, 11 | syl2an 596 | . . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (♯‘(𝐹 ++ 〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) | 
| 13 |  | s1len 14644 | . . . . . . . 8
⊢
(♯‘〈“𝐾”〉) = 1 | 
| 14 | 13 | oveq2i 7442 | . . . . . . 7
⊢
((♯‘𝐹) +
(♯‘〈“𝐾”〉)) = ((♯‘𝐹) + 1) | 
| 15 | 12, 14 | eqtrdi 2793 | . . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (♯‘(𝐹 ++ 〈“𝐾”〉)) = ((♯‘𝐹) + 1)) | 
| 16 | 15 | oveq2d 7447 | . . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (1..^(♯‘(𝐹 ++ 〈“𝐾”〉))) =
(1..^((♯‘𝐹) +
1))) | 
| 17 | 16 | sumeq1d 15736 | . . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → Σ𝑗
∈ (1..^(♯‘(𝐹 ++ 〈“𝐾”〉)))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = Σ𝑗 ∈
(1..^((♯‘𝐹) +
1))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0)) | 
| 18 |  | eldifsn 4786 | . . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) ↔ (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) | 
| 19 |  | lennncl 14572 | . . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) →
(♯‘𝐹) ∈
ℕ) | 
| 20 | 18, 19 | sylbi 217 | . . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ∈ ℕ) | 
| 21 |  | nnuz 12921 | . . . . . . 7
⊢ ℕ =
(ℤ≥‘1) | 
| 22 | 20, 21 | eleqtrdi 2851 | . . . . . 6
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ∈
(ℤ≥‘1)) | 
| 23 | 22 | adantr 480 | . . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (♯‘𝐹) ∈
(ℤ≥‘1)) | 
| 24 |  | 1cnd 11256 | . . . . . 6
⊢ ((((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1...(♯‘𝐹)))
∧ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1))) → 1 ∈
ℂ) | 
| 25 |  | 0cnd 11254 | . . . . . 6
⊢ ((((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1...(♯‘𝐹)))
∧ ¬ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1))) → 0 ∈
ℂ) | 
| 26 | 24, 25 | ifclda 4561 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1...(♯‘𝐹)))
→ if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) ∈
ℂ) | 
| 27 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑗 = (♯‘𝐹) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) = ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹))) | 
| 28 |  | fvoveq1 7454 | . . . . . . 7
⊢ (𝑗 = (♯‘𝐹) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)) = ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1))) | 
| 29 | 27, 28 | neeq12d 3002 | . . . . . 6
⊢ (𝑗 = (♯‘𝐹) → (((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)) ↔ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)))) | 
| 30 | 29 | ifbid 4549 | . . . . 5
⊢ (𝑗 = (♯‘𝐹) → if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)), 1,
0)) | 
| 31 | 23, 26, 30 | fzosump1 15788 | . . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → Σ𝑗
∈ (1..^((♯‘𝐹) + 1))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = (Σ𝑗 ∈
(1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)), 1,
0))) | 
| 32 | 10, 17, 31 | 3eqtrd 2781 | . . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑉‘(𝐹 ++ 〈“𝐾”〉)) = (Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)), 1,
0))) | 
| 33 | 32 | adantlr 715 | . 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ 〈“𝐾”〉)) = (Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)), 1,
0))) | 
| 34 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝐹 ∈
(Word ℝ ∖ {∅})) | 
| 35 | 34 | eldifad 3963 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝐹 ∈
Word ℝ) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ 𝐹 ∈ Word
ℝ) | 
| 37 |  | simplr 769 | . . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ 𝐾 ∈
ℝ) | 
| 38 |  | fzo0ss1 13729 | . . . . . . . . . . 11
⊢
(1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹)) | 
| 39 | 38 | a1i 11 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹))) | 
| 40 | 39 | sselda 3983 | . . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ 𝑗 ∈
(0..^(♯‘𝐹))) | 
| 41 | 5, 6, 7, 8 | signstfvp 34586 | . . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑗 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) = ((𝑇‘𝐹)‘𝑗)) | 
| 42 | 36, 37, 40, 41 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) = ((𝑇‘𝐹)‘𝑗)) | 
| 43 |  | elfzoel2 13698 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈
(1..^(♯‘𝐹))
→ (♯‘𝐹)
∈ ℤ) | 
| 44 | 43 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ (♯‘𝐹)
∈ ℤ) | 
| 45 |  | 1nn0 12542 | . . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 | 
| 46 |  | eluzmn 12885 | . . . . . . . . . . . 12
⊢
(((♯‘𝐹)
∈ ℤ ∧ 1 ∈ ℕ0) → (♯‘𝐹) ∈
(ℤ≥‘((♯‘𝐹) − 1))) | 
| 47 | 44, 45, 46 | sylancl 586 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ (♯‘𝐹)
∈ (ℤ≥‘((♯‘𝐹) − 1))) | 
| 48 |  | fzoss2 13727 | . . . . . . . . . . 11
⊢
((♯‘𝐹)
∈ (ℤ≥‘((♯‘𝐹) − 1)) →
(0..^((♯‘𝐹)
− 1)) ⊆ (0..^(♯‘𝐹))) | 
| 49 | 47, 48 | syl 17 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ (0..^((♯‘𝐹) − 1)) ⊆
(0..^(♯‘𝐹))) | 
| 50 |  | elfzo1elm1fzo0 13807 | . . . . . . . . . . 11
⊢ (𝑗 ∈
(1..^(♯‘𝐹))
→ (𝑗 − 1) ∈
(0..^((♯‘𝐹)
− 1))) | 
| 51 | 50 | adantl 481 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ (𝑗 − 1) ∈
(0..^((♯‘𝐹)
− 1))) | 
| 52 | 49, 51 | sseldd 3984 | . . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ (𝑗 − 1) ∈
(0..^(♯‘𝐹))) | 
| 53 | 5, 6, 7, 8 | signstfvp 34586 | . . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ (𝑗 − 1) ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)) = ((𝑇‘𝐹)‘(𝑗 − 1))) | 
| 54 | 36, 37, 52, 53 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)) = ((𝑇‘𝐹)‘(𝑗 − 1))) | 
| 55 | 42, 54 | neeq12d 3002 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ (((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)) ↔ ((𝑇‘𝐹)‘𝑗) ≠ ((𝑇‘𝐹)‘(𝑗 − 1)))) | 
| 56 | 55 | ifbid 4549 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(♯‘𝐹)))
→ if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = if(((𝑇‘𝐹)‘𝑗) ≠ ((𝑇‘𝐹)‘(𝑗 − 1)), 1, 0)) | 
| 57 | 56 | sumeq2dv 15738 | . . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → Σ𝑗
∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = Σ𝑗 ∈
(1..^(♯‘𝐹))if(((𝑇‘𝐹)‘𝑗) ≠ ((𝑇‘𝐹)‘(𝑗 − 1)), 1, 0)) | 
| 58 | 5, 6, 7, 8 | signsvvfval 34593 | . . . . . 6
⊢ (𝐹 ∈ Word ℝ →
(𝑉‘𝐹) = Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘𝐹)‘𝑗) ≠ ((𝑇‘𝐹)‘(𝑗 − 1)), 1, 0)) | 
| 59 | 35, 58 | syl 17 | . . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑉‘𝐹) = Σ𝑗 ∈ (1..^(♯‘𝐹))if(((𝑇‘𝐹)‘𝑗) ≠ ((𝑇‘𝐹)‘(𝑗 − 1)), 1, 0)) | 
| 60 | 57, 59 | eqtr4d 2780 | . . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → Σ𝑗
∈ (1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = (𝑉‘𝐹)) | 
| 61 | 60 | adantlr 715 | . . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈
(1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = (𝑉‘𝐹)) | 
| 62 | 5, 6, 7, 8 | signstfvn 34584 | . . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾))) | 
| 63 | 62 | adantlr 715 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾))) | 
| 64 | 35 | adantlr 715 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐹 ∈ Word ℝ) | 
| 65 |  | simpr 484 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈ ℝ) | 
| 66 |  | fzo0end 13797 | . . . . . . . . 9
⊢
((♯‘𝐹)
∈ ℕ → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) | 
| 67 | 20, 66 | syl 17 | . . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) | 
| 68 | 67 | ad2antrr 726 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) →
((♯‘𝐹) −
1) ∈ (0..^(♯‘𝐹))) | 
| 69 | 5, 6, 7, 8 | signstfvp 34586 | . . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧
((♯‘𝐹) −
1) ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)) = ((𝑇‘𝐹)‘((♯‘𝐹) − 1))) | 
| 70 | 64, 65, 68, 69 | syl3anc 1373 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)) = ((𝑇‘𝐹)‘((♯‘𝐹) − 1))) | 
| 71 | 63, 70 | neeq12d 3002 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)) ↔ (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾)) ≠ ((𝑇‘𝐹)‘((♯‘𝐹) − 1)))) | 
| 72 | 5, 6, 7, 8 | signstfvcl 34588 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧
((♯‘𝐹) −
1) ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ∈ {-1,
1}) | 
| 73 | 68, 72 | syldan 591 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ∈ {-1,
1}) | 
| 74 |  | rexr 11307 | . . . . . . . 8
⊢ (𝐾 ∈ ℝ → 𝐾 ∈
ℝ*) | 
| 75 |  | sgncl 34541 | . . . . . . . 8
⊢ (𝐾 ∈ ℝ*
→ (sgn‘𝐾) ∈
{-1, 0, 1}) | 
| 76 | 74, 75 | syl 17 | . . . . . . 7
⊢ (𝐾 ∈ ℝ →
(sgn‘𝐾) ∈ {-1,
0, 1}) | 
| 77 | 76 | adantl 481 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (sgn‘𝐾) ∈ {-1, 0,
1}) | 
| 78 | 5, 6 | signswch 34576 | . . . . . 6
⊢ ((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ∈ {-1, 1} ∧
(sgn‘𝐾) ∈ {-1,
0, 1}) → ((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾)) ≠ ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ↔ (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · (sgn‘𝐾)) < 0)) | 
| 79 | 73, 77, 78 | syl2anc 584 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾)) ≠ ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ↔ (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · (sgn‘𝐾)) < 0)) | 
| 80 | 65 | rexrd 11311 | . . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈
ℝ*) | 
| 81 |  | sgnsgn 34551 | . . . . . . . . 9
⊢ (𝐾 ∈ ℝ*
→ (sgn‘(sgn‘𝐾)) = (sgn‘𝐾)) | 
| 82 | 80, 81 | syl 17 | . . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) →
(sgn‘(sgn‘𝐾)) =
(sgn‘𝐾)) | 
| 83 | 82 | oveq2d 7447 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((sgn‘((𝑇‘𝐹)‘((♯‘𝐹) − 1))) ·
(sgn‘(sgn‘𝐾)))
= ((sgn‘((𝑇‘𝐹)‘((♯‘𝐹) − 1))) · (sgn‘𝐾))) | 
| 84 | 83 | breq1d 5153 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((sgn‘((𝑇‘𝐹)‘((♯‘𝐹) − 1))) ·
(sgn‘(sgn‘𝐾)))
< 0 ↔ ((sgn‘((𝑇‘𝐹)‘((♯‘𝐹) − 1))) · (sgn‘𝐾)) < 0)) | 
| 85 |  | neg1rr 12381 | . . . . . . . . 9
⊢ -1 ∈
ℝ | 
| 86 |  | 1re 11261 | . . . . . . . . 9
⊢ 1 ∈
ℝ | 
| 87 |  | prssi 4821 | . . . . . . . . 9
⊢ ((-1
∈ ℝ ∧ 1 ∈ ℝ) → {-1, 1} ⊆
ℝ) | 
| 88 | 85, 86, 87 | mp2an 692 | . . . . . . . 8
⊢ {-1, 1}
⊆ ℝ | 
| 89 | 88, 73 | sselid 3981 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ∈
ℝ) | 
| 90 |  | sgnclre 34542 | . . . . . . . 8
⊢ (𝐾 ∈ ℝ →
(sgn‘𝐾) ∈
ℝ) | 
| 91 | 90 | adantl 481 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (sgn‘𝐾) ∈
ℝ) | 
| 92 |  | sgnmulsgn 34552 | . . . . . . 7
⊢ ((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ∈ ℝ ∧
(sgn‘𝐾) ∈
ℝ) → ((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔
((sgn‘((𝑇‘𝐹)‘((♯‘𝐹) − 1))) ·
(sgn‘(sgn‘𝐾)))
< 0)) | 
| 93 | 89, 91, 92 | syl2anc 584 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔
((sgn‘((𝑇‘𝐹)‘((♯‘𝐹) − 1))) ·
(sgn‘(sgn‘𝐾)))
< 0)) | 
| 94 |  | sgnmulsgn 34552 | . . . . . . 7
⊢ ((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ∈ ℝ ∧ 𝐾 ∈ ℝ) →
((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0 ↔
((sgn‘((𝑇‘𝐹)‘((♯‘𝐹) − 1))) ·
(sgn‘𝐾)) <
0)) | 
| 95 | 89, 94 | sylancom 588 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0 ↔ ((sgn‘((𝑇‘𝐹)‘((♯‘𝐹) − 1))) · (sgn‘𝐾)) < 0)) | 
| 96 | 84, 93, 95 | 3bitr4d 311 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔ (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0)) | 
| 97 | 71, 79, 96 | 3bitrd 305 | . . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)) ↔ (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0)) | 
| 98 | 97 | ifbid 4549 | . . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)), 1, 0) =
if((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0, 1,
0)) | 
| 99 | 61, 98 | oveq12d 7449 | . 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (Σ𝑗 ∈
(1..^(♯‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((♯‘𝐹) − 1)), 1, 0)) = ((𝑉‘𝐹) + if((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0, 1, 0))) | 
| 100 | 33, 99 | eqtrd 2777 | 1
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ 〈“𝐾”〉)) = ((𝑉‘𝐹) + if((((𝑇‘𝐹)‘((♯‘𝐹) − 1)) · 𝐾) < 0, 1, 0))) |