Metamath Proof Explorer

Theorem cusgrm1rusgr

Description: A finite simple graph with n vertices is complete iff it is (n-1)-regular. Hint: If the definition of RegGraph was allowed for k e. ZZ , then the assumption V =/= (/) could be removed. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Hypothesis cusgrrusgr.v ⊢ V = Vtx ⁡ G
Assertion cusgrm1rusgr ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → G ∈ ComplUSGraph ↔ G RegUSGraph V − 1

Proof

Step Hyp Ref Expression
1 cusgrrusgr.v ⊢ V = Vtx ⁡ G
2 simpr ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ ∧ G ∈ ComplUSGraph → G ∈ ComplUSGraph
3 1 fusgrvtxfi ⊢ G ∈ FinUSGraph → V ∈ Fin
4 3 adantr ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → V ∈ Fin
5 4 adantr ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ ∧ G ∈ ComplUSGraph → V ∈ Fin
6 simpr ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → V ≠ ∅
7 6 adantr ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ ∧ G ∈ ComplUSGraph → V ≠ ∅
8 1 cusgrrusgr ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → G RegUSGraph V − 1
9 2 5 7 8 syl3anc ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ ∧ G ∈ ComplUSGraph → G RegUSGraph V − 1
10 9 ex ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → G ∈ ComplUSGraph → G RegUSGraph V − 1
11 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
12 1 11 rusgrprop0 ⊢ G RegUSGraph V − 1 → G ∈ USGraph ∧ V − 1 ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1
13 12 simp3d ⊢ G RegUSGraph V − 1 → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1
14 1 vdiscusgr ⊢ G ∈ FinUSGraph → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1 → G ∈ ComplUSGraph
15 14 adantr ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1 → G ∈ ComplUSGraph
16 13 15 syl5 ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → G RegUSGraph V − 1 → G ∈ ComplUSGraph
17 10 16 impbid ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → G ∈ ComplUSGraph ↔ G RegUSGraph V − 1