signstfvneq0 - Mathbox for Thierry Arnoux

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

Theorem signstfvneq0 30982

Description: In case the first letter is not zero, the zero skipping sign is never zero. (Contributed by Thierry Arnoux, 10-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))

**Assertion**
Ref	Expression
signstfvneq0	⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)

Distinct variable groups: 𝑎,𝑏, ⨣ 𝑓,𝑖,𝑛,𝐹 𝑓,𝑊,𝑖,𝑛 𝑖,𝑁,𝑛 𝑛,𝑎,𝑇,𝑏 Allowed substitution hints: ⨣ (𝑓,𝑖,𝑗,𝑛) 𝑇(𝑓,𝑖,𝑗) 𝐹(𝑗,𝑎,𝑏) 𝑁(𝑓,𝑗,𝑎,𝑏) 𝑉(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏) 𝑊(𝑗,𝑎,𝑏)

Proof of Theorem signstfvneq0 Dummy variables 𝑒 𝑘 𝑚 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 750	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ (Word ℝ ∖ {∅}))
2	1	eldifad 3735	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ Word ℝ)
3		eldifsni 4457	. . . 4 ⊢ (𝐹 ∈ (Word ℝ ∖ {∅}) → 𝐹 ≠ ∅)
4	3	ad2antrr 705	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ≠ ∅)
5		simplr 752	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹‘0) ≠ 0)
6	4, 5	jca 501	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0))
7		simpr 471	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^(♯‘𝐹)))
8		simprr 756	. . 3 ⊢ ((𝐹 ∈ Word ℝ ∧ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → 𝑁 ∈ (0..^(♯‘𝐹)))
9		neeq1 3005	. . . . . . . 8 ⊢ (𝑔 = ∅ → (𝑔 ≠ ∅ ↔ ∅ ≠ ∅))
10		fveq1 6329	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (𝑔‘0) = (∅‘0))
11	10	neeq1d 3002	. . . . . . . 8 ⊢ (𝑔 = ∅ → ((𝑔‘0) ≠ 0 ↔ (∅‘0) ≠ 0))
12	9, 11	anbi12d 616	. . . . . . 7 ⊢ (𝑔 = ∅ → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (∅ ≠ ∅ ∧ (∅‘0) ≠ 0)))
13		fveq2 6330	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (♯‘𝑔) = (♯‘∅))
14	13	oveq2d 6807	. . . . . . . 8 ⊢ (𝑔 = ∅ → (0..^(♯‘𝑔)) = (0..^(♯‘∅)))
15		fveq2 6330	. . . . . . . . . 10 ⊢ (𝑔 = ∅ → (𝑇‘𝑔) = (𝑇‘∅))
16	15	fveq1d 6332	. . . . . . . . 9 ⊢ (𝑔 = ∅ → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘∅)‘𝑚))
17	16	neeq1d 3002	. . . . . . . 8 ⊢ (𝑔 = ∅ → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘∅)‘𝑚) ≠ 0))
18	14, 17	raleqbidv 3301	. . . . . . 7 ⊢ (𝑔 = ∅ → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0))
19	12, 18	imbi12d 333	. . . . . 6 ⊢ (𝑔 = ∅ → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((∅ ≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)))
20		neeq1 3005	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (𝑔 ≠ ∅ ↔ 𝑒 ≠ ∅))
21		fveq1 6329	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (𝑔‘0) = (𝑒‘0))
22	21	neeq1d 3002	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → ((𝑔‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0))
23	20, 22	anbi12d 616	. . . . . . 7 ⊢ (𝑔 = 𝑒 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0)))
24		fveq2 6330	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (♯‘𝑔) = (♯‘𝑒))
25	24	oveq2d 6807	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (0..^(♯‘𝑔)) = (0..^(♯‘𝑒)))
26		fveq2 6330	. . . . . . . . . 10 ⊢ (𝑔 = 𝑒 → (𝑇‘𝑔) = (𝑇‘𝑒))
27	26	fveq1d 6332	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝑒)‘𝑚))
28	27	neeq1d 3002	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0))
29	25, 28	raleqbidv 3301	. . . . . . 7 ⊢ (𝑔 = 𝑒 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))
30	23, 29	imbi12d 333	. . . . . 6 ⊢ (𝑔 = 𝑒 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)))
31		neeq1 3005	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑔 ≠ ∅ ↔ (𝑒 ++ ⟨“𝑘”⟩) ≠ ∅))
32		fveq1 6329	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑔‘0) = ((𝑒 ++ ⟨“𝑘”⟩)‘0))
33	32	neeq1d 3002	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑔‘0) ≠ 0 ↔ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
34	31, 33	anbi12d 616	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)))
35		fveq2 6330	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (♯‘𝑔) = (♯‘(𝑒 ++ ⟨“𝑘”⟩)))
36	35	oveq2d 6807	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (0..^(♯‘𝑔)) = (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))
37		fveq2 6330	. . . . . . . . . 10 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑇‘𝑔) = (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)))
38	37	fveq1d 6332	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚))
39	38	neeq1d 3002	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0))
40	36, 39	raleqbidv 3301	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0))
41	34, 40	imbi12d 333	. . . . . 6 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)))
42		neeq1 3005	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (𝑔 ≠ ∅ ↔ 𝐹 ≠ ∅))
43		fveq1 6329	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → (𝑔‘0) = (𝐹‘0))
44	43	neeq1d 3002	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → ((𝑔‘0) ≠ 0 ↔ (𝐹‘0) ≠ 0))
45	42, 44	anbi12d 616	. . . . . . 7 ⊢ (𝑔 = 𝐹 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)))
46		fveq2 6330	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → (♯‘𝑔) = (♯‘𝐹))
47	46	oveq2d 6807	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (0..^(♯‘𝑔)) = (0..^(♯‘𝐹)))
48		fveq2 6330	. . . . . . . . . 10 ⊢ (𝑔 = 𝐹 → (𝑇‘𝑔) = (𝑇‘𝐹))
49	48	fveq1d 6332	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝐹)‘𝑚))
50	49	neeq1d 3002	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑚) ≠ 0))
51	47, 50	raleqbidv 3301	. . . . . . 7 ⊢ (𝑔 = 𝐹 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))
52	45, 51	imbi12d 333	. . . . . 6 ⊢ (𝑔 = 𝐹 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)))
53		neirr 2952	. . . . . . . 8 ⊢ ¬ ∅ ≠ ∅
54	53	intnanr 475	. . . . . . 7 ⊢ ¬ (∅ ≠ ∅ ∧ (∅‘0) ≠ 0)
55	54	pm2.21i 117	. . . . . 6 ⊢ ((∅ ≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)
56		fveq2 6330	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑚 → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘𝑚))
57	56	neeq1d 3002	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0))
58	57	cbvralv 3320	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)
59	58	imbi2i 325	. . . . . . . . 9 ⊢ (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))
60	59	anbi2i 609	. . . . . . . 8 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ↔ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)))
61		simplr 752	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → 𝑚 ∈ (0..^(♯‘𝑒)))
62		noel 4067	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑚 ∈ ∅
63		fveq2 6330	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ∅ → (♯‘𝑒) = (♯‘∅))
64		hash0 13353	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘∅) = 0
65	63, 64	syl6eq 2821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = ∅ → (♯‘𝑒) = 0)
66	65	oveq2d 6807	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = ∅ → (0..^(♯‘𝑒)) = (0..^0))
67		fzo0 12693	. . . . . . . . . . . . . . . 16 ⊢ (0..^0) = ∅
68	66, 67	syl6eq 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ∅ → (0..^(♯‘𝑒)) = ∅)
69	68	eleq2d 2836	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ∅ → (𝑚 ∈ (0..^(♯‘𝑒)) ↔ 𝑚 ∈ ∅))
70	62, 69	mtbiri 316	. . . . . . . . . . . . 13 ⊢ (𝑒 = ∅ → ¬ 𝑚 ∈ (0..^(♯‘𝑒)))
71	70	adantl 467	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → ¬ 𝑚 ∈ (0..^(♯‘𝑒)))
72	61, 71	pm2.21dd 186	. . . . . . . . . . 11 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
73		simp-6l 776	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ)
74		simp-6r 778	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ)
75		simplr 752	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑚 ∈ (0..^(♯‘𝑒)))
76		signsv.p	. . . . . . . . . . . . . 14 ⊢ ⨣ = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
77		signsv.w	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+_g‘ndx), ⨣ ⟩}
78		signsv.t	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σ_g (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖))))))
79		signsv.v	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0))
80	76, 77, 78, 79	signstfvp 30981	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘𝑒)‘𝑚))
81	73, 74, 75, 80	syl3anc 1476	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘𝑒)‘𝑚))
82		simpr 471	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ≠ ∅)
83		simplll 758	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
84	83	ad2antrr 705	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
85		simplrr 763	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ (𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) ∧ 𝑚 ∈ (0..^(♯‘𝑒)) ∧ 𝑒 ≠ ∅)) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
86	85	3anassrs 1453	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
87		simpll 750	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ)
88		simplr 752	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ)
89	88	s1cld 13576	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ⟨“𝑘”⟩ ∈ Word ℝ)
90		lennncl 13514	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
91	90	adantlr 694	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
92		fzo0end 12761	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑒) ∈ ℕ → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
93		elfzolt3b 12683	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)) → 0 ∈ (0..^(♯‘𝑒)))
94	91, 92, 93	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 0 ∈ (0..^(♯‘𝑒)))
95		ccatval1 13552	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ ⟨“𝑘”⟩ ∈ Word ℝ ∧ 0 ∈ (0..^(♯‘𝑒))) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (𝑒‘0))
96	87, 89, 94, 95	syl3anc 1476	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (𝑒‘0))
97	96	neeq1d 3002	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0))
98	97	biimpa 462	. . . . . . . . . . . . . . 15 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑒‘0) ≠ 0)
99	84, 82, 86, 98	syl21anc 1475	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒‘0) ≠ 0)
100		simp-5r 774	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0))
101	82, 99, 100	mp2and 679	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)
102	57	rspcva 3458	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ (0..^(♯‘𝑒)) ∧ ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) → ((𝑇‘𝑒)‘𝑚) ≠ 0)
103	75, 101, 102	syl2anc 573	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘𝑚) ≠ 0)
104	81, 103	eqnetrd 3010	. . . . . . . . . . 11 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
105	72, 104	pm2.61dane 3030	. . . . . . . . . 10 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
106		simpr 471	. . . . . . . . . . . 12 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → 𝑚 = (♯‘𝑒))
107	106	fveq2d 6334	. . . . . . . . . . 11 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)))
108		simpr 471	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → 𝑒 = ∅)
109		simp-4r 770	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → 𝑘 ∈ ℝ)
110		simplrl 762	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
111	110	simprd 483	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
112		oveq1 6798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = ∅ → (𝑒 ++ ⟨“𝑘”⟩) = (∅ ++ ⟨“𝑘”⟩))
113		s1cl 13575	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ ℝ → ⟨“𝑘”⟩ ∈ Word ℝ)
114		ccatlid 13561	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨“𝑘”⟩ ∈ Word ℝ → (∅ ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
115	113, 114	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℝ → (∅ ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
116	112, 115	sylan9eq 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑒 ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
117	116	fveq2d 6334	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = (𝑇‘⟨“𝑘”⟩))
118	117	adantr 466	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = (𝑇‘⟨“𝑘”⟩))
119		simplr 752	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → 𝑘 ∈ ℝ)
120	76, 77, 78, 79	signstf0 30978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ → (𝑇‘⟨“𝑘”⟩) = ⟨“(sgn‘𝑘)”⟩)
121	119, 120	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘⟨“𝑘”⟩) = ⟨“(sgn‘𝑘)”⟩)
122	118, 121	eqtrd 2805	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = ⟨“(sgn‘𝑘)”⟩)
123	65	ad2antrr 705	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (♯‘𝑒) = 0)
124	122, 123	fveq12d 6336	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (⟨“(sgn‘𝑘)”⟩‘0))
125		sgnclre 30934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ → (sgn‘𝑘) ∈ ℝ)
126		s1fv 13583	. . . . . . . . . . . . . . . . . 18 ⊢ ((sgn‘𝑘) ∈ ℝ → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
127	119, 125, 126	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
128	124, 127	eqtrd 2805	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (sgn‘𝑘))
129	116	fveq1d 6332	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (⟨“𝑘”⟩‘0))
130		s1fv 13583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℝ → (⟨“𝑘”⟩‘0) = 𝑘)
131	130	adantl 467	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (⟨“𝑘”⟩‘0) = 𝑘)
132	129, 131	eqtrd 2805	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = 𝑘)
133	132	neeq1d 3002	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0 ↔ 𝑘 ≠ 0))
134	133	biimpa 462	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → 𝑘 ≠ 0)
135		rexr 10285	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ → 𝑘 ∈ ℝ^*)
136		sgn0bi 30942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ^* → ((sgn‘𝑘) = 0 ↔ 𝑘 = 0))
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → ((sgn‘𝑘) = 0 ↔ 𝑘 = 0))
138	137	necon3bid 2987	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ → ((sgn‘𝑘) ≠ 0 ↔ 𝑘 ≠ 0))
139	138	biimpar 463	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℝ ∧ 𝑘 ≠ 0) → (sgn‘𝑘) ≠ 0)
140	119, 134, 139	syl2anc 573	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (sgn‘𝑘) ≠ 0)
141	128, 140	eqnetrd 3010	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
142	108, 109, 111, 141	syl21anc 1475	. . . . . . . . . . . . . 14 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
143		simplll 758	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ∈ Word ℝ)
144		simpr 471	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ¬ 𝑒 = ∅)
145		velsn 4332	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 ∈ {∅} ↔ 𝑒 = ∅)
146	144, 145	sylnibr 318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ¬ 𝑒 ∈ {∅})
147	143, 146	eldifd 3734	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ∈ (Word ℝ ∖ {∅}))
148		simpllr 760	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑘 ∈ ℝ)
149	76, 77, 78, 79	signstfvn 30979	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ (Word ℝ ∖ {∅}) ∧ 𝑘 ∈ ℝ) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
150	147, 148, 149	syl2anc 573	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
151	150	adantllr 698	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
152	144	neqned 2950	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ≠ ∅)
153	143, 152, 90	syl2anc 573	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (♯‘𝑒) ∈ ℕ)
154	153, 92	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
155	76, 77, 78, 79	signstcl 30975	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒))) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
156	143, 154, 155	syl2anc 573	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
157	156	adantllr 698	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
158	148	rexrd 10289	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑘 ∈ ℝ^*)
159		sgncl 30933	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ^* → (sgn‘𝑘) ∈ {-1, 0, 1})
160	158, 159	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (sgn‘𝑘) ∈ {-1, 0, 1})
161	160	adantllr 698	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (sgn‘𝑘) ∈ {-1, 0, 1})
162	154	adantllr 698	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
163	152	adantllr 698	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ≠ ∅)
164		simplll 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
165		simplrl 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
166	165	simprd 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
167	164, 163, 166, 98	syl21anc 1475	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (𝑒‘0) ≠ 0)
168		simpllr 760	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0))
169	163, 167, 168	mp2and 679	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)
170		fveq2 6330	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = ((♯‘𝑒) − 1) → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘((♯‘𝑒) − 1)))
171	170	neeq1d 3002	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = ((♯‘𝑒) − 1) → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0))
172	171	rspcva 3458	. . . . . . . . . . . . . . . . 17 ⊢ ((((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)) ∧ ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0)
173	162, 169, 172	syl2anc 573	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0)
174	76, 77	signswn0 30970	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1} ∧ (sgn‘𝑘) ∈ {-1, 0, 1}) ∧ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0)
175	157, 161, 173, 174	syl21anc 1475	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0)
176	151, 175	eqnetrd 3010	. . . . . . . . . . . . . 14 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
177	142, 176	pm2.61dan 814	. . . . . . . . . . . . 13 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
178	177	anassrs 453	. . . . . . . . . . . 12 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
179	178	adantr 466	. . . . . . . . . . 11 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
180	107, 179	eqnetrd 3010	. . . . . . . . . 10 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
181		lencl 13513	. . . . . . . . . . . . 13 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ ℕ₀)
182		nn0uz 11922	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
183	181, 182	syl6eleq 2860	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ (ℤ_≥‘0))
184	183	ad4antr 712	. . . . . . . . . . 11 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (♯‘𝑒) ∈ (ℤ_≥‘0))
185		simpr 471	. . . . . . . . . . . 12 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))
186		ccatws1len 13593	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ Word ℝ → (♯‘(𝑒 ++ ⟨“𝑘”⟩)) = ((♯‘𝑒) + 1))
187	186	adantr 466	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (♯‘(𝑒 ++ ⟨“𝑘”⟩)) = ((♯‘𝑒) + 1))
188	187	oveq2d 6807	. . . . . . . . . . . . . 14 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) = (0..^((♯‘𝑒) + 1)))
189	188	eleq2d 2836	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) ↔ 𝑚 ∈ (0..^((♯‘𝑒) + 1))))
190	189	biimpa 462	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1)))
191	83, 185, 190	syl2anc 573	. . . . . . . . . . 11 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1)))
192		fzosplitsni 12780	. . . . . . . . . . . 12 ⊢ ((♯‘𝑒) ∈ (ℤ_≥‘0) → (𝑚 ∈ (0..^((♯‘𝑒) + 1)) ↔ (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒))))
193	192	biimpa 462	. . . . . . . . . . 11 ⊢ (((♯‘𝑒) ∈ (ℤ_≥‘0) ∧ 𝑚 ∈ (0..^((♯‘𝑒) + 1))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒)))
194	184, 191, 193	syl2anc 573	. . . . . . . . . 10 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒)))
195	105, 180, 194	mpjaodan 943	. . . . . . . . 9 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
196	195	ralrimiva 3115	. . . . . . . 8 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
197	60, 196	sylanbr 571	. . . . . . 7 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
198	197	exp31 406	. . . . . 6 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0) → (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)))
199	19, 30, 41, 52, 55, 198	wrdind 13678	. . . . 5 ⊢ (𝐹 ∈ Word ℝ → ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))
200	199	imp 393	. . . 4 ⊢ ((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)
201	200	adantrr 696	. . 3 ⊢ ((𝐹 ∈ Word ℝ ∧ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)
202		fveq2 6330	. . . . 5 ⊢ (𝑚 = 𝑁 → ((𝑇‘𝐹)‘𝑚) = ((𝑇‘𝐹)‘𝑁))
203	202	neeq1d 3002	. . . 4 ⊢ (𝑚 = 𝑁 → (((𝑇‘𝐹)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑁) ≠ 0))
204	203	rspcva 3458	. . 3 ⊢ ((𝑁 ∈ (0..^(♯‘𝐹)) ∧ ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0) → ((𝑇‘𝐹)‘𝑁) ≠ 0)
205	8, 201, 204	syl2anc 573	. 2 ⊢ ((𝐹 ∈ Word ℝ ∧ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)
206	2, 6, 7, 205	syl12anc 1474	1 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 382 ∨ wo 836 ∧ w3a 1071 = wceq 1631 ∈ wcel 2145 ≠ wne 2943 ∀wral 3061 ∖ cdif 3720 ∅c0 4063 ifcif 4225 {csn 4316 {cpr 4318 {ctp 4320 ⟨cop 4322 ↦ cmpt 4863 ‘cfv 6029 (class class class)co 6791 ↦ cmpt2 6793 ℝcr 10135 0cc0 10136 1c1 10137 + caddc 10139 ℝ^*cxr 10273 − cmin 10466 -cneg 10467 ℕcn 11220 ℕ₀cn0 11492 ℤ_≥cuz 11886 ...cfz 12526 ..^cfzo 12666 ♯chash 13314 Word cword 13480 ++ cconcat 13482 ⟨“cs1 13483 sgncsgn 14027 Σcsu 14617 ndxcnx 16054 Basecbs 16057 +_gcplusg 16142 Σ_g cgsu 16302

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4904 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7094 ax-inf2 8700 ax-cnex 10192 ax-resscn 10193 ax-1cn 10194 ax-icn 10195 ax-addcl 10196 ax-addrcl 10197 ax-mulcl 10198 ax-mulrcl 10199 ax-mulcom 10200 ax-addass 10201 ax-mulass 10202 ax-distr 10203 ax-i2m1 10204 ax-1ne0 10205 ax-1rid 10206 ax-rnegex 10207 ax-rrecex 10208 ax-cnre 10209 ax-pre-lttri 10210 ax-pre-lttrn 10211 ax-pre-ltadd 10212 ax-pre-mulgt0 10213

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-int 4612 df-iun 4656 df-br 4787 df-opab 4847 df-mpt 4864 df-tr 4887 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-se 5209 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5821 df-ord 5867 df-on 5868 df-lim 5869 df-suc 5870 df-iota 5992 df-fun 6031 df-fn 6032 df-f 6033 df-f1 6034 df-fo 6035 df-f1o 6036 df-fv 6037 df-isom 6038 df-riota 6752 df-ov 6794 df-oprab 6795 df-mpt2 6796 df-om 7211 df-1st 7313 df-2nd 7314 df-supp 7445 df-wrecs 7557 df-recs 7619 df-rdg 7657 df-1o 7711 df-oadd 7715 df-er 7894 df-en 8108 df-dom 8109 df-sdom 8110 df-fin 8111 df-oi 8569 df-card 8963 df-pnf 10276 df-mnf 10277 df-xr 10278 df-ltxr 10279 df-le 10280 df-sub 10468 df-neg 10469 df-nn 11221 df-2 11279 df-n0 11493 df-xnn0 11564 df-z 11578 df-uz 11887 df-fz 12527 df-fzo 12667 df-seq 13002 df-hash 13315 df-word 13488 df-lsw 13489 df-concat 13490 df-s1 13491 df-substr 13492 df-sgn 14028 df-struct 16059 df-ndx 16060 df-slot 16061 df-base 16063 df-plusg 16155 df-0g 16303 df-gsum 16304 df-mgm 17443 df-sgrp 17485 df-mnd 17496 df-mulg 17742 df-cntz 17950

This theorem is referenced by: signstfvcl 30983

W3C validator