Metamath Proof Explorer

Theorem aks4d1p4

Description: There exists a small enough number such that it does not divide A . (Contributed by metakunt, 28-Oct-2024)

Ref Expression
Hypotheses aks4d1p4.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks4d1p4.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
aks4d1p4.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
aks4d1p4.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
Assertion aks4d1p4 ( 𝜑 → ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 aks4d1p4.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1p4.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p4.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 aks4d1p4.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
5 4 a1i ⊢ ( 𝜑 → 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) )
6 ltso ⊢ < Or ℝ
7 6 a1i ⊢ ( 𝜑 → < Or ℝ )
8 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ∈ Fin )
9 ssrab2 ⊢ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ( 1 ... 𝐵 )
10 9 a1i ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ( 1 ... 𝐵 ) )
11 8 10 ssfid ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin )
12 1 2 3 aks4d1p3 ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )
13 rabn0 ⊢ ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ ↔ ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )
14 12 13 sylibr ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ )
15 elfznn ⊢ ( 𝑜 ∈ ( 1 ... 𝐵 ) → 𝑜 ∈ ℕ )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ( 1 ... 𝐵 ) ) → 𝑜 ∈ ℕ )
17 16 nnred ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ( 1 ... 𝐵 ) ) → 𝑜 ∈ ℝ )
18 17 ex ⊢ ( 𝜑 → ( 𝑜 ∈ ( 1 ... 𝐵 ) → 𝑜 ∈ ℝ ) )
19 18 ssrdv ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ⊆ ℝ )
20 10 19 sstrd ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
21 11 14 20 3jca ⊢ ( 𝜑 → ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ) )
22 fiinfcl ⊢ ( ( < Or ℝ ∧ ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ) ) → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } )
23 7 21 22 syl2anc ⊢ ( 𝜑 → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } )
24 5 23 eqeltrd ⊢ ( 𝜑 → 𝑅 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } )
25 breq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∥ 𝐴 ↔ 𝑅 ∥ 𝐴 ) )
26 25 notbid ⊢ ( 𝑟 = 𝑅 → ( ¬ 𝑟 ∥ 𝐴 ↔ ¬ 𝑅 ∥ 𝐴 ) )
27 26 elrab ⊢ ( 𝑅 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ↔ ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )
28 24 27 sylib ⊢ ( 𝜑 → ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )