This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cusgrsizeindb0

Description: Base case of the induction in cusgrsize . The size of a complete simple graph with 0 vertices, actually of every null graph, is 0=((0-1)*0)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 7-Nov-2020)

Ref Expression
Hypotheses cusgrsizeindb0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
cusgrsizeindb0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion cusgrsizeindb0 ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgrsizeindb0.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 uhgr0vsize0 ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( ♯ ‘ 𝐸 ) = 0 )
4 oveq1 ⊢ ( ( ♯ ‘ 𝑉 ) = 0 → ( ( ♯ ‘ 𝑉 ) C 2 ) = ( 0 C 2 ) )
5 2nn ⊢ 2 ∈ ℕ
6 bc0k ⊢ ( 2 ∈ ℕ → ( 0 C 2 ) = 0 )
7 5 6 ax-mp ⊢ ( 0 C 2 ) = 0
8 4 7 eqtr2di ⊢ ( ( ♯ ‘ 𝑉 ) = 0 → 0 = ( ( ♯ ‘ 𝑉 ) C 2 ) )
9 8 adantl ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → 0 = ( ( ♯ ‘ 𝑉 ) C 2 ) )
10 3 9 eqtrd ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )