lcmineqlem11

Description: Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	lcmineqlem11.1	$⊢ φ \to M \in ℕ$
	lcmineqlem11.2	$⊢ φ \to N \in ℕ$
	lcmineqlem11.3	$⊢ φ \to M < N$
Assertion	lcmineqlem11	$⊢ φ \to \frac{1}{(M + 1) (\binom{N}{M + 1})} = (\frac{M}{N - M}) (\frac{1}{M (\binom{N}{M})})$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem11.1	$⊢ φ \to M \in ℕ$
2		lcmineqlem11.2	$⊢ φ \to N \in ℕ$
3		lcmineqlem11.3	$⊢ φ \to M < N$
4	1	nncnd	$⊢ φ \to M \in ℂ$
5		1cnd	$⊢ φ \to 1 \in ℂ$
6	4 5	addcld	$⊢ φ \to M + 1 \in ℂ$
7	1	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
8		1nn0	$⊢ 1 \in ℕ_{0}$
9	8	a1i	$⊢ φ \to 1 \in ℕ_{0}$
10	7 9	nn0addcld	$⊢ φ \to M + 1 \in ℕ_{0}$
11	1	nnzd	$⊢ φ \to M \in ℤ$
12	2	nnzd	$⊢ φ \to N \in ℤ$
13		zltp1le	$⊢ (M \in ℤ \land N \in ℤ) \to (M < N \leftrightarrow M + 1 \leq N)$
14	11 12 13	syl2anc	$⊢ φ \to (M < N \leftrightarrow M + 1 \leq N)$
15	3 14	mpbid	$⊢ φ \to M + 1 \leq N$
16	2 10 15	bccl2d	$⊢ φ \to (\binom{N}{M + 1}) \in ℕ$
17	16	nncnd	$⊢ φ \to (\binom{N}{M + 1}) \in ℂ$
18	6 17	mulcld	$⊢ φ \to (M + 1) (\binom{N}{M + 1}) \in ℂ$
19	18	div1d	$⊢ φ \to \frac{(M + 1) (\binom{N}{M + 1})}{1} = (M + 1) (\binom{N}{M + 1})$
20	11	peano2zd	$⊢ φ \to M + 1 \in ℤ$
21	1	peano2nnd	$⊢ φ \to M + 1 \in ℕ$
22	21	nnge1d	$⊢ φ \to 1 \leq M + 1$
23	20 22 15	3jca	$⊢ φ \to (M + 1 \in ℤ \land 1 \leq M + 1 \land M + 1 \leq N)$
24		1z	$⊢ 1 \in ℤ$
25		elfz1	$⊢ (1 \in ℤ \land N \in ℤ) \to (M + 1 \in (1 \dots N) \leftrightarrow (M + 1 \in ℤ \land 1 \leq M + 1 \land M + 1 \leq N))$
26	24 25	mpan	$⊢ N \in ℤ \to (M + 1 \in (1 \dots N) \leftrightarrow (M + 1 \in ℤ \land 1 \leq M + 1 \land M + 1 \leq N))$
27	12 26	syl	$⊢ φ \to (M + 1 \in (1 \dots N) \leftrightarrow (M + 1 \in ℤ \land 1 \leq M + 1 \land M + 1 \leq N))$
28	23 27	mpbird	$⊢ φ \to M + 1 \in (1 \dots N)$
29		bcm1k	$⊢ M + 1 \in (1 \dots N) \to (\binom{N}{M + 1}) = (\binom{N}{M + 1 - 1}) (\frac{N - (M + 1 - 1)}{M + 1})$
30	28 29	syl	$⊢ φ \to (\binom{N}{M + 1}) = (\binom{N}{M + 1 - 1}) (\frac{N - (M + 1 - 1)}{M + 1})$
31	4 5	pncand	$⊢ φ \to M + 1 - 1 = M$
32	31	oveq2d	$⊢ φ \to (\binom{N}{M + 1 - 1}) = (\binom{N}{M})$
33	31	oveq2d	$⊢ φ \to N - (M + 1 - 1) = N - M$
34	33	oveq1d	$⊢ φ \to \frac{N - (M + 1 - 1)}{M + 1} = \frac{N - M}{M + 1}$
35	32 34	oveq12d	$⊢ φ \to (\binom{N}{M + 1 - 1}) (\frac{N - (M + 1 - 1)}{M + 1}) = (\binom{N}{M}) (\frac{N - M}{M + 1})$
36	30 35	eqtrd	$⊢ φ \to (\binom{N}{M + 1}) = (\binom{N}{M}) (\frac{N - M}{M + 1})$
37	1	nnred	$⊢ φ \to M \in ℝ$
38	2	nnred	$⊢ φ \to N \in ℝ$
39	37 38 3	ltled	$⊢ φ \to M \leq N$
40	2 7 39	bccl2d	$⊢ φ \to (\binom{N}{M}) \in ℕ$
41	40	nncnd	$⊢ φ \to (\binom{N}{M}) \in ℂ$
42	2	nncnd	$⊢ φ \to N \in ℂ$
43	42 4	subcld	$⊢ φ \to N - M \in ℂ$
44	21	nnne0d	$⊢ φ \to M + 1 \neq 0$
45	41 43 6 44	divassd	$⊢ φ \to \frac{(\binom{N}{M}) (N - M)}{M + 1} = (\binom{N}{M}) (\frac{N - M}{M + 1})$
46	36 45	eqtr4d	$⊢ φ \to (\binom{N}{M + 1}) = \frac{(\binom{N}{M}) (N - M)}{M + 1}$
47	46	eqcomd	$⊢ φ \to \frac{(\binom{N}{M}) (N - M)}{M + 1} = (\binom{N}{M + 1})$
48	41 43	mulcld	$⊢ φ \to (\binom{N}{M}) (N - M) \in ℂ$
49	48 17 6 44	divmul2d	$⊢ φ \to (\frac{(\binom{N}{M}) (N - M)}{M + 1} = (\binom{N}{M + 1}) \leftrightarrow (\binom{N}{M}) (N - M) = (M + 1) (\binom{N}{M + 1}))$
50	47 49	mpbid	$⊢ φ \to (\binom{N}{M}) (N - M) = (M + 1) (\binom{N}{M + 1})$
51	50	eqcomd	$⊢ φ \to (M + 1) (\binom{N}{M + 1}) = (\binom{N}{M}) (N - M)$
52	41 43	mulcomd	$⊢ φ \to (\binom{N}{M}) (N - M) = (N - M) (\binom{N}{M})$
53	51 52	eqtrd	$⊢ φ \to (M + 1) (\binom{N}{M + 1}) = (N - M) (\binom{N}{M})$
54	19 53	eqtrd	$⊢ φ \to \frac{(M + 1) (\binom{N}{M + 1})}{1} = (N - M) (\binom{N}{M})$
55	43 41	mulcld	$⊢ φ \to (N - M) (\binom{N}{M}) \in ℂ$
56	1	nnne0d	$⊢ φ \to M \neq 0$
57	55 4 56	divcan3d	$⊢ φ \to \frac{M (N - M) (\binom{N}{M})}{M} = (N - M) (\binom{N}{M})$
58	54 57	eqtr4d	$⊢ φ \to \frac{(M + 1) (\binom{N}{M + 1})}{1} = \frac{M (N - M) (\binom{N}{M})}{M}$
59	4 43 41	mul12d	$⊢ φ \to M (N - M) (\binom{N}{M}) = (N - M) M (\binom{N}{M})$
60	59	oveq1d	$⊢ φ \to \frac{M (N - M) (\binom{N}{M})}{M} = \frac{(N - M) M (\binom{N}{M})}{M}$
61	58 60	eqtrd	$⊢ φ \to \frac{(M + 1) (\binom{N}{M + 1})}{1} = \frac{(N - M) M (\binom{N}{M})}{M}$
62		0ne1	$⊢ 0 \neq 1$
63	62	a1i	$⊢ φ \to 0 \neq 1$
64	63	necomd	$⊢ φ \to 1 \neq 0$
65	16	nnne0d	$⊢ φ \to (\binom{N}{M + 1}) \neq 0$
66	6 17 44 65	mulne0d	$⊢ φ \to (M + 1) (\binom{N}{M + 1}) \neq 0$
67	4 41	mulcld	$⊢ φ \to M (\binom{N}{M}) \in ℂ$
68	43 67	mulcld	$⊢ φ \to (N - M) M (\binom{N}{M}) \in ℂ$
69	37 3	gtned	$⊢ φ \to N \neq M$
70	42 4 69	subne0d	$⊢ φ \to N - M \neq 0$
71	40	nnne0d	$⊢ φ \to (\binom{N}{M}) \neq 0$
72	4 41 56 71	mulne0d	$⊢ φ \to M (\binom{N}{M}) \neq 0$
73	43 67 70 72	mulne0d	$⊢ φ \to (N - M) M (\binom{N}{M}) \neq 0$
74	5 64 18 66 4 56 68 73	recbothd	$⊢ φ \to (\frac{1}{(M + 1) (\binom{N}{M + 1})} = \frac{M}{(N - M) M (\binom{N}{M})} \leftrightarrow \frac{(M + 1) (\binom{N}{M + 1})}{1} = \frac{(N - M) M (\binom{N}{M})}{M})$
75	61 74	mpbird	$⊢ φ \to \frac{1}{(M + 1) (\binom{N}{M + 1})} = \frac{M}{(N - M) M (\binom{N}{M})}$
76	4	mulid1d	$⊢ φ \to M \cdot 1 = M$
77	76	oveq1d	$⊢ φ \to \frac{M \cdot 1}{(N - M) M (\binom{N}{M})} = \frac{M}{(N - M) M (\binom{N}{M})}$
78	75 77	eqtr4d	$⊢ φ \to \frac{1}{(M + 1) (\binom{N}{M + 1})} = \frac{M \cdot 1}{(N - M) M (\binom{N}{M})}$
79	4 43 5 67 70 72	divmuldivd	$⊢ φ \to (\frac{M}{N - M}) (\frac{1}{M (\binom{N}{M})}) = \frac{M \cdot 1}{(N - M) M (\binom{N}{M})}$
80	78 79	eqtr4d	$⊢ φ \to \frac{1}{(M + 1) (\binom{N}{M + 1})} = (\frac{M}{N - M}) (\frac{1}{M (\binom{N}{M})})$

Metamath Proof Explorer

Theorem lcmineqlem11

Proof