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 34604

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 766	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ (Word ℝ ∖ {∅}))
2	1	eldifad 3938	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ Word ℝ)
3		eldifsni 4766	. . . 4 ⊢ (𝐹 ∈ (Word ℝ ∖ {∅}) → 𝐹 ≠ ∅)
4	3	ad2antrr 726	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ≠ ∅)
5		simplr 768	. . 3 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹‘0) ≠ 0)
6	4, 5	jca 511	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0))
7		simpr 484	. 2 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^(♯‘𝐹)))
8		fveq2 6876	. . . 4 ⊢ (𝑚 = 𝑁 → ((𝑇‘𝐹)‘𝑚) = ((𝑇‘𝐹)‘𝑁))
9	8	neeq1d 2991	. . 3 ⊢ (𝑚 = 𝑁 → (((𝑇‘𝐹)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑁) ≠ 0))
10		neeq1 2994	. . . . . . . 8 ⊢ (𝑔 = ∅ → (𝑔 ≠ ∅ ↔ ∅ ≠ ∅))
11		fveq1 6875	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (𝑔‘0) = (∅‘0))
12	11	neeq1d 2991	. . . . . . . 8 ⊢ (𝑔 = ∅ → ((𝑔‘0) ≠ 0 ↔ (∅‘0) ≠ 0))
13	10, 12	anbi12d 632	. . . . . . 7 ⊢ (𝑔 = ∅ → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (∅ ≠ ∅ ∧ (∅‘0) ≠ 0)))
14		fveq2 6876	. . . . . . . . 9 ⊢ (𝑔 = ∅ → (♯‘𝑔) = (♯‘∅))
15	14	oveq2d 7421	. . . . . . . 8 ⊢ (𝑔 = ∅ → (0..^(♯‘𝑔)) = (0..^(♯‘∅)))
16		fveq2 6876	. . . . . . . . . 10 ⊢ (𝑔 = ∅ → (𝑇‘𝑔) = (𝑇‘∅))
17	16	fveq1d 6878	. . . . . . . . 9 ⊢ (𝑔 = ∅ → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘∅)‘𝑚))
18	17	neeq1d 2991	. . . . . . . 8 ⊢ (𝑔 = ∅ → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘∅)‘𝑚) ≠ 0))
19	15, 18	raleqbidv 3325	. . . . . . 7 ⊢ (𝑔 = ∅ → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0))
20	13, 19	imbi12d 344	. . . . . 6 ⊢ (𝑔 = ∅ → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((∅ ≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)))
21		neeq1 2994	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (𝑔 ≠ ∅ ↔ 𝑒 ≠ ∅))
22		fveq1 6875	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (𝑔‘0) = (𝑒‘0))
23	22	neeq1d 2991	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → ((𝑔‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0))
24	21, 23	anbi12d 632	. . . . . . 7 ⊢ (𝑔 = 𝑒 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0)))
25		fveq2 6876	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (♯‘𝑔) = (♯‘𝑒))
26	25	oveq2d 7421	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (0..^(♯‘𝑔)) = (0..^(♯‘𝑒)))
27		fveq2 6876	. . . . . . . . . 10 ⊢ (𝑔 = 𝑒 → (𝑇‘𝑔) = (𝑇‘𝑒))
28	27	fveq1d 6878	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝑒)‘𝑚))
29	28	neeq1d 2991	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0))
30	26, 29	raleqbidv 3325	. . . . . . 7 ⊢ (𝑔 = 𝑒 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))
31	24, 30	imbi12d 344	. . . . . 6 ⊢ (𝑔 = 𝑒 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)))
32		neeq1 2994	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑔 ≠ ∅ ↔ (𝑒 ++ ⟨“𝑘”⟩) ≠ ∅))
33		fveq1 6875	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑔‘0) = ((𝑒 ++ ⟨“𝑘”⟩)‘0))
34	33	neeq1d 2991	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑔‘0) ≠ 0 ↔ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
35	32, 34	anbi12d 632	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)))
36		fveq2 6876	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (♯‘𝑔) = (♯‘(𝑒 ++ ⟨“𝑘”⟩)))
37	36	oveq2d 7421	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (0..^(♯‘𝑔)) = (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))
38		fveq2 6876	. . . . . . . . . 10 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑇‘𝑔) = (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)))
39	38	fveq1d 6878	. . . . . . . . 9 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚))
40	39	neeq1d 2991	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0))
41	37, 40	raleqbidv 3325	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0))
42	35, 41	imbi12d 344	. . . . . 6 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)))
43		neeq1 2994	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (𝑔 ≠ ∅ ↔ 𝐹 ≠ ∅))
44		fveq1 6875	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → (𝑔‘0) = (𝐹‘0))
45	44	neeq1d 2991	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → ((𝑔‘0) ≠ 0 ↔ (𝐹‘0) ≠ 0))
46	43, 45	anbi12d 632	. . . . . . 7 ⊢ (𝑔 = 𝐹 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)))
47		fveq2 6876	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → (♯‘𝑔) = (♯‘𝐹))
48	47	oveq2d 7421	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (0..^(♯‘𝑔)) = (0..^(♯‘𝐹)))
49		fveq2 6876	. . . . . . . . . 10 ⊢ (𝑔 = 𝐹 → (𝑇‘𝑔) = (𝑇‘𝐹))
50	49	fveq1d 6878	. . . . . . . . 9 ⊢ (𝑔 = 𝐹 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝐹)‘𝑚))
51	50	neeq1d 2991	. . . . . . . 8 ⊢ (𝑔 = 𝐹 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑚) ≠ 0))
52	48, 51	raleqbidv 3325	. . . . . . 7 ⊢ (𝑔 = 𝐹 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))
53	46, 52	imbi12d 344	. . . . . 6 ⊢ (𝑔 = 𝐹 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)))
54		neirr 2941	. . . . . . . 8 ⊢ ¬ ∅ ≠ ∅
55	54	intnanr 487	. . . . . . 7 ⊢ ¬ (∅ ≠ ∅ ∧ (∅‘0) ≠ 0)
56	55	pm2.21i 119	. . . . . 6 ⊢ ((∅ ≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)
57		fveq2 6876	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑚 → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘𝑚))
58	57	neeq1d 2991	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0))
59	58	cbvralvw 3220	. . . . . . . . . 10 ⊢ (∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)
60	59	imbi2i 336	. . . . . . . . 9 ⊢ (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))
61	60	anbi2i 623	. . . . . . . 8 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ↔ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)))
62		simplr 768	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → 𝑚 ∈ (0..^(♯‘𝑒)))
63		noel 4313	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑚 ∈ ∅
64		fveq2 6876	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ∅ → (♯‘𝑒) = (♯‘∅))
65		hash0 14385	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘∅) = 0
66	64, 65	eqtrdi 2786	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = ∅ → (♯‘𝑒) = 0)
67	66	oveq2d 7421	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = ∅ → (0..^(♯‘𝑒)) = (0..^0))
68		fzo0 13700	. . . . . . . . . . . . . . . 16 ⊢ (0..^0) = ∅
69	67, 68	eqtrdi 2786	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ∅ → (0..^(♯‘𝑒)) = ∅)
70	69	eleq2d 2820	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ∅ → (𝑚 ∈ (0..^(♯‘𝑒)) ↔ 𝑚 ∈ ∅))
71	63, 70	mtbiri 327	. . . . . . . . . . . . 13 ⊢ (𝑒 = ∅ → ¬ 𝑚 ∈ (0..^(♯‘𝑒)))
72	71	adantl 481	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → ¬ 𝑚 ∈ (0..^(♯‘𝑒)))
73	62, 72	pm2.21dd 195	. . . . . . . . . . 11 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
74		simp-6l 786	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ)
75		simp-6r 787	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ)
76		simplr 768	. . . . . . . . . . . . 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 34603	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘𝑒)‘𝑚))
82	74, 75, 76, 81	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘𝑒)‘𝑚))
83		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ≠ ∅)
84		simp-5l 784	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
85		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ (𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) ∧ 𝑚 ∈ (0..^(♯‘𝑒)) ∧ 𝑒 ≠ ∅)) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
86	85	3anassrs 1361	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
87		simpll 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ)
88		s1cl 14620	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → ⟨“𝑘”⟩ ∈ Word ℝ)
89	88	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ⟨“𝑘”⟩ ∈ Word ℝ)
90		lennncl 14552	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
91	90	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
92		fzo0end 13774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑒) ∈ ℕ → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
93		elfzolt3b 13688	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)) → 0 ∈ (0..^(♯‘𝑒)))
94	91, 92, 93	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 0 ∈ (0..^(♯‘𝑒)))
95		ccatval1 14595	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ ⟨“𝑘”⟩ ∈ Word ℝ ∧ 0 ∈ (0..^(♯‘𝑒))) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (𝑒‘0))
96	87, 89, 94, 95	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (𝑒‘0))
97	96	neeq1d 2991	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0))
98	97	biimpa 476	. . . . . . . . . . . . . . 15 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑒‘0) ≠ 0)
99	84, 83, 86, 98	syl21anc 837	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒‘0) ≠ 0)
100		simp-5r 785	. . . . . . . . . . . . . 14 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0))
101	83, 99, 100	mp2and 699	. . . . . . . . . . . . 13 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)
102	58, 101, 76	rspcdva 3602	. . . . . . . . . . . 12 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘𝑚) ≠ 0)
103	82, 102	eqnetrd 2999	. . . . . . . . . . 11 ⊢ (((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
104	73, 103	pm2.61dane 3019	. . . . . . . . . 10 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
105		simpr 484	. . . . . . . . . . . 12 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → 𝑚 = (♯‘𝑒))
106	105	fveq2d 6880	. . . . . . . . . . 11 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) = ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)))
107		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → 𝑒 = ∅)
108		simp-4r 783	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → 𝑘 ∈ ℝ)
109		simplrl 776	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
110	109	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
111		oveq1 7412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = ∅ → (𝑒 ++ ⟨“𝑘”⟩) = (∅ ++ ⟨“𝑘”⟩))
112		ccatlid 14604	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨“𝑘”⟩ ∈ Word ℝ → (∅ ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
113	88, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℝ → (∅ ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
114	111, 113	sylan9eq 2790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑒 ++ ⟨“𝑘”⟩) = ⟨“𝑘”⟩)
115	114	fveq2d 6880	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = (𝑇‘⟨“𝑘”⟩))
116	115	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = (𝑇‘⟨“𝑘”⟩))
117	77, 78, 79, 80	signstf0 34600	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ → (𝑇‘⟨“𝑘”⟩) = ⟨“(sgn‘𝑘)”⟩)
118	117	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘⟨“𝑘”⟩) = ⟨“(sgn‘𝑘)”⟩)
119	116, 118	eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (𝑇‘(𝑒 ++ ⟨“𝑘”⟩)) = ⟨“(sgn‘𝑘)”⟩)
120	66	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (♯‘𝑒) = 0)
121	119, 120	fveq12d 6883	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (⟨“(sgn‘𝑘)”⟩‘0))
122		sgnclre 32811	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → (sgn‘𝑘) ∈ ℝ)
123		s1fv 14628	. . . . . . . . . . . . . . . . . . 19 ⊢ ((sgn‘𝑘) ∈ ℝ → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
124	122, 123	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
125	124	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (⟨“(sgn‘𝑘)”⟩‘0) = (sgn‘𝑘))
126	121, 125	eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (sgn‘𝑘))
127		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → 𝑘 ∈ ℝ)
128	114	fveq1d 6878	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = (⟨“𝑘”⟩‘0))
129		s1fv 14628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℝ → (⟨“𝑘”⟩‘0) = 𝑘)
130	129	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (⟨“𝑘”⟩‘0) = 𝑘)
131	128, 130	eqtrd 2770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) = 𝑘)
132	131	neeq1d 2991	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0 ↔ 𝑘 ≠ 0))
133	132	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → 𝑘 ≠ 0)
134		rexr 11281	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ → 𝑘 ∈ ℝ^*)
135		sgn0bi 32819	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℝ^* → ((sgn‘𝑘) = 0 ↔ 𝑘 = 0))
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℝ → ((sgn‘𝑘) = 0 ↔ 𝑘 = 0))
137	136	necon3bid 2976	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ → ((sgn‘𝑘) ≠ 0 ↔ 𝑘 ≠ 0))
138	137	biimpar 477	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℝ ∧ 𝑘 ≠ 0) → (sgn‘𝑘) ≠ 0)
139	127, 133, 138	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → (sgn‘𝑘) ≠ 0)
140	126, 139	eqnetrd 2999	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
141	107, 108, 110, 140	syl21anc 837	. . . . . . . . . . . . . 14 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
142		eldifsn 4762	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 ∈ (Word ℝ ∖ {∅}) ↔ (𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅))
143	142	biimpri 228	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → 𝑒 ∈ (Word ℝ ∖ {∅}))
144	143	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ (Word ℝ ∖ {∅}))
145		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ)
146	77, 78, 79, 80	signstfvn 34601	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ (Word ℝ ∖ {∅}) ∧ 𝑘 ∈ ℝ) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
147	144, 145, 146	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)))
148	147	ad4ant14 752	. . . . . . . . . . . . . . 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 34597	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 ∈ Word ℝ ∧ ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒))) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
151	149, 150	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
152	151	ad5ant15 758	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1})
153		sgncl 32810	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ^* → (sgn‘𝑘) ∈ {-1, 0, 1})
154	134, 153	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℝ → (sgn‘𝑘) ∈ {-1, 0, 1})
155	154	ad4antlr 733	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (sgn‘𝑘) ∈ {-1, 0, 1})
156		fveq2 6876	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = ((♯‘𝑒) − 1) → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘((♯‘𝑒) − 1)))
157	156	neeq1d 2991	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = ((♯‘𝑒) − 1) → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0))
158		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → 𝑒 ≠ ∅)
159		simplll 774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ))
160		simplrl 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0))
161	160	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)
162	159, 158, 161, 98	syl21anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (𝑒‘0) ≠ 0)
163		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0))
164	158, 162, 163	mp2and 699	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)
165	90	ad4ant14 752	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (♯‘𝑒) ∈ ℕ)
166	165, 92	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
167	166	adantllr 719	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒)))
168	157, 164, 167	rspcdva 3602	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0)
169	77, 78	signswn0 34592	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1} ∧ (sgn‘𝑘) ∈ {-1, 0, 1}) ∧ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0)
170	152, 155, 168, 169	syl21anc 837	. . . . . . . . . . . . . . 15 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0)
171	148, 170	eqnetrd 2999	. . . . . . . . . . . . . 14 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
172	141, 171	pm2.61dane 3019	. . . . . . . . . . . . 13 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
173	172	anassrs 467	. . . . . . . . . . . 12 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
174	173	adantr 480	. . . . . . . . . . 11 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘(♯‘𝑒)) ≠ 0)
175	106, 174	eqnetrd 2999	. . . . . . . . . 10 ⊢ ((((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
176		lencl 14551	. . . . . . . . . . . . 13 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ ℕ₀)
177		nn0uz 12894	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
178	176, 177	eleqtrdi 2844	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ (ℤ_≥‘0))
179	178	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (♯‘𝑒) ∈ (ℤ_≥‘0))
180		ccatws1len 14638	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ Word ℝ → (♯‘(𝑒 ++ ⟨“𝑘”⟩)) = ((♯‘𝑒) + 1))
181	180	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (♯‘(𝑒 ++ ⟨“𝑘”⟩)) = ((♯‘𝑒) + 1))
182	181	oveq2d 7421	. . . . . . . . . . . . . 14 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) = (0..^((♯‘𝑒) + 1)))
183	182	eleq2d 2820	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩))) ↔ 𝑚 ∈ (0..^((♯‘𝑒) + 1))))
184	183	biimpa 476	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1)))
185	184	ad4ant14 752	. . . . . . . . . . 11 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1)))
186		fzosplitsni 13794	. . . . . . . . . . . 12 ⊢ ((♯‘𝑒) ∈ (ℤ_≥‘0) → (𝑚 ∈ (0..^((♯‘𝑒) + 1)) ↔ (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒))))
187	186	biimpa 476	. . . . . . . . . . 11 ⊢ (((♯‘𝑒) ∈ (ℤ_≥‘0) ∧ 𝑚 ∈ (0..^((♯‘𝑒) + 1))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒)))
188	179, 185, 187	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒)))
189	104, 175, 188	mpjaodan 960	. . . . . . . . 9 ⊢ (((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) ∧ 𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))) → ((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
190	189	ralrimiva 3132	. . . . . . . 8 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
191	61, 190	sylanbr 582	. . . . . . 7 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) ∧ ((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)
192	191	exp31 419	. . . . . 6 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0) → (((𝑒 ++ ⟨“𝑘”⟩) ≠ ∅ ∧ ((𝑒 ++ ⟨“𝑘”⟩)‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ ⟨“𝑘”⟩)))((𝑇‘(𝑒 ++ ⟨“𝑘”⟩))‘𝑚) ≠ 0)))
193	20, 31, 42, 53, 56, 192	wrdind 14740	. . . . 5 ⊢ (𝐹 ∈ Word ℝ → ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))
194	193	imp 406	. . . 4 ⊢ ((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)
195	194	adantr 480	. . 3 ⊢ (((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)
196		simpr 484	. . 3 ⊢ (((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^(♯‘𝐹)))
197	9, 195, 196	rspcdva 3602	. 2 ⊢ (((𝐹 ∈ Word ℝ ∧ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)
198	2, 6, 7, 197	syl21anc 837	1 ⊢ (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ≠ wne 2932 ∀wral 3051 ∖ cdif 3923 ∅c0 4308 ifcif 4500 {csn 4601 {cpr 4603 {ctp 4605 ⟨cop 4607 ↦ cmpt 5201 ‘cfv 6531 (class class class)co 7405 ∈ cmpo 7407 ℝcr 11128 0cc0 11129 1c1 11130 + caddc 11132 ℝ^*cxr 11268 − cmin 11466 -cneg 11467 ℕcn 12240 ℕ₀cn0 12501 ℤ_≥cuz 12852 ...cfz 13524 ..^cfzo 13671 ♯chash 14348 Word cword 14531 ++ cconcat 14588 ⟨“cs1 14613 sgncsgn 15105 Σcsu 15702 ndxcnx 17212 Basecbs 17228 +_gcplusg 17271 Σ_g cgsu 17454

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-supp 8160 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-er 8719 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-oi 9524 df-card 9953 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-nn 12241 df-2 12303 df-n0 12502 df-xnn0 12575 df-z 12589 df-uz 12853 df-fz 13525 df-fzo 13672 df-seq 14020 df-hash 14349 df-word 14532 df-lsw 14581 df-concat 14589 df-s1 14614 df-substr 14659 df-pfx 14689 df-sgn 15106 df-struct 17166 df-slot 17201 df-ndx 17213 df-base 17229 df-plusg 17284 df-0g 17455 df-gsum 17456 df-mgm 18618 df-sgrp 18697 df-mnd 18713 df-mulg 19051 df-cntz 19300

This theorem is referenced by: signstfvcl 34605

W3C validator