Metamath Proof Explorer

Theorem fusgrvtxdgonume

Description: The number of vertices of odd degree is even in a finite simple graph. Proposition 1.2.1 in Diestel p. 5. See also remark about equation (2) in section I.1 in Bollobas p. 4. (Contributed by AV, 27-Dec-2021)

Ref Expression
Hypotheses finsumvtxdgeven.v ⊢ V = Vtx ⁡ G
finsumvtxdgeven.i ⊢ I = iEdg ⁡ G
finsumvtxdgeven.d ⊢ D = VtxDeg ⁡ G
Assertion fusgrvtxdgonume ⊢ G ∈ FinUSGraph → 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v

Proof

Step Hyp Ref Expression
1 finsumvtxdgeven.v ⊢ V = Vtx ⁡ G
2 finsumvtxdgeven.i ⊢ I = iEdg ⁡ G
3 finsumvtxdgeven.d ⊢ D = VtxDeg ⁡ G
4 1 2 fusgrfupgrfs ⊢ G ∈ FinUSGraph → G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin
5 1 2 3 vtxdgoddnumeven ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v
6 4 5 syl ⊢ G ∈ FinUSGraph → 2 ∥ v ∈ V | ¬ 2 ∥ D ⁡ v