Description: Lemma for eupth2lem3 : Combining trlsegvdeg , eupth2lem3lem3 , eupth2lem3lem4 and eupth2lem3lem6 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 27-Feb-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | trlsegvdeg.v | |
|
trlsegvdeg.i | |
||
trlsegvdeg.f | |
||
trlsegvdeg.n | |
||
trlsegvdeg.u | |
||
trlsegvdeg.w | |
||
trlsegvdeg.vx | |
||
trlsegvdeg.vy | |
||
trlsegvdeg.vz | |
||
trlsegvdeg.ix | |
||
trlsegvdeg.iy | |
||
trlsegvdeg.iz | |
||
eupth2lem3.o | |
||
eupth2lem3.e | |
||
Assertion | eupth2lem3lem7 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trlsegvdeg.v | |
|
2 | trlsegvdeg.i | |
|
3 | trlsegvdeg.f | |
|
4 | trlsegvdeg.n | |
|
5 | trlsegvdeg.u | |
|
6 | trlsegvdeg.w | |
|
7 | trlsegvdeg.vx | |
|
8 | trlsegvdeg.vy | |
|
9 | trlsegvdeg.vz | |
|
10 | trlsegvdeg.ix | |
|
11 | trlsegvdeg.iy | |
|
12 | trlsegvdeg.iz | |
|
13 | eupth2lem3.o | |
|
14 | eupth2lem3.e | |
|
15 | 1 2 3 4 5 6 7 8 9 10 11 12 | trlsegvdeg | |
16 | 15 | breq2d | |
17 | 16 | notbid | |
18 | ifpprsnss | |
|
19 | 14 18 | syl | |
20 | 1 2 3 4 5 6 7 8 9 10 11 12 13 19 | eupth2lem3lem3 | |
21 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 | eupth2lem3lem5 | |
22 | 1 2 3 4 5 6 7 8 9 10 11 12 13 19 21 | eupth2lem3lem4 | |
23 | 22 | 3expa | |
24 | 23 | expcom | |
25 | neanior | |
|
26 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 | eupth2lem3lem6 | |
27 | 26 | 3expa | |
28 | 27 | expcom | |
29 | 25 28 | sylbir | |
30 | 24 29 | pm2.61i | |
31 | 20 30 | pm2.61dane | |
32 | 17 31 | bitrd | |