Description: Lemma 10 for 3wlkd . (Contributed by Alexander van der Vekens, 12-Nov-2017) (Revised by AV, 7-Feb-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 3wlkd.p | |
|
3wlkd.f | |
||
3wlkd.s | |
||
3wlkd.n | |
||
3wlkd.e | |
||
Assertion | 3wlkdlem10 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3wlkd.p | |
|
2 | 3wlkd.f | |
|
3 | 3wlkd.s | |
|
4 | 3wlkd.n | |
|
5 | 3wlkd.e | |
|
6 | 1 2 3 4 5 | 3wlkdlem9 | |
7 | 1 2 3 | 3wlkdlem3 | |
8 | preq12 | |
|
9 | 8 | adantr | |
10 | 9 | sseq1d | |
11 | simplr | |
|
12 | simprl | |
|
13 | 11 12 | preq12d | |
14 | 13 | sseq1d | |
15 | preq12 | |
|
16 | 15 | adantl | |
17 | 16 | sseq1d | |
18 | 10 14 17 | 3anbi123d | |
19 | 7 18 | syl | |
20 | 6 19 | mpbird | |
21 | 1 2 | 3wlkdlem2 | |
22 | 21 | raleqi | |
23 | c0ex | |
|
24 | 1ex | |
|
25 | 2ex | |
|
26 | fveq2 | |
|
27 | fv0p1e1 | |
|
28 | 26 27 | preq12d | |
29 | 2fveq3 | |
|
30 | 28 29 | sseq12d | |
31 | fveq2 | |
|
32 | oveq1 | |
|
33 | 1p1e2 | |
|
34 | 32 33 | eqtrdi | |
35 | 34 | fveq2d | |
36 | 31 35 | preq12d | |
37 | 2fveq3 | |
|
38 | 36 37 | sseq12d | |
39 | fveq2 | |
|
40 | oveq1 | |
|
41 | 2p1e3 | |
|
42 | 40 41 | eqtrdi | |
43 | 42 | fveq2d | |
44 | 39 43 | preq12d | |
45 | 2fveq3 | |
|
46 | 44 45 | sseq12d | |
47 | 23 24 25 30 38 46 | raltp | |
48 | 22 47 | bitri | |
49 | 20 48 | sylibr | |