Proof of Theorem signstfveq0
Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝐹 ∈ (Word ℝ ∖
{∅})) |
2 | 1 | eldifad 3552 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝐹 ∈ Word ℝ) |
3 | | swrdcl 13271 |
. . . . 5
⊢ (𝐹 ∈ Word ℝ →
(𝐹 substr 〈0, (𝑁 − 1)〉) ∈ Word
ℝ) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹 substr 〈0, (𝑁 − 1)〉) ∈ Word
ℝ) |
5 | | 1nn0 11185 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
6 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ∈
ℕ0) |
7 | 6 | nn0red 11229 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ∈
ℝ) |
8 | | 2re 10967 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 2 ∈
ℝ) |
10 | | signstfveq0.1 |
. . . . . . . . . . . . 13
⊢ 𝑁 = (#‘𝐹) |
11 | | lencl 13179 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word ℝ →
(#‘𝐹) ∈
ℕ0) |
12 | 2, 11 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (#‘𝐹) ∈
ℕ0) |
13 | 10, 12 | syl5eqel 2692 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈
ℕ0) |
14 | 13 | nn0red 11229 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈ ℝ) |
15 | | 1le2 11118 |
. . . . . . . . . . . 12
⊢ 1 ≤
2 |
16 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ≤
2) |
17 | | signsv.p |
. . . . . . . . . . . . . 14
⊢ ⨣ =
(𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦
if(𝑏 = 0, 𝑎, 𝑏)) |
18 | | signsv.w |
. . . . . . . . . . . . . 14
⊢ 𝑊 = {〈(Base‘ndx), {-1,
0, 1}〉, 〈(+g‘ndx), ⨣
〉} |
19 | | signsv.t |
. . . . . . . . . . . . . 14
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
20 | | signsv.v |
. . . . . . . . . . . . . 14
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
21 | 17, 18, 19, 20, 10 | signstfveq0a 29979 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈
(ℤ≥‘2)) |
22 | | eluz2 11569 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤
𝑁)) |
23 | 21, 22 | sylib 207 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (2 ∈ ℤ
∧ 𝑁 ∈ ℤ
∧ 2 ≤ 𝑁)) |
24 | 23 | simp3d 1068 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 2 ≤ 𝑁) |
25 | 7, 9, 14, 16, 24 | letrd 10073 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ≤ 𝑁) |
26 | | fznn0 12301 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (1 ∈ (0...𝑁)
↔ (1 ∈ ℕ0 ∧ 1 ≤ 𝑁))) |
27 | 13, 26 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (1 ∈
(0...𝑁) ↔ (1 ∈
ℕ0 ∧ 1 ≤ 𝑁))) |
28 | 6, 25, 27 | mpbir2and 959 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ∈ (0...𝑁)) |
29 | | fznn0sub2 12315 |
. . . . . . . . 9
⊢ (1 ∈
(0...𝑁) → (𝑁 − 1) ∈ (0...𝑁)) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 1) ∈ (0...𝑁)) |
31 | 10 | oveq2i 6560 |
. . . . . . . 8
⊢
(0...𝑁) =
(0...(#‘𝐹)) |
32 | 30, 31 | syl6eleq 2698 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 1) ∈ (0...(#‘𝐹))) |
33 | | swrd0len 13274 |
. . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧
(𝑁 − 1) ∈
(0...(#‘𝐹))) →
(#‘(𝐹 substr 〈0,
(𝑁 − 1)〉)) =
(𝑁 −
1)) |
34 | 2, 32, 33 | syl2anc 691 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) = (𝑁 − 1)) |
35 | | uz2m1nn 11639 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) |
36 | 21, 35 | syl 17 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 1) ∈ ℕ) |
37 | 34, 36 | eqeltrd 2688 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) ∈
ℕ) |
38 | | nnne0 10930 |
. . . . . 6
⊢
((#‘(𝐹 substr
〈0, (𝑁 −
1)〉)) ∈ ℕ → (#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) ≠ 0) |
39 | | fveq2 6103 |
. . . . . . . 8
⊢ ((𝐹 substr 〈0, (𝑁 − 1)〉) = ∅
→ (#‘(𝐹 substr
〈0, (𝑁 −
1)〉)) = (#‘∅)) |
40 | | hash0 13019 |
. . . . . . . 8
⊢
(#‘∅) = 0 |
41 | 39, 40 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝐹 substr 〈0, (𝑁 − 1)〉) = ∅
→ (#‘(𝐹 substr
〈0, (𝑁 −
1)〉)) = 0) |
42 | 41 | necon3i 2814 |
. . . . . 6
⊢
((#‘(𝐹 substr
〈0, (𝑁 −
1)〉)) ≠ 0 → (𝐹
substr 〈0, (𝑁 −
1)〉) ≠ ∅) |
43 | 38, 42 | syl 17 |
. . . . 5
⊢
((#‘(𝐹 substr
〈0, (𝑁 −
1)〉)) ∈ ℕ → (𝐹 substr 〈0, (𝑁 − 1)〉) ≠
∅) |
44 | 37, 43 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹 substr 〈0, (𝑁 − 1)〉) ≠
∅) |
45 | | eldifsn 4260 |
. . . 4
⊢ ((𝐹 substr 〈0, (𝑁 − 1)〉) ∈ (Word
ℝ ∖ {∅}) ↔ ((𝐹 substr 〈0, (𝑁 − 1)〉) ∈ Word ℝ ∧
(𝐹 substr 〈0, (𝑁 − 1)〉) ≠
∅)) |
46 | 4, 44, 45 | sylanbrc 695 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹 substr 〈0, (𝑁 − 1)〉) ∈ (Word ℝ
∖ {∅})) |
47 | | simpr 476 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹‘(𝑁 − 1)) = 0) |
48 | | 0re 9919 |
. . . 4
⊢ 0 ∈
ℝ |
49 | 47, 48 | syl6eqel 2696 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹‘(𝑁 − 1)) ∈
ℝ) |
50 | 17, 18, 19, 20 | signstfvn 29972 |
. . 3
⊢ (((𝐹 substr 〈0, (𝑁 − 1)〉) ∈ (Word
ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ∈ ℝ) → ((𝑇‘((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(#‘(𝐹 substr 〈0, (𝑁 − 1)〉))) = (((𝑇‘(𝐹 substr 〈0, (𝑁 − 1)〉))‘((#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) − 1))
⨣
(sgn‘(𝐹‘(𝑁 − 1))))) |
51 | 46, 49, 50 | syl2anc 691 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(#‘(𝐹 substr 〈0, (𝑁 − 1)〉))) = (((𝑇‘(𝐹 substr 〈0, (𝑁 − 1)〉))‘((#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) − 1))
⨣
(sgn‘(𝐹‘(𝑁 − 1))))) |
52 | 10 | oveq1i 6559 |
. . . . . . . . 9
⊢ (𝑁 − 1) = ((#‘𝐹) − 1) |
53 | 52 | opeq2i 4344 |
. . . . . . . 8
⊢ 〈0,
(𝑁 − 1)〉 =
〈0, ((#‘𝐹)
− 1)〉 |
54 | 53 | oveq2i 6560 |
. . . . . . 7
⊢ (𝐹 substr 〈0, (𝑁 − 1)〉) = (𝐹 substr 〈0, ((#‘𝐹) −
1)〉) |
55 | 54 | a1i 11 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹 substr 〈0, (𝑁 − 1)〉) = (𝐹 substr 〈0, ((#‘𝐹) − 1)〉)) |
56 | | lsw 13204 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ( lastS ‘𝐹) = (𝐹‘((#‘𝐹) − 1))) |
57 | 56 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ( lastS
‘𝐹) = (𝐹‘((#‘𝐹) − 1))) |
58 | 10 | eqcomi 2619 |
. . . . . . . . . . 11
⊢
(#‘𝐹) = 𝑁 |
59 | 58 | oveq1i 6559 |
. . . . . . . . . 10
⊢
((#‘𝐹) −
1) = (𝑁 −
1) |
60 | 59 | fveq2i 6106 |
. . . . . . . . 9
⊢ (𝐹‘((#‘𝐹) − 1)) = (𝐹‘(𝑁 − 1)) |
61 | 57, 60 | syl6eq 2660 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ( lastS
‘𝐹) = (𝐹‘(𝑁 − 1))) |
62 | 61 | s1eqd 13234 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 〈“(
lastS ‘𝐹)”〉 = 〈“(𝐹‘(𝑁 − 1))”〉) |
63 | 62 | eqcomd 2616 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 〈“(𝐹‘(𝑁 − 1))”〉 = 〈“(
lastS ‘𝐹)”〉) |
64 | 55, 63 | oveq12d 6567 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 − 1))”〉) = ((𝐹 substr 〈0, ((#‘𝐹) − 1)〉) ++
〈“( lastS ‘𝐹)”〉)) |
65 | | eldifsn 4260 |
. . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) ↔ (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) |
66 | 1, 65 | sylib 207 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅)) |
67 | | swrdccatwrd 13320 |
. . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → ((𝐹 substr 〈0, ((#‘𝐹) − 1)〉) ++
〈“( lastS ‘𝐹)”〉) = 𝐹) |
68 | 66, 67 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝐹 substr 〈0, ((#‘𝐹) − 1)〉) ++ 〈“( lastS
‘𝐹)”〉) =
𝐹) |
69 | 64, 68 | eqtrd 2644 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 − 1))”〉) = 𝐹) |
70 | 69 | fveq2d 6107 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑇‘((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 − 1))”〉)) = (𝑇‘𝐹)) |
71 | 70, 34 | fveq12d 6109 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(#‘(𝐹 substr 〈0, (𝑁 − 1)〉))) = ((𝑇‘𝐹)‘(𝑁 − 1))) |
72 | 13 | nn0cnd 11230 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈ ℂ) |
73 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ∈
ℂ) |
74 | 72, 73, 73 | subsub4d 10302 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1))) |
75 | | 1p1e2 11011 |
. . . . . . . . . 10
⊢ (1 + 1) =
2 |
76 | 75 | oveq2i 6560 |
. . . . . . . . 9
⊢ (𝑁 − (1 + 1)) = (𝑁 − 2) |
77 | 74, 76 | syl6eq 2660 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
78 | | fzo0end 12426 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈ ℕ
→ ((𝑁 − 1)
− 1) ∈ (0..^(𝑁
− 1))) |
79 | 36, 78 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑁 − 1) − 1) ∈ (0..^(𝑁 − 1))) |
80 | 77, 79 | eqeltrrd 2689 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) |
81 | 34 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) →
(0..^(#‘(𝐹 substr
〈0, (𝑁 −
1)〉))) = (0..^(𝑁
− 1))) |
82 | 80, 81 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) ∈ (0..^(#‘(𝐹 substr 〈0, (𝑁 −
1)〉)))) |
83 | 17, 18, 19, 20 | signstfvp 29974 |
. . . . . 6
⊢ (((𝐹 substr 〈0, (𝑁 − 1)〉) ∈ Word
ℝ ∧ (𝐹‘(𝑁 − 1)) ∈ ℝ ∧ (𝑁 − 2) ∈
(0..^(#‘(𝐹 substr
〈0, (𝑁 −
1)〉)))) → ((𝑇‘((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 − 1))”〉))‘(𝑁 − 2)) = ((𝑇‘(𝐹 substr 〈0, (𝑁 − 1)〉))‘(𝑁 − 2))) |
84 | 4, 49, 82, 83 | syl3anc 1318 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 − 1))”〉))‘(𝑁 − 2)) = ((𝑇‘(𝐹 substr 〈0, (𝑁 − 1)〉))‘(𝑁 − 2))) |
85 | 69 | eqcomd 2616 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝐹 = ((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 − 1))”〉)) |
86 | 85 | fveq2d 6107 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑇‘𝐹) = (𝑇‘((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 −
1))”〉))) |
87 | 86 | fveq1d 6105 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘𝐹)‘(𝑁 − 2)) = ((𝑇‘((𝐹 substr 〈0, (𝑁 − 1)〉) ++ 〈“(𝐹‘(𝑁 − 1))”〉))‘(𝑁 − 2))) |
88 | 34 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) − 1) =
((𝑁 − 1) −
1)) |
89 | 88, 74 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) − 1) =
(𝑁 − (1 +
1))) |
90 | 89, 76 | syl6eq 2660 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) − 1) =
(𝑁 −
2)) |
91 | 90 | fveq2d 6107 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘(𝐹 substr 〈0, (𝑁 − 1)〉))‘((#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) − 1))
= ((𝑇‘(𝐹 substr 〈0, (𝑁 − 1)〉))‘(𝑁 − 2))) |
92 | 84, 87, 91 | 3eqtr4rd 2655 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘(𝐹 substr 〈0, (𝑁 − 1)〉))‘((#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) − 1))
= ((𝑇‘𝐹)‘(𝑁 − 2))) |
93 | | fveq2 6103 |
. . . . . 6
⊢ ((𝐹‘(𝑁 − 1)) = 0 → (sgn‘(𝐹‘(𝑁 − 1))) =
(sgn‘0)) |
94 | | sgn0 13677 |
. . . . . 6
⊢
(sgn‘0) = 0 |
95 | 93, 94 | syl6eq 2660 |
. . . . 5
⊢ ((𝐹‘(𝑁 − 1)) = 0 → (sgn‘(𝐹‘(𝑁 − 1))) = 0) |
96 | 95 | adantl 481 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (sgn‘(𝐹‘(𝑁 − 1))) = 0) |
97 | 92, 96 | oveq12d 6567 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (((𝑇‘(𝐹 substr 〈0, (𝑁 − 1)〉))‘((#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) − 1))
⨣
(sgn‘(𝐹‘(𝑁 − 1)))) = (((𝑇‘𝐹)‘(𝑁 − 2)) ⨣
0)) |
98 | | uznn0sub 11595 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
99 | 21, 98 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) ∈
ℕ0) |
100 | | eluz2nn 11602 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) |
101 | 21, 100 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈ ℕ) |
102 | | 2rp 11713 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
103 | 102 | a1i 11 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 2 ∈
ℝ+) |
104 | 14, 103 | ltsubrpd 11780 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) < 𝑁) |
105 | | elfzo0 12376 |
. . . . . . 7
⊢ ((𝑁 − 2) ∈ (0..^𝑁) ↔ ((𝑁 − 2) ∈ ℕ0 ∧
𝑁 ∈ ℕ ∧
(𝑁 − 2) < 𝑁)) |
106 | 99, 101, 104, 105 | syl3anbrc 1239 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) ∈ (0..^𝑁)) |
107 | 10 | oveq2i 6560 |
. . . . . 6
⊢
(0..^𝑁) =
(0..^(#‘𝐹)) |
108 | 106, 107 | syl6eleq 2698 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) ∈ (0..^(#‘𝐹))) |
109 | 17, 18, 19, 20 | signstcl 29968 |
. . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧
(𝑁 − 2) ∈
(0..^(#‘𝐹))) →
((𝑇‘𝐹)‘(𝑁 − 2)) ∈ {-1, 0,
1}) |
110 | 2, 108, 109 | syl2anc 691 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘𝐹)‘(𝑁 − 2)) ∈ {-1, 0,
1}) |
111 | 17, 18 | signswrid 29961 |
. . . 4
⊢ (((𝑇‘𝐹)‘(𝑁 − 2)) ∈ {-1, 0, 1} →
(((𝑇‘𝐹)‘(𝑁 − 2)) ⨣ 0) = ((𝑇‘𝐹)‘(𝑁 − 2))) |
112 | 110, 111 | syl 17 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (((𝑇‘𝐹)‘(𝑁 − 2)) ⨣ 0) = ((𝑇‘𝐹)‘(𝑁 − 2))) |
113 | 97, 112 | eqtrd 2644 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (((𝑇‘(𝐹 substr 〈0, (𝑁 − 1)〉))‘((#‘(𝐹 substr 〈0, (𝑁 − 1)〉)) − 1))
⨣
(sgn‘(𝐹‘(𝑁 − 1)))) = ((𝑇‘𝐹)‘(𝑁 − 2))) |
114 | 51, 71, 113 | 3eqtr3d 2652 |
1
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘𝐹)‘(𝑁 − 1)) = ((𝑇‘𝐹)‘(𝑁 − 2))) |