Theorem fac2xp3

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

	Ref	Expression
Assertion	fac2xp3	⊢ ( 𝑥 ∈ ℕ0 → ( ! ‘ ( ( 2 · 𝑥 ) + 3 ) ) = ( ( ! ‘ ( ( 2 · 𝑥 ) + 1 ) ) · ( ( ( 2 · 𝑥 ) + 2 ) · ( ( 2 · 𝑥 ) + 3 ) ) ) )

Proof

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