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. E | N e/ e }
Assertion cusgrsize2inds 
|- ( Y e. NN0 -> ( ( G e. ComplUSGraph /\ ( # ` V ) = Y /\ N e. V ) -> ( ( # ` F ) = ( ( # ` ( V \ { N } ) ) _C 2 ) -> ( # ` E ) = ( ( # ` V ) _C 2 ) ) ) )

Proof

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