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 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks4d1.2 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
Assertion aks4d1 ( 𝜑 → ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ( ( 𝑁 gcd 𝑟 ) = 1 ∧ ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑟 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1.2 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
3 oveq2 ⊢ ( 𝑏 = 𝑎 → ( 𝑁 ↑ 𝑏 ) = ( 𝑁 ↑ 𝑎 ) )
4 3 oveq1d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑁 ↑ 𝑏 ) − 1 ) = ( ( 𝑁 ↑ 𝑎 ) − 1 ) )
5 4 cbvprodv ⊢ ∏ 𝑏 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑏 ) − 1 ) = ∏ 𝑎 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑎 ) − 1 )
6 5 oveq2i ⊢ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑏 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑏 ) − 1 ) ) = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑎 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑎 ) − 1 ) )
7 id ⊢ ( ℎ = 𝑘 → ℎ = 𝑘 )
8 oveq2 ⊢ ( 𝑐 = 𝑏 → ( 𝑁 ↑ 𝑐 ) = ( 𝑁 ↑ 𝑏 ) )
9 8 oveq1d ⊢ ( 𝑐 = 𝑏 → ( ( 𝑁 ↑ 𝑐 ) − 1 ) = ( ( 𝑁 ↑ 𝑏 ) − 1 ) )
10 9 cbvprodv ⊢ ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) = ∏ 𝑏 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑏 ) − 1 )
11 10 oveq2i ⊢ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑏 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑏 ) − 1 ) )
12 11 a1i ⊢ ( ℎ = 𝑘 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑏 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑏 ) − 1 ) ) )
13 7 12 breq12d ⊢ ( ℎ = 𝑘 → ( ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) ↔ 𝑘 ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑏 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑏 ) − 1 ) ) ) )
14 13 notbid ⊢ ( ℎ = 𝑘 → ( ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) ↔ ¬ 𝑘 ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑏 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑏 ) − 1 ) ) ) )
15 14 cbvrabv ⊢ { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } = { 𝑘 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑘 ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑏 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑏 ) − 1 ) ) }
16 15 infeq1i ⊢ inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) = inf ( { 𝑘 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑘 ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑏 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑏 ) − 1 ) ) } , ℝ , < )
17 1 6 2 16 aks4d1p4 ⊢ ( 𝜑 → ( inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ∈ ( 1 ... 𝐵 ) ∧ ¬ inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑏 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑏 ) − 1 ) ) ) )
18 17 simpld ⊢ ( 𝜑 → inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ∈ ( 1 ... 𝐵 ) )
19 oveq2 ⊢ ( 𝑟 = inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) → ( 𝑁 gcd 𝑟 ) = ( 𝑁 gcd inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑟 = inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) → ( 𝑁 gcd 𝑟 ) = ( 𝑁 gcd inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) )
21 20 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑟 = inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) → ( ( 𝑁 gcd 𝑟 ) = 1 ↔ ( 𝑁 gcd inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) = 1 ) )
22 fveq2 ⊢ ( 𝑟 = inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) → ( odℤ ‘ 𝑟 ) = ( odℤ ‘ inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑟 = inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) → ( odℤ ‘ 𝑟 ) = ( odℤ ‘ inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) )
24 23 fveq1d ⊢ ( ( 𝜑 ∧ 𝑟 = inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) → ( ( odℤ ‘ 𝑟 ) ‘ 𝑁 ) = ( ( odℤ ‘ inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) ‘ 𝑁 ) )
25 24 breq2d ⊢ ( ( 𝜑 ∧ 𝑟 = inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) → ( ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑟 ) ‘ 𝑁 ) ↔ ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) ‘ 𝑁 ) ) )
26 21 25 anbi12d ⊢ ( ( 𝜑 ∧ 𝑟 = inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) → ( ( ( 𝑁 gcd 𝑟 ) = 1 ∧ ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑟 ) ‘ 𝑁 ) ) ↔ ( ( 𝑁 gcd inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) = 1 ∧ ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) ‘ 𝑁 ) ) ) )
27 1 6 2 16 aks4d1p8 ⊢ ( 𝜑 → ( 𝑁 gcd inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) = 1 )
28 1 6 2 16 aks4d1p9 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) ‘ 𝑁 ) )
29 27 28 jca ⊢ ( 𝜑 → ( ( 𝑁 gcd inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) = 1 ∧ ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ inf ( { ℎ ∈ ( 1 ... 𝐵 ) ∣ ¬ ℎ ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑐 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑐 ) − 1 ) ) } , ℝ , < ) ) ‘ 𝑁 ) ) )
30 18 26 29 rspcedvd ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ( ( 𝑁 gcd 𝑟 ) = 1 ∧ ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑟 ) ‘ 𝑁 ) ) )