Metamath Proof Explorer

Theorem aks4d1p3

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

Ref Expression
Hypotheses aks4d1p3.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks4d1p3.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
aks4d1p3.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
Assertion aks4d1p3 ( 𝜑 → ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )

Proof

Step Hyp Ref Expression
1 aks4d1p3.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1p3.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p3.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 1 2 3 aks4d1p1 ⊢ ( 𝜑 → 𝐴 < ( 2 ↑ 𝐵 ) )
5 4 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → 𝐴 < ( 2 ↑ 𝐵 ) )
6 2re ⊢ 2 ∈ ℝ
7 6 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
8 3 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
9 2pos ⊢ 0 < 2
10 9 a1i ⊢ ( 𝜑 → 0 < 2 )
11 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
12 1 11 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
13 12 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
14 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
15 3re ⊢ 3 ∈ ℝ
16 15 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
17 3pos ⊢ 0 < 3
18 17 a1i ⊢ ( 𝜑 → 0 < 3 )
19 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
20 1 19 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
21 14 16 13 18 20 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
22 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
23 1lt2 ⊢ 1 < 2
24 23 a1i ⊢ ( 𝜑 → 1 < 2 )
25 22 24 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
26 25 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
27 7 10 13 21 26 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
28 5nn0 ⊢ 5 ∈ ℕ0
29 28 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
30 27 29 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
31 ceilcl ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
32 30 31 syl ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
33 8 32 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
34 32 zred ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
35 8 34 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
36 7re ⊢ 7 ∈ ℝ
37 36 a1i ⊢ ( 𝜑 → 7 ∈ ℝ )
38 7pos ⊢ 0 < 7
39 38 a1i ⊢ ( 𝜑 → 0 < 7 )
40 13 20 3lexlogpow5ineq3 ⊢ ( 𝜑 → 7 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
41 14 37 30 39 40 lttrd ⊢ ( 𝜑 → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
42 ceilge ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
43 30 42 syl ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
44 14 30 34 41 43 ltletrd ⊢ ( 𝜑 → 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
45 44 8 breqtrrd ⊢ ( 𝜑 → 0 < 𝐵 )
46 14 35 45 ltled ⊢ ( 𝜑 → 0 ≤ 𝐵 )
47 33 46 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ 0 ≤ 𝐵 ) )
48 elnn0z ⊢ ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℤ ∧ 0 ≤ 𝐵 ) )
49 47 48 sylibr ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
50 7 49 reexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝐵 ) ∈ ℝ )
51 50 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( 2 ↑ 𝐵 ) ∈ ℝ )
52 elfznn ⊢ ( 𝑞 ∈ ( 1 ... 𝐵 ) → 𝑞 ∈ ℕ )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( 1 ... 𝐵 ) ) → 𝑞 ∈ ℕ )
54 53 nnzd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( 1 ... 𝐵 ) ) → 𝑞 ∈ ℤ )
55 54 ex ⊢ ( 𝜑 → ( 𝑞 ∈ ( 1 ... 𝐵 ) → 𝑞 ∈ ℤ ) )
56 55 ssrdv ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ⊆ ℤ )
57 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ∈ Fin )
58 lcmfcl ⊢ ( ( ( 1 ... 𝐵 ) ⊆ ℤ ∧ ( 1 ... 𝐵 ) ∈ Fin ) → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℕ0 )
59 56 57 58 syl2anc ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℕ0 )
60 59 nn0red ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℝ )
61 60 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℝ )
62 2 a1i ⊢ ( 𝜑 → 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
63 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
64 12 21 63 sylanbrc ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
65 7 10 35 45 26 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ )
66 65 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
67 7 10 7 10 26 relogbcld ⊢ ( 𝜑 → ( 2 logb 2 ) ∈ ℝ )
68 0le1 ⊢ 0 ≤ 1
69 68 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
70 7 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
71 14 10 gtned ⊢ ( 𝜑 → 2 ≠ 0 )
72 logbid1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 2 ) = 1 )
73 70 71 26 72 syl3anc ⊢ ( 𝜑 → ( 2 logb 2 ) = 1 )
74 73 eqcomd ⊢ ( 𝜑 → 1 = ( 2 logb 2 ) )
75 69 74 breqtrd ⊢ ( 𝜑 → 0 ≤ ( 2 logb 2 ) )
76 2z ⊢ 2 ∈ ℤ
77 76 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
78 7 leidd ⊢ ( 𝜑 → 2 ≤ 2 )
79 2lt7 ⊢ 2 < 7
80 79 a1i ⊢ ( 𝜑 → 2 < 7 )
81 7 37 80 ltled ⊢ ( 𝜑 → 2 ≤ 7 )
82 37 30 34 40 43 ltletrd ⊢ ( 𝜑 → 7 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
83 82 8 breqtrrd ⊢ ( 𝜑 → 7 < 𝐵 )
84 37 35 83 ltled ⊢ ( 𝜑 → 7 ≤ 𝐵 )
85 7 37 35 81 84 letrd ⊢ ( 𝜑 → 2 ≤ 𝐵 )
86 77 78 7 10 35 45 85 logblebd ⊢ ( 𝜑 → ( 2 logb 2 ) ≤ ( 2 logb 𝐵 ) )
87 14 67 65 75 86 letrd ⊢ ( 𝜑 → 0 ≤ ( 2 logb 𝐵 ) )
88 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
89 flge ⊢ ( ( ( 2 logb 𝐵 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
90 65 88 89 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
91 87 90 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
92 66 91 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
93 elnn0z ⊢ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
94 92 93 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
95 64 94 nnexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℕ )
96 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ Fin )
97 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℤ )
98 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ℕ )
99 98 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ )
100 99 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ0 )
101 zexpcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑘 ) ∈ ℤ )
102 97 100 101 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℤ )
103 1zzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℤ )
104 102 103 zsubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ )
105 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℂ )
106 105 addid1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 1 + 0 ) = 1 )
107 22 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℝ )
108 1nn0 ⊢ 1 ∈ ℕ0
109 108 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
110 13 109 reexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ 1 ) ∈ ℝ )
111 110 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 1 ) ∈ ℝ )
112 102 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℝ )
113 1lt3 ⊢ 1 < 3
114 113 a1i ⊢ ( 𝜑 → 1 < 3 )
115 22 16 13 114 20 ltletrd ⊢ ( 𝜑 → 1 < 𝑁 )
116 13 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
117 116 exp1d ⊢ ( 𝜑 → ( 𝑁 ↑ 1 ) = 𝑁 )
118 117 eqcomd ⊢ ( 𝜑 → 𝑁 = ( 𝑁 ↑ 1 ) )
119 115 118 breqtrd ⊢ ( 𝜑 → 1 < ( 𝑁 ↑ 1 ) )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 < ( 𝑁 ↑ 1 ) )
121 13 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℝ )
122 64 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑁 )
123 122 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ≤ 𝑁 )
124 elfzuz ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
125 124 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
126 121 123 125 leexp2ad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 1 ) ≤ ( 𝑁 ↑ 𝑘 ) )
127 107 111 112 120 126 ltletrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 < ( 𝑁 ↑ 𝑘 ) )
128 106 127 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 1 + 0 ) < ( 𝑁 ↑ 𝑘 ) )
129 14 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 0 ∈ ℝ )
130 107 129 112 ltaddsub2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 1 + 0 ) < ( 𝑁 ↑ 𝑘 ) ↔ 0 < ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
131 128 130 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 0 < ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
132 104 131 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ ∧ 0 < ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
133 elnnz ⊢ ( ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℕ ↔ ( ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ ∧ 0 < ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
134 132 133 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℕ )
135 96 134 fprodnncl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℕ )
136 95 135 nnmulcld ⊢ ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ∈ ℕ )
137 62 136 eqeltrd ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
138 137 nnred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
139 138 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → 𝐴 ∈ ℝ )
140 1 2 3 aks4d1p2 ⊢ ( 𝜑 → ( 2 ↑ 𝐵 ) ≤ ( lcm ‘ ( 1 ... 𝐵 ) ) )
141 140 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( 2 ↑ 𝐵 ) ≤ ( lcm ‘ ( 1 ... 𝐵 ) ) )
142 137 nnzd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
143 142 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → 𝐴 ∈ ℤ )
144 56 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( 1 ... 𝐵 ) ⊆ ℤ )
145 fzfid ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( 1 ... 𝐵 ) ∈ Fin )
146 lcmfdvdsb ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 1 ... 𝐵 ) ⊆ ℤ ∧ ( 1 ... 𝐵 ) ∈ Fin ) → ( ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ↔ ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 ) )
147 143 144 145 146 syl3anc ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ↔ ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 ) )
148 147 biimpd ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 → ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 ) )
149 148 syldbl2 ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 )
150 59 nn0zd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℤ )
151 150 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℤ )
152 137 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → 𝐴 ∈ ℕ )
153 dvdsle ⊢ ( ( ( lcm ‘ ( 1 ... 𝐵 ) ) ∈ ℤ ∧ 𝐴 ∈ ℕ ) → ( ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 → ( lcm ‘ ( 1 ... 𝐵 ) ) ≤ 𝐴 ) )
154 151 152 153 syl2anc ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( ( lcm ‘ ( 1 ... 𝐵 ) ) ∥ 𝐴 → ( lcm ‘ ( 1 ... 𝐵 ) ) ≤ 𝐴 ) )
155 149 154 mpd ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( lcm ‘ ( 1 ... 𝐵 ) ) ≤ 𝐴 )
156 51 61 139 141 155 letrd ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( 2 ↑ 𝐵 ) ≤ 𝐴 )
157 51 139 lenltd ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ( ( 2 ↑ 𝐵 ) ≤ 𝐴 ↔ ¬ 𝐴 < ( 2 ↑ 𝐵 ) ) )
158 156 157 mpbid ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ¬ 𝐴 < ( 2 ↑ 𝐵 ) )
159 5 158 pm2.21dd ⊢ ( ( 𝜑 ∧ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ¬ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 )
160 simpr ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 ) → ¬ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 )
161 159 160 pm2.61dan ⊢ ( 𝜑 → ¬ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 )
162 rexnal ⊢ ( ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 ↔ ¬ ∀ 𝑟 ∈ ( 1 ... 𝐵 ) 𝑟 ∥ 𝐴 )
163 161 162 sylibr ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )