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 31099

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 783	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ (Word ℝ ∖ {∅}))
2	1	eldifad 3744	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ Word ℝ)
3		eldifsni 4476	. . . 4 ⊢ (𝐹 ∈ (Word ℝ ∖ {∅}) → 𝐹 ≠ ∅)
4	3	ad2antrr 717	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ≠ ∅)
5		simplr 785	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹‘0) ≠ 0)
6	4, 5	jca 507	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0))
7		simpr 477	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^(♯‘𝐹)))
8		simprr 789	. . 3 ⊢ ((𝐹 ∈ Word ℝ ∧ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → 𝑁 ∈ (0..^(♯‘𝐹)))
9		neeq1 2999	. . . . . . . 8 ⊢ (𝑔 = ∅ → (𝑔 ≠ ∅ ↔ ∅ ≠ ∅))
10		fveq1 6374	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (𝑔‘0) = (∅‘0))
11	10	neeq1d 2996	. . . . . . . 8 ⊢ (𝑔 = ∅ → ((𝑔‘0) ≠ 0 ↔ (∅‘0) ≠ 0))
12	9, 11	anbi12d 624	. . . . . . 7 ⊢ (𝑔 = ∅ → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (∅ ≠ ∅ ∧ (∅‘0) ≠ 0)))
13		fveq2 6375	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (♯‘𝑔) = (♯‘∅))
14	13	oveq2d 6858	. . . . . . . 8 ⊢ (𝑔 = ∅ → (0..^(♯‘𝑔)) = (0..^(♯‘∅)))
15		fveq2 6375	. . . . . . . . . 10 ⊢ (𝑔 = ∅ → (𝑇‘𝑔) = (𝑇‘∅))
16	15	fveq1d 6377	. . . . . . . . 9 ⊢ (𝑔 = ∅ → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘∅)‘𝑚))
17	16	neeq1d 2996	. . . . . . . 8 ⊢ (𝑔 = ∅ → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘∅)‘𝑚) ≠ 0))
18	14, 17	raleqbidv 3300	. . . . . . 7 ⊢ (𝑔 = ∅ → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0))
19	12, 18	imbi12d 335	. . . . . 6 ⊢ (𝑔 = ∅ → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((∅ ≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)))
20		neeq1 2999	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (𝑔 ≠ ∅ ↔ 𝑒 ≠ ∅))
21		fveq1 6374	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (𝑔‘0) = (𝑒‘0))
22	21	neeq1d 2996	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → ((𝑔‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0))
23	20, 22	anbi12d 624	. . . . . . 7 ⊢ (𝑔 = 𝑒 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0)))
24		fveq2 6375	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (♯‘𝑔) = (♯‘𝑒))
25	24	oveq2d 6858	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (0..^(♯‘𝑔)) = (0..^(♯‘𝑒)))
26		fveq2 6375	. . . . . . . . . 10 ⊢ (𝑔 = 𝑒 → (𝑇‘𝑔) = (𝑇‘𝑒))
27	26	fveq1d 6377	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝑒)‘𝑚))
28	27	neeq1d 2996	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0))
29	25, 28	raleqbidv 3300	. . . . . . 7 ⊢ (𝑔 = 𝑒 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))
30	23, 29	imbi12d 335	. . . . . 6 ⊢ (𝑔 = 𝑒 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)))
31		neeq1 2999	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑔 ≠ ∅ ↔ (𝑒 ++ ⟨“𝑘”⟩) ≠ ∅))
32		fveq1 6374	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑔‘0) = ((𝑒 ++ ⟨“𝑘”⟩)‘0))
33	32	neeq1d 2996	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑔‘0) ≠ 0 ↔ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
34	31, 33	anbi12d 624	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)))
35		fveq2 6375	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (♯‘𝑔) = (♯‘(𝑒 ++ ⟨“𝑘”⟩)))
36	35	oveq2d 6858	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (0..^(♯‘𝑔)) = (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))
37		fveq2 6375	. . . . . . . . . 10 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑇‘𝑔) = (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)))
38	37	fveq1d 6377	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚))
39	38	neeq1d 2996	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0))
40	36, 39	raleqbidv 3300	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0))
41	34, 40	imbi12d 335	. . . . . 6 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)))
42		neeq1 2999	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (𝑔 ≠ ∅ ↔ 𝐹 ≠ ∅))
43		fveq1 6374	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → (𝑔‘0) = (𝐹‘0))
44	43	neeq1d 2996	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → ((𝑔‘0) ≠ 0 ↔ (𝐹‘0) ≠ 0))
45	42, 44	anbi12d 624	. . . . . . 7 ⊢ (𝑔 = 𝐹 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)))
46		fveq2 6375	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → (♯‘𝑔) = (♯‘𝐹))
47	46	oveq2d 6858	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (0..^(♯‘𝑔)) = (0..^(♯‘𝐹)))
48		fveq2 6375	. . . . . . . . . 10 ⊢ (𝑔 = 𝐹 → (𝑇‘𝑔) = (𝑇‘𝐹))
49	48	fveq1d 6377	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝐹)‘𝑚))
50	49	neeq1d 2996	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑚) ≠ 0))
51	47, 50	raleqbidv 3300	. . . . . . 7 ⊢ (𝑔 = 𝐹 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))
52	45, 51	imbi12d 335	. . . . . 6 ⊢ (𝑔 = 𝐹 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)))
53		neirr 2946	. . . . . . . 8 ⊢ ¬ ∅ ≠ ∅
54	53	intnanr 481	. . . . . . 7 ⊢ ¬ (∅ ≠ ∅ ∧ (∅‘0) ≠ 0)
55	54	pm2.21i 117	. . . . . 6 ⊢ ((∅ ≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)
56		fveq2 6375	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑚 → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘𝑚))
57	56	neeq1d 2996	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0))
58	57	cbvralv 3319	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)
59	58	imbi2i 327	. . . . . . . . 9 ⊢ (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))
60	59	anbi2i 616	. . . . . . . 8 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ↔ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)))
61		simplr 785	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → 𝑚 ∈ (0..^(♯‘𝑒)))
62		noel 4083	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑚 ∈ ∅
63		fveq2 6375	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ∅ → (♯‘𝑒) = (♯‘∅))
64		hash0 13360	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘∅) = 0
65	63, 64	syl6eq 2815	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = ∅ → (♯‘𝑒) = 0)
66	65	oveq2d 6858	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = ∅ → (0..^(♯‘𝑒)) = (0..^0))
67		fzo0 12700	. . . . . . . . . . . . . . . 16 ⊢ (0..^0) = ∅
68	66, 67	syl6eq 2815	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ∅ → (0..^(♯‘𝑒)) = ∅)
69	68	eleq2d 2830	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ∅ → (𝑚 ∈ (0..^(♯‘𝑒)) ↔ 𝑚 ∈ ∅))
70	62, 69	mtbiri 318	. . . . . . . . . . . . 13 ⊢ (𝑒 = ∅ → ¬ 𝑚 ∈ (0..^(♯‘𝑒)))
71	70	adantl 473	. . . . . . . . . . . 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 809	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ)
74		simp-6r 811	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ)
75		simplr 785	. . . . . . . . . . . . 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 31098	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘𝑒)‘𝑚))
81	73, 74, 75, 80	syl3anc 1490	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘𝑒)‘𝑚))
82		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ≠ ∅)
83		simplll 791	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
84	83	ad2antrr 717	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
85		simplrr 796	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ (𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) ∧ 𝑚 ∈ (0..^(♯‘𝑒)) ∧ 𝑒 ≠ ∅)) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
86	85	3anassrs 1469	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
87		simpll 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ)
88		simplr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ)
89	88	s1cld 13574	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ⟨“𝑘”⟩ ∈ Word ℝ)
90		lennncl 13506	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
91	90	adantlr 706	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
92		fzo0end 12768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑒) ∈ ℕ → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
93		elfzolt3b 12690	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)) → 0 ∈ (0..^(♯‘𝑒)))
94	91, 92, 93	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 0 ∈ (0..^(♯‘𝑒)))
95		ccatval1 13548	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ ⟨“𝑘”⟩ ∈ Word ℝ ∧ 0 ∈ (0..^(♯‘𝑒))) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (𝑒‘0))
96	87, 89, 94, 95	syl3anc 1490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (𝑒‘0))
97	96	neeq1d 2996	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0))
98	97	biimpa 468	. . . . . . . . . . . . . . 15 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑒‘0) ≠ 0)
99	84, 82, 86, 98	syl21anc 866	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒‘0) ≠ 0)
100		simp-5r 807	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0))
101	82, 99, 100	mp2and 690	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)
102	57	rspcva 3459	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ (0..^(♯‘𝑒)) ∧ ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) → ((𝑇‘𝑒)‘𝑚) ≠ 0)
103	75, 101, 102	syl2anc 579	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘𝑚) ≠ 0)
104	81, 103	eqnetrd 3004	. . . . . . . . . . 11 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
105	72, 104	pm2.61dane 3024	. . . . . . . . . 10 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
106		simpr 477	. . . . . . . . . . . 12 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → 𝑚 = (♯‘𝑒))
107	106	fveq2d 6379	. . . . . . . . . . 11 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)))
108		simpr 477	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → 𝑒 = ∅)
109		simp-4r 803	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → 𝑘 ∈ ℝ)
110		simplrl 795	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
111	110	simprd 489	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
112		oveq1 6849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = ∅ → (𝑒 ++ ⟨“𝑘”⟩) = (∅ ++ ⟨“𝑘”⟩))
113		s1cl 13573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ ℝ → ⟨“𝑘”⟩ ∈ Word ℝ)
114		ccatlid 13557	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨“𝑘”⟩ ∈ Word ℝ → (∅ ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
115	113, 114	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℝ → (∅ ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
116	112, 115	sylan9eq 2819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑒 ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
117	116	fveq2d 6379	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = (𝑇‘⟨“𝑘”⟩))
118	117	adantr 472	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = (𝑇‘⟨“𝑘”⟩))
119		simplr 785	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → 𝑘 ∈ ℝ)
120	76, 77, 78, 79	signstf0 31094	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ → (𝑇‘⟨“𝑘”⟩) = ⟨“(sgn‘𝑘)”⟩)
121	119, 120	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘⟨“𝑘”⟩) = ⟨“(sgn‘𝑘)”⟩)
122	118, 121	eqtrd 2799	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = ⟨“(sgn‘𝑘)”⟩)
123	65	ad2antrr 717	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (♯‘𝑒) = 0)
124	122, 123	fveq12d 6382	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (⟨“(sgn‘𝑘)”⟩‘0))
125		sgnclre 31049	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ → (sgn‘𝑘) ∈ ℝ)
126		s1fv 13581	. . . . . . . . . . . . . . . . . 18 ⊢ ((sgn‘𝑘) ∈ ℝ → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
127	119, 125, 126	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
128	124, 127	eqtrd 2799	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (sgn‘𝑘))
129	116	fveq1d 6377	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (⟨“𝑘”⟩‘0))
130		s1fv 13581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℝ → (⟨“𝑘”⟩‘0) = 𝑘)
131	130	adantl 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (⟨“𝑘”⟩‘0) = 𝑘)
132	129, 131	eqtrd 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = 𝑘)
133	132	neeq1d 2996	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0 ↔ 𝑘 ≠ 0))
134	133	biimpa 468	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → 𝑘 ≠ 0)
135		rexr 10339	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ → 𝑘 ∈ ℝ^*)
136		sgn0bi 31057	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ^* → ((sgn‘𝑘) = 0 ↔ 𝑘 = 0))
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → ((sgn‘𝑘) = 0 ↔ 𝑘 = 0))
138	137	necon3bid 2981	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ → ((sgn‘𝑘) ≠ 0 ↔ 𝑘 ≠ 0))
139	138	biimpar 469	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℝ ∧ 𝑘 ≠ 0) → (sgn‘𝑘) ≠ 0)
140	119, 134, 139	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (sgn‘𝑘) ≠ 0)
141	128, 140	eqnetrd 3004	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
142	108, 109, 111, 141	syl21anc 866	. . . . . . . . . . . . . 14 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
143		simplll 791	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ∈ Word ℝ)
144		simpr 477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ¬ 𝑒 = ∅)
145		velsn 4350	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 ∈ {∅} ↔ 𝑒 = ∅)
146	144, 145	sylnibr 320	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ¬ 𝑒 ∈ {∅})
147	143, 146	eldifd 3743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ∈ (Word ℝ ∖ {∅}))
148		simpllr 793	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑘 ∈ ℝ)
149	76, 77, 78, 79	signstfvn 31095	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ (Word ℝ ∖ {∅}) ∧ 𝑘 ∈ ℝ) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
150	147, 148, 149	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
151	150	adantllr 710	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
152	144	neqned 2944	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ≠ ∅)
153	143, 152, 90	syl2anc 579	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (♯‘𝑒) ∈ ℕ)
154	153, 92	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
155	76, 77, 78, 79	signstcl 31091	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒))) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
156	143, 154, 155	syl2anc 579	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
157	156	adantllr 710	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
158	148	rexrd 10343	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑘 ∈ ℝ^*)
159		sgncl 31048	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ^* → (sgn‘𝑘) ∈ {-1, 0, 1})
160	158, 159	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (sgn‘𝑘) ∈ {-1, 0, 1})
161	160	adantllr 710	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (sgn‘𝑘) ∈ {-1, 0, 1})
162	154	adantllr 710	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
163	152	adantllr 710	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ≠ ∅)
164		simplll 791	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
165		simplrl 795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
166	165	simprd 489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
167	164, 163, 166, 98	syl21anc 866	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (𝑒‘0) ≠ 0)
168		simpllr 793	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0))
169	163, 167, 168	mp2and 690	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)
170		fveq2 6375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = ((♯‘𝑒) − 1) → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘((♯‘𝑒) − 1)))
171	170	neeq1d 2996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = ((♯‘𝑒) − 1) → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0))
172	171	rspcva 3459	. . . . . . . . . . . . . . . . 17 ⊢ ((((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)) ∧ ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0)
173	162, 169, 172	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0)
174	76, 77	signswn0 31086	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1} ∧ (sgn‘𝑘) ∈ {-1, 0, 1}) ∧ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0)
175	157, 161, 173, 174	syl21anc 866	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0)
176	151, 175	eqnetrd 3004	. . . . . . . . . . . . . 14 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
177	142, 176	pm2.61dan 847	. . . . . . . . . . . . 13 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
178	177	anassrs 459	. . . . . . . . . . . 12 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
179	178	adantr 472	. . . . . . . . . . 11 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
180	107, 179	eqnetrd 3004	. . . . . . . . . 10 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
181		lencl 13505	. . . . . . . . . . . . 13 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ ℕ₀)
182		nn0uz 11922	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
183	181, 182	syl6eleq 2854	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ (ℤ_≥‘0))
184	183	ad4antr 724	. . . . . . . . . . 11 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (♯‘𝑒) ∈ (ℤ_≥‘0))
185		simpr 477	. . . . . . . . . . . 12 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))
186		ccatws1len 13591	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ Word ℝ → (♯‘(𝑒 ++ ⟨“𝑘”⟩)) = ((♯‘𝑒) + 1))
187	186	adantr 472	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (♯‘(𝑒 ++ ⟨“𝑘”⟩)) = ((♯‘𝑒) + 1))
188	187	oveq2d 6858	. . . . . . . . . . . . . 14 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) = (0..^((♯‘𝑒) + 1)))
189	188	eleq2d 2830	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) ↔ 𝑚 ∈ (0..^((♯‘𝑒) + 1))))
190	189	biimpa 468	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1)))
191	83, 185, 190	syl2anc 579	. . . . . . . . . . 11 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1)))
192		fzosplitsni 12787	. . . . . . . . . . . 12 ⊢ ((♯‘𝑒) ∈ (ℤ_≥‘0) → (𝑚 ∈ (0..^((♯‘𝑒) + 1)) ↔ (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒))))
193	192	biimpa 468	. . . . . . . . . . 11 ⊢ (((♯‘𝑒) ∈ (ℤ_≥‘0) ∧ 𝑚 ∈ (0..^((♯‘𝑒) + 1))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒)))
194	184, 191, 193	syl2anc 579	. . . . . . . . . 10 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒)))
195	105, 180, 194	mpjaodan 981	. . . . . . . . 9 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
196	195	ralrimiva 3113	. . . . . . . 8 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
197	60, 196	sylanbr 577	. . . . . . 7 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
198	197	exp31 410	. . . . . 6 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0) → (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)))
199	19, 30, 41, 52, 55, 198	wrdind 13720	. . . . 5 ⊢ (𝐹 ∈ Word ℝ → ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))
200	199	imp 395	. . . 4 ⊢ ((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)
201	200	adantrr 708	. . 3 ⊢ ((𝐹 ∈ Word ℝ ∧ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)
202		fveq2 6375	. . . . 5 ⊢ (𝑚 = 𝑁 → ((𝑇‘𝐹)‘𝑚) = ((𝑇‘𝐹)‘𝑁))
203	202	neeq1d 2996	. . . 4 ⊢ (𝑚 = 𝑁 → (((𝑇‘𝐹)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑁) ≠ 0))
204	203	rspcva 3459	. . 3 ⊢ ((𝑁 ∈ (0..^(♯‘𝐹)) ∧ ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0) → ((𝑇‘𝐹)‘𝑁) ≠ 0)
205	8, 201, 204	syl2anc 579	. 2 ⊢ ((𝐹 ∈ Word ℝ ∧ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)
206	2, 6, 7, 205	syl12anc 865	1 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 ∨ wo 873 ∧ w3a 1107 = wceq 1652 ∈ wcel 2155 ≠ wne 2937 ∀wral 3055 ∖ cdif 3729 ∅c0 4079 ifcif 4243 {csn 4334 {cpr 4336 {ctp 4338 ⟨cop 4340 ↦ cmpt 4888 ‘cfv 6068 (class class class)co 6842 ↦ cmpt2 6844 ℝcr 10188 0cc0 10189 1c1 10190 + caddc 10192 ℝ^*cxr 10327 − cmin 10520 -cneg 10521 ℕcn 11274 ℕ₀cn0 11538 ℤ_≥cuz 11886 ...cfz 12533 ..^cfzo 12673 ♯chash 13321 Word cword 13486 ++ cconcat 13541 ⟨“cs1 13566 sgncsgn 14111 Σcsu 14701 ndxcnx 16127 Basecbs 16130 +_gcplusg 16214 Σ_g cgsu 16367

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-rep 4930 ax-sep 4941 ax-nul 4949 ax-pow 5001 ax-pr 5062 ax-un 7147 ax-inf2 8753 ax-cnex 10245 ax-resscn 10246 ax-1cn 10247 ax-icn 10248 ax-addcl 10249 ax-addrcl 10250 ax-mulcl 10251 ax-mulrcl 10252 ax-mulcom 10253 ax-addass 10254 ax-mulass 10255 ax-distr 10256 ax-i2m1 10257 ax-1ne0 10258 ax-1rid 10259 ax-rnegex 10260 ax-rrecex 10261 ax-cnre 10262 ax-pre-lttri 10263 ax-pre-lttrn 10264 ax-pre-ltadd 10265 ax-pre-mulgt0 10266

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-reu 3062 df-rmo 3063 df-rab 3064 df-v 3352 df-sbc 3597 df-csb 3692 df-dif 3735 df-un 3737 df-in 3739 df-ss 3746 df-pss 3748 df-nul 4080 df-if 4244 df-pw 4317 df-sn 4335 df-pr 4337 df-tp 4339 df-op 4341 df-uni 4595 df-int 4634 df-iun 4678 df-br 4810 df-opab 4872 df-mpt 4889 df-tr 4912 df-id 5185 df-eprel 5190 df-po 5198 df-so 5199 df-fr 5236 df-se 5237 df-we 5238 df-xp 5283 df-rel 5284 df-cnv 5285 df-co 5286 df-dm 5287 df-rn 5288 df-res 5289 df-ima 5290 df-pred 5865 df-ord 5911 df-on 5912 df-lim 5913 df-suc 5914 df-iota 6031 df-fun 6070 df-fn 6071 df-f 6072 df-f1 6073 df-fo 6074 df-f1o 6075 df-fv 6076 df-isom 6077 df-riota 6803 df-ov 6845 df-oprab 6846 df-mpt2 6847 df-om 7264 df-1st 7366 df-2nd 7367 df-supp 7498 df-wrecs 7610 df-recs 7672 df-rdg 7710 df-1o 7764 df-oadd 7768 df-er 7947 df-en 8161 df-dom 8162 df-sdom 8163 df-fin 8164 df-oi 8622 df-card 9016 df-pnf 10330 df-mnf 10331 df-xr 10332 df-ltxr 10333 df-le 10334 df-sub 10522 df-neg 10523 df-nn 11275 df-2 11335 df-n0 11539 df-xnn0 11611 df-z 11625 df-uz 11887 df-fz 12534 df-fzo 12674 df-seq 13009 df-hash 13322 df-word 13487 df-lsw 13534 df-concat 13542 df-s1 13567 df-substr 13617 df-pfx 13662 df-sgn 14112 df-struct 16132 df-ndx 16133 df-slot 16134 df-base 16136 df-plusg 16227 df-0g 16368 df-gsum 16369 df-mgm 17508 df-sgrp 17550 df-mnd 17561 df-mulg 17808 df-cntz 18013

This theorem is referenced by: signstfvcl 31100

W3C validator