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 
|- ( x e. NN0 -> ( ! ` ( ( 2 x. x ) + 3 ) ) = ( ( ! ` ( ( 2 x. x ) + 1 ) ) x. ( ( ( 2 x. x ) + 2 ) x. ( ( 2 x. x ) + 3 ) ) ) )

Proof

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