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