Metamath Proof Explorer

Theorem aks6d1c3

Description: Claim 3 of Theorem 6.1 of the AKS inequality lemma. https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 28-Apr-2025)

Ref Expression
Hypotheses aks6d1c3.1 
|- ( ph -> N e. NN )
aks6d1c3.2 
|- ( ph -> P e. Prime )
aks6d1c3.3 
|- ( ph -> P || N )
aks6d1c3.4 
|- ( ph -> R e. NN )
aks6d1c3.5 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c3.6 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
aks6d1c3.7 
|- L = ( ZRHom ` Y )
aks6d1c3.8 
|- Y = ( Z/nZ ` R )
aks6d1c3.9 
|- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
Assertion aks6d1c3 
|- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c3.1 
 |-  ( ph -> N e. NN )
2 aks6d1c3.2 
 |-  ( ph -> P e. Prime )
3 aks6d1c3.3 
 |-  ( ph -> P || N )
4 aks6d1c3.4 
 |-  ( ph -> R e. NN )
5 aks6d1c3.5 
 |-  ( ph -> ( N gcd R ) = 1 )
6 aks6d1c3.6 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
7 aks6d1c3.7 
 |-  L = ( ZRHom ` Y )
8 aks6d1c3.8 
 |-  Y = ( Z/nZ ` R )
9 aks6d1c3.9 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
10 2re 
 |-  2 e. RR
11 10 a1i 
 |-  ( ph -> 2 e. RR )
12 2pos 
 |-  0 < 2
13 12 a1i 
 |-  ( ph -> 0 < 2 )
14 1 nnred 
 |-  ( ph -> N e. RR )
15 1 nngt0d 
 |-  ( ph -> 0 < N )
16 1red 
 |-  ( ph -> 1 e. RR )
17 1lt2 
 |-  1 < 2
18 17 a1i 
 |-  ( ph -> 1 < 2 )
19 16 18 ltned 
 |-  ( ph -> 1 =/= 2 )
20 19 necomd 
 |-  ( ph -> 2 =/= 1 )
21 11 13 14 15 20 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
22 21 resqcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) e. RR )
23 1 nnzd 
 |-  ( ph -> N e. ZZ )
24 odzcl 
 |-  ( ( R e. NN /\ N e. ZZ /\ ( N gcd R ) = 1 ) -> ( ( odZ ` R ) ` N ) e. NN )
25 4 23 5 24 syl3anc 
 |-  ( ph -> ( ( odZ ` R ) ` N ) e. NN )
26 25 nnred 
 |-  ( ph -> ( ( odZ ` R ) ` N ) e. RR )
27 1 2 3 4 5 6 7 8 hashscontpowcl 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
28 27 nn0red 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR )
29 nfv 
 |-  F/ x ph
30 prmnn 
 |-  ( P e. Prime -> P e. NN )
31 2 30 syl 
 |-  ( ph -> P e. NN )
32 31 nnzd 
 |-  ( ph -> P e. ZZ )
33 32 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> P e. ZZ )
34 33 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. NN0 ) -> P e. ZZ )
35 simplr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. NN0 ) -> k e. NN0 )
36 34 35 zexpcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. NN0 ) -> ( P ^ k ) e. ZZ )
37 31 nnne0d 
 |-  ( ph -> P =/= 0 )
38 dvdsval2 
 |-  ( ( P e. ZZ /\ P =/= 0 /\ N e. ZZ ) -> ( P || N <-> ( N / P ) e. ZZ ) )
39 32 37 23 38 syl3anc 
 |-  ( ph -> ( P || N <-> ( N / P ) e. ZZ ) )
40 3 39 mpbid 
 |-  ( ph -> ( N / P ) e. ZZ )
41 40 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( N / P ) e. ZZ )
42 41 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. NN0 ) -> ( N / P ) e. ZZ )
43 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. NN0 ) -> l e. NN0 )
44 42 43 zexpcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. NN0 ) -> ( ( N / P ) ^ l ) e. ZZ )
45 36 44 zmulcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. NN0 ) -> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) e. ZZ )
46 45 ralrimiva 
 |-  ( ( ph /\ k e. NN0 ) -> A. l e. NN0 ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) e. ZZ )
47 46 ralrimiva 
 |-  ( ph -> A. k e. NN0 A. l e. NN0 ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) e. ZZ )
48 6 fmpo 
 |-  ( A. k e. NN0 A. l e. NN0 ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) e. ZZ <-> E : ( NN0 X. NN0 ) --> ZZ )
