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 34561

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 4750	. . . . . . . . . . . 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 14483	. . . . . . . 8 ⊢ (𝐹 ∈ Word ℝ → 𝐹:(0..^(♯‘𝐹))⟶ℝ)
7	5, 6	syl 17	. . . . . . 7 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹:(0..^(♯‘𝐹))⟶ℝ)
8		lennncl 14499	. . . . . . . . . 10 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ∈ ℕ)
9	3, 8	syl 17	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (♯‘𝐹) ∈ ℕ)
10	9	adantr 480	. . . . . . . 8 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (♯‘𝐹) ∈ ℕ)
11		lbfzo0 13660	. . . . . . . 8 ⊢ (0 ∈ (0..^(♯‘𝐹)) ↔ (♯‘𝐹) ∈ ℕ)
12	10, 11	sylibr 234	. . . . . . 7 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 0 ∈ (0..^(♯‘𝐹)))
13	7, 12	ffvelcdmd 7057	. . . . . 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 34559	. . . . . 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 2778	. . . . . . 7 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (♯‘𝐹) = 1)
23		eqs1 14577	. . . . . . 7 ⊢ ((𝐹 ∈ Word ℝ ∧ (♯‘𝐹) = 1) → 𝐹 = ⟨“(𝐹‘0)”⟩)
24	5, 22, 23	syl2anc 584	. . . . . 6 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → 𝐹 = ⟨“(𝐹‘0)”⟩)
25	24	fveq2d 6862	. . . . 5 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘𝐹) = (𝑇‘⟨“(𝐹‘0)”⟩))
26		oveq1 7394	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (𝑁 − 1) = (1 − 1))
27		1m1e0 12258	. . . . . . . . . 10 ⊢ (1 − 1) = 0
28	26, 27	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝑁 = 1 → (𝑁 − 1) = 0)
29	28	fveq2d 6862	. . . . . . . 8 ⊢ (𝑁 = 1 → (𝐹‘(𝑁 − 1)) = (𝐹‘0))
30	29	fveq2d 6862	. . . . . . 7 ⊢ (𝑁 = 1 → (sgn‘(𝐹‘(𝑁 − 1))) = (sgn‘(𝐹‘0)))
31	30	s1eqd 14566	. . . . . 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 2774	. . . 4 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑇‘𝐹) = ⟨“(sgn‘(𝐹‘(𝑁 − 1)))”⟩)
34	21, 28	syl 17	. . . 4 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → (𝑁 − 1) = 0)
35	33, 34	fveq12d 6865	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (⟨“(sgn‘(𝐹‘(𝑁 − 1)))”⟩‘0))
36	4, 6	syl 17	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹:(0..^(♯‘𝐹))⟶ℝ)
37	20	oveq1i 7397	. . . . . . . . 9 ⊢ (𝑁 − 1) = ((♯‘𝐹) − 1)
38		fzo0end 13719	. . . . . . . . . 10 ⊢ ((♯‘𝐹) ∈ ℕ → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
39	3, 8, 38	3syl 18	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
40	37, 39	eqeltrid 2832	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) ∈ (0..^(♯‘𝐹)))
41	36, 40	ffvelcdmd 7057	. . . . . . 7 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ∈ ℝ)
42	41	rexrd 11224	. . . . . 6 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) ∈ ℝ^*)
43		sgncl 32756	. . . . . 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 14575	. . . 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 2764	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 = 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))
49		fzossfz 13639	. . . . . . . . . 10 ⊢ (0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))
50	49, 39	sselid 3944	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((♯‘𝐹) − 1) ∈ (0...(♯‘𝐹)))
51		pfxres 14644	. . . . . . . . 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 7402	. . . . . . 7 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝐹 prefix ((♯‘𝐹) − 1)) ++ ⟨“(lastS‘𝐹)”⟩) = ((𝐹 ↾ (0..^((♯‘𝐹) − 1))) ++ ⟨“(lastS‘𝐹)”⟩))
54		pfxlswccat 14678	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → ((𝐹 prefix ((♯‘𝐹) − 1)) ++ ⟨“(lastS‘𝐹)”⟩) = 𝐹)
55	54	eqcomd 2735	. . . . . . . 8 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → 𝐹 = ((𝐹 prefix ((♯‘𝐹) − 1)) ++ ⟨“(lastS‘𝐹)”⟩))
56	3, 55	syl 17	. . . . . . 7 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 = ((𝐹 prefix ((♯‘𝐹) − 1)) ++ ⟨“(lastS‘𝐹)”⟩))
57	37	oveq2i 7398	. . . . . . . . . 10 ⊢ (0..^(𝑁 − 1)) = (0..^((♯‘𝐹) − 1))
58	57	a1i 11	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^(𝑁 − 1)) = (0..^((♯‘𝐹) − 1)))
59	58	reseq2d 5950	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 ↾ (0..^(𝑁 − 1))) = (𝐹 ↾ (0..^((♯‘𝐹) − 1))))
60	37	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) = ((♯‘𝐹) − 1))
61	60	fveq2d 6862	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) = (𝐹‘((♯‘𝐹) − 1)))
62		lsw 14529	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (Word ℝ ∖ {∅}) → (lastS‘𝐹) = (𝐹‘((♯‘𝐹) − 1)))
63	62	adantr 480	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (lastS‘𝐹) = (𝐹‘((♯‘𝐹) − 1)))
64	61, 63	eqtr4d 2767	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹‘(𝑁 − 1)) = (lastS‘𝐹))
65	64	s1eqd 14566	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ⟨“(𝐹‘(𝑁 − 1))”⟩ = ⟨“(lastS‘𝐹)”⟩)
66	59, 65	oveq12d 7405	. . . . . . 7 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩) = ((𝐹 ↾ (0..^((♯‘𝐹) − 1))) ++ ⟨“(lastS‘𝐹)”⟩))
67	53, 56, 66	3eqtr4d 2774	. . . . . 6 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 = ((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩))
68	67	fveq2d 6862	. . . . 5 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑇‘𝐹) = (𝑇‘((𝐹 ↾ (0..^(𝑁 − 1))) ++ ⟨“(𝐹‘(𝑁 − 1))”⟩)))
69		ffn 6688	. . . . . . . . . . 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 7403	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^𝑁) = (0..^(♯‘𝐹)))
73	72	fneq2d 6612	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 Fn (0..^𝑁) ↔ 𝐹 Fn (0..^(♯‘𝐹))))
74	70, 73	mpbird 257	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝐹 Fn (0..^𝑁))
75	20, 9	eqeltrid 2832	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 ∈ ℕ)
76	75	nnnn0d 12503	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → 𝑁 ∈ ℕ₀)
77		nn0z 12554	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
78		fzossrbm1 13649	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℤ → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
79	76, 77, 78	3syl 18	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁))
80		fnssres 6641	. . . . . . . . 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 14340	. . . . . . . 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 12483	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
85		hashfzo0 14395	. . . . . . . 8 ⊢ ((𝑁 − 1) ∈ ℕ₀ → (♯‘(0..^(𝑁 − 1))) = (𝑁 − 1))
86	75, 84, 85	3syl 18	. . . . . . 7 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (♯‘(0..^(𝑁 − 1))) = (𝑁 − 1))
87	83, 86	eqtrd 2764	. . . . . 6 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (𝑁 − 1))
88	87	eqcomd 2735	. . . . 5 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝑁 − 1) = (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))))
89	68, 88	fveq12d 6865	. . . 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 2767	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 prefix ((♯‘𝐹) − 1)) = (𝐹 ↾ (0..^(𝑁 − 1))))
92		pfxcl 14642	. . . . . . . . 9 ⊢ (𝐹 ∈ Word ℝ → (𝐹 prefix ((♯‘𝐹) − 1)) ∈ Word ℝ)
93	4, 92	syl 17	. . . . . . . 8 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → (𝐹 prefix ((♯‘𝐹) − 1)) ∈ Word ℝ)
94	91, 93	eqeltrrd 2829	. . . . . . 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 12202	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ∈ ℂ)
99		1cnd 11169	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 1 ∈ ℂ)
100		simpr 484	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → 𝑁 ≠ 1)
101	98, 99, 100	subne0d 11542	. . . . . . . 8 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (𝑁 − 1) ≠ 0)
102	96, 101	eqnetrd 2992	. . . . . . 7 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) ≠ 0)
103		fveq2 6858	. . . . . . . . 9 ⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) = ∅ → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) = (♯‘∅))
104		hash0 14332	. . . . . . . . 9 ⊢ (♯‘∅) = 0
105	103, 104	eqtrdi 2780	. . . . . . . 8 ⊢ ((𝐹 ↾ (0..^(𝑁 − 1))) = ∅ → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) = 0)
106	105	necon3i 2957	. . . . . . 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 4750	. . . . 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 34560	. . . 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 14499	. . . . . 6 ⊢ (((𝐹 ↾ (0..^(𝑁 − 1))) ∈ Word ℝ ∧ (𝐹 ↾ (0..^(𝑁 − 1))) ≠ ∅) → (♯‘(𝐹 ↾ (0..^(𝑁 − 1)))) ∈ ℕ)
115		fzo0end 13719	. . . . . 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 34556	. . . . 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 32765	. . . . . . . 8 ⊢ ((𝐹‘(𝑁 − 1)) ∈ ℝ^* → ((sgn‘(𝐹‘(𝑁 − 1))) = 0 ↔ (𝐹‘(𝑁 − 1)) = 0))
122	121	necon3bid 2969	. . . . . . 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 34550	. . . 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 2768	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) ∧ 𝑁 ≠ 1) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))
129	48, 128	pm2.61dane 3012	1 ⊢ ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘(𝑁 − 1)) ≠ 0) → ((𝑇‘𝐹)‘(𝑁 − 1)) = (sgn‘(𝐹‘(𝑁 − 1))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∖ cdif 3911 ⊆ wss 3914 ∅c0 4296 ifcif 4488 {csn 4589 {cpr 4591 {ctp 4593 ⟨cop 4595 ↦ cmpt 5188 ↾ cres 5640 Fn wfn 6506 ⟶wf 6507 ‘cfv 6511 (class class class)co 7387 ∈ cmpo 7389 ℝcr 11067 0cc0 11068 1c1 11069 ℝ^*cxr 11207 − cmin 11405 -cneg 11406 ℕcn 12186 ℕ₀cn0 12442 ℤcz 12529 ...cfz 13468 ..^cfzo 13615 ♯chash 14295 Word cword 14478 lastSclsw 14527 ++ cconcat 14535 ⟨“cs1 14560 prefix cpfx 14635 sgncsgn 15052 Σcsu 15652 ndxcnx 17163 Basecbs 17179 +_gcplusg 17220 Σ_g cgsu 17403

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-nn 12187 df-2 12249 df-n0 12443 df-xnn0 12516 df-z 12530 df-uz 12794 df-fz 13469 df-fzo 13616 df-seq 13967 df-hash 14296 df-word 14479 df-lsw 14528 df-concat 14536 df-s1 14561 df-substr 14606 df-pfx 14636 df-sgn 15053 df-struct 17117 df-slot 17152 df-ndx 17164 df-base 17180 df-plusg 17233 df-0g 17404 df-gsum 17405 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-mulg 19000 df-cntz 19249

This theorem is referenced by: signsvfpn 34576 signsvfnn 34577

W3C validator