| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pthd.p |
|- ( ph -> P e. Word _V ) |
| 2 |
|
pthd.r |
|- R = ( ( # ` P ) - 1 ) |
| 3 |
|
pthd.s |
|- ( ph -> A. i e. ( 0 ..^ ( # ` P ) ) A. j e. ( 1 ..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) ) |
| 4 |
|
lencl |
|- ( P e. Word _V -> ( # ` P ) e. NN0 ) |
| 5 |
|
df-ne |
|- ( ( # ` P ) =/= 0 <-> -. ( # ` P ) = 0 ) |
| 6 |
|
elnnne0 |
|- ( ( # ` P ) e. NN <-> ( ( # ` P ) e. NN0 /\ ( # ` P ) =/= 0 ) ) |
| 7 |
6
|
simplbi2 |
|- ( ( # ` P ) e. NN0 -> ( ( # ` P ) =/= 0 -> ( # ` P ) e. NN ) ) |
| 8 |
5 7
|
biimtrrid |
|- ( ( # ` P ) e. NN0 -> ( -. ( # ` P ) = 0 -> ( # ` P ) e. NN ) ) |
| 9 |
1 4 8
|
3syl |
|- ( ph -> ( -. ( # ` P ) = 0 -> ( # ` P ) e. NN ) ) |
| 10 |
|
eqid |
|- 0 = 0 |
| 11 |
10
|
orci |
|- ( 0 = 0 \/ 0 = R ) |
| 12 |
1 2 3
|
pthdlem2lem |
|- ( ( ph /\ ( # ` P ) e. NN /\ ( 0 = 0 \/ 0 = R ) ) -> ( P ` 0 ) e/ ( P " ( 1 ..^ R ) ) ) |
| 13 |
11 12
|
mp3an3 |
|- ( ( ph /\ ( # ` P ) e. NN ) -> ( P ` 0 ) e/ ( P " ( 1 ..^ R ) ) ) |
| 14 |
|
eqid |
|- R = R |
| 15 |
14
|
olci |
|- ( R = 0 \/ R = R ) |
| 16 |
1 2 3
|
pthdlem2lem |
|- ( ( ph /\ ( # ` P ) e. NN /\ ( R = 0 \/ R = R ) ) -> ( P ` R ) e/ ( P " ( 1 ..^ R ) ) ) |
| 17 |
15 16
|
mp3an3 |
|- ( ( ph /\ ( # ` P ) e. NN ) -> ( P ` R ) e/ ( P " ( 1 ..^ R ) ) ) |
| 18 |
|
wrdffz |
|- ( P e. Word _V -> P : ( 0 ... ( ( # ` P ) - 1 ) ) --> _V ) |
| 19 |
1 18
|
syl |
|- ( ph -> P : ( 0 ... ( ( # ` P ) - 1 ) ) --> _V ) |
| 20 |
19
|
adantr |
|- ( ( ph /\ ( # ` P ) e. NN ) -> P : ( 0 ... ( ( # ` P ) - 1 ) ) --> _V ) |
| 21 |
2
|
oveq2i |
|- ( 0 ... R ) = ( 0 ... ( ( # ` P ) - 1 ) ) |
| 22 |
21
|
feq2i |
|- ( P : ( 0 ... R ) --> _V <-> P : ( 0 ... ( ( # ` P ) - 1 ) ) --> _V ) |
| 23 |
20 22
|
sylibr |
|- ( ( ph /\ ( # ` P ) e. NN ) -> P : ( 0 ... R ) --> _V ) |
| 24 |
|
nnm1nn0 |
|- ( ( # ` P ) e. NN -> ( ( # ` P ) - 1 ) e. NN0 ) |
| 25 |
2 24
|
eqeltrid |
|- ( ( # ` P ) e. NN -> R e. NN0 ) |
| 26 |
25
|
adantl |
|- ( ( ph /\ ( # ` P ) e. NN ) -> R e. NN0 ) |
| 27 |
|
fvinim0ffz |
|- ( ( P : ( 0 ... R ) --> _V /\ R e. NN0 ) -> ( ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) <-> ( ( P ` 0 ) e/ ( P " ( 1 ..^ R ) ) /\ ( P ` R ) e/ ( P " ( 1 ..^ R ) ) ) ) ) |
| 28 |
23 26 27
|
syl2anc |
|- ( ( ph /\ ( # ` P ) e. NN ) -> ( ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) <-> ( ( P ` 0 ) e/ ( P " ( 1 ..^ R ) ) /\ ( P ` R ) e/ ( P " ( 1 ..^ R ) ) ) ) ) |
| 29 |
13 17 28
|
mpbir2and |
|- ( ( ph /\ ( # ` P ) e. NN ) -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) ) |
| 30 |
29
|
ex |
|- ( ph -> ( ( # ` P ) e. NN -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) ) ) |
| 31 |
9 30
|
syld |
|- ( ph -> ( -. ( # ` P ) = 0 -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) ) ) |
| 32 |
|
oveq1 |
|- ( ( # ` P ) = 0 -> ( ( # ` P ) - 1 ) = ( 0 - 1 ) ) |
| 33 |
2 32
|
eqtrid |
|- ( ( # ` P ) = 0 -> R = ( 0 - 1 ) ) |
| 34 |
33
|
oveq2d |
|- ( ( # ` P ) = 0 -> ( 1 ..^ R ) = ( 1 ..^ ( 0 - 1 ) ) ) |
| 35 |
|
0le2 |
|- 0 <_ 2 |
| 36 |
|
1p1e2 |
|- ( 1 + 1 ) = 2 |
| 37 |
35 36
|
breqtrri |
|- 0 <_ ( 1 + 1 ) |
| 38 |
|
0re |
|- 0 e. RR |
| 39 |
|
1re |
|- 1 e. RR |
| 40 |
38 39 39
|
lesubadd2i |
|- ( ( 0 - 1 ) <_ 1 <-> 0 <_ ( 1 + 1 ) ) |
| 41 |
37 40
|
mpbir |
|- ( 0 - 1 ) <_ 1 |
| 42 |
|
1z |
|- 1 e. ZZ |
| 43 |
|
0z |
|- 0 e. ZZ |
| 44 |
|
peano2zm |
|- ( 0 e. ZZ -> ( 0 - 1 ) e. ZZ ) |
| 45 |
43 44
|
ax-mp |
|- ( 0 - 1 ) e. ZZ |
| 46 |
|
fzon |
|- ( ( 1 e. ZZ /\ ( 0 - 1 ) e. ZZ ) -> ( ( 0 - 1 ) <_ 1 <-> ( 1 ..^ ( 0 - 1 ) ) = (/) ) ) |
| 47 |
42 45 46
|
mp2an |
|- ( ( 0 - 1 ) <_ 1 <-> ( 1 ..^ ( 0 - 1 ) ) = (/) ) |
| 48 |
41 47
|
mpbi |
|- ( 1 ..^ ( 0 - 1 ) ) = (/) |
| 49 |
34 48
|
eqtrdi |
|- ( ( # ` P ) = 0 -> ( 1 ..^ R ) = (/) ) |
| 50 |
49
|
imaeq2d |
|- ( ( # ` P ) = 0 -> ( P " ( 1 ..^ R ) ) = ( P " (/) ) ) |
| 51 |
|
ima0 |
|- ( P " (/) ) = (/) |
| 52 |
50 51
|
eqtrdi |
|- ( ( # ` P ) = 0 -> ( P " ( 1 ..^ R ) ) = (/) ) |
| 53 |
52
|
ineq2d |
|- ( ( # ` P ) = 0 -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = ( ( P " { 0 , R } ) i^i (/) ) ) |
| 54 |
|
in0 |
|- ( ( P " { 0 , R } ) i^i (/) ) = (/) |
| 55 |
53 54
|
eqtrdi |
|- ( ( # ` P ) = 0 -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) ) |
| 56 |
31 55
|
pm2.61d2 |
|- ( ph -> ( ( P " { 0 , R } ) i^i ( P " ( 1 ..^ R ) ) ) = (/) ) |