Metamath Proof Explorer


Theorem 4fvwrd4

Description: The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017)

Ref Expression
Assertion 4fvwrd4 L 3 P : 0 L V a V b V c V d V P 0 = a P 1 = b P 2 = c P 3 = d

Proof

Step Hyp Ref Expression
1 simpr L 3 P : 0 L V P : 0 L V
2 0nn0 0 0
3 elnn0uz 0 0 0 0
4 2 3 mpbi 0 0
5 3nn0 3 0
6 elnn0uz 3 0 3 0
7 5 6 mpbi 3 0
8 uzss 3 0 3 0
9 7 8 ax-mp 3 0
10 9 sseli L 3 L 0
11 eluzfz 0 0 L 0 0 0 L
12 4 10 11 sylancr L 3 0 0 L
13 12 adantr L 3 P : 0 L V 0 0 L
14 1 13 ffvelrnd L 3 P : 0 L V P 0 V
15 clel5 P 0 V a V P 0 = a
16 14 15 sylib L 3 P : 0 L V a V P 0 = a
17 1eluzge0 1 0
18 1z 1
19 3z 3
20 1le3 1 3
21 eluz2 3 1 1 3 1 3
22 18 19 20 21 mpbir3an 3 1
23 uzss 3 1 3 1
24 22 23 ax-mp 3 1
25 24 sseli L 3 L 1
26 eluzfz 1 0 L 1 1 0 L
27 17 25 26 sylancr L 3 1 0 L
28 27 adantr L 3 P : 0 L V 1 0 L
29 1 28 ffvelrnd L 3 P : 0 L V P 1 V
30 clel5 P 1 V b V P 1 = b
31 29 30 sylib L 3 P : 0 L V b V P 1 = b
32 16 31 jca L 3 P : 0 L V a V P 0 = a b V P 1 = b
33 2eluzge0 2 0
34 uzuzle23 L 3 L 2
35 eluzfz 2 0 L 2 2 0 L
36 33 34 35 sylancr L 3 2 0 L
37 36 adantr L 3 P : 0 L V 2 0 L
38 1 37 ffvelrnd L 3 P : 0 L V P 2 V
39 clel5 P 2 V c V P 2 = c
40 38 39 sylib L 3 P : 0 L V c V P 2 = c
41 eluzfz 3 0 L 3 3 0 L
42 7 41 mpan L 3 3 0 L
43 42 adantr L 3 P : 0 L V 3 0 L
44 1 43 ffvelrnd L 3 P : 0 L V P 3 V
45 clel5 P 3 V d V P 3 = d
46 44 45 sylib L 3 P : 0 L V d V P 3 = d
47 32 40 46 jca32 L 3 P : 0 L V a V P 0 = a b V P 1 = b c V P 2 = c d V P 3 = d
48 r19.42v d V P 0 = a P 1 = b P 2 = c P 3 = d P 0 = a P 1 = b d V P 2 = c P 3 = d
49 r19.42v d V P 2 = c P 3 = d P 2 = c d V P 3 = d
50 49 anbi2i P 0 = a P 1 = b d V P 2 = c P 3 = d P 0 = a P 1 = b P 2 = c d V P 3 = d
51 48 50 bitri d V P 0 = a P 1 = b P 2 = c P 3 = d P 0 = a P 1 = b P 2 = c d V P 3 = d
52 51 rexbii c V d V P 0 = a P 1 = b P 2 = c P 3 = d c V P 0 = a P 1 = b P 2 = c d V P 3 = d
53 52 2rexbii a V b V c V d V P 0 = a P 1 = b P 2 = c P 3 = d a V b V c V P 0 = a P 1 = b P 2 = c d V P 3 = d
54 r19.42v c V P 0 = a P 1 = b P 2 = c d V P 3 = d P 0 = a P 1 = b c V P 2 = c d V P 3 = d
55 r19.41v c V P 2 = c d V P 3 = d c V P 2 = c d V P 3 = d
56 55 anbi2i P 0 = a P 1 = b c V P 2 = c d V P 3 = d P 0 = a P 1 = b c V P 2 = c d V P 3 = d
57 54 56 bitri c V P 0 = a P 1 = b P 2 = c d V P 3 = d P 0 = a P 1 = b c V P 2 = c d V P 3 = d
58 57 2rexbii a V b V c V P 0 = a P 1 = b P 2 = c d V P 3 = d a V b V P 0 = a P 1 = b c V P 2 = c d V P 3 = d
59 r19.41v b V P 0 = a P 1 = b c V P 2 = c d V P 3 = d b V P 0 = a P 1 = b c V P 2 = c d V P 3 = d
60 r19.42v b V P 0 = a P 1 = b P 0 = a b V P 1 = b
61 60 anbi1i b V P 0 = a P 1 = b c V P 2 = c d V P 3 = d P 0 = a b V P 1 = b c V P 2 = c d V P 3 = d
62 59 61 bitri b V P 0 = a P 1 = b c V P 2 = c d V P 3 = d P 0 = a b V P 1 = b c V P 2 = c d V P 3 = d
63 62 rexbii a V b V P 0 = a P 1 = b c V P 2 = c d V P 3 = d a V P 0 = a b V P 1 = b c V P 2 = c d V P 3 = d
64 r19.41v a V P 0 = a b V P 1 = b c V P 2 = c d V P 3 = d a V P 0 = a b V P 1 = b c V P 2 = c d V P 3 = d
65 r19.41v a V P 0 = a b V P 1 = b a V P 0 = a b V P 1 = b
66 65 anbi1i a V P 0 = a b V P 1 = b c V P 2 = c d V P 3 = d a V P 0 = a b V P 1 = b c V P 2 = c d V P 3 = d
67 63 64 66 3bitri a V b V P 0 = a P 1 = b c V P 2 = c d V P 3 = d a V P 0 = a b V P 1 = b c V P 2 = c d V P 3 = d
68 53 58 67 3bitri a V b V c V d V P 0 = a P 1 = b P 2 = c P 3 = d a V P 0 = a b V P 1 = b c V P 2 = c d V P 3 = d
69 47 68 sylibr L 3 P : 0 L V a V b V c V d V P 0 = a P 1 = b P 2 = c P 3 = d