Proof of Theorem signsvfn
Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝐹 ∈
(Word ℝ ∖ {∅})) |
2 | 1 | eldifad 3586 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝐹 ∈
Word ℝ) |
3 | | simpr 477 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝐾 ∈
ℝ) |
4 | 3 | s1cld 13383 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 〈“𝐾”〉 ∈ Word
ℝ) |
5 | | ccatcl 13359 |
. . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ) |
6 | 2, 4, 5 | syl2anc 693 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝐹 ++
〈“𝐾”〉) ∈ Word
ℝ) |
7 | | signsv.p |
. . . . . 6
⊢ ⨣ =
(𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦
if(𝑏 = 0, 𝑎, 𝑏)) |
8 | | signsv.w |
. . . . . 6
⊢ 𝑊 = {〈(Base‘ndx), {-1,
0, 1}〉, 〈(+g‘ndx), ⨣
〉} |
9 | | signsv.t |
. . . . . 6
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
10 | | signsv.v |
. . . . . 6
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
11 | 7, 8, 9, 10 | signsvvfval 30655 |
. . . . 5
⊢ ((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ → (𝑉‘(𝐹 ++ 〈“𝐾”〉)) = Σ𝑗 ∈ (1..^(#‘(𝐹 ++ 〈“𝐾”〉)))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0)) |
12 | 6, 11 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑉‘(𝐹 ++ 〈“𝐾”〉)) = Σ𝑗 ∈ (1..^(#‘(𝐹 ++ 〈“𝐾”〉)))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0)) |
13 | | ccatlen 13360 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (#‘(𝐹 ++ 〈“𝐾”〉)) = ((#‘𝐹) + (#‘〈“𝐾”〉))) |
14 | 2, 4, 13 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘(𝐹
++ 〈“𝐾”〉)) = ((#‘𝐹) + (#‘〈“𝐾”〉))) |
15 | | s1len 13385 |
. . . . . . . 8
⊢
(#‘〈“𝐾”〉) = 1 |
16 | 15 | oveq2i 6661 |
. . . . . . 7
⊢
((#‘𝐹) +
(#‘〈“𝐾”〉)) = ((#‘𝐹) + 1) |
17 | 14, 16 | syl6eq 2672 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘(𝐹
++ 〈“𝐾”〉)) = ((#‘𝐹) + 1)) |
18 | 17 | oveq2d 6666 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (1..^(#‘(𝐹 ++ 〈“𝐾”〉))) = (1..^((#‘𝐹) + 1))) |
19 | 18 | sumeq1d 14431 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → Σ𝑗
∈ (1..^(#‘(𝐹 ++
〈“𝐾”〉)))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = Σ𝑗 ∈ (1..^((#‘𝐹) + 1))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0)) |
20 | | eldifsn 4317 |
. . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) ↔ (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) |
21 | | lennncl 13325 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) →
(#‘𝐹) ∈
ℕ) |
22 | 20, 21 | sylbi 207 |
. . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (#‘𝐹) ∈ ℕ) |
23 | | nnuz 11723 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
24 | 22, 23 | syl6eleq 2711 |
. . . . . 6
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (#‘𝐹) ∈
(ℤ≥‘1)) |
25 | 24 | adantr 481 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘𝐹)
∈ (ℤ≥‘1)) |
26 | | 1cnd 10056 |
. . . . . 6
⊢ ((((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1...(#‘𝐹))) ∧
((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1))) → 1 ∈
ℂ) |
27 | | 0cnd 10033 |
. . . . . 6
⊢ ((((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1...(#‘𝐹))) ∧
¬ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1))) → 0 ∈
ℂ) |
28 | 26, 27 | ifclda 4120 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1...(#‘𝐹))) →
if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) ∈
ℂ) |
29 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑗 = (#‘𝐹) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) = ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹))) |
30 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑗 = (#‘𝐹) → (𝑗 − 1) = ((#‘𝐹) − 1)) |
31 | 30 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑗 = (#‘𝐹) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)) = ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1))) |
32 | 29, 31 | neeq12d 2855 |
. . . . . 6
⊢ (𝑗 = (#‘𝐹) → (((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)) ↔ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)))) |
33 | 32 | ifbid 4108 |
. . . . 5
⊢ (𝑗 = (#‘𝐹) → if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)), 1,
0)) |
34 | 25, 28, 33 | fzosump1 14481 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → Σ𝑗
∈ (1..^((#‘𝐹) +
1))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = (Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)), 1,
0))) |
35 | 12, 19, 34 | 3eqtrd 2660 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑉‘(𝐹 ++ 〈“𝐾”〉)) = (Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)), 1,
0))) |
36 | 35 | adantlr 751 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ 〈“𝐾”〉)) = (Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)), 1,
0))) |
37 | 2 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
𝐹 ∈ Word
ℝ) |
38 | 3 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
𝐾 ∈
ℝ) |
39 | | fzo0ss1 12498 |
. . . . . . . . . . 11
⊢
(1..^(#‘𝐹))
⊆ (0..^(#‘𝐹)) |
40 | 39 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (1..^(#‘𝐹)) ⊆ (0..^(#‘𝐹))) |
41 | 40 | sselda 3603 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
𝑗 ∈
(0..^(#‘𝐹))) |
42 | 7, 8, 9, 10 | signstfvp 30648 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) = ((𝑇‘𝐹)‘𝑗)) |
43 | 37, 38, 41, 42 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) = ((𝑇‘𝐹)‘𝑗)) |
44 | | elfzoel2 12469 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1..^(#‘𝐹)) → (#‘𝐹) ∈
ℤ) |
45 | 44 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
(#‘𝐹) ∈
ℤ) |
46 | | 1nn0 11308 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
47 | | eluzmn 11694 |
. . . . . . . . . . . 12
⊢
(((#‘𝐹) ∈
ℤ ∧ 1 ∈ ℕ0) → (#‘𝐹) ∈
(ℤ≥‘((#‘𝐹) − 1))) |
48 | 45, 46, 47 | sylancl 694 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
(#‘𝐹) ∈
(ℤ≥‘((#‘𝐹) − 1))) |
49 | | fzoss2 12496 |
. . . . . . . . . . 11
⊢
((#‘𝐹) ∈
(ℤ≥‘((#‘𝐹) − 1)) → (0..^((#‘𝐹) − 1)) ⊆
(0..^(#‘𝐹))) |
50 | 48, 49 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
(0..^((#‘𝐹) −
1)) ⊆ (0..^(#‘𝐹))) |
51 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
𝑗 ∈
(1..^(#‘𝐹))) |
52 | | elfzoelz 12470 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1..^(#‘𝐹)) → 𝑗 ∈ ℤ) |
53 | 52 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
𝑗 ∈
ℤ) |
54 | | elfzom1b 12567 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℤ ∧
(#‘𝐹) ∈ ℤ)
→ (𝑗 ∈
(1..^(#‘𝐹)) ↔
(𝑗 − 1) ∈
(0..^((#‘𝐹) −
1)))) |
55 | 53, 45, 54 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
(𝑗 ∈
(1..^(#‘𝐹)) ↔
(𝑗 − 1) ∈
(0..^((#‘𝐹) −
1)))) |
56 | 51, 55 | mpbid 222 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
(𝑗 − 1) ∈
(0..^((#‘𝐹) −
1))) |
57 | 50, 56 | sseldd 3604 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
(𝑗 − 1) ∈
(0..^(#‘𝐹))) |
58 | 7, 8, 9, 10 | signstfvp 30648 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ (𝑗 − 1) ∈
(0..^(#‘𝐹))) →
((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)) = ((𝑇‘𝐹)‘(𝑗 − 1))) |
59 | 37, 38, 57, 58 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)) = ((𝑇‘𝐹)‘(𝑗 − 1))) |
60 | 43, 59 | neeq12d 2855 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)) ↔ ((𝑇‘𝐹)‘𝑗) ≠ ((𝑇‘𝐹)‘(𝑗 − 1)))) |
61 | 60 | ifbid 4108 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑗 ∈
(1..^(#‘𝐹))) →
if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = if(((𝑇‘𝐹)‘𝑗) ≠ ((𝑇‘𝐹)‘(𝑗 − 1)), 1, 0)) |
62 | 61 | sumeq2dv 14433 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → Σ𝑗
∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘𝐹)‘𝑗) ≠ ((𝑇‘𝐹)‘(𝑗 − 1)), 1, 0)) |
63 | 7, 8, 9, 10 | signsvvfval 30655 |
. . . . . 6
⊢ (𝐹 ∈ Word ℝ →
(𝑉‘𝐹) = Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘𝐹)‘𝑗) ≠ ((𝑇‘𝐹)‘(𝑗 − 1)), 1, 0)) |
64 | 2, 63 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑉‘𝐹) = Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘𝐹)‘𝑗) ≠ ((𝑇‘𝐹)‘(𝑗 − 1)), 1, 0)) |
65 | 62, 64 | eqtr4d 2659 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → Σ𝑗
∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = (𝑉‘𝐹)) |
66 | 65 | adantlr 751 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) = (𝑉‘𝐹)) |
67 | 7, 8, 9, 10 | signstfvn 30646 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) = (((𝑇‘𝐹)‘((#‘𝐹) − 1)) ⨣ (sgn‘𝐾))) |
68 | 67 | adantlr 751 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) = (((𝑇‘𝐹)‘((#‘𝐹) − 1)) ⨣ (sgn‘𝐾))) |
69 | 2 | adantlr 751 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐹 ∈ Word ℝ) |
70 | | simpr 477 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈ ℝ) |
71 | 22 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) ∈
ℕ) |
72 | | fzo0end 12560 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
ℕ → ((#‘𝐹)
− 1) ∈ (0..^(#‘𝐹))) |
73 | 71, 72 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((#‘𝐹) − 1) ∈
(0..^(#‘𝐹))) |
74 | 7, 8, 9, 10 | signstfvp 30648 |
. . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧
((#‘𝐹) − 1)
∈ (0..^(#‘𝐹)))
→ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)) = ((𝑇‘𝐹)‘((#‘𝐹) − 1))) |
75 | 69, 70, 73, 74 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)) = ((𝑇‘𝐹)‘((#‘𝐹) − 1))) |
76 | 68, 75 | neeq12d 2855 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)) ↔ (((𝑇‘𝐹)‘((#‘𝐹) − 1)) ⨣ (sgn‘𝐾)) ≠ ((𝑇‘𝐹)‘((#‘𝐹) − 1)))) |
77 | 7, 8, 9, 10 | signstfvcl 30650 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ ((#‘𝐹) − 1) ∈
(0..^(#‘𝐹))) →
((𝑇‘𝐹)‘((#‘𝐹) − 1)) ∈ {-1,
1}) |
78 | 73, 77 | syldan 487 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘𝐹)‘((#‘𝐹) − 1)) ∈ {-1,
1}) |
79 | 70 | rexrd 10089 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈
ℝ*) |
80 | | sgncl 30600 |
. . . . . . 7
⊢ (𝐾 ∈ ℝ*
→ (sgn‘𝐾) ∈
{-1, 0, 1}) |
81 | 79, 80 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (sgn‘𝐾) ∈ {-1, 0,
1}) |
82 | 7, 8 | signswch 30638 |
. . . . . 6
⊢ ((((𝑇‘𝐹)‘((#‘𝐹) − 1)) ∈ {-1, 1} ∧
(sgn‘𝐾) ∈ {-1,
0, 1}) → ((((𝑇‘𝐹)‘((#‘𝐹) − 1)) ⨣ (sgn‘𝐾)) ≠ ((𝑇‘𝐹)‘((#‘𝐹) − 1)) ↔ (((𝑇‘𝐹)‘((#‘𝐹) − 1)) · (sgn‘𝐾)) < 0)) |
83 | 78, 81, 82 | syl2anc 693 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇‘𝐹)‘((#‘𝐹) − 1)) ⨣ (sgn‘𝐾)) ≠ ((𝑇‘𝐹)‘((#‘𝐹) − 1)) ↔ (((𝑇‘𝐹)‘((#‘𝐹) − 1)) · (sgn‘𝐾)) < 0)) |
84 | | sgnsgn 30610 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℝ*
→ (sgn‘(sgn‘𝐾)) = (sgn‘𝐾)) |
85 | 79, 84 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) →
(sgn‘(sgn‘𝐾)) =
(sgn‘𝐾)) |
86 | 85 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((sgn‘((𝑇‘𝐹)‘((#‘𝐹) − 1))) ·
(sgn‘(sgn‘𝐾)))
= ((sgn‘((𝑇‘𝐹)‘((#‘𝐹) − 1))) · (sgn‘𝐾))) |
87 | 86 | breq1d 4663 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((sgn‘((𝑇‘𝐹)‘((#‘𝐹) − 1))) ·
(sgn‘(sgn‘𝐾)))
< 0 ↔ ((sgn‘((𝑇‘𝐹)‘((#‘𝐹) − 1))) · (sgn‘𝐾)) < 0)) |
88 | | neg1rr 11125 |
. . . . . . . . 9
⊢ -1 ∈
ℝ |
89 | | 1re 10039 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
90 | | prssi 4353 |
. . . . . . . . 9
⊢ ((-1
∈ ℝ ∧ 1 ∈ ℝ) → {-1, 1} ⊆
ℝ) |
91 | 88, 89, 90 | mp2an 708 |
. . . . . . . 8
⊢ {-1, 1}
⊆ ℝ |
92 | 91, 78 | sseldi 3601 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘𝐹)‘((#‘𝐹) − 1)) ∈
ℝ) |
93 | | sgnclre 30601 |
. . . . . . . 8
⊢ (𝐾 ∈ ℝ →
(sgn‘𝐾) ∈
ℝ) |
94 | 93 | adantl 482 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (sgn‘𝐾) ∈
ℝ) |
95 | | sgnmulsgn 30611 |
. . . . . . 7
⊢ ((((𝑇‘𝐹)‘((#‘𝐹) − 1)) ∈ ℝ ∧
(sgn‘𝐾) ∈
ℝ) → ((((𝑇‘𝐹)‘((#‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔
((sgn‘((𝑇‘𝐹)‘((#‘𝐹) − 1))) ·
(sgn‘(sgn‘𝐾)))
< 0)) |
96 | 92, 94, 95 | syl2anc 693 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇‘𝐹)‘((#‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔
((sgn‘((𝑇‘𝐹)‘((#‘𝐹) − 1))) ·
(sgn‘(sgn‘𝐾)))
< 0)) |
97 | | sgnmulsgn 30611 |
. . . . . . 7
⊢ ((((𝑇‘𝐹)‘((#‘𝐹) − 1)) ∈ ℝ ∧ 𝐾 ∈ ℝ) →
((((𝑇‘𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0 ↔
((sgn‘((𝑇‘𝐹)‘((#‘𝐹) − 1))) ·
(sgn‘𝐾)) <
0)) |
98 | 92, 70, 97 | syl2anc 693 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇‘𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0 ↔ ((sgn‘((𝑇‘𝐹)‘((#‘𝐹) − 1))) · (sgn‘𝐾)) < 0)) |
99 | 87, 96, 98 | 3bitr4d 300 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇‘𝐹)‘((#‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔ (((𝑇‘𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0)) |
100 | 76, 83, 99 | 3bitrd 294 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)) ↔ (((𝑇‘𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0)) |
101 | 100 | ifbid 4108 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)), 1, 0) =
if((((𝑇‘𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0, 1,
0)) |
102 | 66, 101 | oveq12d 6668 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑗) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘((#‘𝐹) − 1)), 1, 0)) = ((𝑉‘𝐹) + if((((𝑇‘𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0, 1, 0))) |
103 | 36, 102 | eqtrd 2656 |
1
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ 〈“𝐾”〉)) = ((𝑉‘𝐹) + if((((𝑇‘𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0, 1, 0))) |