Metamath Proof Explorer

Theorem aks6d1c2p1

Description: In the AKS-theorem the subset defined by E takes values in the positive integers. (Contributed by metakunt, 7-Jan-2025)

Ref Expression
Hypotheses aks6d1c2p1.1 
|- ( ph -> N e. NN )
aks6d1c2p1.2 
|- ( ph -> P e. Prime )
aks6d1c2p1.3 
|- ( ph -> P || N )
aks6d1c2p1.4 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
Assertion aks6d1c2p1 
|- ( ph -> E : ( NN0 X. NN0 ) --> NN )

Proof

Step Hyp Ref Expression
1 aks6d1c2p1.1 
 |-  ( ph -> N e. NN )
2 aks6d1c2p1.2 
 |-  ( ph -> P e. Prime )
3 aks6d1c2p1.3 
 |-  ( ph -> P || N )
4 aks6d1c2p1.4 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
5 prmnn 
 |-  ( P e. Prime -> P e. NN )
6 2 5 syl 
 |-  ( ph -> P e. NN )
7 6 adantr 
 |-  ( ( ph /\ a e. ( NN0 X. NN0 ) ) -> P e. NN )
8 simpr 
 |-  ( ( ph /\ a e. ( NN0 X. NN0 ) ) -> a e. ( NN0 X. NN0 ) )
9 xp1st 
 |-  ( a e. ( NN0 X. NN0 ) -> ( 1st ` a ) e. NN0 )
10 8 9 syl 
 |-  ( ( ph /\ a e. ( NN0 X. NN0 ) ) -> ( 1st ` a ) e. NN0 )
11 7 10 nnexpcld 
 |-  ( ( ph /\ a e. ( NN0 X. NN0 ) ) -> ( P ^ ( 1st ` a ) ) e. NN )
12 1 6 jca 
 |-  ( ph -> ( N e. NN /\ P e. NN ) )
13 nndivdvds 
 |-  ( ( N e. NN /\ P e. NN ) -> ( P || N <-> ( N / P ) e. NN ) )
14 12 13 syl 
 |-  ( ph -> ( P || N <-> ( N / P ) e. NN ) )
15 3 14 mpbid 
 |-  ( ph -> ( N / P ) e. NN )
16 15 adantr 
 |-  ( ( ph /\ a e. ( NN0 X. NN0 ) ) -> ( N / P ) e. NN )
17 xp2nd 
 |-  ( a e. ( NN0 X. NN0 ) -> ( 2nd ` a ) e. NN0 )
18 8 17 syl 
 |-  ( ( ph /\ a e. ( NN0 X. NN0 ) ) -> ( 2nd ` a ) e. NN0 )
19 16 18 nnexpcld 
 |-  ( ( ph /\ a e. ( NN0 X. NN0 ) ) -> ( ( N / P ) ^ ( 2nd ` a ) ) e. NN )
20 11 19 nnmulcld 
 |-  ( ( ph /\ a e. ( NN0 X. NN0 ) ) -> ( ( P ^ ( 1st ` a ) ) x. ( ( N / P ) ^ ( 2nd ` a ) ) ) e. NN )
21 vex 
 |-  k e. _V
22 vex 
 |-  l e. _V
23 21 22 op1std 
 |-  ( a = <. k , l >. -> ( 1st ` a ) = k )
24 23 oveq2d 
 |-  ( a = <. k , l >. -> ( P ^ ( 1st ` a ) ) = ( P ^ k ) )
25 21 22 op2ndd 
 |-  ( a = <. k , l >. -> ( 2nd ` a ) = l )
26 25 oveq2d 
 |-  ( a = <. k , l >. -> ( ( N / P ) ^ ( 2nd ` a ) ) = ( ( N / P ) ^ l ) )
27 24 26 oveq12d 
 |-  ( a = <. k , l >. -> ( ( P ^ ( 1st ` a ) ) x. ( ( N / P ) ^ ( 2nd ` a ) ) ) = ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
28 27 mpompt 
 |-  ( a e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` a ) ) x. ( ( N / P ) ^ ( 2nd ` a ) ) ) ) = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
29 28 eqcomi 
 |-  ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) = ( a e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` a ) ) x. ( ( N / P ) ^ ( 2nd ` a ) ) ) )
30 4 29 eqtri 
 |-  E = ( a e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` a ) ) x. ( ( N / P ) ^ ( 2nd ` a ) ) ) )
31 20 30 fmptd 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> NN )