Proof of Theorem signsvtn0
Step | Hyp | Ref
| Expression |
1 | | eldifsn 4260 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) ↔ (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) |
2 | 1 | biimpi 205 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) |
3 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅)) |
4 | 3 | simpld 474 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 ∈ Word
ℝ) |
5 | 4 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹 ∈ Word ℝ) |
6 | | wrdf 13165 |
. . . . . . . 8
⊢ (𝐹 ∈ Word ℝ →
𝐹:(0..^(#‘𝐹))⟶ℝ) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹:(0..^(#‘𝐹))⟶ℝ) |
8 | | lennncl 13180 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) →
(#‘𝐹) ∈
ℕ) |
9 | 3, 8 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (#‘𝐹) ∈
ℕ) |
10 | 9 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (#‘𝐹) ∈ ℕ) |
11 | | lbfzo0 12375 |
. . . . . . . 8
⊢ (0 ∈
(0..^(#‘𝐹)) ↔
(#‘𝐹) ∈
ℕ) |
12 | 10, 11 | sylibr 223 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 0 ∈ (0..^(#‘𝐹))) |
13 | 7, 12 | ffvelrnd 6268 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝐹‘0) ∈ ℝ) |
14 | | signsv.p |
. . . . . . 7
⊢ ⨣ =
(𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦
if(𝑏 = 0, 𝑎, 𝑏)) |
15 | | signsv.w |
. . . . . . 7
⊢ 𝑊 = {〈(Base‘ndx), {-1,
0, 1}〉, 〈(+g‘ndx), ⨣
〉} |
16 | | signsv.t |
. . . . . . 7
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
17 | | signsv.v |
. . . . . . 7
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
18 | 14, 15, 16, 17 | signstf0 29971 |
. . . . . 6
⊢ ((𝐹‘0) ∈ ℝ →
(𝑇‘〈“(𝐹‘0)”〉) =
〈“(sgn‘(𝐹‘0))”〉) |
19 | 13, 18 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘〈“(𝐹‘0)”〉) =
〈“(sgn‘(𝐹‘0))”〉) |
20 | | signsvtn0.1 |
. . . . . . . 8
⊢ 𝑁 = (#‘𝐹) |
21 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝑁 = 1) |
22 | 20, 21 | syl5eqr 2658 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (#‘𝐹) = 1) |
23 | | eqs1 13245 |
. . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧
(#‘𝐹) = 1) →
𝐹 = 〈“(𝐹‘0)”〉) |
24 | 5, 22, 23 | syl2anc 691 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹 = 〈“(𝐹‘0)”〉) |
25 | 24 | fveq2d 6107 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘𝐹) = (𝑇‘〈“(𝐹‘0)”〉)) |
26 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑁 = 1 → (𝑁 − 1) = (1 −
1)) |
27 | | 1m1e0 10966 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
28 | 26, 27 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑁 = 1 → (𝑁 − 1) = 0) |
29 | 28 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑁 = 1 → (𝐹‘(𝑁 − 1)) = (𝐹‘0)) |
30 | 29 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑁 = 1 → (sgn‘(𝐹‘(𝑁 − 1))) = (sgn‘(𝐹‘0))) |
31 | 30 | s1eqd 13234 |
. . . . . 6
⊢ (𝑁 = 1 →
〈“(sgn‘(𝐹‘(𝑁 − 1)))”〉 =
〈“(sgn‘(𝐹‘0))”〉) |
32 | 21, 31 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 〈“(sgn‘(𝐹‘(𝑁 − 1)))”〉 =
〈“(sgn‘(𝐹‘0))”〉) |
33 | 19, 25, 32 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘𝐹) = 〈“(sgn‘(𝐹‘(𝑁 − 1)))”〉) |
34 | 21, 28 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑁 − 1) = 0) |
35 | 33, 34 | fveq12d 6109 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) =
(〈“(sgn‘(𝐹‘(𝑁 −
1)))”〉‘0)) |
36 | 4, 6 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹:(0..^(#‘𝐹))⟶ℝ) |
37 | 20 | oveq1i 6559 |
. . . . . . . . 9
⊢ (𝑁 − 1) = ((#‘𝐹) − 1) |
38 | | fzo0end 12426 |
. . . . . . . . . 10
⊢
((#‘𝐹) ∈
ℕ → ((#‘𝐹)
− 1) ∈ (0..^(#‘𝐹))) |
39 | 3, 8, 38 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((#‘𝐹) − 1) ∈
(0..^(#‘𝐹))) |
40 | 37, 39 | syl5eqel 2692 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) ∈
(0..^(#‘𝐹))) |
41 | 36, 40 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ∈
ℝ) |
42 | 41 | rexrd 9968 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ∈
ℝ*) |
43 | | sgncl 29927 |
. . . . . 6
⊢ ((𝐹‘(𝑁 − 1)) ∈ ℝ*
→ (sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0,
1}) |
44 | 42, 43 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0,
1}) |
45 | 44 | adantr 480 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0,
1}) |
46 | | s1fv 13243 |
. . . 4
⊢
((sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0, 1} →
(〈“(sgn‘(𝐹‘(𝑁 − 1)))”〉‘0) =
(sgn‘(𝐹‘(𝑁 − 1)))) |
47 | 45, 46 | syl 17 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (〈“(sgn‘(𝐹‘(𝑁 − 1)))”〉‘0) =
(sgn‘(𝐹‘(𝑁 − 1)))) |
48 | 35, 47 | eqtrd 2644 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1)))) |
49 | | fzossfz 12357 |
. . . . . . . . . 10
⊢
(0..^(#‘𝐹))
⊆ (0...(#‘𝐹)) |
50 | 49, 39 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((#‘𝐹) − 1) ∈
(0...(#‘𝐹))) |
51 | | swrd0val 13273 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧
((#‘𝐹) − 1)
∈ (0...(#‘𝐹)))
→ (𝐹 substr 〈0,
((#‘𝐹) −
1)〉) = (𝐹 ↾
(0..^((#‘𝐹) −
1)))) |
52 | 4, 50, 51 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 substr 〈0, ((#‘𝐹) − 1)〉) = (𝐹 ↾ (0..^((#‘𝐹) − 1)))) |
53 | 52 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝐹 substr 〈0, ((#‘𝐹) − 1)〉) ++
〈“( lastS ‘𝐹)”〉) = ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ++ 〈“( lastS
‘𝐹)”〉)) |
54 | | swrdccatwrd 13320 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → ((𝐹 substr 〈0, ((#‘𝐹) − 1)〉) ++
〈“( lastS ‘𝐹)”〉) = 𝐹) |
55 | 54 | eqcomd 2616 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → 𝐹 = ((𝐹 substr 〈0, ((#‘𝐹) − 1)〉) ++ 〈“( lastS
‘𝐹)”〉)) |
56 | 3, 55 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 = ((𝐹 substr 〈0, ((#‘𝐹) − 1)〉) ++ 〈“( lastS
‘𝐹)”〉)) |
57 | 37 | oveq2i 6560 |
. . . . . . . . . 10
⊢
(0..^(𝑁 − 1))
= (0..^((#‘𝐹) −
1)) |
58 | 57 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^(𝑁 − 1)) =
(0..^((#‘𝐹) −
1))) |
59 | 58 | reseq2d 5317 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) = (𝐹 ↾ (0..^((#‘𝐹) − 1)))) |
60 | 37 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) = ((#‘𝐹) − 1)) |
61 | 60 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) = (𝐹‘((#‘𝐹) − 1))) |
62 | | lsw 13204 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ( lastS ‘𝐹) = (𝐹‘((#‘𝐹) − 1))) |
63 | 62 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ( lastS
‘𝐹) = (𝐹‘((#‘𝐹) − 1))) |
64 | 61, 63 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) = ( lastS ‘𝐹)) |
65 | 64 | s1eqd 13234 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
〈“(𝐹‘(𝑁 − 1))”〉 = 〈“(
lastS ‘𝐹)”〉) |
66 | 59, 65 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 − 1))”〉) = ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ++ 〈“(
lastS ‘𝐹)”〉)) |
67 | 53, 56, 66 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 = ((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 − 1))”〉)) |
68 | 67 | fveq2d 6107 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑇‘𝐹) = (𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 −
1))”〉))) |
69 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝐹:(0..^(#‘𝐹))⟶ℝ → 𝐹 Fn (0..^(#‘𝐹))) |
70 | 4, 6, 69 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 Fn (0..^(#‘𝐹))) |
71 | 20 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 = (#‘𝐹)) |
72 | 71 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^𝑁) = (0..^(#‘𝐹))) |
73 | 72 | fneq2d 5896 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 Fn (0..^𝑁) ↔ 𝐹 Fn (0..^(#‘𝐹)))) |
74 | 70, 73 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 Fn (0..^𝑁)) |
75 | 20, 9 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 ∈
ℕ) |
76 | 75 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 ∈
ℕ0) |
77 | | nn0z 11277 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
78 | | fzossrbm1 12366 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ →
(0..^(𝑁 − 1)) ⊆
(0..^𝑁)) |
79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) |
80 | | fnssres 5918 |
. . . . . . . . 9
⊢ ((𝐹 Fn (0..^𝑁) ∧ (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) → (𝐹 ↾ (0..^(𝑁 − 1))) Fn (0..^(𝑁 − 1))) |
81 | 74, 79, 80 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) Fn (0..^(𝑁 − 1))) |
82 | | hashfn 13025 |
. . . . . . . 8
⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) Fn (0..^(𝑁 − 1)) → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (#‘(0..^(𝑁 − 1)))) |
83 | 81, 82 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (#‘(0..^(𝑁 − 1)))) |
84 | | nnm1nn0 11211 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
85 | | hashfzo0 13077 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈
ℕ0 → (#‘(0..^(𝑁 − 1))) = (𝑁 − 1)) |
86 | 75, 84, 85 | 3syl 18 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(#‘(0..^(𝑁 −
1))) = (𝑁 −
1)) |
87 | 83, 86 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (𝑁 − 1)) |
88 | 87 | eqcomd 2616 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) = (#‘(𝐹 ↾ (0..^(𝑁 − 1))))) |
89 | 68, 88 | fveq12d 6109 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝑇‘𝐹)‘(𝑁 − 1)) = ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(#‘(𝐹 ↾ (0..^(𝑁 − 1)))))) |
90 | 89 | adantr 480 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(#‘(𝐹 ↾ (0..^(𝑁 − 1)))))) |
91 | 52, 59 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 substr 〈0, ((#‘𝐹) − 1)〉) = (𝐹 ↾ (0..^(𝑁 − 1)))) |
92 | | swrdcl 13271 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word ℝ →
(𝐹 substr 〈0,
((#‘𝐹) −
1)〉) ∈ Word ℝ) |
93 | 4, 92 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 substr 〈0, ((#‘𝐹) − 1)〉) ∈ Word
ℝ) |
94 | 91, 93 | eqeltrrd 2689 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word
ℝ) |
95 | 94 | adantr 480 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word
ℝ) |
96 | 87 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (𝑁 − 1)) |
97 | 75 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ∈ ℕ) |
98 | 97 | nncnd 10913 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ∈ ℂ) |
99 | | 1cnd 9935 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 1 ∈
ℂ) |
100 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ≠ 1) |
101 | 98, 99, 100 | subne0d 10280 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝑁 − 1) ≠ 0) |
102 | 96, 101 | eqnetrd 2849 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) ≠ 0) |
103 | | fveq2 6103 |
. . . . . . . . 9
⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) = ∅ →
(#‘(𝐹 ↾
(0..^(𝑁 − 1)))) =
(#‘∅)) |
104 | | hash0 13019 |
. . . . . . . . 9
⊢
(#‘∅) = 0 |
105 | 103, 104 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) = ∅ →
(#‘(𝐹 ↾
(0..^(𝑁 − 1)))) =
0) |
106 | 105 | necon3i 2814 |
. . . . . . 7
⊢
((#‘(𝐹 ↾
(0..^(𝑁 − 1)))) ≠
0 → (𝐹 ↾
(0..^(𝑁 − 1))) ≠
∅) |
107 | 102, 106 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅) |
108 | 95, 107 | jca 553 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧
(𝐹 ↾ (0..^(𝑁 − 1))) ≠
∅)) |
109 | | eldifsn 4260 |
. . . . 5
⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖
{∅}) ↔ ((𝐹
↾ (0..^(𝑁 −
1))) ∈ Word ℝ ∧ (𝐹 ↾ (0..^(𝑁 − 1))) ≠
∅)) |
110 | 108, 109 | sylibr 223 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖
{∅})) |
111 | 41 | adantr 480 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹‘(𝑁 − 1)) ∈
ℝ) |
112 | 14, 15, 16, 17 | signstfvn 29972 |
. . . 4
⊢ (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ∈ ℝ) → ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(#‘(𝐹 ↾ (0..^(𝑁 − 1))))) = (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ⨣
(sgn‘(𝐹‘(𝑁 − 1))))) |
113 | 110, 111,
112 | syl2anc 691 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(#‘(𝐹 ↾ (0..^(𝑁 − 1))))) = (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ⨣
(sgn‘(𝐹‘(𝑁 − 1))))) |
114 | | lennncl 13180 |
. . . . . 6
⊢ (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧
(𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅)
→ (#‘(𝐹 ↾
(0..^(𝑁 − 1))))
∈ ℕ) |
115 | | fzo0end 12426 |
. . . . . 6
⊢
((#‘(𝐹 ↾
(0..^(𝑁 − 1))))
∈ ℕ → ((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1) ∈
(0..^(#‘(𝐹 ↾
(0..^(𝑁 −
1)))))) |
116 | 108, 114,
115 | 3syl 18 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1) ∈
(0..^(#‘(𝐹 ↾
(0..^(𝑁 −
1)))))) |
117 | 14, 15, 16, 17 | signstcl 29968 |
. . . . 5
⊢ (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧
((#‘(𝐹 ↾
(0..^(𝑁 − 1))))
− 1) ∈ (0..^(#‘(𝐹 ↾ (0..^(𝑁 − 1)))))) → ((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ∈ {-1, 0,
1}) |
118 | 95, 116, 117 | syl2anc 691 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ∈ {-1, 0,
1}) |
119 | 44 | adantr 480 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0,
1}) |
120 | | simpr 476 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ≠ 0) |
121 | | sgn0bi 29936 |
. . . . . . . 8
⊢ ((𝐹‘(𝑁 − 1)) ∈ ℝ*
→ ((sgn‘(𝐹‘(𝑁 − 1))) = 0 ↔ (𝐹‘(𝑁 − 1)) = 0)) |
122 | 121 | necon3bid 2826 |
. . . . . . 7
⊢ ((𝐹‘(𝑁 − 1)) ∈ ℝ*
→ ((sgn‘(𝐹‘(𝑁 − 1))) ≠ 0 ↔ (𝐹‘(𝑁 − 1)) ≠ 0)) |
123 | 122 | biimpar 501 |
. . . . . 6
⊢ (((𝐹‘(𝑁 − 1)) ∈ ℝ*
∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(sgn‘(𝐹‘(𝑁 − 1))) ≠
0) |
124 | 42, 120, 123 | syl2anc 691 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(sgn‘(𝐹‘(𝑁 − 1))) ≠
0) |
125 | 124 | adantr 480 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (sgn‘(𝐹‘(𝑁 − 1))) ≠ 0) |
126 | 14, 15 | signswlid 29962 |
. . . 4
⊢
(((((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ∈ {-1, 0, 1}
∧ (sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0, 1}) ∧
(sgn‘(𝐹‘(𝑁 − 1))) ≠ 0) →
(((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ⨣
(sgn‘(𝐹‘(𝑁 − 1)))) =
(sgn‘(𝐹‘(𝑁 − 1)))) |
127 | 118, 119,
125, 126 | syl21anc 1317 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ⨣
(sgn‘(𝐹‘(𝑁 − 1)))) =
(sgn‘(𝐹‘(𝑁 − 1)))) |
128 | 90, 113, 127 | 3eqtrd 2648 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1)))) |
129 | 48, 128 | pm2.61dane 2869 |
1
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1)))) |