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