Metamath Proof Explorer


Theorem cusgrsize2inds

Description: Induction step in cusgrsize . If the size of the complete graph with n vertices reduced by one vertex is " ( n - 1 ) choose 2", the size of the complete graph with n vertices is " n choose 2". (Contributed by Alexander van der Vekens, 11-Jan-2018) (Revised by AV, 9-Nov-2020)

Ref Expression
Hypotheses cusgrsizeindb0.v V = Vtx G
cusgrsizeindb0.e E = Edg G
cusgrsizeinds.f F = e E | N e
Assertion cusgrsize2inds Y 0 G ComplUSGraph V = Y N V F = ( V N 2 ) E = ( V 2 )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v V = Vtx G
2 cusgrsizeindb0.e E = Edg G
3 cusgrsizeinds.f F = e E | N e
4 1 fvexi V V
5 hashnn0n0nn V V Y 0 V = Y N V Y
6 5 anassrs V V Y 0 V = Y N V Y
7 simplll V V V = Y N V Y V V
8 simplr V V V = Y N V Y N V
9 eleq1 Y = V Y V
10 9 eqcoms V = Y Y V
11 nnm1nn0 V V 1 0
12 10 11 syl6bi V = Y Y V 1 0
13 12 ad2antlr V V V = Y N V Y V 1 0
14 13 imp V V V = Y N V Y V 1 0
15 nncn V V
16 1cnd V 1
17 15 16 npcand V V - 1 + 1 = V
18 17 eqcomd V V = V - 1 + 1
19 10 18 syl6bi V = Y Y V = V - 1 + 1
20 19 ad2antlr V V V = Y N V Y V = V - 1 + 1
21 20 imp V V V = Y N V Y V = V - 1 + 1
22 hashdifsnp1 V V N V V 1 0 V = V - 1 + 1 V N = V 1
23 22 imp V V N V V 1 0 V = V - 1 + 1 V N = V 1
24 7 8 14 21 23 syl31anc V V V = Y N V Y V N = V 1
25 oveq1 V N = V 1 ( V N 2 ) = ( V 1 2 )
26 25 eqeq2d V N = V 1 F = ( V N 2 ) F = ( V 1 2 )
27 10 ad2antlr V V V = Y N V Y V
28 nnnn0 V V 0
29 hashclb V V V Fin V 0
30 28 29 syl5ibrcom V V V V Fin
31 1 2 3 cusgrsizeinds G ComplUSGraph V Fin N V E = V - 1 + F
32 oveq2 F = ( V 1 2 ) V - 1 + F = V - 1 + ( V 1 2 )
33 32 eqeq2d F = ( V 1 2 ) E = V - 1 + F E = V - 1 + ( V 1 2 )
34 33 adantl V F = ( V 1 2 ) E = V - 1 + F E = V - 1 + ( V 1 2 )
35 bcn2m1 V V - 1 + ( V 1 2 ) = ( V 2 )
36 35 eqeq2d V E = V - 1 + ( V 1 2 ) E = ( V 2 )
37 36 biimpd V E = V - 1 + ( V 1 2 ) E = ( V 2 )
38 37 adantr V F = ( V 1 2 ) E = V - 1 + ( V 1 2 ) E = ( V 2 )
39 34 38 sylbid V F = ( V 1 2 ) E = V - 1 + F E = ( V 2 )
40 39 ex V F = ( V 1 2 ) E = V - 1 + F E = ( V 2 )
41 40 com3r E = V - 1 + F V F = ( V 1 2 ) E = ( V 2 )
42 31 41 syl G ComplUSGraph V Fin N V V F = ( V 1 2 ) E = ( V 2 )
43 42 3exp G ComplUSGraph V Fin N V V F = ( V 1 2 ) E = ( V 2 )
44 43 com14 V V Fin N V G ComplUSGraph F = ( V 1 2 ) E = ( V 2 )
45 30 44 syldc V V V N V G ComplUSGraph F = ( V 1 2 ) E = ( V 2 )
46 45 com23 V V N V V G ComplUSGraph F = ( V 1 2 ) E = ( V 2 )
47 46 adantr V V V = Y N V V G ComplUSGraph F = ( V 1 2 ) E = ( V 2 )
48 47 imp V V V = Y N V V G ComplUSGraph F = ( V 1 2 ) E = ( V 2 )
49 27 48 sylbid V V V = Y N V Y G ComplUSGraph F = ( V 1 2 ) E = ( V 2 )
50 49 imp V V V = Y N V Y G ComplUSGraph F = ( V 1 2 ) E = ( V 2 )
51 50 com13 F = ( V 1 2 ) G ComplUSGraph V V V = Y N V Y E = ( V 2 )
52 26 51 syl6bi V N = V 1 F = ( V N 2 ) G ComplUSGraph V V V = Y N V Y E = ( V 2 )
53 52 com24 V N = V 1 V V V = Y N V Y G ComplUSGraph F = ( V N 2 ) E = ( V 2 )
54 24 53 mpcom V V V = Y N V Y G ComplUSGraph F = ( V N 2 ) E = ( V 2 )
55 54 ex V V V = Y N V Y G ComplUSGraph F = ( V N 2 ) E = ( V 2 )
56 55 adantllr V V Y 0 V = Y N V Y G ComplUSGraph F = ( V N 2 ) E = ( V 2 )
57 6 56 mpd V V Y 0 V = Y N V G ComplUSGraph F = ( V N 2 ) E = ( V 2 )
58 57 exp41 V V Y 0 V = Y N V G ComplUSGraph F = ( V N 2 ) E = ( V 2 )
59 58 com25 V V G ComplUSGraph V = Y N V Y 0 F = ( V N 2 ) E = ( V 2 )
60 4 59 ax-mp G ComplUSGraph V = Y N V Y 0 F = ( V N 2 ) E = ( V 2 )
61 60 3imp G ComplUSGraph V = Y N V Y 0 F = ( V N 2 ) E = ( V 2 )
62 61 com12 Y 0 G ComplUSGraph V = Y N V F = ( V N 2 ) E = ( V 2 )