Metamath Proof Explorer

Theorem aks4d1p2

Description: Technical lemma for existence of non-divisor. (Contributed by metakunt, 27-Oct-2024)

Ref Expression
Hypotheses aks4d1p2.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks4d1p2.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
aks4d1p2.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
Assertion aks4d1p2 ( 𝜑 → ( 2 ↑ 𝐵 ) ≤ ( lcm ‘ ( 1 ... 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p2.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1p2.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p2.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 3 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
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 5nn0 ⊢ 5 ∈ ℕ0
27 26 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
28 25 27 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
29 ceilcl ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
30 28 29 syl ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
31 4 30 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
32 30 zred ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
33 7re ⊢ 7 ∈ ℝ
34 33 a1i ⊢ ( 𝜑 → 7 ∈ ℝ )
35 7pos ⊢ 0 < 7
36 35 a1i ⊢ ( 𝜑 → 0 < 7 )
37 11 18 3lexlogpow5ineq3 ⊢ ( 𝜑 → 7 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
38 12 34 28 36 37 lttrd ⊢ ( 𝜑 → 0 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
39 ceilge ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
40 28 39 syl ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
41 12 28 32 38 40 ltletrd ⊢ ( 𝜑 → 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
42 41 4 breqtrrd ⊢ ( 𝜑 → 0 < 𝐵 )
43 31 42 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ 0 < 𝐵 ) )
44 elnnz ⊢ ( 𝐵 ∈ ℕ ↔ ( 𝐵 ∈ ℤ ∧ 0 < 𝐵 ) )
45 43 44 sylibr ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
46 34 28 37 ltled ⊢ ( 𝜑 → 7 ≤ ( ( 2 logb 𝑁 ) ↑ 5 ) )
47 34 28 32 46 40 letrd ⊢ ( 𝜑 → 7 ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
48 47 4 breqtrrd ⊢ ( 𝜑 → 7 ≤ 𝐵 )
49 45 48 lcmineqlem ⊢ ( 𝜑 → ( 2 ↑ 𝐵 ) ≤ ( lcm ‘ ( 1 ... 𝐵 ) ) )