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 35312

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 779	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ (Word ℝ ∖ {∅}))
2	1	eldifad 4054	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ Word ℝ)
3		eldifsni 4755	. . . 4 ⊢ (𝐹 ∈ (Word ℝ ∖ {∅}) → 𝐹 ≠ ∅)
4	3	ad2antrr 739	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ≠ ∅)
5		simplr 781	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹‘0) ≠ 0)
6	4, 5	jca 521	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0))
7		simpr 490	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^(♯‘𝐹)))
8		fveq2 6916	. . . 4 ⊢ (𝑚 = 𝑁 → ((𝑇‘𝐹)‘𝑚) = ((𝑇‘𝐹)‘𝑁))
9	8	neeq1d 3018	. . 3 ⊢ (𝑚 = 𝑁 → (((𝑇‘𝐹)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑁) ≠ 0))
10		neeq1 3021	. . . . . . . 8 ⊢ (𝑔 = ∅ → (𝑔 ≠ ∅ ↔ ∅ ≠ ∅))
11		fveq1 6915	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (𝑔‘0) = (∅‘0))
12	11	neeq1d 3018	. . . . . . . 8 ⊢ (𝑔 = ∅ → ((𝑔‘0) ≠ 0 ↔ (∅‘0) ≠ 0))
13	10, 12	anbi12d 644	. . . . . . 7 ⊢ (𝑔 = ∅ → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (∅ ≠ ∅ ∧ (∅‘0) ≠ 0)))
14		fveq2 6916	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (♯‘𝑔) = (♯‘∅))
15	14	oveq2d 7467	. . . . . . . 8 ⊢ (𝑔 = ∅ → (0..^(♯‘𝑔)) = (0..^(♯‘∅)))
16		fveq2 6916	. . . . . . . . . 10 ⊢ (𝑔 = ∅ → (𝑇‘𝑔) = (𝑇‘∅))
17	16	fveq1d 6918	. . . . . . . . 9 ⊢ (𝑔 = ∅ → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘∅)‘𝑚))
18	17	neeq1d 3018	. . . . . . . 8 ⊢ (𝑔 = ∅ → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘∅)‘𝑚) ≠ 0))
19	15, 18	raleqbidv 3338	. . . . . . 7 ⊢ (𝑔 = ∅ → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0))
20	13, 19	imbi12d 347	. . . . . 6 ⊢ (𝑔 = ∅ → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((∅ ≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)))
21		neeq1 3021	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (𝑔 ≠ ∅ ↔ 𝑒 ≠ ∅))
22		fveq1 6915	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (𝑔‘0) = (𝑒‘0))
23	22	neeq1d 3018	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → ((𝑔‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0))
24	21, 23	anbi12d 644	. . . . . . 7 ⊢ (𝑔 = 𝑒 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0)))
25		fveq2 6916	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (♯‘𝑔) = (♯‘𝑒))
26	25	oveq2d 7467	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (0..^(♯‘𝑔)) = (0..^(♯‘𝑒)))
27		fveq2 6916	. . . . . . . . . 10 ⊢ (𝑔 = 𝑒 → (𝑇‘𝑔) = (𝑇‘𝑒))
28	27	fveq1d 6918	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝑒)‘𝑚))
29	28	neeq1d 3018	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0))
30	26, 29	raleqbidv 3338	. . . . . . 7 ⊢ (𝑔 = 𝑒 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))
31	24, 30	imbi12d 347	. . . . . 6 ⊢ (𝑔 = 𝑒 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)))
32		neeq1 3021	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑔 ≠ ∅ ↔ (𝑒 ++ ⟨“𝑘”⟩) ≠ ∅))
33		fveq1 6915	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑔‘0) = ((𝑒 ++ ⟨“𝑘”⟩)‘0))
34	33	neeq1d 3018	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑔‘0) ≠ 0 ↔ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
35	32, 34	anbi12d 644	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)))
36		fveq2 6916	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (♯‘𝑔) = (♯‘(𝑒 ++ ⟨“𝑘”⟩)))
37	36	oveq2d 7467	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (0..^(♯‘𝑔)) = (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))
38		fveq2 6916	. . . . . . . . . 10 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑇‘𝑔) = (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)))
39	38	fveq1d 6918	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚))
40	39	neeq1d 3018	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0))
41	37, 40	raleqbidv 3338	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0))
42	35, 41	imbi12d 347	. . . . . 6 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)))
43		neeq1 3021	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (𝑔 ≠ ∅ ↔ 𝐹 ≠ ∅))
44		fveq1 6915	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → (𝑔‘0) = (𝐹‘0))
45	44	neeq1d 3018	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → ((𝑔‘0) ≠ 0 ↔ (𝐹‘0) ≠ 0))
46	43, 45	anbi12d 644	. . . . . . 7 ⊢ (𝑔 = 𝐹 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)))
47		fveq2 6916	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → (♯‘𝑔) = (♯‘𝐹))
48	47	oveq2d 7467	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (0..^(♯‘𝑔)) = (0..^(♯‘𝐹)))
49		fveq2 6916	. . . . . . . . . 10 ⊢ (𝑔 = 𝐹 → (𝑇‘𝑔) = (𝑇‘𝐹))
50	49	fveq1d 6918	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝐹)‘𝑚))
51	50	neeq1d 3018	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑚) ≠ 0))
52	48, 51	raleqbidv 3338	. . . . . . 7 ⊢ (𝑔 = 𝐹 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))
53	46, 52	imbi12d 347	. . . . . 6 ⊢ (𝑔 = 𝐹 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)))
54		neirr 2968	. . . . . . . 8 ⊢ ¬ ∅ ≠ ∅
55	54	intnanr 493	. . . . . . 7 ⊢ ¬ (∅ ≠ ∅ ∧ (∅‘0) ≠ 0)
56	55	pm2.21i 120	. . . . . 6 ⊢ ((∅ ≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)
57		fveq2 6916	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑚 → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘𝑚))
58	57	neeq1d 3018	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0))
59	58	cbvralvw 3244	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)
60	59	imbi2i 339	. . . . . . . . 9 ⊢ (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))
61	60	anbi2i 635	. . . . . . . 8 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ↔ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)))
62		simplr 781	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → 𝑚 ∈ (0..^(♯‘𝑒)))
63		noel 4286	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑚 ∈ ∅
64		fveq2 6916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ∅ → (♯‘𝑒) = (♯‘∅))
65		hash0 14552	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘∅) = 0
66	64, 65	eqtrdi 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = ∅ → (♯‘𝑒) = 0)
67	66	oveq2d 7467	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = ∅ → (0..^(♯‘𝑒)) = (0..^0))
68		fzo0 13858	. . . . . . . . . . . . . . . 16 ⊢ (0..^0) = ∅
69	67, 68	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ∅ → (0..^(♯‘𝑒)) = ∅)
70	69	eleq2d 2850	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ∅ → (𝑚 ∈ (0..^(♯‘𝑒)) ↔ 𝑚 ∈ ∅))
71	63, 70	mtbiri 330	. . . . . . . . . . . . 13 ⊢ (𝑒 = ∅ → ¬ 𝑚 ∈ (0..^(♯‘𝑒)))
72	71	adantl 487	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → ¬ 𝑚 ∈ (0..^(♯‘𝑒)))
73	62, 72	pm2.21dd 198	. . . . . . . . . . 11 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
74		simp-6l 799	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ)
75		simp-6r 800	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ)
76		simplr 781	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑚 ∈ (0..^(♯‘𝑒)))
77		signsv.p	. . . . . . . . . . . . . 14 ⊢ ⨣ = (𝑎 ∈ { -1, 0, 1}, 𝑏 ∈ { -1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
78		signsv.w	. . . . . . . . . . . . . 14 ⊢ 𝑊 = {⟨(Base‘ndx), { -1, 0, 1}⟩, ⟨(+_g‘ndx), ⨣ ⟩}
79		signsv.t	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σ_g (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖))))))
80		signsv.v	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0))
81	77, 78, 79, 80	signstfvp 35311	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘𝑒)‘𝑚))
82	74, 75, 76, 81	syl3anc 1399	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘𝑒)‘𝑚))
83		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ≠ ∅)
84		simp-5l 797	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
85		simplrr 790	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ (𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) ∧ 𝑚 ∈ (0..^(♯‘𝑒)) ∧ 𝑒 ≠ ∅)) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
86	85	3anassrs 1382	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
87		simpll 779	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ)
88		s1cl 14790	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → ⟨“𝑘”⟩ ∈ Word ℝ)
89	88	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ⟨“𝑘”⟩ ∈ Word ℝ)
90		lennncl 14720	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
91	90	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
92		fzo0end 13933	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑒) ∈ ℕ → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
93		elfzolt3b 13846	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)) → 0 ∈ (0..^(♯‘𝑒)))
94	91, 92, 93	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 0 ∈ (0..^(♯‘𝑒)))
95		ccatval1 14763	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ ⟨“𝑘”⟩ ∈ Word ℝ ∧ 0 ∈ (0..^(♯‘𝑒))) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (𝑒‘0))
96	87, 89, 94, 95	syl3anc 1399	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (𝑒‘0))
97	96	neeq1d 3018	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0))
98	97	biimpa 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑒‘0) ≠ 0)
99	84, 83, 86, 98	syl21anc 851	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒‘0) ≠ 0)
100		simp-5r 798	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0))
101	83, 99, 100	mp2and 712	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)
102	58, 101, 76	rspcdva 3581	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘𝑚) ≠ 0)
103	82, 102	eqnetrd 3026	. . . . . . . . . . 11 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
104	73, 103	pm2.61dane 3046	. . . . . . . . . 10 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
105		simpr 490	. . . . . . . . . . . 12 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → 𝑚 = (♯‘𝑒))
106	105	fveq2d 6920	. . . . . . . . . . 11 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)))
107		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → 𝑒 = ∅)
108		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → 𝑘 ∈ ℝ)
109		simplrl 789	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
110	109	simprd 501	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
111		oveq1 7458	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = ∅ → (𝑒 ++ ⟨“𝑘”⟩) = (∅ ++ ⟨“𝑘”⟩))
112		ccatlid 14773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨“𝑘”⟩ ∈ Word ℝ → (∅ ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
113	88, 112	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℝ → (∅ ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
114	111, 113	sylan9eq 2818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑒 ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
115	114	fveq2d 6920	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = (𝑇‘⟨“𝑘”⟩))
116	115	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = (𝑇‘⟨“𝑘”⟩))
117	77, 78, 79, 80	signstf0 35308	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ → (𝑇‘⟨“𝑘”⟩) = ⟨“(sgn‘𝑘)”⟩)
118	117	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘⟨“𝑘”⟩) = ⟨“(sgn‘𝑘)”⟩)
119	116, 118	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = ⟨“(sgn‘𝑘)”⟩)
120	66	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (♯‘𝑒) = 0)
121	119, 120	fveq12d 6923	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (⟨“(sgn‘𝑘)”⟩‘0))
122		sgnclre 15298	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → (sgn‘𝑘) ∈ ℝ)
123		s1fv 14800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((sgn‘𝑘) ∈ ℝ → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
124	122, 123	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
125	124	ad2antlr 740	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
126	121, 125	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (sgn‘𝑘))
127		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → 𝑘 ∈ ℝ)
128	114	fveq1d 6918	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (⟨“𝑘”⟩‘0))
129		s1fv 14800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℝ → (⟨“𝑘”⟩‘0) = 𝑘)
130	129	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (⟨“𝑘”⟩‘0) = 𝑘)
131	128, 130	eqtrd 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = 𝑘)
132	131	neeq1d 3018	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0 ↔ 𝑘 ≠ 0))
133	132	biimpa 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → 𝑘 ≠ 0)
134		rexr 11394	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ → 𝑘 ∈ ℝ^*)
135		sgn0bi 15299	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ^* → ((sgn‘𝑘) = 0 ↔ 𝑘 = 0))
136	134, 135	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → ((sgn‘𝑘) = 0 ↔ 𝑘 = 0))
137	136	necon3bid 3003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ → ((sgn‘𝑘) ≠ 0 ↔ 𝑘 ≠ 0))
138	137	biimpar 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℝ ∧ 𝑘 ≠ 0) → (sgn‘𝑘) ≠ 0)
139	127, 133, 138	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (sgn‘𝑘) ≠ 0)
140	126, 139	eqnetrd 3026	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
141	107, 108, 110, 140	syl21anc 851	. . . . . . . . . . . . . 14 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
142		eldifsn 4750	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 ∈ (Word ℝ ∖ {∅}) ↔ (𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅))
143	142	biimpri 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → 𝑒 ∈ (Word ℝ ∖ {∅}))
144	143	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ (Word ℝ ∖ {∅}))
145		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ)
146	77, 78, 79, 80	signstfvn 35309	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ (Word ℝ ∖ {∅}) ∧ 𝑘 ∈ ℝ) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
147	144, 145, 146	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
148	147	ad4ant14 765	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
149	90, 92	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
150	77, 78, 79, 80	signstcl 35305	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒))) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ { -1, 0, 1})
151	149, 150	syldan 603	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ { -1, 0, 1})
152	151	ad5ant15 771	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ { -1, 0, 1})
153		sgncl 15293	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ^* → (sgn‘𝑘) ∈ { -1, 0, 1})
154	134, 153	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℝ → (sgn‘𝑘) ∈ { -1, 0, 1})
155	154	ad4antlr 746	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (sgn‘𝑘) ∈ { -1, 0, 1})
156		fveq2 6916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = ((♯‘𝑒) − 1) → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘((♯‘𝑒) − 1)))
157	156	neeq1d 3018	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = ((♯‘𝑒) − 1) → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0))
158		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → 𝑒 ≠ ∅)
159		simplll 787	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
160		simplrl 789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
161	160	simprd 501	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
162	159, 158, 161, 98	syl21anc 851	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (𝑒‘0) ≠ 0)
163		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0))
164	158, 162, 163	mp2and 712	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)
165	90	ad4ant14 765	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
166	165, 92	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
167	166	adantllr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
168	157, 164, 167	rspcdva 3581	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0)
169	77, 78	signswn0 35300	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ { -1, 0, 1} ∧ (sgn‘𝑘) ∈ { -1, 0, 1}) ∧ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0)
170	152, 155, 168, 169	syl21anc 851	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0)
171	148, 170	eqnetrd 3026	. . . . . . . . . . . . . 14 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
172	141, 171	pm2.61dane 3046	. . . . . . . . . . . . 13 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
173	172	anassrs 473	. . . . . . . . . . . 12 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
174	173	adantr 486	. . . . . . . . . . 11 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
175	106, 174	eqnetrd 3026	. . . . . . . . . 10 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
176		lencl 14719	. . . . . . . . . . . . 13 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ ℕ₀)
177		nn0uz 13043	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
178	176, 177	eleqtrdi 2874	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ (ℤ_≥‘0))
179	178	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (♯‘𝑒) ∈ (ℤ_≥‘0))
180		ccatws1len 14810	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ Word ℝ → (♯‘(𝑒 ++ ⟨“𝑘”⟩)) = ((♯‘𝑒) + 1))
181	180	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (♯‘(𝑒 ++ ⟨“𝑘”⟩)) = ((♯‘𝑒) + 1))
182	181	oveq2d 7467	. . . . . . . . . . . . . 14 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) = (0..^((♯‘𝑒) + 1)))
183	182	eleq2d 2850	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) ↔ 𝑚 ∈ (0..^((♯‘𝑒) + 1))))
184	183	biimpa 482	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1)))
185	184	ad4ant14 765	. . . . . . . . . . 11 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1)))
186		fzosplitsni 13954	. . . . . . . . . . . 12 ⊢ ((♯‘𝑒) ∈ (ℤ_≥‘0) → (𝑚 ∈ (0..^((♯‘𝑒) + 1)) ↔ (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒))))
187	186	biimpa 482	. . . . . . . . . . 11 ⊢ (((♯‘𝑒) ∈ (ℤ_≥‘0) ∧ 𝑚 ∈ (0..^((♯‘𝑒) + 1))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒)))
188	179, 185, 187	syl2anc 596	. . . . . . . . . 10 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒)))
189	104, 175, 188	mpjaodan 973	. . . . . . . . 9 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
190	189	ralrimiva 3158	. . . . . . . 8 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
191	61, 190	sylanbr 594	. . . . . . 7 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
192	191	exp31 425	. . . . . 6 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0) → (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)))
193	20, 31, 42, 53, 56, 192	wrdind 14913	. . . . 5 ⊢ (𝐹 ∈ Word ℝ → ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))
194	193	imp 412	. . . 4 ⊢ ((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)
195	194	adantr 486	. . 3 ⊢ (((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)
196		simpr 490	. . 3 ⊢ (((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^(♯‘𝐹)))
197	9, 195, 196	rspcdva 3581	. 2 ⊢ (((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)
198	2, 6, 7, 197	syl21anc 851	1 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∖ cdif 4048 ∅c0 4281 ifcif 4485 {csn 4588 {cpr 4590 {ctp 4592 ⟨cop 4840 ↦ cmpt 5192 ‘cfv 6566 (class class class)co 7451 ∈ cmpo 7453 ℝcr 11238 0cc0 11239 1c1 11240 + caddc 11242 ℝ^*cxr 11381 − cmin 11580 -cneg 11581 ℕcn 12375 ℕ₀cn0 12646 ℤ_≥cuz 13005 ...cfz 13679 ..^cfzo 13828 ♯chash 14515 Word cword 14699 ++ cconcat 14756 ⟨“cs1 14783 sgncsgn 15282 Σcsu 15897 ndxcnx 17415 Basecbs 17431 +_gcplusg 17472 Σ_g cgsu 17661

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-supp 8215 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-er 8755 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-oi 9541 df-card 10057 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-nn 12376 df-2 12445 df-n0 12647 df-xnn0 12720 df-z 12734 df-uz 13006 df-fz 13680 df-fzo 13829 df-seq 14185 df-hash 14516 df-word 14700 df-lsw 14749 df-concat 14757 df-s1 14784 df-substr 14831 df-pfx 14863 df-sgn 15283 df-struct 17369 df-slot 17404 df-ndx 17416 df-base 17432 df-plusg 17486 df-0g 17662 df-gsum 17663 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-mulg 19328 df-cntz 19582

This theorem is used by: signstfvcl 35313

W3C validator