mccllem

Description: * Induction step for mccl . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	mccllem.a	$⊢ φ \to A \in Fin$
	mccllem.c	$⊢ φ \to C \subseteq A$
	mccllem.d	$⊢ φ \to D \in (A ∖ C)$
	mccllem.b	$⊢ φ \to B \in ({ℕ_{0}}^{(C \cup \{D\})})$
	mccllem.6	$⊢ φ \to \forall b \in ({ℕ_{0}}^{C}) \frac{\sum_{k \in C} b (k)!}{\prod_{k \in C} b (k)!} \in ℕ$
Assertion	mccllem	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C \cup \{D\}} B (k)!} \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		mccllem.a	$⊢ φ \to A \in Fin$
2		mccllem.c	$⊢ φ \to C \subseteq A$
3		mccllem.d	$⊢ φ \to D \in (A ∖ C)$
4		mccllem.b	$⊢ φ \to B \in ({ℕ_{0}}^{(C \cup \{D\})})$
5		mccllem.6	$⊢ φ \to \forall b \in ({ℕ_{0}}^{C}) \frac{\sum_{k \in C} b (k)!}{\prod_{k \in C} b (k)!} \in ℕ$
6		nfv	$⊢ Ⅎ k φ$
7		nfcv	$⊢ \underline{Ⅎ} k B (D)!$
8		ssfi	$⊢ (A \in Fin \land C \subseteq A) \to C \in Fin$
9	1 2 8	syl2anc	$⊢ φ \to C \in Fin$
10		eldifn	$⊢ D \in (A ∖ C) \to \neg D \in C$
11	3 10	syl	$⊢ φ \to \neg D \in C$
12		elmapi	$⊢ B \in ({ℕ_{0}}^{(C \cup \{D\})}) \to B : C \cup \{D\} ⟶ ℕ_{0}$
13	4 12	syl	$⊢ φ \to B : C \cup \{D\} ⟶ ℕ_{0}$
14	13	adantr	$⊢ (φ \land k \in C) \to B : C \cup \{D\} ⟶ ℕ_{0}$
15		elun1	$⊢ k \in C \to k \in (C \cup \{D\})$
16	15	adantl	$⊢ (φ \land k \in C) \to k \in (C \cup \{D\})$
17	14 16	ffvelrnd	$⊢ (φ \land k \in C) \to B (k) \in ℕ_{0}$
18	17	faccld	$⊢ (φ \land k \in C) \to B (k)! \in ℕ$
19	18	nncnd	$⊢ (φ \land k \in C) \to B (k)! \in ℂ$
20		2fveq3	$⊢ k = D \to B (k)! = B (D)!$
21		snidg	$⊢ D \in (A ∖ C) \to D \in \{D\}$
22	3 21	syl	$⊢ φ \to D \in \{D\}$
23		elun2	$⊢ D \in \{D\} \to D \in (C \cup \{D\})$
24	22 23	syl	$⊢ φ \to D \in (C \cup \{D\})$
25	13 24	ffvelrnd	$⊢ φ \to B (D) \in ℕ_{0}$
26	25	faccld	$⊢ φ \to B (D)! \in ℕ$
27	26	nncnd	$⊢ φ \to B (D)! \in ℂ$
28	6 7 9 3 11 19 20 27	fprodsplitsn	$⊢ φ \to \prod_{k \in C \cup \{D\}} B (k)! = \prod_{k \in C} B (k)! B (D)!$
29	28	oveq2d	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C \cup \{D\}} B (k)!} = \frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C} B (k)! B (D)!}$
30	3	eldifad	$⊢ φ \to D \in A$
31		snssi	$⊢ D \in A \to \{D\} \subseteq A$
32	30 31	syl	$⊢ φ \to \{D\} \subseteq A$
33	2 32	unssd	$⊢ φ \to C \cup \{D\} \subseteq A$
34		ssfi	$⊢ (A \in Fin \land C \cup \{D\} \subseteq A) \to C \cup \{D\} \in Fin$
35	1 33 34	syl2anc	$⊢ φ \to C \cup \{D\} \in Fin$
36	13	ffvelrnda	$⊢ (φ \land k \in (C \cup \{D\})) \to B (k) \in ℕ_{0}$
37	35 36	fsumnn0cl	$⊢ φ \to \sum_{k \in C \cup \{D\}} B (k) \in ℕ_{0}$
38	37	faccld	$⊢ φ \to \sum_{k \in C \cup \{D\}} B (k)! \in ℕ$
39	38	nncnd	$⊢ φ \to \sum_{k \in C \cup \{D\}} B (k)! \in ℂ$
40	6 9 19	fprodclf	$⊢ φ \to \prod_{k \in C} B (k)! \in ℂ$
41	40 27	mulcld	$⊢ φ \to \prod_{k \in C} B (k)! B (D)! \in ℂ$
42	18	nnne0d	$⊢ (φ \land k \in C) \to B (k)! \neq 0$
43	9 19 42	fprodn0	$⊢ φ \to \prod_{k \in C} B (k)! \neq 0$
44	26	nnne0d	$⊢ φ \to B (D)! \neq 0$
45	40 27 43 44	mulne0d	$⊢ φ \to \prod_{k \in C} B (k)! B (D)! \neq 0$
46	39 41 45	divcld	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C} B (k)! B (D)!} \in ℂ$
47	46	mulid2d	$⊢ φ \to 1 (\frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C} B (k)! B (D)!}) = \frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C} B (k)! B (D)!}$
48	47	eqcomd	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C} B (k)! B (D)!} = 1 (\frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C} B (k)! B (D)!})$
49	9 17	fsumnn0cl	$⊢ φ \to \sum_{k \in C} B (k) \in ℕ_{0}$
50	49	faccld	$⊢ φ \to \sum_{k \in C} B (k)! \in ℕ$
51	50	nncnd	$⊢ φ \to \sum_{k \in C} B (k)! \in ℂ$
52		nnne0	$⊢ \sum_{k \in C} B (k)! \in ℕ \to \sum_{k \in C} B (k)! \neq 0$
53	50 52	syl	$⊢ φ \to \sum_{k \in C} B (k)! \neq 0$
54	51 53	dividd	$⊢ φ \to \frac{\sum_{k \in C} B (k)!}{\sum_{k \in C} B (k)!} = 1$
55	54	eqcomd	$⊢ φ \to 1 = \frac{\sum_{k \in C} B (k)!}{\sum_{k \in C} B (k)!}$
56	40 27	mulcomd	$⊢ φ \to \prod_{k \in C} B (k)! B (D)! = B (D)! \prod_{k \in C} B (k)!$
57	56	oveq2d	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C} B (k)! B (D)!} = \frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)! \prod_{k \in C} B (k)!}$
58	39 27 40 44 43	divdiv1d	$⊢ φ \to \frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\prod_{k \in C} B (k)!} = \frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)! \prod_{k \in C} B (k)!}$
59	58	eqcomd	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)! \prod_{k \in C} B (k)!} = \frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\prod_{k \in C} B (k)!}$
60	57 59	eqtrd	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C} B (k)! B (D)!} = \frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\prod_{k \in C} B (k)!}$
61	55 60	oveq12d	$⊢ φ \to 1 (\frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C} B (k)! B (D)!}) = (\frac{\sum_{k \in C} B (k)!}{\sum_{k \in C} B (k)!}) (\frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\prod_{k \in C} B (k)!})$
62	39 27 44	divcld	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!} \in ℂ$
63	51 51 62 40 53 43	divmul13d	$⊢ φ \to (\frac{\sum_{k \in C} B (k)!}{\sum_{k \in C} B (k)!}) (\frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\prod_{k \in C} B (k)!}) = (\frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\sum_{k \in C} B (k)!}) (\frac{\sum_{k \in C} B (k)!}{\prod_{k \in C} B (k)!})$
64	61 63	eqtrd	$⊢ φ \to 1 (\frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C} B (k)! B (D)!}) = (\frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\sum_{k \in C} B (k)!}) (\frac{\sum_{k \in C} B (k)!}{\prod_{k \in C} B (k)!})$
65	29 48 64	3eqtrd	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C \cup \{D\}} B (k)!} = (\frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\sum_{k \in C} B (k)!}) (\frac{\sum_{k \in C} B (k)!}{\prod_{k \in C} B (k)!})$
66	39 27 51 44 53	divdiv1d	$⊢ φ \to \frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\sum_{k \in C} B (k)!} = \frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)! \sum_{k \in C} B (k)!}$
67		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ D / k ⦌ B (k)$
68	17	nn0cnd	$⊢ (φ \land k \in C) \to B (k) \in ℂ$
69		csbeq1a	$⊢ k = D \to B (k) = ⦋ D / k ⦌ B (k)$
70		csbfv	$⊢ ⦋ D / k ⦌ B (k) = B (D)$
71	70	a1i	$⊢ φ \to ⦋ D / k ⦌ B (k) = B (D)$
72	25	nn0cnd	$⊢ φ \to B (D) \in ℂ$
73	71 72	eqeltrd	$⊢ φ \to ⦋ D / k ⦌ B (k) \in ℂ$
74	6 67 9 30 11 68 69 73	fsumsplitsn	$⊢ φ \to \sum_{k \in C \cup \{D\}} B (k) = \sum_{k \in C} B (k) + ⦋ D / k ⦌ B (k)$
75	74	oveq1d	$⊢ φ \to \sum_{k \in C \cup \{D\}} B (k) - \sum_{k \in C} B (k) = \sum_{k \in C} B (k) + ⦋ D / k ⦌ B (k) - \sum_{k \in C} B (k)$
76	49	nn0cnd	$⊢ φ \to \sum_{k \in C} B (k) \in ℂ$
77	76 73	pncan2d	$⊢ φ \to \sum_{k \in C} B (k) + ⦋ D / k ⦌ B (k) - \sum_{k \in C} B (k) = ⦋ D / k ⦌ B (k)$
78	75 77 71	3eqtrrd	$⊢ φ \to B (D) = \sum_{k \in C \cup \{D\}} B (k) - \sum_{k \in C} B (k)$
79	78	fveq2d	$⊢ φ \to B (D)! = (\sum_{k \in C \cup \{D\}} B (k) - \sum_{k \in C} B (k))!$
80	79	oveq1d	$⊢ φ \to B (D)! \sum_{k \in C} B (k)! = (\sum_{k \in C \cup \{D\}} B (k) - \sum_{k \in C} B (k))! \sum_{k \in C} B (k)!$
81	80	oveq2d	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)! \sum_{k \in C} B (k)!} = \frac{\sum_{k \in C \cup \{D\}} B (k)!}{(\sum_{k \in C \cup \{D\}} B (k) - \sum_{k \in C} B (k))! \sum_{k \in C} B (k)!}$
82		0zd	$⊢ φ \to 0 \in ℤ$
83	37	nn0zd	$⊢ φ \to \sum_{k \in C \cup \{D\}} B (k) \in ℤ$
84	49	nn0zd	$⊢ φ \to \sum_{k \in C} B (k) \in ℤ$
85	82 83 84	3jca	$⊢ φ \to (0 \in ℤ \land \sum_{k \in C \cup \{D\}} B (k) \in ℤ \land \sum_{k \in C} B (k) \in ℤ)$
86	49	nn0ge0d	$⊢ φ \to 0 \leq \sum_{k \in C} B (k)$
87	25	nn0ge0d	$⊢ φ \to 0 \leq B (D)$
88	71	eqcomd	$⊢ φ \to B (D) = ⦋ D / k ⦌ B (k)$
89	87 88	breqtrd	$⊢ φ \to 0 \leq ⦋ D / k ⦌ B (k)$
90	49	nn0red	$⊢ φ \to \sum_{k \in C} B (k) \in ℝ$
91	25	nn0red	$⊢ φ \to B (D) \in ℝ$
92	71 91	eqeltrd	$⊢ φ \to ⦋ D / k ⦌ B (k) \in ℝ$
93	90 92	addge01d	$⊢ φ \to (0 \leq ⦋ D / k ⦌ B (k) \leftrightarrow \sum_{k \in C} B (k) \leq \sum_{k \in C} B (k) + ⦋ D / k ⦌ B (k))$
94	89 93	mpbid	$⊢ φ \to \sum_{k \in C} B (k) \leq \sum_{k \in C} B (k) + ⦋ D / k ⦌ B (k)$
95	74	eqcomd	$⊢ φ \to \sum_{k \in C} B (k) + ⦋ D / k ⦌ B (k) = \sum_{k \in C \cup \{D\}} B (k)$
96	94 95	breqtrd	$⊢ φ \to \sum_{k \in C} B (k) \leq \sum_{k \in C \cup \{D\}} B (k)$
97	85 86 96	jca32	$⊢ φ \to ((0 \in ℤ \land \sum_{k \in C \cup \{D\}} B (k) \in ℤ \land \sum_{k \in C} B (k) \in ℤ) \land (0 \leq \sum_{k \in C} B (k) \land \sum_{k \in C} B (k) \leq \sum_{k \in C \cup \{D\}} B (k)))$
98		elfz2	$⊢ \sum_{k \in C} B (k) \in (0 \dots \sum_{k \in C \cup \{D\}} B (k)) \leftrightarrow ((0 \in ℤ \land \sum_{k \in C \cup \{D\}} B (k) \in ℤ \land \sum_{k \in C} B (k) \in ℤ) \land (0 \leq \sum_{k \in C} B (k) \land \sum_{k \in C} B (k) \leq \sum_{k \in C \cup \{D\}} B (k)))$
99	97 98	sylibr	$⊢ φ \to \sum_{k \in C} B (k) \in (0 \dots \sum_{k \in C \cup \{D\}} B (k))$
100		bcval2	$⊢ \sum_{k \in C} B (k) \in (0 \dots \sum_{k \in C \cup \{D\}} B (k)) \to (\binom{\sum_{k \in C \cup \{D\}} B (k)}{\sum_{k \in C} B (k)}) = \frac{\sum_{k \in C \cup \{D\}} B (k)!}{(\sum_{k \in C \cup \{D\}} B (k) - \sum_{k \in C} B (k))! \sum_{k \in C} B (k)!}$
101	99 100	syl	$⊢ φ \to (\binom{\sum_{k \in C \cup \{D\}} B (k)}{\sum_{k \in C} B (k)}) = \frac{\sum_{k \in C \cup \{D\}} B (k)!}{(\sum_{k \in C \cup \{D\}} B (k) - \sum_{k \in C} B (k))! \sum_{k \in C} B (k)!}$
102	101	eqcomd	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{(\sum_{k \in C \cup \{D\}} B (k) - \sum_{k \in C} B (k))! \sum_{k \in C} B (k)!} = (\binom{\sum_{k \in C \cup \{D\}} B (k)}{\sum_{k \in C} B (k)})$
103	66 81 102	3eqtrd	$⊢ φ \to \frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\sum_{k \in C} B (k)!} = (\binom{\sum_{k \in C \cup \{D\}} B (k)}{\sum_{k \in C} B (k)})$
104		bccl2	$⊢ \sum_{k \in C} B (k) \in (0 \dots \sum_{k \in C \cup \{D\}} B (k)) \to (\binom{\sum_{k \in C \cup \{D\}} B (k)}{\sum_{k \in C} B (k)}) \in ℕ$
105	99 104	syl	$⊢ φ \to (\binom{\sum_{k \in C \cup \{D\}} B (k)}{\sum_{k \in C} B (k)}) \in ℕ$
106	103 105	eqeltrd	$⊢ φ \to \frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\sum_{k \in C} B (k)!} \in ℕ$
107		ssun1	$⊢ C \subseteq C \cup \{D\}$
108	107	a1i	$⊢ φ \to C \subseteq C \cup \{D\}$
109		elmapssres	$⊢ (B \in ({ℕ_{0}}^{(C \cup \{D\})}) \land C \subseteq C \cup \{D\}) \to {B ↾}_{C} \in ({ℕ_{0}}^{C})$
110	4 108 109	syl2anc	$⊢ φ \to {B ↾}_{C} \in ({ℕ_{0}}^{C})$
111		fveq1	$⊢ b = {B ↾}_{C} \to b (k) = ({B ↾}_{C}) (k)$
112	111	adantr	$⊢ (b = {B ↾}_{C} \land k \in C) \to b (k) = ({B ↾}_{C}) (k)$
113		fvres	$⊢ k \in C \to ({B ↾}_{C}) (k) = B (k)$
114	113	adantl	$⊢ (b = {B ↾}_{C} \land k \in C) \to ({B ↾}_{C}) (k) = B (k)$
115	112 114	eqtrd	$⊢ (b = {B ↾}_{C} \land k \in C) \to b (k) = B (k)$
116	115	sumeq2dv	$⊢ b = {B ↾}_{C} \to \sum_{k \in C} b (k) = \sum_{k \in C} B (k)$
117	116	fveq2d	$⊢ b = {B ↾}_{C} \to \sum_{k \in C} b (k)! = \sum_{k \in C} B (k)!$
118	115	fveq2d	$⊢ (b = {B ↾}_{C} \land k \in C) \to b (k)! = B (k)!$
119	118	prodeq2dv	$⊢ b = {B ↾}_{C} \to \prod_{k \in C} b (k)! = \prod_{k \in C} B (k)!$
120	117 119	oveq12d	$⊢ b = {B ↾}_{C} \to \frac{\sum_{k \in C} b (k)!}{\prod_{k \in C} b (k)!} = \frac{\sum_{k \in C} B (k)!}{\prod_{k \in C} B (k)!}$
121	120	eleq1d	$⊢ b = {B ↾}_{C} \to (\frac{\sum_{k \in C} b (k)!}{\prod_{k \in C} b (k)!} \in ℕ \leftrightarrow \frac{\sum_{k \in C} B (k)!}{\prod_{k \in C} B (k)!} \in ℕ)$
122	121	rspccva	$⊢ (\forall b \in ({ℕ_{0}}^{C}) \frac{\sum_{k \in C} b (k)!}{\prod_{k \in C} b (k)!} \in ℕ \land {B ↾}_{C} \in ({ℕ_{0}}^{C})) \to \frac{\sum_{k \in C} B (k)!}{\prod_{k \in C} B (k)!} \in ℕ$
123	5 110 122	syl2anc	$⊢ φ \to \frac{\sum_{k \in C} B (k)!}{\prod_{k \in C} B (k)!} \in ℕ$
124	106 123	nnmulcld	$⊢ φ \to (\frac{\frac{\sum_{k \in C \cup \{D\}} B (k)!}{B (D)!}}{\sum_{k \in C} B (k)!}) (\frac{\sum_{k \in C} B (k)!}{\prod_{k \in C} B (k)!}) \in ℕ$
125	65 124	eqeltrd	$⊢ φ \to \frac{\sum_{k \in C \cup \{D\}} B (k)!}{\prod_{k \in C \cup \{D\}} B (k)!} \in ℕ$

Metamath Proof Explorer

Theorem mccllem

Proof