Proof of Theorem signsvtn0
Step | Hyp | Ref
| Expression |
1 | | eldifsn 4676 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) ↔ (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) |
2 | 1 | biimpi 219 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) |
3 | 2 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅)) |
4 | 3 | simpld 498 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 ∈ Word
ℝ) |
5 | 4 | adantr 484 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹 ∈ Word ℝ) |
6 | | wrdf 13963 |
. . . . . . . 8
⊢ (𝐹 ∈ Word ℝ →
𝐹:(0..^(♯‘𝐹))⟶ℝ) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹:(0..^(♯‘𝐹))⟶ℝ) |
8 | | lennncl 13978 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) →
(♯‘𝐹) ∈
ℕ) |
9 | 3, 8 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(♯‘𝐹) ∈
ℕ) |
10 | 9 | adantr 484 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (♯‘𝐹) ∈
ℕ) |
11 | | lbfzo0 13171 |
. . . . . . . 8
⊢ (0 ∈
(0..^(♯‘𝐹))
↔ (♯‘𝐹)
∈ ℕ) |
12 | 10, 11 | sylibr 237 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 0 ∈
(0..^(♯‘𝐹))) |
13 | 7, 12 | ffvelrnd 6865 |
. . . . . 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 32120 |
. . . . . 6
⊢ ((𝐹‘0) ∈ ℝ →
(𝑇‘〈“(𝐹‘0)”〉) =
〈“(sgn‘(𝐹‘0))”〉) |
19 | 13, 18 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘〈“(𝐹‘0)”〉) =
〈“(sgn‘(𝐹‘0))”〉) |
20 | | signsvtn0.1 |
. . . . . . . 8
⊢ 𝑁 = (♯‘𝐹) |
21 | | simpr 488 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝑁 = 1) |
22 | 20, 21 | eqtr3id 2788 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (♯‘𝐹) = 1) |
23 | | eqs1 14058 |
. . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧
(♯‘𝐹) = 1)
→ 𝐹 =
〈“(𝐹‘0)”〉) |
24 | 5, 22, 23 | syl2anc 587 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹 = 〈“(𝐹‘0)”〉) |
25 | 24 | fveq2d 6681 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘𝐹) = (𝑇‘〈“(𝐹‘0)”〉)) |
26 | | oveq1 7180 |
. . . . . . . . . 10
⊢ (𝑁 = 1 → (𝑁 − 1) = (1 −
1)) |
27 | | 1m1e0 11791 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
28 | 26, 27 | eqtrdi 2790 |
. . . . . . . . 9
⊢ (𝑁 = 1 → (𝑁 − 1) = 0) |
29 | 28 | fveq2d 6681 |
. . . . . . . 8
⊢ (𝑁 = 1 → (𝐹‘(𝑁 − 1)) = (𝐹‘0)) |
30 | 29 | fveq2d 6681 |
. . . . . . 7
⊢ (𝑁 = 1 → (sgn‘(𝐹‘(𝑁 − 1))) = (sgn‘(𝐹‘0))) |
31 | 30 | s1eqd 14047 |
. . . . . 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 2784 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘𝐹) = 〈“(sgn‘(𝐹‘(𝑁 − 1)))”〉) |
34 | 21, 28 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑁 − 1) = 0) |
35 | 33, 34 | fveq12d 6684 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) =
(〈“(sgn‘(𝐹‘(𝑁 −
1)))”〉‘0)) |
36 | 4, 6 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹:(0..^(♯‘𝐹))⟶ℝ) |
37 | 20 | oveq1i 7183 |
. . . . . . . . 9
⊢ (𝑁 − 1) =
((♯‘𝐹) −
1) |
38 | | fzo0end 13223 |
. . . . . . . . . 10
⊢
((♯‘𝐹)
∈ ℕ → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) |
39 | 3, 8, 38 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
((♯‘𝐹) −
1) ∈ (0..^(♯‘𝐹))) |
40 | 37, 39 | eqeltrid 2838 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) ∈
(0..^(♯‘𝐹))) |
41 | 36, 40 | ffvelrnd 6865 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ∈
ℝ) |
42 | 41 | rexrd 10772 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ∈
ℝ*) |
43 | | sgncl 32078 |
. . . . . 6
⊢ ((𝐹‘(𝑁 − 1)) ∈ ℝ*
→ (sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0,
1}) |
44 | 42, 43 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0,
1}) |
45 | 44 | adantr 484 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0,
1}) |
46 | | s1fv 14056 |
. . . 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 2774 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1)))) |
49 | | fzossfz 13150 |
. . . . . . . . . 10
⊢
(0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹)) |
50 | 49, 39 | sseldi 3876 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
((♯‘𝐹) −
1) ∈ (0...(♯‘𝐹))) |
51 | | pfxres 14133 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧
((♯‘𝐹) −
1) ∈ (0...(♯‘𝐹))) → (𝐹 prefix ((♯‘𝐹) − 1)) = (𝐹 ↾ (0..^((♯‘𝐹) − 1)))) |
52 | 4, 50, 51 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 prefix ((♯‘𝐹) − 1)) = (𝐹 ↾
(0..^((♯‘𝐹)
− 1)))) |
53 | 52 | oveq1d 7188 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝐹 prefix ((♯‘𝐹) − 1)) ++
〈“(lastS‘𝐹)”〉) = ((𝐹 ↾ (0..^((♯‘𝐹) − 1))) ++
〈“(lastS‘𝐹)”〉)) |
54 | | pfxlswccat 14167 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → ((𝐹 prefix ((♯‘𝐹) − 1)) ++
〈“(lastS‘𝐹)”〉) = 𝐹) |
55 | 54 | eqcomd 2745 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → 𝐹 = ((𝐹 prefix ((♯‘𝐹) − 1)) ++
〈“(lastS‘𝐹)”〉)) |
56 | 3, 55 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 = ((𝐹 prefix ((♯‘𝐹) − 1)) ++
〈“(lastS‘𝐹)”〉)) |
57 | 37 | oveq2i 7184 |
. . . . . . . . . 10
⊢
(0..^(𝑁 − 1))
= (0..^((♯‘𝐹)
− 1)) |
58 | 57 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^(𝑁 − 1)) =
(0..^((♯‘𝐹)
− 1))) |
59 | 58 | reseq2d 5826 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) = (𝐹 ↾ (0..^((♯‘𝐹) − 1)))) |
60 | 37 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) =
((♯‘𝐹) −
1)) |
61 | 60 | fveq2d 6681 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) = (𝐹‘((♯‘𝐹) − 1))) |
62 | | lsw 14008 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (lastS‘𝐹) = (𝐹‘((♯‘𝐹) − 1))) |
63 | 62 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(lastS‘𝐹) = (𝐹‘((♯‘𝐹) − 1))) |
64 | 61, 63 | eqtr4d 2777 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) = (lastS‘𝐹)) |
65 | 64 | s1eqd 14047 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
〈“(𝐹‘(𝑁 − 1))”〉 =
〈“(lastS‘𝐹)”〉) |
66 | 59, 65 | oveq12d 7191 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 − 1))”〉) = ((𝐹 ↾
(0..^((♯‘𝐹)
− 1))) ++ 〈“(lastS‘𝐹)”〉)) |
67 | 53, 56, 66 | 3eqtr4d 2784 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 = ((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 − 1))”〉)) |
68 | 67 | fveq2d 6681 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑇‘𝐹) = (𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 −
1))”〉))) |
69 | | ffn 6505 |
. . . . . . . . . . 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 7189 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^𝑁) = (0..^(♯‘𝐹))) |
73 | 72 | fneq2d 6433 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 Fn (0..^𝑁) ↔ 𝐹 Fn (0..^(♯‘𝐹)))) |
74 | 70, 73 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 Fn (0..^𝑁)) |
75 | 20, 9 | eqeltrid 2838 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 ∈
ℕ) |
76 | 75 | nnnn0d 12039 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 ∈
ℕ0) |
77 | | nn0z 12089 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
78 | | fzossrbm1 13160 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ →
(0..^(𝑁 − 1)) ⊆
(0..^𝑁)) |
79 | 76, 77, 78 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) |
80 | | fnssres 6460 |
. . . . . . . . 9
⊢ ((𝐹 Fn (0..^𝑁) ∧ (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) → (𝐹 ↾ (0..^(𝑁 − 1))) Fn (0..^(𝑁 − 1))) |
81 | 74, 79, 80 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) Fn (0..^(𝑁 − 1))) |
82 | | hashfn 13831 |
. . . . . . . 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 12020 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
85 | | hashfzo0 13886 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈
ℕ0 → (♯‘(0..^(𝑁 − 1))) = (𝑁 − 1)) |
86 | 75, 84, 85 | 3syl 18 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(♯‘(0..^(𝑁
− 1))) = (𝑁 −
1)) |
87 | 83, 86 | eqtrd 2774 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(♯‘(𝐹 ↾
(0..^(𝑁 − 1)))) =
(𝑁 −
1)) |
88 | 87 | eqcomd 2745 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) =
(♯‘(𝐹 ↾
(0..^(𝑁 −
1))))) |
89 | 68, 88 | fveq12d 6684 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝑇‘𝐹)‘(𝑁 − 1)) = ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(♯‘(𝐹 ↾ (0..^(𝑁 − 1)))))) |
90 | 89 | adantr 484 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(♯‘(𝐹 ↾ (0..^(𝑁 − 1)))))) |
91 | 52, 59 | eqtr4d 2777 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 prefix ((♯‘𝐹) − 1)) = (𝐹 ↾ (0..^(𝑁 − 1)))) |
92 | | pfxcl 14131 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word ℝ →
(𝐹 prefix
((♯‘𝐹) −
1)) ∈ Word ℝ) |
93 | 4, 92 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 prefix ((♯‘𝐹) − 1)) ∈ Word
ℝ) |
94 | 91, 93 | eqeltrrd 2835 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word
ℝ) |
95 | 94 | adantr 484 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word
ℝ) |
96 | 87 | adantr 484 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (𝑁 − 1)) |
97 | 75 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ∈ ℕ) |
98 | 97 | nncnd 11735 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ∈ ℂ) |
99 | | 1cnd 10717 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 1 ∈
ℂ) |
100 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ≠ 1) |
101 | 98, 99, 100 | subne0d 11087 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝑁 − 1) ≠ 0) |
102 | 96, 101 | eqnetrd 3002 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) ≠ 0) |
103 | | fveq2 6677 |
. . . . . . . . 9
⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) = ∅ →
(♯‘(𝐹 ↾
(0..^(𝑁 − 1)))) =
(♯‘∅)) |
104 | | hash0 13823 |
. . . . . . . . 9
⊢
(♯‘∅) = 0 |
105 | 103, 104 | eqtrdi 2790 |
. . . . . . . 8
⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) = ∅ →
(♯‘(𝐹 ↾
(0..^(𝑁 − 1)))) =
0) |
106 | 105 | necon3i 2967 |
. . . . . . 7
⊢
((♯‘(𝐹
↾ (0..^(𝑁 −
1)))) ≠ 0 → (𝐹
↾ (0..^(𝑁 −
1))) ≠ ∅) |
107 | 102, 106 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅) |
108 | 95, 107 | jca 515 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧
(𝐹 ↾ (0..^(𝑁 − 1))) ≠
∅)) |
109 | | eldifsn 4676 |
. . . . 5
⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖
{∅}) ↔ ((𝐹
↾ (0..^(𝑁 −
1))) ∈ Word ℝ ∧ (𝐹 ↾ (0..^(𝑁 − 1))) ≠
∅)) |
110 | 108, 109 | sylibr 237 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖
{∅})) |
111 | 41 | adantr 484 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹‘(𝑁 − 1)) ∈
ℝ) |
112 | 14, 15, 16, 17 | signstfvn 32121 |
. . . 4
⊢ (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ∈ ℝ) → ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(♯‘(𝐹 ↾ (0..^(𝑁 − 1))))) = (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ⨣
(sgn‘(𝐹‘(𝑁 − 1))))) |
113 | 110, 111,
112 | syl2anc 587 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(♯‘(𝐹 ↾ (0..^(𝑁 − 1))))) = (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ⨣
(sgn‘(𝐹‘(𝑁 − 1))))) |
114 | | lennncl 13978 |
. . . . . 6
⊢ (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧
(𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅)
→ (♯‘(𝐹
↾ (0..^(𝑁 −
1)))) ∈ ℕ) |
115 | | fzo0end 13223 |
. . . . . 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 32117 |
. . . . 5
⊢ (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧
((♯‘(𝐹 ↾
(0..^(𝑁 − 1))))
− 1) ∈ (0..^(♯‘(𝐹 ↾ (0..^(𝑁 − 1)))))) → ((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ∈ {-1, 0,
1}) |
118 | 95, 116, 117 | syl2anc 587 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ∈ {-1, 0,
1}) |
119 | 44 | adantr 484 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0,
1}) |
120 | | simpr 488 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ≠ 0) |
121 | | sgn0bi 32087 |
. . . . . . . 8
⊢ ((𝐹‘(𝑁 − 1)) ∈ ℝ*
→ ((sgn‘(𝐹‘(𝑁 − 1))) = 0 ↔ (𝐹‘(𝑁 − 1)) = 0)) |
122 | 121 | necon3bid 2979 |
. . . . . . 7
⊢ ((𝐹‘(𝑁 − 1)) ∈ ℝ*
→ ((sgn‘(𝐹‘(𝑁 − 1))) ≠ 0 ↔ (𝐹‘(𝑁 − 1)) ≠ 0)) |
123 | 122 | biimpar 481 |
. . . . . 6
⊢ (((𝐹‘(𝑁 − 1)) ∈ ℝ*
∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(sgn‘(𝐹‘(𝑁 − 1))) ≠
0) |
124 | 42, 120, 123 | syl2anc 587 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) →
(sgn‘(𝐹‘(𝑁 − 1))) ≠
0) |
125 | 124 | adantr 484 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (sgn‘(𝐹‘(𝑁 − 1))) ≠ 0) |
126 | 14, 15 | signswlid 32111 |
. . . 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 837 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ⨣
(sgn‘(𝐹‘(𝑁 − 1)))) =
(sgn‘(𝐹‘(𝑁 − 1)))) |
128 | 90, 113, 127 | 3eqtrd 2778 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1)))) |
129 | 48, 128 | pm2.61dane 3022 |
1
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1)))) |