signsvtn0 - Mathbox for Thierry Arnoux

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

Theorem signsvtn0 34585

Description: If the last letter is nonzero, then this is the zero-skipping sign. (Contributed by Thierry Arnoux, 8-Oct-2018.) (Proof shortened by AV, 3-Nov-2022.)

**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**
Step	Hyp	Ref	Expression
1		eldifsn 4786	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Word ℝ ∖ {∅}) ↔ (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅))
2	1	biimpi 216	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Word ℝ ∖ {∅}) → (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅))
3	2	adantr 480	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅))
4	3	simpld 494	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 ∈ Word ℝ)
5	4	adantr 480	. . . . . . . 8 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹 ∈ Word ℝ)
6		wrdf 14557	. . . . . . . 8 ⊢ (𝐹 ∈ Word ℝ → 𝐹:(0..^(♯‘𝐹))⟶ℝ)
7	5, 6	syl 17	. . . . . . 7 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹:(0..^(♯‘𝐹))⟶ℝ)
8		lennncl 14572	. . . . . . . . . 10 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ∈ ℕ)
9	3, 8	syl 17	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (♯‘𝐹) ∈ ℕ)
10	9	adantr 480	. . . . . . . 8 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (♯‘𝐹) ∈ ℕ)
11		lbfzo0 13739	. . . . . . . 8 ⊢ (0 ∈ (0..^(♯‘𝐹)) ↔ (♯‘𝐹) ∈ ℕ)
12	10, 11	sylibr 234	. . . . . . 7 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 0 ∈ (0..^(♯‘𝐹)))
13	7, 12	ffvelcdmd 7105	. . . . . 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 34583	. . . . . 6 ⊢ ((𝐹‘0) ∈ ℝ → (𝑇‘⟨“(𝐹‘0)”⟩) = ⟨“(sgn‘(𝐹‘0))”⟩)
19	13, 18	syl 17	. . . . 5 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘⟨“(𝐹‘0)”⟩) = ⟨“(sgn‘(𝐹‘0))”⟩)
20		signsvtn0.1	. . . . . . . 8 ⊢ 𝑁 = (♯‘𝐹)
21		simpr 484	. . . . . . . 8 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝑁 = 1)
22	20, 21	eqtr3id 2791	. . . . . . 7 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (♯‘𝐹) = 1)
23		eqs1 14650	. . . . . . 7 ⊢ ((𝐹 ∈ Word ℝ ∧ (♯‘𝐹) = 1) → 𝐹 = ⟨“(𝐹‘0)”⟩)
24	5, 22, 23	syl2anc 584	. . . . . 6 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹 = ⟨“(𝐹‘0)”⟩)
25	24	fveq2d 6910	. . . . 5 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘𝐹) = (𝑇‘⟨“(𝐹‘0)”⟩))
26		oveq1 7438	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
27		1m1e0 12338	. . . . . . . . . 10 ⊢ (1 − 1) = 0
28	26, 27	eqtrdi 2793	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
29	28	fveq2d 6910	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝐹‘(𝑁 − 1)) = (𝐹‘0))
30	29	fveq2d 6910	. . . . . . 7 ⊢ (𝑁 = 1 → (sgn‘(𝐹‘(𝑁 − 1))) = (sgn‘(𝐹‘0)))
31	30	s1eqd 14639	. . . . . 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 2787	. . . 4 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘𝐹) = ⟨“(sgn‘(𝐹‘(𝑁 − 1)))”⟩)
34	21, 28	syl 17	. . . 4 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑁 − 1) = 0)
35	33, 34	fveq12d 6913	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (⟨“(sgn‘(𝐹‘(𝑁 − 1)))”⟩‘0))
36	4, 6	syl 17	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹:(0..^(♯‘𝐹))⟶ℝ)
37	20	oveq1i 7441	. . . . . . . . 9 ⊢ (𝑁 − 1) = ((♯‘𝐹) − 1)
38		fzo0end 13797	. . . . . . . . . 10 ⊢ ((♯‘𝐹) ∈ ℕ → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
39	3, 8, 38	3syl 18	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
40	37, 39	eqeltrid 2845	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) ∈ (0..^(♯‘𝐹)))
41	36, 40	ffvelcdmd 7105	. . . . . . 7 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ∈ ℝ)
42	41	rexrd 11311	. . . . . 6 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ∈ ℝ^*)
43		sgncl 34541	. . . . . 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 14648	. . . 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 2777	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))
49		fzossfz 13718	. . . . . . . . . 10 ⊢ (0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))
50	49, 39	sselid 3981	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((♯‘𝐹) − 1) ∈ (0...(♯‘𝐹)))
51		pfxres 14717	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word ℝ ∧ ((♯‘𝐹) − 1) ∈ (0...(♯‘𝐹))) → (𝐹 prefix ((♯‘𝐹) − 1)) = (𝐹 ↾ (0..^((♯‘𝐹) − 1))))
52	4, 50, 51	syl2anc 584	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 prefix ((♯‘𝐹) − 1)) = (𝐹 ↾ (0..^((♯‘𝐹) − 1))))
53	52	oveq1d 7446	. . . . . . 7 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝐹 prefix ((♯‘𝐹) − 1)) ++ ⟨“(lastS‘𝐹)”⟩) = ((𝐹 ↾ (0..^((♯‘𝐹) − 1))) ++ ⟨“(lastS‘𝐹)”⟩))
54		pfxlswccat 14751	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → ((𝐹 prefix ((♯‘𝐹) − 1)) ++ ⟨“(lastS‘𝐹)”⟩) = 𝐹)
55	54	eqcomd 2743	. . . . . . . 8 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → 𝐹 = ((𝐹 prefix ((♯‘𝐹) − 1)) ++ ⟨“(lastS‘𝐹)”⟩))
56	3, 55	syl 17	. . . . . . 7 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 = ((𝐹 prefix ((♯‘𝐹) − 1)) ++ ⟨“(lastS‘𝐹)”⟩))
57	37	oveq2i 7442	. . . . . . . . . 10 ⊢ (0..^(𝑁 − 1)) = (0..^((♯‘𝐹) − 1))
58	57	a1i 11	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^(𝑁 − 1)) = (0..^((♯‘𝐹) − 1)))
59	58	reseq2d 5997	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) = (𝐹 ↾ (0..^((♯‘𝐹) − 1))))
60	37	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) = ((♯‘𝐹) − 1))
61	60	fveq2d 6910	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) = (𝐹‘((♯‘𝐹) − 1)))
62		lsw 14602	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Word ℝ ∖ {∅}) → (lastS‘𝐹) = (𝐹‘((♯‘𝐹) − 1)))
63	62	adantr 480	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (lastS‘𝐹) = (𝐹‘((♯‘𝐹) − 1)))
64	61, 63	eqtr4d 2780	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) = (lastS‘𝐹))
65	64	s1eqd 14639	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ⟨“(𝐹‘(𝑁 − 1))”⟩ = ⟨“(lastS‘𝐹)”⟩)
66	59, 65	oveq12d 7449	. . . . . . 7 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩) = ((𝐹 ↾ (0..^((♯‘𝐹) − 1))) ++ ⟨“(lastS‘𝐹)”⟩))
67	53, 56, 66	3eqtr4d 2787	. . . . . 6 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 = ((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩))
68	67	fveq2d 6910	. . . . 5 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑇‘𝐹) = (𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩)))
69		ffn 6736	. . . . . . . . . . 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 7447	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^𝑁) = (0..^(♯‘𝐹)))
73	72	fneq2d 6662	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 Fn (0..^𝑁) ↔ 𝐹 Fn (0..^(♯‘𝐹))))
74	70, 73	mpbird 257	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 Fn (0..^𝑁))
75	20, 9	eqeltrid 2845	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 ∈ ℕ)
76	75	nnnn0d 12587	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 ∈ ℕ₀)
77		nn0z 12638	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
78		fzossrbm1 13728	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℤ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
79	76, 77, 78	3syl 18	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
80		fnssres 6691	. . . . . . . . 9 ⊢ ((𝐹 Fn (0..^𝑁) ∧ (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) → (𝐹 ↾ (0..^(𝑁 − 1))) Fn (0..^(𝑁 − 1)))
81	74, 79, 80	syl2anc 584	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) Fn (0..^(𝑁 − 1)))
82		hashfn 14414	. . . . . . . 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 12567	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
85		hashfzo0 14469	. . . . . . . 8 ⊢ ((𝑁 − 1) ∈ ℕ₀ → (♯‘(0..^(𝑁 − 1))) = (𝑁 − 1))
86	75, 84, 85	3syl 18	. . . . . . 7 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (♯‘(0..^(𝑁 − 1))) = (𝑁 − 1))
87	83, 86	eqtrd 2777	. . . . . 6 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (𝑁 − 1))
88	87	eqcomd 2743	. . . . 5 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) = (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))))
89	68, 88	fveq12d 6913	. . . 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 2780	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 prefix ((♯‘𝐹) − 1)) = (𝐹 ↾ (0..^(𝑁 − 1))))
92		pfxcl 14715	. . . . . . . . 9 ⊢ (𝐹 ∈ Word ℝ → (𝐹 prefix ((♯‘𝐹) − 1)) ∈ Word ℝ)
93	4, 92	syl 17	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 prefix ((♯‘𝐹) − 1)) ∈ Word ℝ)
94	91, 93	eqeltrrd 2842	. . . . . . 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 12282	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ∈ ℂ)
99		1cnd 11256	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 1 ∈ ℂ)
100		simpr 484	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ≠ 1)
101	98, 99, 100	subne0d 11629	. . . . . . . 8 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝑁 − 1) ≠ 0)
102	96, 101	eqnetrd 3008	. . . . . . 7 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) ≠ 0)
103		fveq2 6906	. . . . . . . . 9 ⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) = ∅ → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (♯‘∅))
104		hash0 14406	. . . . . . . . 9 ⊢ (♯‘∅) = 0
105	103, 104	eqtrdi 2793	. . . . . . . 8 ⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) = ∅ → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) = 0)
106	105	necon3i 2973	. . . . . . 7 ⊢ ((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) ≠ 0 → (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅)
107	102, 106	syl 17	. . . . . 6 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅)
108	95, 107	jca 511	. . . . 5 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧ (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅))
109		eldifsn 4786	. . . . 5 ⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖ {∅}) ↔ ((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧ (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅))
110	108, 109	sylibr 234	. . . 4 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖ {∅}))
111	41	adantr 480	. . . 4 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝐹‘(𝑁 − 1)) ∈ ℝ)
112	14, 15, 16, 17	signstfvn 34584	. . . 4 ⊢ (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ∈ ℝ) → ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩))‘(♯‘(𝐹 ↾ (0..^(𝑁 − 1))))) = (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ⨣ (sgn‘(𝐹‘(𝑁 − 1)))))
113	110, 111, 112	syl2anc 584	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩))‘(♯‘(𝐹 ↾ (0..^(𝑁 − 1))))) = (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ⨣ (sgn‘(𝐹‘(𝑁 − 1)))))
114		lennncl 14572	. . . . . 6 ⊢ (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧ (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅) → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) ∈ ℕ)
115		fzo0end 13797	. . . . . 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 34580	. . . . 5 ⊢ (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧ ((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1) ∈ (0..^(♯‘(𝐹 ↾ (0..^(𝑁 − 1)))))) → ((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ∈ {-1, 0, 1})
118	95, 116, 117	syl2anc 584	. . . 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 484	. . . . . 6 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ≠ 0)
121		sgn0bi 34550	. . . . . . . 8 ⊢ ((𝐹‘(𝑁 − 1)) ∈ ℝ^* → ((sgn‘(𝐹‘(𝑁 − 1))) = 0 ↔ (𝐹‘(𝑁 − 1)) = 0))
122	121	necon3bid 2985	. . . . . . 7 ⊢ ((𝐹‘(𝑁 − 1)) ∈ ℝ^* → ((sgn‘(𝐹‘(𝑁 − 1))) ≠ 0 ↔ (𝐹‘(𝑁 − 1)) ≠ 0))
123	122	biimpar 477	. . . . . 6 ⊢ (((𝐹‘(𝑁 − 1)) ∈ ℝ^* ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (sgn‘(𝐹‘(𝑁 − 1))) ≠ 0)
124	42, 120, 123	syl2anc 584	. . . . 5 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (sgn‘(𝐹‘(𝑁 − 1))) ≠ 0)
125	124	adantr 480	. . . 4 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (sgn‘(𝐹‘(𝑁 − 1))) ≠ 0)
126	14, 15	signswlid 34574	. . . 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 838	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (((𝑇‘(𝐹 ↾ (0..^(𝑁 − 1))))‘((♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) − 1)) ⨣ (sgn‘(𝐹‘(𝑁 − 1)))) = (sgn‘(𝐹‘(𝑁 − 1))))
128	90, 113, 127	3eqtrd 2781	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))
129	48, 128	pm2.61dane 3029	1 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∖ cdif 3948 ⊆ wss 3951 ∅c0 4333 ifcif 4525 {csn 4626 {cpr 4628 {ctp 4630 ⟨cop 4632 ↦ cmpt 5225 ↾ cres 5687 Fn wfn 6556 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ∈ cmpo 7433 ℝcr 11154 0cc0 11155 1c1 11156 ℝ^*cxr 11294 − cmin 11492 -cneg 11493 ℕcn 12266 ℕ₀cn0 12526 ℤcz 12613 ...cfz 13547 ..^cfzo 13694 ♯chash 14369 Word cword 14552 lastSclsw 14600 ++ cconcat 14608 ⟨“cs1 14633 prefix cpfx 14708 sgncsgn 15125 Σcsu 15722 ndxcnx 17230 Basecbs 17247 +_gcplusg 17297 Σ_g cgsu 17485

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-oi 9550 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-2 12329 df-n0 12527 df-xnn0 12600 df-z 12614 df-uz 12879 df-fz 13548 df-fzo 13695 df-seq 14043 df-hash 14370 df-word 14553 df-lsw 14601 df-concat 14609 df-s1 14634 df-substr 14679 df-pfx 14709 df-sgn 15126 df-struct 17184 df-slot 17219 df-ndx 17231 df-base 17248 df-plusg 17310 df-0g 17486 df-gsum 17487 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-mulg 19086 df-cntz 19335

This theorem is referenced by: signsvfpn 34600 signsvfnn 34601

W3C validator