fac2xp3

Description: Factorial of 2x+3, sublemma for sublemma for AKS. (Contributed by metakunt, 19-Apr-2024)

		Ref	Expression
	Assertion	fac2xp3	$⊢ x \in ℕ_{0} \to (2 x + 3)! = (2 x + 1)! (2 x + 2) (2 x + 3)$

Proof

Step	Hyp	Ref	Expression
1		2cn	$⊢ 2 \in ℂ$
2		nn0cn	$⊢ x \in ℕ_{0} \to x \in ℂ$
3		mulcl	$⊢ (2 \in ℂ \land x \in ℂ) \to 2 x \in ℂ$
4	1 2 3	sylancr	$⊢ x \in ℕ_{0} \to 2 x \in ℂ$
5		ax-1cn	$⊢ 1 \in ℂ$
6		addass	$⊢ (2 x \in ℂ \land 2 \in ℂ \land 1 \in ℂ) \to 2 x + 2 + 1 = 2 x + 2 + 1$
7	1 5 6	mp3an23	$⊢ 2 x \in ℂ \to 2 x + 2 + 1 = 2 x + 2 + 1$
8	4 7	syl	$⊢ x \in ℕ_{0} \to 2 x + 2 + 1 = 2 x + 2 + 1$
9		df-3	$⊢ 3 = 2 + 1$
10	9	a1i	$⊢ x \in ℕ_{0} \to 3 = 2 + 1$
11	10	oveq2d	$⊢ x \in ℕ_{0} \to 2 x + 3 = 2 x + 2 + 1$
12	8 11	eqtr4d	$⊢ x \in ℕ_{0} \to 2 x + 2 + 1 = 2 x + 3$
13	12	fveq2d	$⊢ x \in ℕ_{0} \to (2 x + 2 + 1)! = (2 x + 3)!$
14		2nn0	$⊢ 2 \in ℕ_{0}$
15		nn0mulcl	$⊢ (2 \in ℕ_{0} \land x \in ℕ_{0}) \to 2 x \in ℕ_{0}$
16	14 15	mpan	$⊢ x \in ℕ_{0} \to 2 x \in ℕ_{0}$
17		nn0addcl	$⊢ (2 x \in ℕ_{0} \land 2 \in ℕ_{0}) \to 2 x + 2 \in ℕ_{0}$
18	14 17	mpan2	$⊢ 2 x \in ℕ_{0} \to 2 x + 2 \in ℕ_{0}$
19	16 18	syl	$⊢ x \in ℕ_{0} \to 2 x + 2 \in ℕ_{0}$
20		facp1	$⊢ 2 x + 2 \in ℕ_{0} \to (2 x + 2 + 1)! = (2 x + 2)! (2 x + 2 + 1)$
21	19 20	syl	$⊢ x \in ℕ_{0} \to (2 x + 2 + 1)! = (2 x + 2)! (2 x + 2 + 1)$
22	13 21	eqtr3d	$⊢ x \in ℕ_{0} \to (2 x + 3)! = (2 x + 2)! (2 x + 2 + 1)$
23	12	oveq2d	$⊢ x \in ℕ_{0} \to (2 x + 2)! (2 x + 2 + 1) = (2 x + 2)! (2 x + 3)$
24	22 23	eqtrd	$⊢ x \in ℕ_{0} \to (2 x + 3)! = (2 x + 2)! (2 x + 3)$
25		addass	$⊢ (2 x \in ℂ \land 1 \in ℂ \land 1 \in ℂ) \to 2 x + 1 + 1 = 2 x + 1 + 1$
26	5 5 25	mp3an23	$⊢ 2 x \in ℂ \to 2 x + 1 + 1 = 2 x + 1 + 1$
27	4 26	syl	$⊢ x \in ℕ_{0} \to 2 x + 1 + 1 = 2 x + 1 + 1$
28		df-2	$⊢ 2 = 1 + 1$
29	28	a1i	$⊢ x \in ℕ_{0} \to 2 = 1 + 1$
30	29	oveq2d	$⊢ x \in ℕ_{0} \to 2 x + 2 = 2 x + 1 + 1$
31	27 30	eqtr4d	$⊢ x \in ℕ_{0} \to 2 x + 1 + 1 = 2 x + 2$
32	31	fveq2d	$⊢ x \in ℕ_{0} \to (2 x + 1 + 1)! = (2 x + 2)!$
33		peano2nn0	$⊢ 2 x \in ℕ_{0} \to 2 x + 1 \in ℕ_{0}$
34	16 33	syl	$⊢ x \in ℕ_{0} \to 2 x + 1 \in ℕ_{0}$
35		facp1	$⊢ 2 x + 1 \in ℕ_{0} \to (2 x + 1 + 1)! = (2 x + 1)! (2 x + 1 + 1)$
36	34 35	syl	$⊢ x \in ℕ_{0} \to (2 x + 1 + 1)! = (2 x + 1)! (2 x + 1 + 1)$
37	32 36	eqtr3d	$⊢ x \in ℕ_{0} \to (2 x + 2)! = (2 x + 1)! (2 x + 1 + 1)$
38	31	oveq2d	$⊢ x \in ℕ_{0} \to (2 x + 1)! (2 x + 1 + 1) = (2 x + 1)! (2 x + 2)$
39	37 38	eqtrd	$⊢ x \in ℕ_{0} \to (2 x + 2)! = (2 x + 1)! (2 x + 2)$
40	39	oveq1d	$⊢ x \in ℕ_{0} \to (2 x + 2)! (2 x + 3) = (2 x + 1)! (2 x + 2) (2 x + 3)$
41	40	eqeq2d	$⊢ x \in ℕ_{0} \to ((2 x + 3)! = (2 x + 2)! (2 x + 3) \leftrightarrow (2 x + 3)! = (2 x + 1)! (2 x + 2) (2 x + 3))$
42	24 41	mpbid	$⊢ x \in ℕ_{0} \to (2 x + 3)! = (2 x + 1)! (2 x + 2) (2 x + 3)$
43		faccl	$⊢ 2 x + 1 \in ℕ_{0} \to (2 x + 1)! \in ℕ$
44	34 43	syl	$⊢ x \in ℕ_{0} \to (2 x + 1)! \in ℕ$
45		nncn	$⊢ (2 x + 1)! \in ℕ \to (2 x + 1)! \in ℂ$
46	44 45	syl	$⊢ x \in ℕ_{0} \to (2 x + 1)! \in ℂ$
47		addcl	$⊢ (2 x \in ℂ \land 2 \in ℂ) \to 2 x + 2 \in ℂ$
48	4 1 47	sylancl	$⊢ x \in ℕ_{0} \to 2 x + 2 \in ℂ$
49		3cn	$⊢ 3 \in ℂ$
50		addcl	$⊢ (2 x \in ℂ \land 3 \in ℂ) \to 2 x + 3 \in ℂ$
51	4 49 50	sylancl	$⊢ x \in ℕ_{0} \to 2 x + 3 \in ℂ$
52		mulass	$⊢ ((2 x + 1)! \in ℂ \land 2 x + 2 \in ℂ \land 2 x + 3 \in ℂ) \to (2 x + 1)! (2 x + 2) (2 x + 3) = (2 x + 1)! (2 x + 2) (2 x + 3)$
53	46 48 51 52	syl3anc	$⊢ x \in ℕ_{0} \to (2 x + 1)! (2 x + 2) (2 x + 3) = (2 x + 1)! (2 x + 2) (2 x + 3)$
54	42 53	eqtrd	$⊢ x \in ℕ_{0} \to (2 x + 3)! = (2 x + 1)! (2 x + 2) (2 x + 3)$

Metamath Proof Explorer

Theorem fac2xp3

Proof