Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  signsvtn0 Structured version   Visualization version   GIF version

Theorem signsvtn0 29973
Description: If the last letter is non zero, then this is the zero-skipping sign. (Contributed by Thierry Arnoux, 8-Oct-2018.)
Hypotheses
Ref Expression
signsv.p = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
signsv.w 𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}
signsv.t 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))
signsv.v 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))
signsvtn0.1 𝑁 = (#‘𝐹)
Assertion
Ref Expression
signsvtn0 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝑇𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))
Distinct variable groups:   𝑎,𝑏,   𝑓,𝑖,𝑛,𝐹   𝑓,𝑊,𝑖,𝑛   𝐹,𝑎,𝑏,𝑓,𝑖,𝑛   𝑁,𝑎   𝑓,𝑏,𝑖,𝑛,𝑁   𝑇,𝑎,𝑏
Allowed substitution hints:   (𝑓,𝑖,𝑗,𝑛)   𝑇(𝑓,𝑖,𝑗,𝑛)   𝐹(𝑗)   𝑁(𝑗)   𝑉(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏)   𝑊(𝑗,𝑎,𝑏)

Proof of Theorem signsvtn0
StepHypRef Expression
1 eldifsn 4260 . . . . . . . . . . . 12 (𝐹 ∈ (Word ℝ ∖ {∅}) ↔ (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅))
21biimpi 205 . . . . . . . . . . 11 (𝐹 ∈ (Word ℝ ∖ {∅}) → (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅))
32adantr 480 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅))
43simpld 474 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 ∈ Word ℝ)
54adantr 480 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹 ∈ Word ℝ)
6 wrdf 13165 . . . . . . . 8 (𝐹 ∈ Word ℝ → 𝐹:(0..^(#‘𝐹))⟶ℝ)
75, 6syl 17 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹:(0..^(#‘𝐹))⟶ℝ)
8 lennncl 13180 . . . . . . . . . 10 ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → (#‘𝐹) ∈ ℕ)
93, 8syl 17 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (#‘𝐹) ∈ ℕ)
109adantr 480 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (#‘𝐹) ∈ ℕ)
11 lbfzo0 12375 . . . . . . . 8 (0 ∈ (0..^(#‘𝐹)) ↔ (#‘𝐹) ∈ ℕ)
1210, 11sylibr 223 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 0 ∈ (0..^(#‘𝐹)))
137, 12ffvelrnd 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))
1814, 15, 16, 17signstf0 29971 . . . . . 6 ((𝐹‘0) ∈ ℝ → (𝑇‘⟨“(𝐹‘0)”⟩) = ⟨“(sgn‘(𝐹‘0))”⟩)
1913, 18syl 17 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘⟨“(𝐹‘0)”⟩) = ⟨“(sgn‘(𝐹‘0))”⟩)
20 signsvtn0.1 . . . . . . . 8 𝑁 = (#‘𝐹)
21 simpr 476 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝑁 = 1)
2220, 21syl5eqr 2658 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (#‘𝐹) = 1)
23 eqs1 13245 . . . . . . 7 ((𝐹 ∈ Word ℝ ∧ (#‘𝐹) = 1) → 𝐹 = ⟨“(𝐹‘0)”⟩)
245, 22, 23syl2anc 691 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹 = ⟨“(𝐹‘0)”⟩)
2524fveq2d 6107 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇𝐹) = (𝑇‘⟨“(𝐹‘0)”⟩))
26 oveq1 6556 . . . . . . . . . 10 (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
27 1m1e0 10966 . . . . . . . . . 10 (1 − 1) = 0
2826, 27syl6eq 2660 . . . . . . . . 9 (𝑁 = 1 → (𝑁 − 1) = 0)
2928fveq2d 6107 . . . . . . . 8 (𝑁 = 1 → (𝐹‘(𝑁 − 1)) = (𝐹‘0))
3029fveq2d 6107 . . . . . . 7 (𝑁 = 1 → (sgn‘(𝐹‘(𝑁 − 1))) = (sgn‘(𝐹‘0)))
3130s1eqd 13234 . . . . . 6 (𝑁 = 1 → ⟨“(sgn‘(𝐹‘(𝑁 − 1)))”⟩ = ⟨“(sgn‘(𝐹‘0))”⟩)
3221, 31syl 17 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ⟨“(sgn‘(𝐹‘(𝑁 − 1)))”⟩ = ⟨“(sgn‘(𝐹‘0))”⟩)
3319, 25, 323eqtr4d 2654 . . . 4 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇𝐹) = ⟨“(sgn‘(𝐹‘(𝑁 − 1)))”⟩)
3421, 28syl 17 . . . 4 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑁 − 1) = 0)
3533, 34fveq12d 6109 . . 3 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ((𝑇𝐹)‘(𝑁 − 1)) = (⟨“(sgn‘(𝐹‘(𝑁 − 1)))”⟩‘0))
364, 6syl 17 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹:(0..^(#‘𝐹))⟶ℝ)
3720oveq1i 6559 . . . . . . . . 9 (𝑁 − 1) = ((#‘𝐹) − 1)
38 fzo0end 12426 . . . . . . . . . 10 ((#‘𝐹) ∈ ℕ → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
393, 8, 383syl 18 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
4037, 39syl5eqel 2692 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) ∈ (0..^(#‘𝐹)))
4136, 40ffvelrnd 6268 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ∈ ℝ)
4241rexrd 9968 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ∈ ℝ*)
43 sgncl 29927 . . . . . 6 ((𝐹‘(𝑁 − 1)) ∈ ℝ* → (sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0, 1})
4442, 43syl 17 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (sgn‘(𝐹‘(𝑁 − 1))) ∈ {-1, 0, 1})
4544adantr 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))))
4745, 46syl 17 . . 3 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (⟨“(sgn‘(𝐹‘(𝑁 − 1)))”⟩‘0) = (sgn‘(𝐹‘(𝑁 − 1))))
4835, 47eqtrd 2644 . 2 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ((𝑇𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))
49 fzossfz 12357 . . . . . . . . . 10 (0..^(#‘𝐹)) ⊆ (0...(#‘𝐹))
5049, 39sseldi 3566 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((#‘𝐹) − 1) ∈ (0...(#‘𝐹)))
51 swrd0val 13273 . . . . . . . . 9 ((𝐹 ∈ Word ℝ ∧ ((#‘𝐹) − 1) ∈ (0...(#‘𝐹))) → (𝐹 substr ⟨0, ((#‘𝐹) − 1)⟩) = (𝐹 ↾ (0..^((#‘𝐹) − 1))))
524, 50, 51syl2anc 691 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 substr ⟨0, ((#‘𝐹) − 1)⟩) = (𝐹 ↾ (0..^((#‘𝐹) − 1))))
5352oveq1d 6564 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝐹 substr ⟨0, ((#‘𝐹) − 1)⟩) ++ ⟨“( lastS ‘𝐹)”⟩) = ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ++ ⟨“( lastS ‘𝐹)”⟩))
54 swrdccatwrd 13320 . . . . . . . . 9 ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → ((𝐹 substr ⟨0, ((#‘𝐹) − 1)⟩) ++ ⟨“( lastS ‘𝐹)”⟩) = 𝐹)
5554eqcomd 2616 . . . . . . . 8 ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → 𝐹 = ((𝐹 substr ⟨0, ((#‘𝐹) − 1)⟩) ++ ⟨“( lastS ‘𝐹)”⟩))
563, 55syl 17 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 = ((𝐹 substr ⟨0, ((#‘𝐹) − 1)⟩) ++ ⟨“( lastS ‘𝐹)”⟩))
5737oveq2i 6560 . . . . . . . . . 10 (0..^(𝑁 − 1)) = (0..^((#‘𝐹) − 1))
5857a1i 11 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^(𝑁 − 1)) = (0..^((#‘𝐹) − 1)))
5958reseq2d 5317 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) = (𝐹 ↾ (0..^((#‘𝐹) − 1))))
6037a1i 11 . . . . . . . . . . 11 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) = ((#‘𝐹) − 1))
6160fveq2d 6107 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) = (𝐹‘((#‘𝐹) − 1)))
62 lsw 13204 . . . . . . . . . . 11 (𝐹 ∈ (Word ℝ ∖ {∅}) → ( lastS ‘𝐹) = (𝐹‘((#‘𝐹) − 1)))
6362adantr 480 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ( lastS ‘𝐹) = (𝐹‘((#‘𝐹) − 1)))
6461, 63eqtr4d 2647 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) = ( lastS ‘𝐹))
6564s1eqd 13234 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ⟨“(𝐹‘(𝑁 − 1))”⟩ = ⟨“( lastS ‘𝐹)”⟩)
6659, 65oveq12d 6567 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩) = ((𝐹 ↾ (0..^((#‘𝐹) − 1))) ++ ⟨“( lastS ‘𝐹)”⟩))
6753, 56, 663eqtr4d 2654 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 = ((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩))
6867fveq2d 6107 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑇𝐹) = (𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩)))
69 ffn 5958 . . . . . . . . . . 11 (𝐹:(0..^(#‘𝐹))⟶ℝ → 𝐹 Fn (0..^(#‘𝐹)))
704, 6, 693syl 18 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 Fn (0..^(#‘𝐹)))
7120a1i 11 . . . . . . . . . . . 12 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 = (#‘𝐹))
7271oveq2d 6565 . . . . . . . . . . 11 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^𝑁) = (0..^(#‘𝐹)))
7372fneq2d 5896 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 Fn (0..^𝑁) ↔ 𝐹 Fn (0..^(#‘𝐹))))
7470, 73mpbird 246 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 Fn (0..^𝑁))
7520, 9syl5eqel 2692 . . . . . . . . . . 11 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 ∈ ℕ)
7675nnnn0d 11228 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 ∈ ℕ0)
77 nn0z 11277 . . . . . . . . . 10 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
78 fzossrbm1 12366 . . . . . . . . . 10 (𝑁 ∈ ℤ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
7976, 77, 783syl 18 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
80 fnssres 5918 . . . . . . . . 9 ((𝐹 Fn (0..^𝑁) ∧ (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) → (𝐹 ↾ (0..^(𝑁 − 1))) Fn (0..^(𝑁 − 1)))
8174, 79, 80syl2anc 691 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) Fn (0..^(𝑁 − 1)))
82 hashfn 13025 . . . . . . . 8 ((𝐹 ↾ (0..^(𝑁 − 1))) Fn (0..^(𝑁 − 1)) → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (#‘(0..^(𝑁 − 1))))
8381, 82syl 17 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (#‘(0..^(𝑁 − 1))))
84 nnm1nn0 11211 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
85 hashfzo0 13077 . . . . . . . 8 ((𝑁 − 1) ∈ ℕ0 → (#‘(0..^(𝑁 − 1))) = (𝑁 − 1))
8675, 84, 853syl 18 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (#‘(0..^(𝑁 − 1))) = (𝑁 − 1))
8783, 86eqtrd 2644 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (𝑁 − 1))
8887eqcomd 2616 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) = (#‘(𝐹 ↾ (0..^(𝑁 − 1)))))
8968, 88fveq12d 6109 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝑇𝐹)‘(𝑁 − 1)) = ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩))‘(#‘(𝐹 ↾ (0..^(𝑁 − 1))))))
9089adantr 480 . . 3 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇𝐹)‘(𝑁 − 1)) = ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩))‘(#‘(𝐹 ↾ (0..^(𝑁 − 1))))))
9152, 59eqtr4d 2647 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 substr ⟨0, ((#‘𝐹) − 1)⟩) = (𝐹 ↾ (0..^(𝑁 − 1))))
92 swrdcl 13271 . . . . . . . . 9 (𝐹 ∈ Word ℝ → (𝐹 substr ⟨0, ((#‘𝐹) − 1)⟩) ∈ Word ℝ)
934, 92syl 17 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 substr ⟨0, ((#‘𝐹) − 1)⟩) ∈ Word ℝ)
9491, 93eqeltrrd 2689 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ)
9594adantr 480 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ)
9687adantr 480 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (𝑁 − 1))
9775adantr 480 . . . . . . . . . 10 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ∈ ℕ)
9897nncnd 10913 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ∈ ℂ)
99 1cnd 9935 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 1 ∈ ℂ)
100 simpr 476 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ≠ 1)
10198, 99, 100subne0d 10280 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝑁 − 1) ≠ 0)
10296, 101eqnetrd 2849 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) ≠ 0)
103 fveq2 6103 . . . . . . . . 9 ((𝐹 ↾ (0..^(𝑁 − 1))) = ∅ → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (#‘∅))
104 hash0 13019 . . . . . . . . 9 (#‘∅) = 0
105103, 104syl6eq 2660 . . . . . . . 8 ((𝐹 ↾ (0..^(𝑁 − 1))) = ∅ → (#‘(𝐹 ↾ (0..^(𝑁 − 1)))) = 0)
106105necon3i 2814 . . . . . . 7 ((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) ≠ 0 → (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅)
107102, 106syl 17 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅)
10895, 107jca 553 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧ (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅))
109 eldifsn 4260 . . . . 5 ((𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖ {∅}) ↔ ((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧ (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅))
110108, 109sylibr 223 . . . 4 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖ {∅}))
11141adantr 480 . . . 4 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹‘(𝑁 − 1)) ∈ ℝ)
11214, 15, 16, 17signstfvn 29972 . . . 4 (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ∈ ℝ) → ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩))‘(#‘(𝐹 ↾ (0..^(𝑁 − 1))))) = (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) (sgn‘(𝐹‘(𝑁 − 1)))))
113110, 111, 112syl2anc 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))))))
116108, 114, 1153syl 18 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1) ∈ (0..^(#‘(𝐹 ↾ (0..^(𝑁 − 1))))))
11714, 15, 16, 17signstcl 29968 . . . . 5 (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧ ((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1) ∈ (0..^(#‘(𝐹 ↾ (0..^(𝑁 − 1)))))) → ((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ∈ {-1, 0, 1})
11895, 116, 117syl2anc 691 . . . 4 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ∈ {-1, 0, 1})
11944adantr 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))
122121necon3bid 2826 . . . . . . 7 ((𝐹‘(𝑁 − 1)) ∈ ℝ* → ((sgn‘(𝐹‘(𝑁 − 1))) ≠ 0 ↔ (𝐹‘(𝑁 − 1)) ≠ 0))
123122biimpar 501 . . . . . 6 (((𝐹‘(𝑁 − 1)) ∈ ℝ* ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (sgn‘(𝐹‘(𝑁 − 1))) ≠ 0)
12442, 120, 123syl2anc 691 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (sgn‘(𝐹‘(𝑁 − 1))) ≠ 0)
125124adantr 480 . . . 4 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (sgn‘(𝐹‘(𝑁 − 1))) ≠ 0)
12614, 15signswlid 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))))
127118, 119, 125, 126syl21anc 1317 . . 3 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((#‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) (sgn‘(𝐹‘(𝑁 − 1)))) = (sgn‘(𝐹‘(𝑁 − 1))))
12890, 113, 1273eqtrd 2648 . 2 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))
12948, 128pm2.61dane 2869 1 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝑇𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  wne 2780  cdif 3537  wss 3540  c0 3874  ifcif 4036  {csn 4125  {cpr 4127  {ctp 4129  cop 4131  cmpt 4643  cres 5040   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  cmpt2 6551  cr 9814  0cc0 9815  1c1 9816  *cxr 9952  cmin 10145  -cneg 10146  cn 10897  0cn0 11169  cz 11254  ...cfz 12197  ..^cfzo 12334  #chash 12979  Word cword 13146   lastS clsw 13147   ++ cconcat 13148  ⟨“cs1 13149   substr csubstr 13150  sgncsgn 13674  Σcsu 14264  ndxcnx 15692  Basecbs 15695  +gcplusg 15768   Σg cgsu 15924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-word 13154  df-lsw 13155  df-concat 13156  df-s1 13157  df-substr 13158  df-sgn 13675  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-plusg 15781  df-0g 15925  df-gsum 15926  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mulg 17364  df-cntz 17573
This theorem is referenced by:  signsvfpn  29988  signsvfnn  29989
  Copyright terms: Public domain W3C validator