Metamath Proof Explorer


Theorem eupth2lem3lem7

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 V=VtxG
trlsegvdeg.i I=iEdgG
trlsegvdeg.f φFunI
trlsegvdeg.n φN0..^F
trlsegvdeg.u φUV
trlsegvdeg.w φFTrailsGP
trlsegvdeg.vx φVtxX=V
trlsegvdeg.vy φVtxY=V
trlsegvdeg.vz φVtxZ=V
trlsegvdeg.ix φiEdgX=IF0..^N
trlsegvdeg.iy φiEdgY=FNIFN
trlsegvdeg.iz φiEdgZ=IF0N
eupth2lem3.o φxV|¬2VtxDegXx=ifP0=PNP0PN
eupth2lem3.e φIFN=PNPN+1
Assertion eupth2lem3lem7 φ¬2VtxDegZUUifP0=PN+1P0PN+1

Proof

Step Hyp Ref Expression
1 trlsegvdeg.v V=VtxG
2 trlsegvdeg.i I=iEdgG
3 trlsegvdeg.f φFunI
4 trlsegvdeg.n φN0..^F
5 trlsegvdeg.u φUV
6 trlsegvdeg.w φFTrailsGP
7 trlsegvdeg.vx φVtxX=V
8 trlsegvdeg.vy φVtxY=V
9 trlsegvdeg.vz φVtxZ=V
10 trlsegvdeg.ix φiEdgX=IF0..^N
11 trlsegvdeg.iy φiEdgY=FNIFN
12 trlsegvdeg.iz φiEdgZ=IF0N
13 eupth2lem3.o φxV|¬2VtxDegXx=ifP0=PNP0PN
14 eupth2lem3.e φIFN=PNPN+1
15 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeg φVtxDegZU=VtxDegXU+VtxDegYU
16 15 breq2d φ2VtxDegZU2VtxDegXU+VtxDegYU
17 16 notbid φ¬2VtxDegZU¬2VtxDegXU+VtxDegYU
18 ifpprsnss IFN=PNPN+1if-PN=PN+1IFN=PNPNPN+1IFN
19 14 18 syl φif-PN=PN+1IFN=PNPNPN+1IFN
20 1 2 3 4 5 6 7 8 9 10 11 12 13 19 eupth2lem3lem3 φPN=PN+1¬2VtxDegXU+VtxDegYUUifP0=PN+1P0PN+1
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 eupth2lem3lem5 φIFN𝒫V
22 1 2 3 4 5 6 7 8 9 10 11 12 13 19 21 eupth2lem3lem4 φPNPN+1U=PNU=PN+1¬2VtxDegXU+VtxDegYUUifP0=PN+1P0PN+1
23 22 3expa φPNPN+1U=PNU=PN+1¬2VtxDegXU+VtxDegYUUifP0=PN+1P0PN+1
24 23 expcom U=PNU=PN+1φPNPN+1¬2VtxDegXU+VtxDegYUUifP0=PN+1P0PN+1
25 neanior UPNUPN+1¬U=PNU=PN+1
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 eupth2lem3lem6 φPNPN+1UPNUPN+1¬2VtxDegXU+VtxDegYUUifP0=PN+1P0PN+1
27 26 3expa φPNPN+1UPNUPN+1¬2VtxDegXU+VtxDegYUUifP0=PN+1P0PN+1
28 27 expcom UPNUPN+1φPNPN+1¬2VtxDegXU+VtxDegYUUifP0=PN+1P0PN+1
29 25 28 sylbir ¬U=PNU=PN+1φPNPN+1¬2VtxDegXU+VtxDegYUUifP0=PN+1P0PN+1
30 24 29 pm2.61i φPNPN+1¬2VtxDegXU+VtxDegYUUifP0=PN+1P0PN+1
31 20 30 pm2.61dane φ¬2VtxDegXU+VtxDegYUUifP0=PN+1P0PN+1
32 17 31 bitrd φ¬2VtxDegZUUifP0=PN+1P0PN+1