Metamath Proof Explorer

Theorem aks4d1p9

Description: Show that the order is bound by the squared binary logarithm. (Contributed by metakunt, 14-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 aks4d1p9.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1p9.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p9.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 aks4d1p9.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
5 2re ⊢ 2 ∈ ℝ
6 5 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
7 2pos ⊢ 0 < 2
8 7 a1i ⊢ ( 𝜑 → 0 < 2 )
9 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
10 1 9 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
11 10 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
12 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
13 3re ⊢ 3 ∈ ℝ
14 13 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
15 3pos ⊢ 0 < 3
16 15 a1i ⊢ ( 𝜑 → 0 < 3 )
17 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
18 1 17 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
19 12 14 11 16 18 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
20 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
21 1lt2 ⊢ 1 < 2
22 21 a1i ⊢ ( 𝜑 → 1 < 2 )
23 20 22 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
24 23 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
25 6 8 11 19 24 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
26 25 resqcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ )
27 1 2 3 4 aks4d1p4 ⊢ ( 𝜑 → ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )
28 27 simpld ⊢ ( 𝜑 → 𝑅 ∈ ( 1 ... 𝐵 ) )
29 elfznn ⊢ ( 𝑅 ∈ ( 1 ... 𝐵 ) → 𝑅 ∈ ℕ )
30 28 29 syl ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
31 1 2 3 4 aks4d1p8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
32 30 10 31 3jca ⊢ ( 𝜑 → ( 𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 gcd 𝑅 ) = 1 ) )
33 odzcl ⊢ ( ( 𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 gcd 𝑅 ) = 1 ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ )
34 32 33 syl ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ )
35 34 nnzd ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℤ )
36 flge ⊢ ( ( ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℤ ) → ( ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ↔ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) )
37 26 35 36 syl2anc ⊢ ( 𝜑 → ( ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ↔ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) )
38 37 biimpd ⊢ ( 𝜑 → ( ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) )
39 38 imp ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) )
40 30 nnzd ⊢ ( 𝜑 → 𝑅 ∈ ℤ )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑅 ∈ ℤ )
42 10 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑁 ∈ ℤ )
43 34 nnnn0d ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ0 )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ0 )
45 42 44 zexpcld ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ∈ ℤ )
46 1zzd ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 1 ∈ ℤ )
47 45 46 zsubcld ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) ∈ ℤ )
48 1 3 aks4d1lem1 ⊢ ( 𝜑 → ( 𝐵 ∈ ℕ ∧ 9 < 𝐵 ) )
49 48 simpld ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
50 49 nnred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
51 49 nngt0d ⊢ ( 𝜑 → 0 < 𝐵 )
52 6 8 50 51 24 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ )
53 52 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
54 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
55 12 8 gtned ⊢ ( 𝜑 → 2 ≠ 0 )
56 54 55 24 3jca ⊢ ( 𝜑 → ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) )
57 logb1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 1 ) = 0 )
58 56 57 syl ⊢ ( 𝜑 → ( 2 logb 1 ) = 0 )
59 2z ⊢ 2 ∈ ℤ
60 59 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
61 6 leidd ⊢ ( 𝜑 → 2 ≤ 2 )
62 0lt1 ⊢ 0 < 1
63 62 a1i ⊢ ( 𝜑 → 0 < 1 )
64 49 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐵 )
65 60 61 20 63 50 51 64 logblebd ⊢ ( 𝜑 → ( 2 logb 1 ) ≤ ( 2 logb 𝐵 ) )
66 58 65 eqbrtrrd ⊢ ( 𝜑 → 0 ≤ ( 2 logb 𝐵 ) )
67 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
68 flge ⊢ ( ( ( 2 logb 𝐵 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
69 52 67 68 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
70 66 69 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
71 53 70 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
72 elnn0z ⊢ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
73 71 72 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
74 10 73 zexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℤ )
75 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ Fin )
76 10 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℤ )
77 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ℕ )
78 77 nnnn0d ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ℕ0 )
79 78 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ0 )
80 76 79 zexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℤ )
81 1zzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℤ )
82 80 81 zsubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ )
83 75 82 fprodzcl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ )
84 74 83 zmulcld ⊢ ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ∈ ℤ )
85 2 a1i ⊢ ( 𝜑 → 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
86 85 eleq1d ⊢ ( 𝜑 → ( 𝐴 ∈ ℤ ↔ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ∈ ℤ ) )
87 84 86 mpbird ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
88 87 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝐴 ∈ ℤ )
89 iddvds ⊢ ( ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℤ → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∥ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
90 35 89 syl ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∥ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
91 odzdvds ⊢ ( ( ( 𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 gcd 𝑅 ) = 1 ) ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ0 ) → ( 𝑅 ∥ ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∥ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
92 32 43 91 syl2anc ⊢ ( 𝜑 → ( 𝑅 ∥ ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∥ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
93 90 92 mpbird ⊢ ( 𝜑 → 𝑅 ∥ ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) )
94 93 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑅 ∥ ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) )
95 73 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
96 42 95 zexpcld ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℤ )
97 fzfid ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ Fin )
98 42 adantr ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℤ )
99 77 adantl ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ )
100 99 nnnn0d ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ0 )
101 98 100 zexpcld ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℤ )
102 1zzd ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℤ )
103 101 102 zsubcld ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ )
104 97 103 fprodzcl ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ )
105 fveq2 ⊢ ( 𝑧 = ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) → ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
106 105 breq1d ⊢ ( 𝑧 = ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) → ( ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑧 ) ∥ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑘 ) ↔ ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ∥ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑘 ) ) )
107 ssidd ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) )
108 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℤ )
109 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑥 ∈ ℕ )
110 109 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑥 ∈ ℕ )
111 110 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑥 ∈ ℕ0 )
112 108 111 zexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑥 ) ∈ ℤ )
113 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℤ )
114 112 113 zsubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑥 ) − 1 ) ∈ ℤ )
115 114 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) : ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ⟶ ℤ )
116 75 107 115 fprodfvdvdsd ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑧 ) ∥ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑘 ) )
117 116 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ∀ 𝑧 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑧 ) ∥ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑘 ) )
118 25 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( 2 logb 𝑁 ) ∈ ℝ )
119 118 resqcld ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ )
120 119 flcld ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∈ ℤ )
121 35 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℤ )
122 34 nnge1d ⊢ ( 𝜑 → 1 ≤ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
123 122 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 1 ≤ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
124 simpr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) )
125 46 120 121 123 124 elfzd ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) )
126 106 117 125 rspcdva ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ∥ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑘 ) )
127 eqidd ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) = ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) )
128 simpr ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑥 = ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) → 𝑥 = ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
129 128 oveq2d ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑥 = ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) → ( 𝑁 ↑ 𝑥 ) = ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) )
130 129 oveq1d ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑥 = ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) → ( ( 𝑁 ↑ 𝑥 ) − 1 ) = ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) )
131 127 130 125 47 fvmptd ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) = ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) )
132 eqidd ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) = ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) )
133 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) ∧ 𝑥 = 𝑘 ) → 𝑥 = 𝑘 )
134 133 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) ∧ 𝑥 = 𝑘 ) → ( 𝑁 ↑ 𝑥 ) = ( 𝑁 ↑ 𝑘 ) )
135 134 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) ∧ 𝑥 = 𝑘 ) → ( ( 𝑁 ↑ 𝑥 ) − 1 ) = ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
136 simpr ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) )
137 132 135 136 103 fvmptd ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑘 ) = ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
138 137 prodeq2dv ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑘 ) = ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
139 131 138 breq12d ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) ∥ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ↦ ( ( 𝑁 ↑ 𝑥 ) − 1 ) ) ‘ 𝑘 ) ↔ ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) ∥ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
140 126 139 mpbid ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) ∥ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
141 47 96 104 140 dvdsmultr2d ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
142 2 a1i ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
143 141 142 breqtrrd ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → ( ( 𝑁 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ) − 1 ) ∥ 𝐴 )
144 41 47 88 94 143 dvdstrd ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑅 ∥ 𝐴 )
145 144 ex ⊢ ( 𝜑 → ( ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) → 𝑅 ∥ 𝐴 ) )
146 145 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ) → ( ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) → 𝑅 ∥ 𝐴 ) )
147 146 imp ⊢ ( ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑅 ∥ 𝐴 )
148 39 147 mpdan ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ) → 𝑅 ∥ 𝐴 )
149 27 simprd ⊢ ( 𝜑 → ¬ 𝑅 ∥ 𝐴 )
150 149 adantr ⊢ ( ( 𝜑 ∧ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ) → ¬ 𝑅 ∥ 𝐴 )
151 148 150 pm2.65da ⊢ ( 𝜑 → ¬ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) )
152 34 nnred ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℝ )
153 26 152 ltnled ⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ↔ ¬ ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) ) )
154 151 153 mpbird ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )