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

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 ) )