49 47 48 sylib 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> ZZ )
50 49 ffund 
 |-  ( ph -> Fun E )
51 49 ffvelcdmda 
 |-  ( ( ph /\ x e. ( NN0 X. NN0 ) ) -> ( E ` x ) e. ZZ )
52 29 50 51 funimassd 
 |-  ( ph -> ( E " ( NN0 X. NN0 ) ) C_ ZZ )
53 49 ffnd 
 |-  ( ph -> E Fn ( NN0 X. NN0 ) )
54 53 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> E Fn ( NN0 X. NN0 ) )
55 simpr 
 |-  ( ( ph /\ i e. NN0 ) -> i e. NN0 )
56 55 55 opelxpd 
 |-  ( ( ph /\ i e. NN0 ) -> <. i , i >. e. ( NN0 X. NN0 ) )
57 54 56 56 fnfvimad 
 |-  ( ( ph /\ i e. NN0 ) -> ( E ` <. i , i >. ) e. ( E " ( NN0 X. NN0 ) ) )
58 vex 
 |-  k e. _V
59 vex 
 |-  l e. _V
60 58 59 op1std 
 |-  ( q = <. k , l >. -> ( 1st ` q ) = k )
61 60 oveq2d 
 |-  ( q = <. k , l >. -> ( P ^ ( 1st ` q ) ) = ( P ^ k ) )
62 58 59 op2ndd 
 |-  ( q = <. k , l >. -> ( 2nd ` q ) = l )
63 62 oveq2d 
 |-  ( q = <. k , l >. -> ( ( N / P ) ^ ( 2nd ` q ) ) = ( ( N / P ) ^ l ) )
64 61 63 oveq12d 
 |-  ( q = <. k , l >. -> ( ( P ^ ( 1st ` q ) ) x. ( ( N / P ) ^ ( 2nd ` q ) ) ) = ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
65 64 mpompt 
 |-  ( q e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` q ) ) x. ( ( N / P ) ^ ( 2nd ` q ) ) ) ) = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
66 6 65 eqtr4i 
 |-  E = ( q e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` q ) ) x. ( ( N / P ) ^ ( 2nd ` q ) ) ) )
67 66 a1i 
 |-  ( ( ph /\ i e. NN0 ) -> E = ( q e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` q ) ) x. ( ( N / P ) ^ ( 2nd ` q ) ) ) ) )
68 simpr 
 |-  ( ( ( ph /\ i e. NN0 ) /\ q = <. i , i >. ) -> q = <. i , i >. )
69 68 fveq2d 
 |-  ( ( ( ph /\ i e. NN0 ) /\ q = <. i , i >. ) -> ( 1st ` q ) = ( 1st ` <. i , i >. ) )
70 69 oveq2d 
 |-  ( ( ( ph /\ i e. NN0 ) /\ q = <. i , i >. ) -> ( P ^ ( 1st ` q ) ) = ( P ^ ( 1st ` <. i , i >. ) ) )
71 68 fveq2d 
 |-  ( ( ( ph /\ i e. NN0 ) /\ q = <. i , i >. ) -> ( 2nd ` q ) = ( 2nd ` <. i , i >. ) )
72 71 oveq2d 
 |-  ( ( ( ph /\ i e. NN0 ) /\ q = <. i , i >. ) -> ( ( N / P ) ^ ( 2nd ` q ) ) = ( ( N / P ) ^ ( 2nd ` <. i , i >. ) ) )
73 70 72 oveq12d 
 |-  ( ( ( ph /\ i e. NN0 ) /\ q = <. i , i >. ) -> ( ( P ^ ( 1st ` q ) ) x. ( ( N / P ) ^ ( 2nd ` q ) ) ) = ( ( P ^ ( 1st ` <. i , i >. ) ) x. ( ( N / P ) ^ ( 2nd ` <. i , i >. ) ) ) )
74 opelxp 
 |-  ( <. i , i >. e. ( NN0 X. NN0 ) <-> ( i e. NN0 /\ i e. NN0 ) )
75 56 74 sylib 
 |-  ( ( ph /\ i e. NN0 ) -> ( i e. NN0 /\ i e. NN0 ) )
76 75 74 sylibr 
 |-  ( ( ph /\ i e. NN0 ) -> <. i , i >. e. ( NN0 X. NN0 ) )
77 32 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> P e. ZZ )
78 xp1st 
 |-  ( <. i , i >. e. ( NN0 X. NN0 ) -> ( 1st ` <. i , i >. ) e. NN0 )
79 56 78 syl 
 |-  ( ( ph /\ i e. NN0 ) -> ( 1st ` <. i , i >. ) e. NN0 )
