Theorem 2np3bcnp1

Description: Part of induction step for 2ap1caineq . (Contributed by metakunt, 8-Jun-2024)

	Ref	Expression
Hypothesis	2np3bcnp1.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	2np3bcnp1	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2\left(N+1\right)+1}{N+1}\right)=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		2np3bcnp1.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		2cnd	$$⊢\phi \to 2\in ℂ$$
3	1	nn0cnd	$$⊢\phi \to N\in ℂ$$
4		1cnd	$$⊢\phi \to 1\in ℂ$$
5	2 3 4	adddid	$$⊢\phi \to 2\left(N+1\right)=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot 1$$
6		2t1e2	$$⊢2\cdot 1=2$$
7	6	oveq2i	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\cdot 1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2$$
8	5 7	eqtrdi	$$⊢\phi \to 2\left(N+1\right)=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2$$
9	8	oveq1d	$$⊢\phi \to 2\left(N+1\right)+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2+1$$
10	2 3	mulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
11	10 2 4	addassd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2+1$$
12	9 11	eqtrd	$$⊢\phi \to 2\left(N+1\right)+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2+1$$
13		2p1e3	$$⊢2+1=3$$
14	13	a1i	$$⊢\phi \to 2+1=3$$
15	14	oveq2d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3$$
16	12 15	eqtrd	$$⊢\phi \to 2\left(N+1\right)+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3$$
17	16	oveq1d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2\left(N+1\right)+1}{N+1}\right)=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+1}\right)$$
18		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
19		2z	$$⊢2\in \mathbb{Z}$$
20	19	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
21	1	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
22	20 21	zmulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}$$
23		3z	$$⊢3\in \mathbb{Z}$$
24	23	a1i	$$⊢\phi \to 3\in \mathbb{Z}$$
25	22 24	zaddcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\in \mathbb{Z}$$
26	21	peano2zd	$$⊢\phi \to N+1\in \mathbb{Z}$$
27	1	nn0red	$$⊢\phi \to N\in ℝ$$
28		1red	$$⊢\phi \to 1\in ℝ$$
29	1	nn0ge0d	$$⊢\phi \to 0\le N$$
30		0le1	$$⊢0\le 1$$
31	30	a1i	$$⊢\phi \to 0\le 1$$
32	27 28 29 31	addge0d	$$⊢\phi \to 0\le N+1$$
33		2re	$$⊢2\in ℝ$$
34	33	a1i	$$⊢\phi \to 2\in ℝ$$
35	34 27	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
36		3re	$$⊢3\in ℝ$$
37	36	a1i	$$⊢\phi \to 3\in ℝ$$
38		1le2	$$⊢1\le 2$$
39	38	a1i	$$⊢\phi \to 1\le 2$$
40	27 34 29 39	lemulge12d	$$⊢\phi \to N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
41		1le3	$$⊢1\le 3$$
42	41	a1i	$$⊢\phi \to 1\le 3$$
43	27 28 35 37 40 42	le2addd	$$⊢\phi \to N+1\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3$$
44	18 25 26 32 43	elfzd	$$⊢\phi \to N+1\in \left(0\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)$$
45		bcval2	$$⊢N+1\in \left(0\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)\to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+1}\right)=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!}{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3-\left(N+1\right)\right)!\left(N+1\right)!}$$
46	44 45	syl	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+1}\right)=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!}{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3-\left(N+1\right)\right)!\left(N+1\right)!}$$
47	37	recnd	$$⊢\phi \to 3\in ℂ$$
48	10 47 3 4	addsub4d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3-\left(N+1\right)=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N\right)+3-1$$
49		2txmxeqx	$$⊢N\in ℂ\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N=N$$
50	3 49	syl	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N=N$$
51		3m1e2	$$⊢3-1=2$$
52	51	a1i	$$⊢\phi \to 3-1=2$$
53	50 52	oveq12d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N\right)+3-1=N+2$$
54	48 53	eqtrd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3-\left(N+1\right)=N+2$$
55	54	fveq2d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3-\left(N+1\right)\right)!=\left(N+2\right)!$$
56	55	oveq1d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3-\left(N+1\right)\right)!\left(N+1\right)!=\left(N+2\right)!\left(N+1\right)!$$
57	56	oveq2d	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!}{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3-\left(N+1\right)\right)!\left(N+1\right)!}=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!}{\left(N+2\right)!\left(N+1\right)!}$$
58		2nn0	$$⊢2\in {\mathbb{N}}_0$$
59	58	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
60	1 59	nn0addcld	$$⊢\phi \to N+2\in {\mathbb{N}}_0$$
61	60	faccld	$$⊢\phi \to \left(N+2\right)!\in \mathbb{N}$$
62	61	nncnd	$$⊢\phi \to \left(N+2\right)!\in ℂ$$
63		1nn0	$$⊢1\in {\mathbb{N}}_0$$
64	63	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
65	1 64	nn0addcld	$$⊢\phi \to N+1\in {\mathbb{N}}_0$$
66	65	faccld	$$⊢\phi \to \left(N+1\right)!\in \mathbb{N}$$
67	66	nncnd	$$⊢\phi \to \left(N+1\right)!\in ℂ$$
68	62 67	mulcomd	$$⊢\phi \to \left(N+2\right)!\left(N+1\right)!=\left(N+1\right)!\left(N+2\right)!$$
69	68	oveq2d	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!}{\left(N+2\right)!\left(N+1\right)!}=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!}{\left(N+1\right)!\left(N+2\right)!}$$
70	10 4 2	addassd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2$$
71		1p2e3	$$⊢1+2=3$$
72	71	oveq2i	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3$$
73	70 72	eqtrdi	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3$$
74	73	fveq2d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2\right)!=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!$$
75	74	eqcomd	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2\right)!$$
76	59 1	nn0mulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0$$
77	76 64	nn0addcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in {\mathbb{N}}_0$$
78		facp2	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in {\mathbb{N}}_0\to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2\right)!=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2\right)$$
79	77 78	syl	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2\right)!=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2\right)$$
80	75 79	eqtrd	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2\right)$$
81	10 4 4	addassd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1$$
82		1p1e2	$$⊢1+1=2$$
83	82	a1i	$$⊢\phi \to 1+1=2$$
84	83	oveq2d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2$$
85	81 84	eqtrd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2$$
86	71	a1i	$$⊢\phi \to 1+2=3$$
87	86	oveq2d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3$$
88	70 87	eqtrd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3$$
89	85 88	oveq12d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2\right)=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)$$
90	89	oveq2d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+1\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1+2\right)=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)$$
91	80 90	eqtrd	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)$$
92	91	oveq1d	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!}{\left(N+1\right)!\left(N+2\right)!}=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)!\left(N+2\right)!}$$
93		facp2	$$⊢N\in {\mathbb{N}}_0\to \left(N+2\right)!=N!\left(N+1\right)\left(N+2\right)$$
94	1 93	syl	$$⊢\phi \to \left(N+2\right)!=N!\left(N+1\right)\left(N+2\right)$$
95	94	oveq2d	$$⊢\phi \to \left(N+1\right)!\left(N+2\right)!=\left(N+1\right)!N!\left(N+1\right)\left(N+2\right)$$
96	95	oveq2d	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)!\left(N+2\right)!}=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)!N!\left(N+1\right)\left(N+2\right)}$$
97	1	faccld	$$⊢\phi \to N!\in \mathbb{N}$$
98	97	nncnd	$$⊢\phi \to N!\in ℂ$$
99	3 4	addcld	$$⊢\phi \to N+1\in ℂ$$
100	3 2	addcld	$$⊢\phi \to N+2\in ℂ$$
101	99 100	mulcld	$$⊢\phi \to \left(N+1\right)\left(N+2\right)\in ℂ$$
102	67 98 101	mulassd	$$⊢\phi \to \left(N+1\right)!N!\left(N+1\right)\left(N+2\right)=\left(N+1\right)!N!\left(N+1\right)\left(N+2\right)$$
103	102	eqcomd	$$⊢\phi \to \left(N+1\right)!N!\left(N+1\right)\left(N+2\right)=\left(N+1\right)!N!\left(N+1\right)\left(N+2\right)$$
104	103	oveq2d	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)!N!\left(N+1\right)\left(N+2\right)}=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)!N!\left(N+1\right)\left(N+2\right)}$$
105	77	faccld	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\in \mathbb{N}$$
106	105	nncnd	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\in ℂ$$
107	67 98	mulcld	$$⊢\phi \to \left(N+1\right)!N!\in ℂ$$
108	10 2	addcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\in ℂ$$
109	10 47	addcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\in ℂ$$
110	108 109	mulcld	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)\in ℂ$$
111	66	nnne0d	$$⊢\phi \to \left(N+1\right)!\ne 0$$
112	97	nnne0d	$$⊢\phi \to N!\ne 0$$
113	67 98 111 112	mulne0d	$$⊢\phi \to \left(N+1\right)!N!\ne 0$$
114		0red	$$⊢\phi \to 0\in ℝ$$
115	27 28	readdcld	$$⊢\phi \to N+1\in ℝ$$
116	27	ltp1d	$$⊢\phi \to N<N+1$$
117	114 27 115 29 116	lelttrd	$$⊢\phi \to 0<N+1$$
118	114 117	ltned	$$⊢\phi \to 0\ne N+1$$
119	118	necomd	$$⊢\phi \to N+1\ne 0$$
120	27 34	readdcld	$$⊢\phi \to N+2\in ℝ$$
121		2rp	$$⊢2\in {ℝ}^{+}$$
122	121	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
123	27 122	ltaddrpd	$$⊢\phi \to N<N+2$$
124	114 27 120 29 123	lelttrd	$$⊢\phi \to 0<N+2$$
125	114 124	ltned	$$⊢\phi \to 0\ne N+2$$
126	125	necomd	$$⊢\phi \to N+2\ne 0$$
127	99 100 119 126	mulne0d	$$⊢\phi \to \left(N+1\right)\left(N+2\right)\ne 0$$
128	106 107 110 101 113 127	divmuldivd	$$⊢\phi \to \left(\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!}{\left(N+1\right)!N!}\right)\left(\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)\left(N+2\right)}\right)=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)!N!\left(N+1\right)\left(N+2\right)}$$
129	128	eqcomd	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)!N!\left(N+1\right)\left(N+2\right)}=\left(\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!}{\left(N+1\right)!N!}\right)\left(\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)\left(N+2\right)}\right)$$
130	22	peano2zd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in \mathbb{Z}$$
131	35 28	readdcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in ℝ$$
132	35	lep1d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
133	27 35 131 40 132	letrd	$$⊢\phi \to N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
134	18 130 21 29 133	elfzd	$$⊢\phi \to N\in \left(0\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)$$
135		bcval2	$$⊢N\in \left(0\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!}{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-N\right)!N!}$$
136	134 135	syl	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!}{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-N\right)!N!}$$
137	10 4 3	addsubd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-N=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N+1$$
138	50	oveq1d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-N+1=N+1$$
139	137 138	eqtrd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-N=N+1$$
140	139	fveq2d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-N\right)!=\left(N+1\right)!$$
141	140	oveq1d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-N\right)!N!=\left(N+1\right)!N!$$
142	141	oveq2d	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!}{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-N\right)!N!}=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!}{\left(N+1\right)!N!}$$
143	136 142	eqtrd	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!}{\left(N+1\right)!N!}$$
144	143	eqcomd	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!}{\left(N+1\right)!N!}=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)$$
145	108 99 109 100 119 126	divmuldivd	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}{N+1}\right)\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)=\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)\left(N+2\right)}$$
146	145	eqcomd	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)\left(N+2\right)}=\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}{N+1}\right)\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
147	8	eqcomd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2=2\left(N+1\right)$$
148	147	oveq1d	$$⊢\phi \to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}{N+1}=\frac{2\left(N+1\right)}{N+1}$$
149	2 99 119	divcan4d	$$⊢\phi \to \frac{2\left(N+1\right)}{N+1}=2$$
150	148 149	eqtrd	$$⊢\phi \to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}{N+1}=2$$
151		eqidd	$$⊢\phi \to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}=\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}$$
152	150 151	oveq12d	$$⊢\phi \to \left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}{N+1}\right)\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)=2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
153	146 152	eqtrd	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)\left(N+2\right)}=2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
154	144 153	oveq12d	$$⊢\phi \to \left(\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!}{\left(N+1\right)!N!}\right)\left(\frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)\left(N+2\right)}\right)=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
155	129 154	eqtrd	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)!N!\left(N+1\right)\left(N+2\right)}=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
156	104 155	eqtrd	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)!N!\left(N+1\right)\left(N+2\right)}=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
157	96 156	eqtrd	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)!\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)}{\left(N+1\right)!\left(N+2\right)!}=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
158	92 157	eqtrd	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!}{\left(N+1\right)!\left(N+2\right)!}=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
159	69 158	eqtrd	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!}{\left(N+2\right)!\left(N+1\right)!}=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
160	57 159	eqtrd	$$⊢\phi \to \frac{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3\right)!}{\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3-\left(N+1\right)\right)!\left(N+1\right)!}=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
161	46 160	eqtrd	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+1}\right)=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$
162	17 161	eqtrd	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2\left(N+1\right)+1}{N+1}\right)=\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N}\right)2\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+3}{N+2}\right)$$