Description: If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, each vertex except the first mentioned vertex is a neighbor of this vertex. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 16-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | hashnbusgrnn0.v | |
|
Assertion | nbusgrvtxm1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hashnbusgrnn0.v | |
|
2 | ax-1 | |
|
3 | 2 | 2a1d | |
4 | simpr | |
|
5 | 4 | adantr | |
6 | simprl | |
|
7 | simpr | |
|
8 | 7 | adantl | |
9 | df-nel | |
|
10 | 9 | biimpri | |
11 | 10 | adantr | |
12 | 11 | adantr | |
13 | 1 | nbfusgrlevtxm2 | |
14 | 5 6 8 12 13 | syl13anc | |
15 | breq1 | |
|
16 | 15 | adantl | |
17 | 1 | fusgrvtxfi | |
18 | hashcl | |
|
19 | nn0re | |
|
20 | 1red | |
|
21 | 2re | |
|
22 | 21 | a1i | |
23 | id | |
|
24 | 1lt2 | |
|
25 | 24 | a1i | |
26 | 20 22 23 25 | ltsub2dd | |
27 | 23 22 | resubcld | |
28 | peano2rem | |
|
29 | 27 28 | ltnled | |
30 | 26 29 | mpbid | |
31 | 19 30 | syl | |
32 | 17 18 31 | 3syl | |
33 | 32 | pm2.21d | |
34 | 33 | adantr | |
35 | 34 | ad3antlr | |
36 | 16 35 | sylbid | |
37 | 36 | ex | |
38 | 14 37 | mpid | |
39 | 38 | ex | |
40 | 39 | com23 | |
41 | 40 | ex | |
42 | 3 41 | pm2.61i | |