80 77 79 zexpcld 
 |-  ( ( ph /\ i e. NN0 ) -> ( P ^ ( 1st ` <. i , i >. ) ) e. ZZ )
81 40 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> ( N / P ) e. ZZ )
82 xp2nd 
 |-  ( <. i , i >. e. ( NN0 X. NN0 ) -> ( 2nd ` <. i , i >. ) e. NN0 )
83 56 82 syl 
 |-  ( ( ph /\ i e. NN0 ) -> ( 2nd ` <. i , i >. ) e. NN0 )
84 81 83 zexpcld 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( N / P ) ^ ( 2nd ` <. i , i >. ) ) e. ZZ )
85 80 84 zmulcld 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( P ^ ( 1st ` <. i , i >. ) ) x. ( ( N / P ) ^ ( 2nd ` <. i , i >. ) ) ) e. ZZ )
86 67 73 76 85 fvmptd 
 |-  ( ( ph /\ i e. NN0 ) -> ( E ` <. i , i >. ) = ( ( P ^ ( 1st ` <. i , i >. ) ) x. ( ( N / P ) ^ ( 2nd ` <. i , i >. ) ) ) )
87 vex 
 |-  i e. _V
88 87 87 op1st 
 |-  ( 1st ` <. i , i >. ) = i
89 88 a1i 
 |-  ( ( ph /\ i e. NN0 ) -> ( 1st ` <. i , i >. ) = i )
90 89 oveq2d 
 |-  ( ( ph /\ i e. NN0 ) -> ( P ^ ( 1st ` <. i , i >. ) ) = ( P ^ i ) )
91 87 87 op2nd 
 |-  ( 2nd ` <. i , i >. ) = i
92 91 a1i 
 |-  ( ( ph /\ i e. NN0 ) -> ( 2nd ` <. i , i >. ) = i )
93 92 oveq2d 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( N / P ) ^ ( 2nd ` <. i , i >. ) ) = ( ( N / P ) ^ i ) )
94 90 93 oveq12d 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( P ^ ( 1st ` <. i , i >. ) ) x. ( ( N / P ) ^ ( 2nd ` <. i , i >. ) ) ) = ( ( P ^ i ) x. ( ( N / P ) ^ i ) ) )
95 14 recnd 
 |-  ( ph -> N e. CC )
96 95 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> N e. CC )
97 77 zcnd 
 |-  ( ( ph /\ i e. NN0 ) -> P e. CC )
98 37 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> P =/= 0 )
99 96 97 98 divcan2d 
 |-  ( ( ph /\ i e. NN0 ) -> ( P x. ( N / P ) ) = N )
100 99 eqcomd 
 |-  ( ( ph /\ i e. NN0 ) -> N = ( P x. ( N / P ) ) )
101 100 oveq1d 
 |-  ( ( ph /\ i e. NN0 ) -> ( N ^ i ) = ( ( P x. ( N / P ) ) ^ i ) )
102 81 zcnd 
 |-  ( ( ph /\ i e. NN0 ) -> ( N / P ) e. CC )
103 97 102 55 mulexpd 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( P x. ( N / P ) ) ^ i ) = ( ( P ^ i ) x. ( ( N / P ) ^ i ) ) )
104 101 103 eqtr2d 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( P ^ i ) x. ( ( N / P ) ^ i ) ) = ( N ^ i ) )
105 94 104 eqtrd 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( P ^ ( 1st ` <. i , i >. ) ) x. ( ( N / P ) ^ ( 2nd ` <. i , i >. ) ) ) = ( N ^ i ) )
106 86 105 eqtrd 
 |-  ( ( ph /\ i e. NN0 ) -> ( E ` <. i , i >. ) = ( N ^ i ) )
107 106 eleq1d 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( E ` <. i , i >. ) e. ( E " ( NN0 X. NN0 ) ) <-> ( N ^ i ) e. ( E " ( NN0 X. NN0 ) ) ) )
108 57 107 mpbid 
 |-  ( ( ph /\ i e. NN0 ) -> ( N ^ i ) e. ( E " ( NN0 X. NN0 ) ) )
109 108 ralrimiva 
 |-  ( ph -> A. i e. NN0 ( N ^ i ) e. ( E " ( NN0 X. NN0 ) ) )
110 52 1 109 4 5 7 8 hashscontpow 
 |-  ( ph -> ( ( odZ ` R ) ` N ) <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
111 22 26 28 9 110 ltletrd 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )