Proof of Theorem signstfveq0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpll 766 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝐹 ∈ (Word ℝ ∖
{∅})) | 
| 2 | 1 | eldifad 3962 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝐹 ∈ Word ℝ) | 
| 3 |  | pfxcl 14716 | . . . . 5
⊢ (𝐹 ∈ Word ℝ →
(𝐹 prefix (𝑁 − 1)) ∈ Word
ℝ) | 
| 4 | 2, 3 | syl 17 | . . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹 prefix (𝑁 − 1)) ∈ Word
ℝ) | 
| 5 |  | 1nn0 12544 | . . . . . . . . . . 11
⊢ 1 ∈
ℕ0 | 
| 6 | 5 | a1i 11 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ∈
ℕ0) | 
| 7 | 6 | nn0red 12590 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ∈
ℝ) | 
| 8 |  | 2re 12341 | . . . . . . . . . . . 12
⊢ 2 ∈
ℝ | 
| 9 | 8 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 2 ∈
ℝ) | 
| 10 |  | signstfveq0.1 | . . . . . . . . . . . . 13
⊢ 𝑁 = (♯‘𝐹) | 
| 11 |  | lencl 14572 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℕ0) | 
| 12 | 2, 11 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) →
(♯‘𝐹) ∈
ℕ0) | 
| 13 | 10, 12 | eqeltrid 2844 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈
ℕ0) | 
| 14 | 13 | nn0red 12590 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈ ℝ) | 
| 15 |  | 1le2 12476 | . . . . . . . . . . . 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 34592 | . . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈
(ℤ≥‘2)) | 
| 22 |  | eluz2 12885 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤
𝑁)) | 
| 23 | 21, 22 | sylib 218 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (2 ∈ ℤ
∧ 𝑁 ∈ ℤ
∧ 2 ≤ 𝑁)) | 
| 24 | 23 | simp3d 1144 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 2 ≤ 𝑁) | 
| 25 | 7, 9, 14, 16, 24 | letrd 11419 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ≤ 𝑁) | 
| 26 |  | fznn0 13660 | . . . . . . . . . . 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 713 | . . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ∈ (0...𝑁)) | 
| 29 |  | fznn0sub2 13676 | . . . . . . . . 9
⊢ (1 ∈
(0...𝑁) → (𝑁 − 1) ∈ (0...𝑁)) | 
| 30 | 28, 29 | syl 17 | . . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 1) ∈ (0...𝑁)) | 
| 31 | 10 | oveq2i 7443 | . . . . . . . 8
⊢
(0...𝑁) =
(0...(♯‘𝐹)) | 
| 32 | 30, 31 | eleqtrdi 2850 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 1) ∈ (0...(♯‘𝐹))) | 
| 33 |  | pfxlen 14722 | . . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧
(𝑁 − 1) ∈
(0...(♯‘𝐹)))
→ (♯‘(𝐹
prefix (𝑁 − 1))) =
(𝑁 −
1)) | 
| 34 | 2, 32, 33 | syl2anc 584 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) →
(♯‘(𝐹 prefix
(𝑁 − 1))) = (𝑁 − 1)) | 
| 35 |  | uz2m1nn 12966 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) | 
| 36 | 21, 35 | syl 17 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 1) ∈ ℕ) | 
| 37 | 34, 36 | eqeltrd 2840 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) →
(♯‘(𝐹 prefix
(𝑁 − 1))) ∈
ℕ) | 
| 38 |  | nnne0 12301 | . . . . . 6
⊢
((♯‘(𝐹
prefix (𝑁 − 1)))
∈ ℕ → (♯‘(𝐹 prefix (𝑁 − 1))) ≠ 0) | 
| 39 |  | fveq2 6905 | . . . . . . . 8
⊢ ((𝐹 prefix (𝑁 − 1)) = ∅ →
(♯‘(𝐹 prefix
(𝑁 − 1))) =
(♯‘∅)) | 
| 40 |  | hash0 14407 | . . . . . . . 8
⊢
(♯‘∅) = 0 | 
| 41 | 39, 40 | eqtrdi 2792 | . . . . . . 7
⊢ ((𝐹 prefix (𝑁 − 1)) = ∅ →
(♯‘(𝐹 prefix
(𝑁 − 1))) =
0) | 
| 42 | 41 | necon3i 2972 | . . . . . 6
⊢
((♯‘(𝐹
prefix (𝑁 − 1))) ≠
0 → (𝐹 prefix (𝑁 − 1)) ≠
∅) | 
| 43 | 38, 42 | syl 17 | . . . . 5
⊢
((♯‘(𝐹
prefix (𝑁 − 1)))
∈ ℕ → (𝐹
prefix (𝑁 − 1)) ≠
∅) | 
| 44 | 37, 43 | syl 17 | . . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹 prefix (𝑁 − 1)) ≠ ∅) | 
| 45 |  | eldifsn 4785 | . . . 4
⊢ ((𝐹 prefix (𝑁 − 1)) ∈ (Word ℝ ∖
{∅}) ↔ ((𝐹
prefix (𝑁 − 1))
∈ Word ℝ ∧ (𝐹 prefix (𝑁 − 1)) ≠ ∅)) | 
| 46 | 4, 44, 45 | sylanbrc 583 | . . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹 prefix (𝑁 − 1)) ∈ (Word ℝ ∖
{∅})) | 
| 47 |  | simpr 484 | . . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹‘(𝑁 − 1)) = 0) | 
| 48 |  | 0re 11264 | . . . 4
⊢ 0 ∈
ℝ | 
| 49 | 47, 48 | eqeltrdi 2848 | . . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹‘(𝑁 − 1)) ∈
ℝ) | 
| 50 | 17, 18, 19, 20 | signstfvn 34585 | . . 3
⊢ (((𝐹 prefix (𝑁 − 1)) ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘(𝑁 − 1)) ∈ ℝ) → ((𝑇‘((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(♯‘(𝐹 prefix (𝑁 − 1)))) = (((𝑇‘(𝐹 prefix (𝑁 − 1)))‘((♯‘(𝐹 prefix (𝑁 − 1))) − 1)) ⨣ (sgn‘(𝐹‘(𝑁 − 1))))) | 
| 51 | 46, 49, 50 | syl2anc 584 | . 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(♯‘(𝐹 prefix (𝑁 − 1)))) = (((𝑇‘(𝐹 prefix (𝑁 − 1)))‘((♯‘(𝐹 prefix (𝑁 − 1))) − 1)) ⨣ (sgn‘(𝐹‘(𝑁 − 1))))) | 
| 52 | 10 | oveq1i 7442 | . . . . . . . 8
⊢ (𝑁 − 1) =
((♯‘𝐹) −
1) | 
| 53 | 52 | oveq2i 7443 | . . . . . . 7
⊢ (𝐹 prefix (𝑁 − 1)) = (𝐹 prefix ((♯‘𝐹) − 1)) | 
| 54 | 53 | a1i 11 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹 prefix (𝑁 − 1)) = (𝐹 prefix ((♯‘𝐹) − 1))) | 
| 55 |  | lsw 14603 | . . . . . . . . . 10
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (lastS‘𝐹) = (𝐹‘((♯‘𝐹) − 1))) | 
| 56 | 55 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (lastS‘𝐹) = (𝐹‘((♯‘𝐹) − 1))) | 
| 57 | 10 | eqcomi 2745 | . . . . . . . . . . 11
⊢
(♯‘𝐹) =
𝑁 | 
| 58 | 57 | oveq1i 7442 | . . . . . . . . . 10
⊢
((♯‘𝐹)
− 1) = (𝑁 −
1) | 
| 59 | 58 | fveq2i 6908 | . . . . . . . . 9
⊢ (𝐹‘((♯‘𝐹) − 1)) = (𝐹‘(𝑁 − 1)) | 
| 60 | 56, 59 | eqtrdi 2792 | . . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (lastS‘𝐹) = (𝐹‘(𝑁 − 1))) | 
| 61 | 60 | s1eqd 14640 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) →
〈“(lastS‘𝐹)”〉 = 〈“(𝐹‘(𝑁 − 1))”〉) | 
| 62 | 61 | eqcomd 2742 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 〈“(𝐹‘(𝑁 − 1))”〉 =
〈“(lastS‘𝐹)”〉) | 
| 63 | 54, 62 | oveq12d 7450 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 − 1))”〉) = ((𝐹 prefix ((♯‘𝐹) − 1)) ++
〈“(lastS‘𝐹)”〉)) | 
| 64 |  | eldifsn 4785 | . . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) ↔ (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) | 
| 65 | 1, 64 | sylib 218 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅)) | 
| 66 |  | pfxlswccat 14752 | . . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → ((𝐹 prefix ((♯‘𝐹) − 1)) ++
〈“(lastS‘𝐹)”〉) = 𝐹) | 
| 67 | 65, 66 | syl 17 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝐹 prefix ((♯‘𝐹) − 1)) ++
〈“(lastS‘𝐹)”〉) = 𝐹) | 
| 68 | 63, 67 | eqtrd 2776 | . . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 − 1))”〉) = 𝐹) | 
| 69 | 68 | fveq2d 6909 | . . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑇‘((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 − 1))”〉)) = (𝑇‘𝐹)) | 
| 70 | 69, 34 | fveq12d 6912 | . 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 −
1))”〉))‘(♯‘(𝐹 prefix (𝑁 − 1)))) = ((𝑇‘𝐹)‘(𝑁 − 1))) | 
| 71 | 13 | nn0cnd 12591 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈ ℂ) | 
| 72 |  | 1cnd 11257 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 1 ∈
ℂ) | 
| 73 | 71, 72, 72 | subsub4d 11652 | . . . . . . . . 9
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1))) | 
| 74 |  | 1p1e2 12392 | . . . . . . . . . 10
⊢ (1 + 1) =
2 | 
| 75 | 74 | oveq2i 7443 | . . . . . . . . 9
⊢ (𝑁 − (1 + 1)) = (𝑁 − 2) | 
| 76 | 73, 75 | eqtrdi 2792 | . . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑁 − 1) − 1) = (𝑁 − 2)) | 
| 77 |  | fzo0end 13798 | . . . . . . . . 9
⊢ ((𝑁 − 1) ∈ ℕ
→ ((𝑁 − 1)
− 1) ∈ (0..^(𝑁
− 1))) | 
| 78 | 36, 77 | syl 17 | . . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑁 − 1) − 1) ∈ (0..^(𝑁 − 1))) | 
| 79 | 76, 78 | eqeltrrd 2841 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) ∈ (0..^(𝑁 − 1))) | 
| 80 | 34 | oveq2d 7448 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) →
(0..^(♯‘(𝐹
prefix (𝑁 − 1)))) =
(0..^(𝑁 −
1))) | 
| 81 | 79, 80 | eleqtrrd 2843 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) ∈
(0..^(♯‘(𝐹
prefix (𝑁 −
1))))) | 
| 82 | 17, 18, 19, 20 | signstfvp 34587 | . . . . . 6
⊢ (((𝐹 prefix (𝑁 − 1)) ∈ Word ℝ ∧
(𝐹‘(𝑁 − 1)) ∈ ℝ ∧ (𝑁 − 2) ∈
(0..^(♯‘(𝐹
prefix (𝑁 − 1)))))
→ ((𝑇‘((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 − 1))”〉))‘(𝑁 − 2)) = ((𝑇‘(𝐹 prefix (𝑁 − 1)))‘(𝑁 − 2))) | 
| 83 | 4, 49, 81, 82 | syl3anc 1372 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 − 1))”〉))‘(𝑁 − 2)) = ((𝑇‘(𝐹 prefix (𝑁 − 1)))‘(𝑁 − 2))) | 
| 84 | 68 | eqcomd 2742 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝐹 = ((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 − 1))”〉)) | 
| 85 | 84 | fveq2d 6909 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑇‘𝐹) = (𝑇‘((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 −
1))”〉))) | 
| 86 | 85 | fveq1d 6907 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘𝐹)‘(𝑁 − 2)) = ((𝑇‘((𝐹 prefix (𝑁 − 1)) ++ 〈“(𝐹‘(𝑁 − 1))”〉))‘(𝑁 − 2))) | 
| 87 | 34 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) →
((♯‘(𝐹 prefix
(𝑁 − 1))) − 1)
= ((𝑁 − 1) −
1)) | 
| 88 | 87, 73 | eqtrd 2776 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) →
((♯‘(𝐹 prefix
(𝑁 − 1))) − 1)
= (𝑁 − (1 +
1))) | 
| 89 | 88, 75 | eqtrdi 2792 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) →
((♯‘(𝐹 prefix
(𝑁 − 1))) − 1)
= (𝑁 −
2)) | 
| 90 | 89 | fveq2d 6909 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘(𝐹 prefix (𝑁 − 1)))‘((♯‘(𝐹 prefix (𝑁 − 1))) − 1)) = ((𝑇‘(𝐹 prefix (𝑁 − 1)))‘(𝑁 − 2))) | 
| 91 | 83, 86, 90 | 3eqtr4rd 2787 | . . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘(𝐹 prefix (𝑁 − 1)))‘((♯‘(𝐹 prefix (𝑁 − 1))) − 1)) = ((𝑇‘𝐹)‘(𝑁 − 2))) | 
| 92 |  | fveq2 6905 | . . . . . 6
⊢ ((𝐹‘(𝑁 − 1)) = 0 → (sgn‘(𝐹‘(𝑁 − 1))) =
(sgn‘0)) | 
| 93 |  | sgn0 15129 | . . . . . 6
⊢
(sgn‘0) = 0 | 
| 94 | 92, 93 | eqtrdi 2792 | . . . . 5
⊢ ((𝐹‘(𝑁 − 1)) = 0 → (sgn‘(𝐹‘(𝑁 − 1))) = 0) | 
| 95 | 94 | adantl 481 | . . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (sgn‘(𝐹‘(𝑁 − 1))) = 0) | 
| 96 | 91, 95 | oveq12d 7450 | . . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (((𝑇‘(𝐹 prefix (𝑁 − 1)))‘((♯‘(𝐹 prefix (𝑁 − 1))) − 1)) ⨣ (sgn‘(𝐹‘(𝑁 − 1)))) = (((𝑇‘𝐹)‘(𝑁 − 2)) ⨣
0)) | 
| 97 |  | uznn0sub 12918 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) | 
| 98 | 21, 97 | syl 17 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) ∈
ℕ0) | 
| 99 |  | eluz2nn 12925 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) | 
| 100 | 21, 99 | syl 17 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 𝑁 ∈ ℕ) | 
| 101 |  | 2rp 13040 | . . . . . . . . 9
⊢ 2 ∈
ℝ+ | 
| 102 | 101 | a1i 11 | . . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → 2 ∈
ℝ+) | 
| 103 | 14, 102 | ltsubrpd 13110 | . . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) < 𝑁) | 
| 104 |  | elfzo0 13741 | . . . . . . 7
⊢ ((𝑁 − 2) ∈ (0..^𝑁) ↔ ((𝑁 − 2) ∈ ℕ0 ∧
𝑁 ∈ ℕ ∧
(𝑁 − 2) < 𝑁)) | 
| 105 | 98, 100, 103, 104 | syl3anbrc 1343 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) ∈ (0..^𝑁)) | 
| 106 | 10 | oveq2i 7443 | . . . . . 6
⊢
(0..^𝑁) =
(0..^(♯‘𝐹)) | 
| 107 | 105, 106 | eleqtrdi 2850 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (𝑁 − 2) ∈ (0..^(♯‘𝐹))) | 
| 108 | 17, 18, 19, 20 | signstcl 34581 | . . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧
(𝑁 − 2) ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘𝐹)‘(𝑁 − 2)) ∈ {-1, 0,
1}) | 
| 109 | 2, 107, 108 | syl2anc 584 | . . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘𝐹)‘(𝑁 − 2)) ∈ {-1, 0,
1}) | 
| 110 | 17, 18 | signswrid 34574 | . . . 4
⊢ (((𝑇‘𝐹)‘(𝑁 − 2)) ∈ {-1, 0, 1} →
(((𝑇‘𝐹)‘(𝑁 − 2)) ⨣ 0) = ((𝑇‘𝐹)‘(𝑁 − 2))) | 
| 111 | 109, 110 | syl 17 | . . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (((𝑇‘𝐹)‘(𝑁 − 2)) ⨣ 0) = ((𝑇‘𝐹)‘(𝑁 − 2))) | 
| 112 | 96, 111 | eqtrd 2776 | . 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → (((𝑇‘(𝐹 prefix (𝑁 − 1)))‘((♯‘(𝐹 prefix (𝑁 − 1))) − 1)) ⨣ (sgn‘(𝐹‘(𝑁 − 1)))) = ((𝑇‘𝐹)‘(𝑁 − 2))) | 
| 113 | 51, 70, 112 | 3eqtr3d 2784 | 1
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ (𝐹‘(𝑁 − 1)) = 0) → ((𝑇‘𝐹)‘(𝑁 − 1)) = ((𝑇‘𝐹)‘(𝑁 − 2))) |