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