lcmineqlem18

Description: Technical lemma to shift factors in binomial coefficient. (Contributed by metakunt, 12-May-2024)

		Ref	Expression
	Hypothesis	lcmineqlem18.1	$⊢ φ \to N \in ℕ$
	Assertion	lcmineqlem18	$⊢ φ \to (N + 1) (\binom{2 \cdot N + 1}{N + 1}) = (2 \cdot N + 1) (\binom{2 \cdot N}{N})$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem18.1	$⊢ φ \to N \in ℕ$
2		0zd	$⊢ φ \to 0 \in ℤ$
3		2z	$⊢ 2 \in ℤ$
4	3	a1i	$⊢ φ \to 2 \in ℤ$
5	1	nnzd	$⊢ φ \to N \in ℤ$
6	4 5	zmulcld	$⊢ φ \to 2 \cdot N \in ℤ$
7	6	peano2zd	$⊢ φ \to 2 \cdot N + 1 \in ℤ$
8	5	peano2zd	$⊢ φ \to N + 1 \in ℤ$
9	2 7 8	3jca	$⊢ φ \to (0 \in ℤ \land 2 \cdot N + 1 \in ℤ \land N + 1 \in ℤ)$
10	1	nnred	$⊢ φ \to N \in ℝ$
11		1red	$⊢ φ \to 1 \in ℝ$
12	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
13	12	nn0ge0d	$⊢ φ \to 0 \leq N$
14		0le1	$⊢ 0 \leq 1$
15	14	a1i	$⊢ φ \to 0 \leq 1$
16	10 11 13 15	addge0d	$⊢ φ \to 0 \leq N + 1$
17	10 11	readdcld	$⊢ φ \to N + 1 \in ℝ$
18	17 10	addge01d	$⊢ φ \to (0 \leq N \leftrightarrow N + 1 \leq N + 1 + N)$
19	13 18	mpbid	$⊢ φ \to N + 1 \leq N + 1 + N$
20	10	recnd	$⊢ φ \to N \in ℂ$
21		1cnd	$⊢ φ \to 1 \in ℂ$
22	20 21 20	add32d	$⊢ φ \to N + 1 + N = N + N + 1$
23	20	2timesd	$⊢ φ \to 2 \cdot N = N + N$
24	23	oveq1d	$⊢ φ \to 2 \cdot N + 1 = N + N + 1$
25	24	eqcomd	$⊢ φ \to N + N + 1 = 2 \cdot N + 1$
26	22 25	eqtrd	$⊢ φ \to N + 1 + N = 2 \cdot N + 1$
27	19 26	breqtrd	$⊢ φ \to N + 1 \leq 2 \cdot N + 1$
28	16 27	jca	$⊢ φ \to (0 \leq N + 1 \land N + 1 \leq 2 \cdot N + 1)$
29	9 28	jca	$⊢ φ \to ((0 \in ℤ \land 2 \cdot N + 1 \in ℤ \land N + 1 \in ℤ) \land (0 \leq N + 1 \land N + 1 \leq 2 \cdot N + 1))$
30		elfz2	$⊢ N + 1 \in (0 \dots 2 \cdot N + 1) \leftrightarrow ((0 \in ℤ \land 2 \cdot N + 1 \in ℤ \land N + 1 \in ℤ) \land (0 \leq N + 1 \land N + 1 \leq 2 \cdot N + 1))$
31	29 30	sylibr	$⊢ φ \to N + 1 \in (0 \dots 2 \cdot N + 1)$
32		bcval2	$⊢ N + 1 \in (0 \dots 2 \cdot N + 1) \to (\binom{2 \cdot N + 1}{N + 1}) = \frac{(2 \cdot N + 1)!}{(2 \cdot N + 1 - (N + 1))! (N + 1)!}$
33	31 32	syl	$⊢ φ \to (\binom{2 \cdot N + 1}{N + 1}) = \frac{(2 \cdot N + 1)!}{(2 \cdot N + 1 - (N + 1))! (N + 1)!}$
34	6	zcnd	$⊢ φ \to 2 \cdot N \in ℂ$
35	34 21 20 21	addsub4d	$⊢ φ \to 2 \cdot N + 1 - (N + 1) = (2 \cdot N - N) + 1 - 1$
36	23	oveq1d	$⊢ φ \to 2 \cdot N - N = N + N - N$
37	20 20	pncand	$⊢ φ \to N + N - N = N$
38	36 37	eqtrd	$⊢ φ \to 2 \cdot N - N = N$
39		1m1e0	$⊢ 1 - 1 = 0$
40	39	a1i	$⊢ φ \to 1 - 1 = 0$
41	38 40	oveq12d	$⊢ φ \to (2 \cdot N - N) + 1 - 1 = N + 0$
42	20	addid1d	$⊢ φ \to N + 0 = N$
43	41 42	eqtrd	$⊢ φ \to (2 \cdot N - N) + 1 - 1 = N$
44	35 43	eqtrd	$⊢ φ \to 2 \cdot N + 1 - (N + 1) = N$
45	44	fveq2d	$⊢ φ \to (2 \cdot N + 1 - (N + 1))! = N!$
46	45	oveq1d	$⊢ φ \to (2 \cdot N + 1 - (N + 1))! (N + 1)! = N! (N + 1)!$
47	46	oveq2d	$⊢ φ \to \frac{(2 \cdot N + 1)!}{(2 \cdot N + 1 - (N + 1))! (N + 1)!} = \frac{(2 \cdot N + 1)!}{N! (N + 1)!}$
48	33 47	eqtrd	$⊢ φ \to (\binom{2 \cdot N + 1}{N + 1}) = \frac{(2 \cdot N + 1)!}{N! (N + 1)!}$
49		faccl	$⊢ N \in ℕ_{0} \to N! \in ℕ$
50	12 49	syl	$⊢ φ \to N! \in ℕ$
51	50	nncnd	$⊢ φ \to N! \in ℂ$
52		1nn0	$⊢ 1 \in ℕ_{0}$
53	52	a1i	$⊢ φ \to 1 \in ℕ_{0}$
54	12 53	nn0addcld	$⊢ φ \to N + 1 \in ℕ_{0}$
55		faccl	$⊢ N + 1 \in ℕ_{0} \to (N + 1)! \in ℕ$
56	54 55	syl	$⊢ φ \to (N + 1)! \in ℕ$
57	56	nncnd	$⊢ φ \to (N + 1)! \in ℂ$
58	51 57	mulcomd	$⊢ φ \to N! (N + 1)! = (N + 1)! N!$
59		facp1	$⊢ N \in ℕ_{0} \to (N + 1)! = N! (N + 1)$
60	12 59	syl	$⊢ φ \to (N + 1)! = N! (N + 1)$
61	20 21	addcld	$⊢ φ \to N + 1 \in ℂ$
62	51 61	mulcomd	$⊢ φ \to N! (N + 1) = (N + 1) N!$
63	60 62	eqtrd	$⊢ φ \to (N + 1)! = (N + 1) N!$
64	63	oveq1d	$⊢ φ \to (N + 1)! N! = (N + 1) N! N!$
65	61 51 51	mulassd	$⊢ φ \to (N + 1) N! N! = (N + 1) N! N!$
66	64 65	eqtrd	$⊢ φ \to (N + 1)! N! = (N + 1) N! N!$
67	58 66	eqtrd	$⊢ φ \to N! (N + 1)! = (N + 1) N! N!$
68	67	oveq2d	$⊢ φ \to \frac{(2 \cdot N + 1)!}{N! (N + 1)!} = \frac{(2 \cdot N + 1)!}{(N + 1) N! N!}$
69	48 68	eqtrd	$⊢ φ \to (\binom{2 \cdot N + 1}{N + 1}) = \frac{(2 \cdot N + 1)!}{(N + 1) N! N!}$
70		2nn0	$⊢ 2 \in ℕ_{0}$
71	70	a1i	$⊢ φ \to 2 \in ℕ_{0}$
72	71 12	nn0mulcld	$⊢ φ \to 2 \cdot N \in ℕ_{0}$
73		facp1	$⊢ 2 \cdot N \in ℕ_{0} \to (2 \cdot N + 1)! = 2 \cdot N! (2 \cdot N + 1)$
74	72 73	syl	$⊢ φ \to (2 \cdot N + 1)! = 2 \cdot N! (2 \cdot N + 1)$
75		faccl	$⊢ 2 \cdot N \in ℕ_{0} \to 2 \cdot N! \in ℕ$
76	72 75	syl	$⊢ φ \to 2 \cdot N! \in ℕ$
77	76	nncnd	$⊢ φ \to 2 \cdot N! \in ℂ$
78	34 21	addcld	$⊢ φ \to 2 \cdot N + 1 \in ℂ$
79	77 78	mulcomd	$⊢ φ \to 2 \cdot N! (2 \cdot N + 1) = (2 \cdot N + 1) 2 \cdot N!$
80	74 79	eqtrd	$⊢ φ \to (2 \cdot N + 1)! = (2 \cdot N + 1) 2 \cdot N!$
81	80	oveq1d	$⊢ φ \to \frac{(2 \cdot N + 1)!}{(N + 1) N! N!} = \frac{(2 \cdot N + 1) 2 \cdot N!}{(N + 1) N! N!}$
82	69 81	eqtrd	$⊢ φ \to (\binom{2 \cdot N + 1}{N + 1}) = \frac{(2 \cdot N + 1) 2 \cdot N!}{(N + 1) N! N!}$
83	82	oveq2d	$⊢ φ \to (N + 1) (\binom{2 \cdot N + 1}{N + 1}) = (N + 1) (\frac{(2 \cdot N + 1) 2 \cdot N!}{(N + 1) N! N!})$
84	78 77	mulcld	$⊢ φ \to (2 \cdot N + 1) 2 \cdot N! \in ℂ$
85	51 51	mulcld	$⊢ φ \to N! N! \in ℂ$
86	61 85	mulcld	$⊢ φ \to (N + 1) N! N! \in ℂ$
87	1	peano2nnd	$⊢ φ \to N + 1 \in ℕ$
88	87	nnne0d	$⊢ φ \to N + 1 \neq 0$
89	50	nnne0d	$⊢ φ \to N! \neq 0$
90	51 51 89 89	mulne0d	$⊢ φ \to N! N! \neq 0$
91	61 85 88 90	mulne0d	$⊢ φ \to (N + 1) N! N! \neq 0$
92	61 84 86 91	divassd	$⊢ φ \to \frac{(N + 1) (2 \cdot N + 1) 2 \cdot N!}{(N + 1) N! N!} = (N + 1) (\frac{(2 \cdot N + 1) 2 \cdot N!}{(N + 1) N! N!})$
93	92	eqcomd	$⊢ φ \to (N + 1) (\frac{(2 \cdot N + 1) 2 \cdot N!}{(N + 1) N! N!}) = \frac{(N + 1) (2 \cdot N + 1) 2 \cdot N!}{(N + 1) N! N!}$
94	83 93	eqtrd	$⊢ φ \to (N + 1) (\binom{2 \cdot N + 1}{N + 1}) = \frac{(N + 1) (2 \cdot N + 1) 2 \cdot N!}{(N + 1) N! N!}$
95	61 61 84 85 88 90	divmuldivd	$⊢ φ \to (\frac{N + 1}{N + 1}) (\frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!}) = \frac{(N + 1) (2 \cdot N + 1) 2 \cdot N!}{(N + 1) N! N!}$
96	95	eqcomd	$⊢ φ \to \frac{(N + 1) (2 \cdot N + 1) 2 \cdot N!}{(N + 1) N! N!} = (\frac{N + 1}{N + 1}) (\frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!})$
97	94 96	eqtrd	$⊢ φ \to (N + 1) (\binom{2 \cdot N + 1}{N + 1}) = (\frac{N + 1}{N + 1}) (\frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!})$
98	61 88	dividd	$⊢ φ \to \frac{N + 1}{N + 1} = 1$
99	98	oveq1d	$⊢ φ \to (\frac{N + 1}{N + 1}) (\frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!}) = 1 (\frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!})$
100	84 85 90	divcld	$⊢ φ \to \frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!} \in ℂ$
101	100	mulid2d	$⊢ φ \to 1 (\frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!}) = \frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!}$
102	99 101	eqtrd	$⊢ φ \to (\frac{N + 1}{N + 1}) (\frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!}) = \frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!}$
103	97 102	eqtrd	$⊢ φ \to (N + 1) (\binom{2 \cdot N + 1}{N + 1}) = \frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!}$
104	78 77 85 90	divassd	$⊢ φ \to \frac{(2 \cdot N + 1) 2 \cdot N!}{N! N!} = (2 \cdot N + 1) (\frac{2 \cdot N!}{N! N!})$
105	103 104	eqtrd	$⊢ φ \to (N + 1) (\binom{2 \cdot N + 1}{N + 1}) = (2 \cdot N + 1) (\frac{2 \cdot N!}{N! N!})$
106	2 6 5	3jca	$⊢ φ \to (0 \in ℤ \land 2 \cdot N \in ℤ \land N \in ℤ)$
107	10 10	addge01d	$⊢ φ \to (0 \leq N \leftrightarrow N \leq N + N)$
108	23	breq2d	$⊢ φ \to (N \leq 2 \cdot N \leftrightarrow N \leq N + N)$
109	107 108	bitr4d	$⊢ φ \to (0 \leq N \leftrightarrow N \leq 2 \cdot N)$
110	13 109	mpbid	$⊢ φ \to N \leq 2 \cdot N$
111	13 110	jca	$⊢ φ \to (0 \leq N \land N \leq 2 \cdot N)$
112	106 111	jca	$⊢ φ \to ((0 \in ℤ \land 2 \cdot N \in ℤ \land N \in ℤ) \land (0 \leq N \land N \leq 2 \cdot N))$
113		elfz2	$⊢ N \in (0 \dots 2 \cdot N) \leftrightarrow ((0 \in ℤ \land 2 \cdot N \in ℤ \land N \in ℤ) \land (0 \leq N \land N \leq 2 \cdot N))$
114	112 113	sylibr	$⊢ φ \to N \in (0 \dots 2 \cdot N)$
115		bcval2	$⊢ N \in (0 \dots 2 \cdot N) \to (\binom{2 \cdot N}{N}) = \frac{2 \cdot N!}{(2 \cdot N - N)! N!}$
116	114 115	syl	$⊢ φ \to (\binom{2 \cdot N}{N}) = \frac{2 \cdot N!}{(2 \cdot N - N)! N!}$
117	38	fveq2d	$⊢ φ \to (2 \cdot N - N)! = N!$
118	117	oveq1d	$⊢ φ \to (2 \cdot N - N)! N! = N! N!$
119	118	oveq2d	$⊢ φ \to \frac{2 \cdot N!}{(2 \cdot N - N)! N!} = \frac{2 \cdot N!}{N! N!}$
120	116 119	eqtrd	$⊢ φ \to (\binom{2 \cdot N}{N}) = \frac{2 \cdot N!}{N! N!}$
121	120	oveq2d	$⊢ φ \to (2 \cdot N + 1) (\binom{2 \cdot N}{N}) = (2 \cdot N + 1) (\frac{2 \cdot N!}{N! N!})$
122	121	eqcomd	$⊢ φ \to (2 \cdot N + 1) (\frac{2 \cdot N!}{N! N!}) = (2 \cdot N + 1) (\binom{2 \cdot N}{N})$
123	105 122	eqtrd	$⊢ φ \to (N + 1) (\binom{2 \cdot N + 1}{N + 1}) = (2 \cdot N + 1) (\binom{2 \cdot N}{N})$

Metamath Proof Explorer

Theorem lcmineqlem18

Proof