Metamath Proof Explorer

Theorem aks4d1p1p3

Description: Bound of a ceiling of the binary logarithm to the fifth power. (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses aks4d1p1p3.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks4d1p1p3.2 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
aks4d1p1p3.3 ⊢ ( 𝜑 → 3 ≤ 𝑁 )
Assertion aks4d1p1p3 ( 𝜑 → ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) < ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p3.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 aks4d1p1p3.2 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
3 aks4d1p1p3.3 ⊢ ( 𝜑 → 3 ≤ 𝑁 )
4 2re ⊢ 2 ∈ ℝ
5 4 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
6 2pos ⊢ 0 < 2
7 6 a1i ⊢ ( 𝜑 → 0 < 2 )
8 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
9 1 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
10 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
11 1lt2 ⊢ 1 < 2
12 11 a1i ⊢ ( 𝜑 → 1 < 2 )
13 10 12 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
14 13 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
15 5 7 8 9 14 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
16 5nn0 ⊢ 5 ∈ ℕ0
17 16 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
18 15 17 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
19 ceilcl ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
20 18 19 syl ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
21 20 zred ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
22 2 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
23 22 eleq1d ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ↔ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ ) )
24 21 23 mpbird ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
25 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
26 7re ⊢ 7 ∈ ℝ
27 26 a1i ⊢ ( 𝜑 → 7 ∈ ℝ )
28 7pos ⊢ 0 < 7
29 28 a1i ⊢ ( 𝜑 → 0 < 7 )
30 8 3 3lexlogpow5ineq3 ⊢ ( 𝜑 → 7 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
31 ceilge ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
32 18 31 syl ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
33 27 18 21 30 32 ltletrd ⊢ ( 𝜑 → 7 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
34 22 eqcomd ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) = 𝐵 )
35 33 34 breqtrd ⊢ ( 𝜑 → 7 < 𝐵 )
36 25 27 24 29 35 lttrd ⊢ ( 𝜑 → 0 < 𝐵 )
37 5 7 24 36 14 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ )
38 37 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
39 38 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℝ )
40 18 10 readdcld ⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ∈ ℝ )
41 18 ltp1d ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
42 27 18 40 30 41 lttrd ⊢ ( 𝜑 → 7 < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
43 25 27 40 29 42 lttrd ⊢ ( 𝜑 → 0 < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
44 5 7 40 43 14 relogbcld ⊢ ( 𝜑 → ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ∈ ℝ )
45 flle ⊢ ( ( 2 logb 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ≤ ( 2 logb 𝐵 ) )
46 37 45 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ≤ ( 2 logb 𝐵 ) )
47 ceilm1lt ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) − 1 ) < ( ( 2 logb 𝑁 ) ↑ 5 ) )
48 18 47 syl ⊢ ( 𝜑 → ( ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) − 1 ) < ( ( 2 logb 𝑁 ) ↑ 5 ) )
49 21 10 18 ltsubaddd ⊢ ( 𝜑 → ( ( ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) − 1 ) < ( ( 2 logb 𝑁 ) ↑ 5 ) ↔ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) )
50 48 49 mpbid ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
51 22 50 eqbrtrd ⊢ ( 𝜑 → 𝐵 < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
52 2z ⊢ 2 ∈ ℤ
53 52 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
54 53 uzidd ⊢ ( 𝜑 → 2 ∈ ( ℤ≥ ‘ 2 ) )
55 24 36 elrpd ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
56 40 43 elrpd ⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ∈ ℝ+ )
57 logblt ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℝ+ ∧ ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ∈ ℝ+ ) → ( 𝐵 < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ↔ ( 2 logb 𝐵 ) < ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) )
58 54 55 56 57 syl3anc ⊢ ( 𝜑 → ( 𝐵 < ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ↔ ( 2 logb 𝐵 ) < ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) )
59 51 58 mpbid ⊢ ( 𝜑 → ( 2 logb 𝐵 ) < ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) )
60 39 37 44 46 59 lelttrd ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) < ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) )
61 3re ⊢ 3 ∈ ℝ
62 61 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
63 1lt3 ⊢ 1 < 3
64 63 a1i ⊢ ( 𝜑 → 1 < 3 )
65 10 62 8 64 3 ltletrd ⊢ ( 𝜑 → 1 < 𝑁 )
66 8 65 39 44 cxpltd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) < ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ↔ ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) < ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) ) )
67 60 66 mpbid ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) < ( 𝑁 ↑𝑐 ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) )