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 
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
signsv.w 
|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
signsv.t 
|- T = ( f e. Word RR |-> ( n e. ( 0 ..^ ( # ` f ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( f ` i ) ) ) ) ) )
signsv.v 
|- V = ( f e. Word RR |-> sum_ j e. ( 1 ..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )
Assertion signstfvneq0 
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) =/= 0 )

Proof

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