Metamath Proof Explorer

Theorem aks4d1

Description: Lemma 4.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf , existence of a polynomially bounded number by the digit size of N that asserts the polynomial subspace that we need to search to guarantee that N is prime. Eventually we want to show that the polynomial searching space is bounded by degree B . (Contributed by metakunt, 14-Nov-2024)

Ref Expression
Hypotheses aks4d1.1 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks4d1.2 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
Assertion aks4d1 
|- ( ph -> E. r e. ( 1 ... B ) ( ( N gcd r ) = 1 /\ ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` r ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1.2 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
3 oveq2 
 |-  ( b = a -> ( N ^ b ) = ( N ^ a ) )
4 3 oveq1d 
 |-  ( b = a -> ( ( N ^ b ) - 1 ) = ( ( N ^ a ) - 1 ) )
5 4 cbvprodv 
 |-  prod_ b e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ b ) - 1 ) = prod_ a e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ a ) - 1 )
6 5 oveq2i 
 |-  ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ b e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ b ) - 1 ) ) = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ a e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ a ) - 1 ) )
7 id 
 |-  ( h = k -> h = k )
8 oveq2 
 |-  ( c = b -> ( N ^ c ) = ( N ^ b ) )
9 8 oveq1d 
 |-  ( c = b -> ( ( N ^ c ) - 1 ) = ( ( N ^ b ) - 1 ) )
10 9 cbvprodv 
 |-  prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) = prod_ b e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ b ) - 1 )
11 10 oveq2i 
 |-  ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ b e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ b ) - 1 ) )
12 11 a1i 
 |-  ( h = k -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ b e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ b ) - 1 ) ) )
13 7 12 breq12d 
 |-  ( h = k -> ( h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) <-> k || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ b e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ b ) - 1 ) ) ) )
14 13 notbid 
 |-  ( h = k -> ( -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) <-> -. k || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ b e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ b ) - 1 ) ) ) )
15 14 cbvrabv 
 |-  { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } = { k e. ( 1 ... B ) | -. k || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ b e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ b ) - 1 ) ) }
16 15 infeq1i 
 |-  inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) = inf ( { k e. ( 1 ... B ) | -. k || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ b e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ b ) - 1 ) ) } , RR , < )
17 1 6 2 16 aks4d1p4 
 |-  ( ph -> ( inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) e. ( 1 ... B ) /\ -. inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ b e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ b ) - 1 ) ) ) )
18 17 simpld 
 |-  ( ph -> inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) e. ( 1 ... B ) )
19 oveq2 
 |-  ( r = inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) -> ( N gcd r ) = ( N gcd inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) )
20 19 adantl 
 |-  ( ( ph /\ r = inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) -> ( N gcd r ) = ( N gcd inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) )
21 20 eqeq1d 
 |-  ( ( ph /\ r = inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) -> ( ( N gcd r ) = 1 <-> ( N gcd inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) = 1 ) )
22 fveq2 
 |-  ( r = inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) -> ( odZ ` r ) = ( odZ ` inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) )
23 22 adantl 
 |-  ( ( ph /\ r = inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) -> ( odZ ` r ) = ( odZ ` inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) )
24 23 fveq1d 
 |-  ( ( ph /\ r = inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) -> ( ( odZ ` r ) ` N ) = ( ( odZ ` inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) ` N ) )
25 24 breq2d 
 |-  ( ( ph /\ r = inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) -> ( ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` r ) ` N ) <-> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) ` N ) ) )
26 21 25 anbi12d 
 |-  ( ( ph /\ r = inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) -> ( ( ( N gcd r ) = 1 /\ ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` r ) ` N ) ) <-> ( ( N gcd inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) = 1 /\ ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) ` N ) ) ) )
27 1 6 2 16 aks4d1p8 
 |-  ( ph -> ( N gcd inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) = 1 )
28 1 6 2 16 aks4d1p9 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) ` N ) )
29 27 28 jca 
 |-  ( ph -> ( ( N gcd inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) = 1 /\ ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` inf ( { h e. ( 1 ... B ) | -. h || ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ c e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ c ) - 1 ) ) } , RR , < ) ) ` N ) ) )
30 18 26 29 rspcedvd 
 |-  ( ph -> E. r e. ( 1 ... B ) ( ( N gcd r ) = 1 /\ ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` r ) ` N ) ) )