Metamath Proof Explorer

Theorem signstfvneq0

Description: In case the first letter is not zero, the zero skipping sign is never zero. (Contributed by Thierry Arnoux, 10-Oct-2018)

Ref Expression
Hypotheses 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 signstfvneq0 ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 signsv.p ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
2 signsv.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
3 signsv.t ⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) )
4 signsv.v ⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
5 simpll ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) )
6 5 eldifad ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ∈ Word ℝ )
7 eldifsni ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) → 𝐹 ≠ ∅ )
8 7 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ≠ ∅ )
9 simplr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 0 ) ≠ 0 )
10 8 9 jca ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ≠ ∅ ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) )
11 simpr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
12 fveq2 ⊢ ( 𝑚 = 𝑁 → ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) )
13 12 neeq1d ⊢ ( 𝑚 = 𝑁 → ( ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 ↔ ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 ) )
14 neeq1 ⊢ ( 𝑔 = ∅ → ( 𝑔 ≠ ∅ ↔ ∅ ≠ ∅ ) )
15 fveq1 ⊢ ( 𝑔 = ∅ → ( 𝑔 ‘ 0 ) = ( ∅ ‘ 0 ) )
16 15 neeq1d ⊢ ( 𝑔 = ∅ → ( ( 𝑔 ‘ 0 ) ≠ 0 ↔ ( ∅ ‘ 0 ) ≠ 0 ) )
17 14 16 anbi12d ⊢ ( 𝑔 = ∅ → ( ( 𝑔 ≠ ∅ ∧ ( 𝑔 ‘ 0 ) ≠ 0 ) ↔ ( ∅ ≠ ∅ ∧ ( ∅ ‘ 0 ) ≠ 0 ) ) )
18 fveq2 ⊢ ( 𝑔 = ∅ → ( ♯ ‘ 𝑔 ) = ( ♯ ‘ ∅ ) )
19 18 oveq2d ⊢ ( 𝑔 = ∅ → ( 0 ..^ ( ♯ ‘ 𝑔 ) ) = ( 0 ..^ ( ♯ ‘ ∅ ) ) )
20 fveq2 ⊢ ( 𝑔 = ∅ → ( 𝑇 ‘ 𝑔 ) = ( 𝑇 ‘ ∅ ) )
21 20 fveq1d ⊢ ( 𝑔 = ∅ → ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) = ( ( 𝑇 ‘ ∅ ) ‘ 𝑚 ) )
22 21 neeq1d ⊢ ( 𝑔 = ∅ → ( ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ↔ ( ( 𝑇 ‘ ∅ ) ‘ 𝑚 ) ≠ 0 ) )
23 19 22 raleqbidv ⊢ ( 𝑔 = ∅ → ( ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ↔ ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ( 𝑇 ‘ ∅ ) ‘ 𝑚 ) ≠ 0 ) )
24 17 23 imbi12d ⊢ ( 𝑔 = ∅ → ( ( ( 𝑔 ≠ ∅ ∧ ( 𝑔 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ) ↔ ( ( ∅ ≠ ∅ ∧ ( ∅ ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ( 𝑇 ‘ ∅ ) ‘ 𝑚 ) ≠ 0 ) ) )
25 neeq1 ⊢ ( 𝑔 = 𝑒 → ( 𝑔 ≠ ∅ ↔ 𝑒 ≠ ∅ ) )
26 fveq1 ⊢ ( 𝑔 = 𝑒 → ( 𝑔 ‘ 0 ) = ( 𝑒 ‘ 0 ) )
27 26 neeq1d ⊢ ( 𝑔 = 𝑒 → ( ( 𝑔 ‘ 0 ) ≠ 0 ↔ ( 𝑒 ‘ 0 ) ≠ 0 ) )
28 25 27 anbi12d ⊢ ( 𝑔 = 𝑒 → ( ( 𝑔 ≠ ∅ ∧ ( 𝑔 ‘ 0 ) ≠ 0 ) ↔ ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) ) )
29 fveq2 ⊢ ( 𝑔 = 𝑒 → ( ♯ ‘ 𝑔 ) = ( ♯ ‘ 𝑒 ) )
30 29 oveq2d ⊢ ( 𝑔 = 𝑒 → ( 0 ..^ ( ♯ ‘ 𝑔 ) ) = ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
31 fveq2 ⊢ ( 𝑔 = 𝑒 → ( 𝑇 ‘ 𝑔 ) = ( 𝑇 ‘ 𝑒 ) )
32 31 fveq1d ⊢ ( 𝑔 = 𝑒 → ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) = ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) )
33 32 neeq1d ⊢ ( 𝑔 = 𝑒 → ( ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ↔ ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) ≠ 0 ) )
34 30 33 raleqbidv ⊢ ( 𝑔 = 𝑒 → ( ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ↔ ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) ≠ 0 ) )
35 28 34 imbi12d ⊢ ( 𝑔 = 𝑒 → ( ( ( 𝑔 ≠ ∅ ∧ ( 𝑔 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ) ↔ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) ≠ 0 ) ) )
36 neeq1 ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( 𝑔 ≠ ∅ ↔ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ) )
37 fveq1 ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( 𝑔 ‘ 0 ) = ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) )
38 37 neeq1d ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( ( 𝑔 ‘ 0 ) ≠ 0 ↔ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) )
39 36 38 anbi12d ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( ( 𝑔 ≠ ∅ ∧ ( 𝑔 ‘ 0 ) ≠ 0 ) ↔ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) )
40 fveq2 ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( ♯ ‘ 𝑔 ) = ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) )
41 40 oveq2d ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( 0 ..^ ( ♯ ‘ 𝑔 ) ) = ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) )
42 fveq2 ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( 𝑇 ‘ 𝑔 ) = ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) )
43 42 fveq1d ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) = ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) )
44 43 neeq1d ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ↔ ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 ) )
45 41 44 raleqbidv ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ↔ ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 ) )
46 39 45 imbi12d ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( ( ( 𝑔 ≠ ∅ ∧ ( 𝑔 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ) ↔ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 ) ) )
47 neeq1 ⊢ ( 𝑔 = 𝐹 → ( 𝑔 ≠ ∅ ↔ 𝐹 ≠ ∅ ) )
48 fveq1 ⊢ ( 𝑔 = 𝐹 → ( 𝑔 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
49 48 neeq1d ⊢ ( 𝑔 = 𝐹 → ( ( 𝑔 ‘ 0 ) ≠ 0 ↔ ( 𝐹 ‘ 0 ) ≠ 0 ) )
50 47 49 anbi12d ⊢ ( 𝑔 = 𝐹 → ( ( 𝑔 ≠ ∅ ∧ ( 𝑔 ‘ 0 ) ≠ 0 ) ↔ ( 𝐹 ≠ ∅ ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ) )
51 fveq2 ⊢ ( 𝑔 = 𝐹 → ( ♯ ‘ 𝑔 ) = ( ♯ ‘ 𝐹 ) )
52 51 oveq2d ⊢ ( 𝑔 = 𝐹 → ( 0 ..^ ( ♯ ‘ 𝑔 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
53 fveq2 ⊢ ( 𝑔 = 𝐹 → ( 𝑇 ‘ 𝑔 ) = ( 𝑇 ‘ 𝐹 ) )
54 53 fveq1d ⊢ ( 𝑔 = 𝐹 → ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) )
55 54 neeq1d ⊢ ( 𝑔 = 𝐹 → ( ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ↔ ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 ) )
56 52 55 raleqbidv ⊢ ( 𝑔 = 𝐹 → ( ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ↔ ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 ) )
57 50 56 imbi12d ⊢ ( 𝑔 = 𝐹 → ( ( ( 𝑔 ≠ ∅ ∧ ( 𝑔 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑔 ) ) ( ( 𝑇 ‘ 𝑔 ) ‘ 𝑚 ) ≠ 0 ) ↔ ( ( 𝐹 ≠ ∅ ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 ) ) )
58 neirr ⊢ ¬ ∅ ≠ ∅
59 58 intnanr ⊢ ¬ ( ∅ ≠ ∅ ∧ ( ∅ ‘ 0 ) ≠ 0 )
60 59 pm2.21i ⊢ ( ( ∅ ≠ ∅ ∧ ( ∅ ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ( ( 𝑇 ‘ ∅ ) ‘ 𝑚 ) ≠ 0 )
61 fveq2 ⊢ ( 𝑛 = 𝑚 → ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) )
62 61 neeq1d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ↔ ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) ≠ 0 ) )
63 62 cbvralvw ⊢ ( ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ↔ ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) ≠ 0 )
64 63 imbi2i ⊢ ( ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ↔ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) ≠ 0 ) )
65 64 anbi2i ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ↔ ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) ≠ 0 ) ) )
66 simplr ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 = ∅ ) → 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
67 noel ⊢ ¬ 𝑚 ∈ ∅
68 fveq2 ⊢ ( 𝑒 = ∅ → ( ♯ ‘ 𝑒 ) = ( ♯ ‘ ∅ ) )
69 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
70 68 69 eqtrdi ⊢ ( 𝑒 = ∅ → ( ♯ ‘ 𝑒 ) = 0 )
71 70 oveq2d ⊢ ( 𝑒 = ∅ → ( 0 ..^ ( ♯ ‘ 𝑒 ) ) = ( 0 ..^ 0 ) )
72 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
73 71 72 eqtrdi ⊢ ( 𝑒 = ∅ → ( 0 ..^ ( ♯ ‘ 𝑒 ) ) = ∅ )
74 73 eleq2d ⊢ ( 𝑒 = ∅ → ( 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ↔ 𝑚 ∈ ∅ ) )
75 67 74 mtbiri ⊢ ( 𝑒 = ∅ → ¬ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
76 75 adantl ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 = ∅ ) → ¬ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
77 66 76 pm2.21dd ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 = ∅ ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 )
78 simp-6l ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → 𝑒 ∈ Word ℝ )
79 simp-6r ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → 𝑘 ∈ ℝ )
80 simplr ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
81 1 2 3 4 signstfvp ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) = ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) )
82 78 79 80 81 syl3anc ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) = ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) )
83 simpr ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → 𝑒 ≠ ∅ )
84 simp-5l ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) )
85 simplrr ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ ( 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ∧ 𝑒 ≠ ∅ ) ) → ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 )
86 85 3anassrs ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 )
87 simpll ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑒 ≠ ∅ ) → 𝑒 ∈ Word ℝ )
88 s1cl ⊢ ( 𝑘 ∈ ℝ → ⟨“ 𝑘 ”⟩ ∈ Word ℝ )
89 88 ad2antlr ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑒 ≠ ∅ ) → ⟨“ 𝑘 ”⟩ ∈ Word ℝ )
90 lennncl ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅ ) → ( ♯ ‘ 𝑒 ) ∈ ℕ )
91 90 adantlr ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑒 ≠ ∅ ) → ( ♯ ‘ 𝑒 ) ∈ ℕ )
92 fzo0end ⊢ ( ( ♯ ‘ 𝑒 ) ∈ ℕ → ( ( ♯ ‘ 𝑒 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
93 elfzolt3b ⊢ ( ( ( ♯ ‘ 𝑒 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
94 91 92 93 3syl ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑒 ≠ ∅ ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
95 ccatval1 ⊢ ( ( 𝑒 ∈ Word ℝ ∧ ⟨“ 𝑘 ”⟩ ∈ Word ℝ ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) → ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) = ( 𝑒 ‘ 0 ) )
96 87 89 94 95 syl3anc ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) = ( 𝑒 ‘ 0 ) )
97 96 neeq1d ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑒 ≠ ∅ ) → ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ↔ ( 𝑒 ‘ 0 ) ≠ 0 ) )
98 97 biimpa ⊢ ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑒 ≠ ∅ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ( 𝑒 ‘ 0 ) ≠ 0 )
99 84 83 86 98 syl21anc ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → ( 𝑒 ‘ 0 ) ≠ 0 )
100 simp-5r ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) )
101 83 99 100 mp2and ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 )
102 62 101 80 rspcdva ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) ≠ 0 )
103 82 102 eqnetrd ⊢ ( ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 )
104 77 103 pm2.61dane ⊢ ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 )
105 simpr ⊢ ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 = ( ♯ ‘ 𝑒 ) ) → 𝑚 = ( ♯ ‘ 𝑒 ) )
106 105 fveq2d ⊢ ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 = ( ♯ ‘ 𝑒 ) ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) = ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) )
107 simpr ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 = ∅ ) → 𝑒 = ∅ )
108 simp-4r ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 = ∅ ) → 𝑘 ∈ ℝ )
109 simplrl ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 = ∅ ) → ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) )
110 109 simprd ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 = ∅ ) → ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 )
111 oveq1 ⊢ ( 𝑒 = ∅ → ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) = ( ∅ ++ ⟨“ 𝑘 ”⟩ ) )
112 ccatlid ⊢ ( ⟨“ 𝑘 ”⟩ ∈ Word ℝ → ( ∅ ++ ⟨“ 𝑘 ”⟩ ) = ⟨“ 𝑘 ”⟩ )
113 88 112 syl ⊢ ( 𝑘 ∈ ℝ → ( ∅ ++ ⟨“ 𝑘 ”⟩ ) = ⟨“ 𝑘 ”⟩ )
114 111 113 sylan9eq ⊢ ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) → ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) = ⟨“ 𝑘 ”⟩ )
115 114 fveq2d ⊢ ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) → ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) = ( 𝑇 ‘ ⟨“ 𝑘 ”⟩ ) )
116 115 adantr ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) = ( 𝑇 ‘ ⟨“ 𝑘 ”⟩ ) )
117 1 2 3 4 signstf0 ⊢ ( 𝑘 ∈ ℝ → ( 𝑇 ‘ ⟨“ 𝑘 ”⟩ ) = ⟨“ ( sgn ‘ 𝑘 ) ”⟩ )
118 117 ad2antlr ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ( 𝑇 ‘ ⟨“ 𝑘 ”⟩ ) = ⟨“ ( sgn ‘ 𝑘 ) ”⟩ )
119 116 118 eqtrd ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) = ⟨“ ( sgn ‘ 𝑘 ) ”⟩ )
120 70 ad2antrr ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ( ♯ ‘ 𝑒 ) = 0 )
121 119 120 fveq12d ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) = ( ⟨“ ( sgn ‘ 𝑘 ) ”⟩ ‘ 0 ) )
122 sgnclre ⊢ ( 𝑘 ∈ ℝ → ( sgn ‘ 𝑘 ) ∈ ℝ )
123 s1fv ⊢ ( ( sgn ‘ 𝑘 ) ∈ ℝ → ( ⟨“ ( sgn ‘ 𝑘 ) ”⟩ ‘ 0 ) = ( sgn ‘ 𝑘 ) )
124 122 123 syl ⊢ ( 𝑘 ∈ ℝ → ( ⟨“ ( sgn ‘ 𝑘 ) ”⟩ ‘ 0 ) = ( sgn ‘ 𝑘 ) )
125 124 ad2antlr ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ( ⟨“ ( sgn ‘ 𝑘 ) ”⟩ ‘ 0 ) = ( sgn ‘ 𝑘 ) )
126 121 125 eqtrd ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) = ( sgn ‘ 𝑘 ) )
127 simplr ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → 𝑘 ∈ ℝ )
128 114 fveq1d ⊢ ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) → ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) = ( ⟨“ 𝑘 ”⟩ ‘ 0 ) )
129 s1fv ⊢ ( 𝑘 ∈ ℝ → ( ⟨“ 𝑘 ”⟩ ‘ 0 ) = 𝑘 )
130 129 adantl ⊢ ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) → ( ⟨“ 𝑘 ”⟩ ‘ 0 ) = 𝑘 )
131 128 130 eqtrd ⊢ ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) → ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) = 𝑘 )
132 131 neeq1d ⊢ ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) → ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ↔ 𝑘 ≠ 0 ) )
133 132 biimpa ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → 𝑘 ≠ 0 )
134 rexr ⊢ ( 𝑘 ∈ ℝ → 𝑘 ∈ ℝ* )
135 sgn0bi ⊢ ( 𝑘 ∈ ℝ* → ( ( sgn ‘ 𝑘 ) = 0 ↔ 𝑘 = 0 ) )
136 134 135 syl ⊢ ( 𝑘 ∈ ℝ → ( ( sgn ‘ 𝑘 ) = 0 ↔ 𝑘 = 0 ) )
137 136 necon3bid ⊢ ( 𝑘 ∈ ℝ → ( ( sgn ‘ 𝑘 ) ≠ 0 ↔ 𝑘 ≠ 0 ) )
138 137 biimpar ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑘 ≠ 0 ) → ( sgn ‘ 𝑘 ) ≠ 0 )
139 127 133 138 syl2anc ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ( sgn ‘ 𝑘 ) ≠ 0 )
140 126 139 eqnetrd ⊢ ( ( ( 𝑒 = ∅ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) ≠ 0 )
141 107 108 110 140 syl21anc ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 = ∅ ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) ≠ 0 )
142 eldifsn ⊢ ( 𝑒 ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( 𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅ ) )
143 142 biimpri ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅ ) → 𝑒 ∈ ( Word ℝ ∖ { ∅ } ) )
144 143 adantlr ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑒 ≠ ∅ ) → 𝑒 ∈ ( Word ℝ ∖ { ∅ } ) )
145 simplr ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑒 ≠ ∅ ) → 𝑘 ∈ ℝ )
146 1 2 3 4 signstfvn ⊢ ( ( 𝑒 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝑘 ∈ ℝ ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) = ( ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ⨣ ( sgn ‘ 𝑘 ) ) )
147 144 145 146 syl2anc ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) = ( ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ⨣ ( sgn ‘ 𝑘 ) ) )
148 147 ad4ant14 ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) = ( ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ⨣ ( sgn ‘ 𝑘 ) ) )
149 90 92 syl ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅ ) → ( ( ♯ ‘ 𝑒 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
150 1 2 3 4 signstcl ⊢ ( ( 𝑒 ∈ Word ℝ ∧ ( ( ♯ ‘ 𝑒 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ) → ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ∈ { - 1 , 0 , 1 } )
151 149 150 syldan ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅ ) → ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ∈ { - 1 , 0 , 1 } )
152 151 ad5ant15 ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ∈ { - 1 , 0 , 1 } )
153 sgncl ⊢ ( 𝑘 ∈ ℝ* → ( sgn ‘ 𝑘 ) ∈ { - 1 , 0 , 1 } )
154 134 153 syl ⊢ ( 𝑘 ∈ ℝ → ( sgn ‘ 𝑘 ) ∈ { - 1 , 0 , 1 } )
155 154 ad4antlr ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( sgn ‘ 𝑘 ) ∈ { - 1 , 0 , 1 } )
156 fveq2 ⊢ ( 𝑛 = ( ( ♯ ‘ 𝑒 ) − 1 ) → ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) = ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) )
157 156 neeq1d ⊢ ( 𝑛 = ( ( ♯ ‘ 𝑒 ) − 1 ) → ( ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ↔ ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ≠ 0 ) )
158 simpr ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → 𝑒 ≠ ∅ )
159 simplll ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) )
160 simplrl ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) )
161 160 simprd ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 )
162 159 158 161 98 syl21anc ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( 𝑒 ‘ 0 ) ≠ 0 )
163 simpllr ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) )
164 158 162 163 mp2and ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 )
165 90 ad4ant14 ⊢ ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ♯ ‘ 𝑒 ) ∈ ℕ )
166 165 92 syl ⊢ ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( ♯ ‘ 𝑒 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
167 166 adantllr ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( ♯ ‘ 𝑒 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) )
168 157 164 167 rspcdva ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ≠ 0 )
169 1 2 signswn0 ⊢ ( ( ( ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ∈ { - 1 , 0 , 1 } ∧ ( sgn ‘ 𝑘 ) ∈ { - 1 , 0 , 1 } ) ∧ ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ≠ 0 ) → ( ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ⨣ ( sgn ‘ 𝑘 ) ) ≠ 0 )
170 152 155 168 169 syl21anc ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( ( 𝑇 ‘ 𝑒 ) ‘ ( ( ♯ ‘ 𝑒 ) − 1 ) ) ⨣ ( sgn ‘ 𝑘 ) ) ≠ 0 )
171 148 170 eqnetrd ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) ∧ 𝑒 ≠ ∅ ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) ≠ 0 )
172 141 171 pm2.61dane ⊢ ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) ≠ 0 )
173 172 anassrs ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) ≠ 0 )
174 173 adantr ⊢ ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 = ( ♯ ‘ 𝑒 ) ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ ( ♯ ‘ 𝑒 ) ) ≠ 0 )
175 106 174 eqnetrd ⊢ ( ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) ∧ 𝑚 = ( ♯ ‘ 𝑒 ) ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 )
176 lencl ⊢ ( 𝑒 ∈ Word ℝ → ( ♯ ‘ 𝑒 ) ∈ ℕ0 )
177 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
178 176 177 eleqtrdi ⊢ ( 𝑒 ∈ Word ℝ → ( ♯ ‘ 𝑒 ) ∈ ( ℤ≥ ‘ 0 ) )
179 178 ad4antr ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) → ( ♯ ‘ 𝑒 ) ∈ ( ℤ≥ ‘ 0 ) )
180 ccatws1len ⊢ ( 𝑒 ∈ Word ℝ → ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) = ( ( ♯ ‘ 𝑒 ) + 1 ) )
181 180 adantr ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) → ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) = ( ( ♯ ‘ 𝑒 ) + 1 ) )
182 181 oveq2d ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) → ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑒 ) + 1 ) ) )
183 182 eleq2d ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ↔ 𝑚 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑒 ) + 1 ) ) ) )
184 183 biimpa ⊢ ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) → 𝑚 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑒 ) + 1 ) ) )
185 184 ad4ant14 ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) → 𝑚 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑒 ) + 1 ) ) )
186 fzosplitsni ⊢ ( ( ♯ ‘ 𝑒 ) ∈ ( ℤ≥ ‘ 0 ) → ( 𝑚 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑒 ) + 1 ) ) ↔ ( 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ∨ 𝑚 = ( ♯ ‘ 𝑒 ) ) ) )
187 186 biimpa ⊢ ( ( ( ♯ ‘ 𝑒 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑚 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑒 ) + 1 ) ) ) → ( 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ∨ 𝑚 = ( ♯ ‘ 𝑒 ) ) )
188 179 185 187 syl2anc ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) → ( 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ∨ 𝑚 = ( ♯ ‘ 𝑒 ) ) )
189 104 175 188 mpjaodan ⊢ ( ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ) → ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 )
190 189 ralrimiva ⊢ ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑛 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 )
191 65 190 sylanbr ⊢ ( ( ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ∧ ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) ≠ 0 ) ) ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 )
192 191 exp31 ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) → ( ( ( 𝑒 ≠ ∅ ∧ ( 𝑒 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝑒 ) ) ( ( 𝑇 ‘ 𝑒 ) ‘ 𝑚 ) ≠ 0 ) → ( ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ≠ ∅ ∧ ( ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ( ( 𝑇 ‘ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑚 ) ≠ 0 ) ) )
193 24 35 46 57 60 192 wrdind ⊢ ( 𝐹 ∈ Word ℝ → ( ( 𝐹 ≠ ∅ ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 ) )
194 193 imp ⊢ ( ( 𝐹 ∈ Word ℝ ∧ ( 𝐹 ≠ ∅ ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 )
195 194 adantr ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ ( 𝐹 ≠ ∅ ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ∀ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) ≠ 0 )
196 simpr ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ ( 𝐹 ≠ ∅ ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
197 13 195 196 rspcdva ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ ( 𝐹 ≠ ∅ ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 )
198 6 10 11 197 syl21anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ≠ 0 )