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 ⊢ V = Vtx ⁡ G
cusgrsizeindb0.e ⊢ E = Edg ⁡ G
Assertion cusgrsizeindb1 ⊢ G ∈ USGraph ∧ V = 1 → E = ( V 2 )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v ⊢ V = Vtx ⁡ G
2 cusgrsizeindb0.e ⊢ E = Edg ⁡ G
3 1 2 usgr1v0e ⊢ G ∈ USGraph ∧ V = 1 → E = 0
4 oveq1 ⊢ V = 1 → ( V 2 ) = ( 1 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 2 ) = 0
10 5 6 8 9 mp3an ⊢ ( 1 2 ) = 0
11 4 10 eqtrdi ⊢ V = 1 → ( V 2 ) = 0
12 11 eqeq2d ⊢ V = 1 → E = ( V 2 ) ↔ E = 0
13 12 adantl ⊢ G ∈ USGraph ∧ V = 1 → E = ( V 2 ) ↔ E = 0
14 3 13 mpbird ⊢ G ∈ USGraph ∧ V = 1 → E = ( V 2 )