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 \in E \| N \notin e\}$
Assertion	cusgrsize2inds	$⊢ Y \in ℕ_{0} \to ((G \in ComplUSGraph \land \|V\| = Y \land N \in V) \to (\|F\| = (\binom{\|V ∖ \{N\}\|}{2}) \to \|E\| = (\binom{\|V\|}{2})))$

Proof

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

Metamath Proof Explorer

Theorem cusgrsize2inds

Proof