Step |
Hyp |
Ref |
Expression |
1 |
|
lencl |
|- ( A e. Word V -> ( # ` A ) e. NN0 ) |
2 |
|
elnnnn0b |
|- ( ( # ` A ) e. NN <-> ( ( # ` A ) e. NN0 /\ 0 < ( # ` A ) ) ) |
3 |
2
|
biimpri |
|- ( ( ( # ` A ) e. NN0 /\ 0 < ( # ` A ) ) -> ( # ` A ) e. NN ) |
4 |
1 3
|
sylan |
|- ( ( A e. Word V /\ 0 < ( # ` A ) ) -> ( # ` A ) e. NN ) |
5 |
|
lbfzo0 |
|- ( 0 e. ( 0 ..^ ( # ` A ) ) <-> ( # ` A ) e. NN ) |
6 |
4 5
|
sylibr |
|- ( ( A e. Word V /\ 0 < ( # ` A ) ) -> 0 e. ( 0 ..^ ( # ` A ) ) ) |
7 |
6
|
3adant2 |
|- ( ( A e. Word V /\ B e. Word V /\ 0 < ( # ` A ) ) -> 0 e. ( 0 ..^ ( # ` A ) ) ) |
8 |
|
ccatval1 |
|- ( ( A e. Word V /\ B e. Word V /\ 0 e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` 0 ) = ( A ` 0 ) ) |
9 |
7 8
|
syld3an3 |
|- ( ( A e. Word V /\ B e. Word V /\ 0 < ( # ` A ) ) -> ( ( A ++ B ) ` 0 ) = ( A ` 0 ) ) |