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 33881

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 763	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ (Word ℝ ∖ {∅}))
2	1	eldifad 3959	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ Word ℝ)
3		eldifsni 4792	. . . 4 ⊢ (𝐹 ∈ (Word ℝ ∖ {∅}) → 𝐹 ≠ ∅)
4	3	ad2antrr 722	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ≠ ∅)
5		simplr 765	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹‘0) ≠ 0)
6	4, 5	jca 510	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0))
7		simpr 483	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^(♯‘𝐹)))
8		fveq2 6890	. . . 4 ⊢ (𝑚 = 𝑁 → ((𝑇‘𝐹)‘𝑚) = ((𝑇‘𝐹)‘𝑁))
9	8	neeq1d 2998	. . 3 ⊢ (𝑚 = 𝑁 → (((𝑇‘𝐹)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑁) ≠ 0))
10		neeq1 3001	. . . . . . . 8 ⊢ (𝑔 = ∅ → (𝑔 ≠ ∅ ↔ ∅ ≠ ∅))
11		fveq1 6889	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (𝑔‘0) = (∅‘0))
12	11	neeq1d 2998	. . . . . . . 8 ⊢ (𝑔 = ∅ → ((𝑔‘0) ≠ 0 ↔ (∅‘0) ≠ 0))
13	10, 12	anbi12d 629	. . . . . . 7 ⊢ (𝑔 = ∅ → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (∅ ≠ ∅ ∧ (∅‘0) ≠ 0)))
14		fveq2 6890	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (♯‘𝑔) = (♯‘∅))
15	14	oveq2d 7427	. . . . . . . 8 ⊢ (𝑔 = ∅ → (0..^(♯‘𝑔)) = (0..^(♯‘∅)))
16		fveq2 6890	. . . . . . . . . 10 ⊢ (𝑔 = ∅ → (𝑇‘𝑔) = (𝑇‘∅))
17	16	fveq1d 6892	. . . . . . . . 9 ⊢ (𝑔 = ∅ → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘∅)‘𝑚))
18	17	neeq1d 2998	. . . . . . . 8 ⊢ (𝑔 = ∅ → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘∅)‘𝑚) ≠ 0))
19	15, 18	raleqbidv 3340	. . . . . . 7 ⊢ (𝑔 = ∅ → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0))
20	13, 19	imbi12d 343	. . . . . 6 ⊢ (𝑔 = ∅ → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((∅ ≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)))
21		neeq1 3001	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (𝑔 ≠ ∅ ↔ 𝑒 ≠ ∅))
22		fveq1 6889	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (𝑔‘0) = (𝑒‘0))
23	22	neeq1d 2998	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → ((𝑔‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0))
24	21, 23	anbi12d 629	. . . . . . 7 ⊢ (𝑔 = 𝑒 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0)))
25		fveq2 6890	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (♯‘𝑔) = (♯‘𝑒))
26	25	oveq2d 7427	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (0..^(♯‘𝑔)) = (0..^(♯‘𝑒)))
27		fveq2 6890	. . . . . . . . . 10 ⊢ (𝑔 = 𝑒 → (𝑇‘𝑔) = (𝑇‘𝑒))
28	27	fveq1d 6892	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝑒)‘𝑚))
29	28	neeq1d 2998	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0))
30	26, 29	raleqbidv 3340	. . . . . . 7 ⊢ (𝑔 = 𝑒 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))
31	24, 30	imbi12d 343	. . . . . 6 ⊢ (𝑔 = 𝑒 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)))
32		neeq1 3001	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑔 ≠ ∅ ↔ (𝑒 ++ ⟨“𝑘”⟩) ≠ ∅))
33		fveq1 6889	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑔‘0) = ((𝑒 ++ ⟨“𝑘”⟩)‘0))
34	33	neeq1d 2998	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑔‘0) ≠ 0 ↔ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
35	32, 34	anbi12d 629	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)))
36		fveq2 6890	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (♯‘𝑔) = (♯‘(𝑒 ++ ⟨“𝑘”⟩)))
37	36	oveq2d 7427	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (0..^(♯‘𝑔)) = (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))
38		fveq2 6890	. . . . . . . . . 10 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑇‘𝑔) = (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)))
39	38	fveq1d 6892	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚))
40	39	neeq1d 2998	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0))
41	37, 40	raleqbidv 3340	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0))
42	35, 41	imbi12d 343	. . . . . 6 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)))
43		neeq1 3001	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (𝑔 ≠ ∅ ↔ 𝐹 ≠ ∅))
44		fveq1 6889	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → (𝑔‘0) = (𝐹‘0))
45	44	neeq1d 2998	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → ((𝑔‘0) ≠ 0 ↔ (𝐹‘0) ≠ 0))
46	43, 45	anbi12d 629	. . . . . . 7 ⊢ (𝑔 = 𝐹 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)))
47		fveq2 6890	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → (♯‘𝑔) = (♯‘𝐹))
48	47	oveq2d 7427	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (0..^(♯‘𝑔)) = (0..^(♯‘𝐹)))
49		fveq2 6890	. . . . . . . . . 10 ⊢ (𝑔 = 𝐹 → (𝑇‘𝑔) = (𝑇‘𝐹))
50	49	fveq1d 6892	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝐹)‘𝑚))
51	50	neeq1d 2998	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑚) ≠ 0))
52	48, 51	raleqbidv 3340	. . . . . . 7 ⊢ (𝑔 = 𝐹 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))
53	46, 52	imbi12d 343	. . . . . 6 ⊢ (𝑔 = 𝐹 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)))
54		neirr 2947	. . . . . . . 8 ⊢ ¬ ∅ ≠ ∅
55	54	intnanr 486	. . . . . . 7 ⊢ ¬ (∅ ≠ ∅ ∧ (∅‘0) ≠ 0)
56	55	pm2.21i 119	. . . . . 6 ⊢ ((∅ ≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)
57		fveq2 6890	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑚 → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘𝑚))
58	57	neeq1d 2998	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0))
59	58	cbvralvw 3232	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)
60	59	imbi2i 335	. . . . . . . . 9 ⊢ (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))
61	60	anbi2i 621	. . . . . . . 8 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ↔ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)))
62		simplr 765	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → 𝑚 ∈ (0..^(♯‘𝑒)))
63		noel 4329	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑚 ∈ ∅
64		fveq2 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ∅ → (♯‘𝑒) = (♯‘∅))
65		hash0 14331	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘∅) = 0
66	64, 65	eqtrdi 2786	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = ∅ → (♯‘𝑒) = 0)
67	66	oveq2d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = ∅ → (0..^(♯‘𝑒)) = (0..^0))
68		fzo0 13660	. . . . . . . . . . . . . . . 16 ⊢ (0..^0) = ∅
69	67, 68	eqtrdi 2786	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ∅ → (0..^(♯‘𝑒)) = ∅)
70	69	eleq2d 2817	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ∅ → (𝑚 ∈ (0..^(♯‘𝑒)) ↔ 𝑚 ∈ ∅))
71	63, 70	mtbiri 326	. . . . . . . . . . . . 13 ⊢ (𝑒 = ∅ → ¬ 𝑚 ∈ (0..^(♯‘𝑒)))
72	71	adantl 480	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → ¬ 𝑚 ∈ (0..^(♯‘𝑒)))
73	62, 72	pm2.21dd 194	. . . . . . . . . . 11 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
74		simp-6l 783	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ)
75		simp-6r 784	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ)
76		simplr 765	. . . . . . . . . . . . 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 33880	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘𝑒)‘𝑚))
82	74, 75, 76, 81	syl3anc 1369	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘𝑒)‘𝑚))
83		simpr 483	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ≠ ∅)
84		simp-5l 781	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
85		simplrr 774	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ (𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) ∧ 𝑚 ∈ (0..^(♯‘𝑒)) ∧ 𝑒 ≠ ∅)) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
86	85	3anassrs 1358	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
87		simpll 763	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ)
88		s1cl 14556	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → ⟨“𝑘”⟩ ∈ Word ℝ)
89	88	ad2antlr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ⟨“𝑘”⟩ ∈ Word ℝ)
90		lennncl 14488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
91	90	adantlr 711	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
92		fzo0end 13728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑒) ∈ ℕ → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
93		elfzolt3b 13648	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)) → 0 ∈ (0..^(♯‘𝑒)))
94	91, 92, 93	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 0 ∈ (0..^(♯‘𝑒)))
95		ccatval1 14531	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ ⟨“𝑘”⟩ ∈ Word ℝ ∧ 0 ∈ (0..^(♯‘𝑒))) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (𝑒‘0))
96	87, 89, 94, 95	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (𝑒‘0))
97	96	neeq1d 2998	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0))
98	97	biimpa 475	. . . . . . . . . . . . . . 15 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑒‘0) ≠ 0)
99	84, 83, 86, 98	syl21anc 834	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒‘0) ≠ 0)
100		simp-5r 782	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0))
101	83, 99, 100	mp2and 695	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)
102	58, 101, 76	rspcdva 3612	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘𝑚) ≠ 0)
103	82, 102	eqnetrd 3006	. . . . . . . . . . 11 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
104	73, 103	pm2.61dane 3027	. . . . . . . . . 10 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
105		simpr 483	. . . . . . . . . . . 12 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → 𝑚 = (♯‘𝑒))
106	105	fveq2d 6894	. . . . . . . . . . 11 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)))
107		simpr 483	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → 𝑒 = ∅)
108		simp-4r 780	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → 𝑘 ∈ ℝ)
109		simplrl 773	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
110	109	simprd 494	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
111		oveq1 7418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = ∅ → (𝑒 ++ ⟨“𝑘”⟩) = (∅ ++ ⟨“𝑘”⟩))
112		ccatlid 14540	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨“𝑘”⟩ ∈ Word ℝ → (∅ ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
113	88, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℝ → (∅ ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
114	111, 113	sylan9eq 2790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑒 ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
115	114	fveq2d 6894	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = (𝑇‘⟨“𝑘”⟩))
116	115	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = (𝑇‘⟨“𝑘”⟩))
117	77, 78, 79, 80	signstf0 33877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ → (𝑇‘⟨“𝑘”⟩) = ⟨“(sgn‘𝑘)”⟩)
118	117	ad2antlr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘⟨“𝑘”⟩) = ⟨“(sgn‘𝑘)”⟩)
119	116, 118	eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = ⟨“(sgn‘𝑘)”⟩)
120	66	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (♯‘𝑒) = 0)
121	119, 120	fveq12d 6897	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (⟨“(sgn‘𝑘)”⟩‘0))
122		sgnclre 33836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → (sgn‘𝑘) ∈ ℝ)
123		s1fv 14564	. . . . . . . . . . . . . . . . . . 19 ⊢ ((sgn‘𝑘) ∈ ℝ → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
124	122, 123	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
125	124	ad2antlr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
126	121, 125	eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (sgn‘𝑘))
127		simplr 765	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → 𝑘 ∈ ℝ)
128	114	fveq1d 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (⟨“𝑘”⟩‘0))
129		s1fv 14564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℝ → (⟨“𝑘”⟩‘0) = 𝑘)
130	129	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (⟨“𝑘”⟩‘0) = 𝑘)
131	128, 130	eqtrd 2770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = 𝑘)
132	131	neeq1d 2998	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0 ↔ 𝑘 ≠ 0))
133	132	biimpa 475	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → 𝑘 ≠ 0)
134		rexr 11264	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ → 𝑘 ∈ ℝ^*)
135		sgn0bi 33844	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ^* → ((sgn‘𝑘) = 0 ↔ 𝑘 = 0))
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → ((sgn‘𝑘) = 0 ↔ 𝑘 = 0))
137	136	necon3bid 2983	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ → ((sgn‘𝑘) ≠ 0 ↔ 𝑘 ≠ 0))
138	137	biimpar 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℝ ∧ 𝑘 ≠ 0) → (sgn‘𝑘) ≠ 0)
139	127, 133, 138	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (sgn‘𝑘) ≠ 0)
140	126, 139	eqnetrd 3006	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
141	107, 108, 110, 140	syl21anc 834	. . . . . . . . . . . . . 14 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
142		eldifsn 4789	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 ∈ (Word ℝ ∖ {∅}) ↔ (𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅))
143	142	biimpri 227	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → 𝑒 ∈ (Word ℝ ∖ {∅}))
144	143	adantlr 711	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ (Word ℝ ∖ {∅}))
145		simplr 765	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ)
146	77, 78, 79, 80	signstfvn 33878	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ (Word ℝ ∖ {∅}) ∧ 𝑘 ∈ ℝ) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
147	144, 145, 146	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
148	147	ad4ant14 748	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
149	90, 92	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
150	77, 78, 79, 80	signstcl 33874	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒))) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
151	149, 150	syldan 589	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
152	151	ad5ant15 755	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
153		sgncl 33835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ^* → (sgn‘𝑘) ∈ {-1, 0, 1})
154	134, 153	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℝ → (sgn‘𝑘) ∈ {-1, 0, 1})
155	154	ad4antlr 729	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (sgn‘𝑘) ∈ {-1, 0, 1})
156		fveq2 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = ((♯‘𝑒) − 1) → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘((♯‘𝑒) − 1)))
157	156	neeq1d 2998	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = ((♯‘𝑒) − 1) → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0))
158		simpr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → 𝑒 ≠ ∅)
159		simplll 771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
160		simplrl 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
161	160	simprd 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
162	159, 158, 161, 98	syl21anc 834	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (𝑒‘0) ≠ 0)
163		simpllr 772	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0))
164	158, 162, 163	mp2and 695	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)
165	90	ad4ant14 748	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
166	165, 92	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
167	166	adantllr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
168	157, 164, 167	rspcdva 3612	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0)
169	77, 78	signswn0 33869	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1} ∧ (sgn‘𝑘) ∈ {-1, 0, 1}) ∧ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0)
170	152, 155, 168, 169	syl21anc 834	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0)
171	148, 170	eqnetrd 3006	. . . . . . . . . . . . . 14 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
172	141, 171	pm2.61dane 3027	. . . . . . . . . . . . 13 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
173	172	anassrs 466	. . . . . . . . . . . 12 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
174	173	adantr 479	. . . . . . . . . . 11 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
175	106, 174	eqnetrd 3006	. . . . . . . . . 10 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
176		lencl 14487	. . . . . . . . . . . . 13 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ ℕ₀)
177		nn0uz 12868	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
178	176, 177	eleqtrdi 2841	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ (ℤ_≥‘0))
179	178	ad4antr 728	. . . . . . . . . . 11 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (♯‘𝑒) ∈ (ℤ_≥‘0))
180		ccatws1len 14574	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ Word ℝ → (♯‘(𝑒 ++ ⟨“𝑘”⟩)) = ((♯‘𝑒) + 1))
181	180	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (♯‘(𝑒 ++ ⟨“𝑘”⟩)) = ((♯‘𝑒) + 1))
182	181	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) = (0..^((♯‘𝑒) + 1)))
183	182	eleq2d 2817	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) ↔ 𝑚 ∈ (0..^((♯‘𝑒) + 1))))
184	183	biimpa 475	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1)))
185	184	ad4ant14 748	. . . . . . . . . . 11 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1)))
186		fzosplitsni 13747	. . . . . . . . . . . 12 ⊢ ((♯‘𝑒) ∈ (ℤ_≥‘0) → (𝑚 ∈ (0..^((♯‘𝑒) + 1)) ↔ (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒))))
187	186	biimpa 475	. . . . . . . . . . 11 ⊢ (((♯‘𝑒) ∈ (ℤ_≥‘0) ∧ 𝑚 ∈ (0..^((♯‘𝑒) + 1))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒)))
188	179, 185, 187	syl2anc 582	. . . . . . . . . 10 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒)))
189	104, 175, 188	mpjaodan 955	. . . . . . . . 9 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
190	189	ralrimiva 3144	. . . . . . . 8 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
191	61, 190	sylanbr 580	. . . . . . 7 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
192	191	exp31 418	. . . . . 6 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0) → (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)))
193	20, 31, 42, 53, 56, 192	wrdind 14676	. . . . 5 ⊢ (𝐹 ∈ Word ℝ → ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))
194	193	imp 405	. . . 4 ⊢ ((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)
195	194	adantr 479	. . 3 ⊢ (((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)
196		simpr 483	. . 3 ⊢ (((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^(♯‘𝐹)))
197	9, 195, 196	rspcdva 3612	. 2 ⊢ (((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)
198	2, 6, 7, 197	syl21anc 834	1 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 843 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 ∀wral 3059 ∖ cdif 3944 ∅c0 4321 ifcif 4527 {csn 4627 {cpr 4629 {ctp 4631 ⟨cop 4633 ↦ cmpt 5230 ‘cfv 6542 (class class class)co 7411 ∈ cmpo 7413 ℝcr 11111 0cc0 11112 1c1 11113 + caddc 11115 ℝ^*cxr 11251 − cmin 11448 -cneg 11449 ℕcn 12216 ℕ₀cn0 12476 ℤ_≥cuz 12826 ...cfz 13488 ..^cfzo 13631 ♯chash 14294 Word cword 14468 ++ cconcat 14524 ⟨“cs1 14549 sgncsgn 15037 Σcsu 15636 ndxcnx 17130 Basecbs 17148 +_gcplusg 17201 Σ_g cgsu 17390

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-supp 8149 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-oi 9507 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-2 12279 df-n0 12477 df-xnn0 12549 df-z 12563 df-uz 12827 df-fz 13489 df-fzo 13632 df-seq 13971 df-hash 14295 df-word 14469 df-lsw 14517 df-concat 14525 df-s1 14550 df-substr 14595 df-pfx 14625 df-sgn 15038 df-struct 17084 df-slot 17119 df-ndx 17131 df-base 17149 df-plusg 17214 df-0g 17391 df-gsum 17392 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-mulg 18987 df-cntz 19222

This theorem is referenced by: signstfvcl 33882

W3C validator