Metamath Proof Explorer


Theorem cusgrsizeindb1

Description: Base case of the induction in cusgrsize . The size of a (complete) simple graph with 1 vertex is 0=((1-1)*1)/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 cusgrsizeindb1 ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgrsizeindb0.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 usgr1v0e ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ♯ ‘ 𝐸 ) = 0 )
4 oveq1 ( ( ♯ ‘ 𝑉 ) = 1 → ( ( ♯ ‘ 𝑉 ) C 2 ) = ( 1 C 2 ) )
5 1nn0 1 ∈ ℕ0
6 2z 2 ∈ ℤ
7 1lt2 1 < 2
8 7 olci ( 2 < 0 ∨ 1 < 2 )
9 bcval4 ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℤ ∧ ( 2 < 0 ∨ 1 < 2 ) ) → ( 1 C 2 ) = 0 )
10 5 6 8 9 mp3an ( 1 C 2 ) = 0
11 4 10 eqtrdi ( ( ♯ ‘ 𝑉 ) = 1 → ( ( ♯ ‘ 𝑉 ) C 2 ) = 0 )
12 11 eqeq2d ( ( ♯ ‘ 𝑉 ) = 1 → ( ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ↔ ( ♯ ‘ 𝐸 ) = 0 ) )
13 12 adantl ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) ↔ ( ♯ ‘ 𝐸 ) = 0 ) )
14 3 13 mpbird ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑉 ) = 1 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )