Metamath Proof Explorer

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 ) ) ) )