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=\mathrm{Vtx}\left(G\right)$$
	finsumvtxdgeven.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	finsumvtxdgeven.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
Assertion	fusgrvtxdgonume	$$⊢G\in \mathrm{FinUSGraph}\to 2\parallel \left|\left\{v\in V|\neg 2\parallel D\left(v\right)\right\}\right|$$

Proof

Step	Hyp	Ref	Expression
1		finsumvtxdgeven.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		finsumvtxdgeven.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		finsumvtxdgeven.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
4	1 2	fusgrfupgrfs	$$⊢G\in \mathrm{FinUSGraph}\to \left(G\in \mathrm{UPGraph}\wedge V\in \mathrm{Fin}\wedge I\in \mathrm{Fin}\right)$$
5	1 2 3	vtxdgoddnumeven	$$⊢\left(G\in \mathrm{UPGraph}\wedge V\in \mathrm{Fin}\wedge I\in \mathrm{Fin}\right)\to 2\parallel \left|\left\{v\in V|\neg 2\parallel D\left(v\right)\right\}\right|$$
6	4 5	syl	$$⊢G\in \mathrm{FinUSGraph}\to 2\parallel \left|\left\{v\in V|\neg 2\parallel D\left(v\right)\right\}\right|$$