Metamath Proof Explorer

Theorem aks4d1lem1

Description: Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024)

Ref Expression
Hypotheses aks4d1lem1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks4d1lem1.2 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
Assertion aks4d1lem1 ( 𝜑 → ( 𝐵 ∈ ℕ ∧ 9 < 𝐵 ) )

Proof

Step Hyp Ref Expression
1 aks4d1lem1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1lem1.2 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
3 2re ⊢ 2 ∈ ℝ
4 3 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
5 2pos ⊢ 0 < 2
6 5 a1i ⊢ ( 𝜑 → 0 < 2 )
7 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
8 1 7 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
9 8 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
10 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
11 3re ⊢ 3 ∈ ℝ
12 11 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
13 3pos ⊢ 0 < 3
14 13 a1i ⊢ ( 𝜑 → 0 < 3 )
15 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
16 1 15 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
17 10 12 9 14 16 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
18 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
19 1lt2 ⊢ 1 < 2
20 19 a1i ⊢ ( 𝜑 → 1 < 2 )
21 18 20 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
22 21 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
23 4 6 9 17 22 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
24 5nn0 ⊢ 5 ∈ ℕ0
25 24 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
26 23 25 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
27 26 ceilcld ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
28 9re ⊢ 9 ∈ ℝ
29 28 a1i ⊢ ( 𝜑 → 9 ∈ ℝ )
30 27 zred ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
31 9pos ⊢ 0 < 9
32 31 a1i ⊢ ( 𝜑 → 0 < 9 )
33 9 16 3lexlogpow5ineq4 ⊢ ( 𝜑 → 9 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
34 ceilge ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
35 26 34 syl ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
36 29 26 30 33 35 ltletrd ⊢ ( 𝜑 → 9 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
37 10 29 30 32 36 lttrd ⊢ ( 𝜑 → 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
38 27 37 jca ⊢ ( 𝜑 → ( ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ ∧ 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) )
39 elnnz ⊢ ( ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℕ ↔ ( ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ ∧ 0 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ) )
40 38 39 sylibr ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℕ )
41 2 eleq1i ⊢ ( 𝐵 ∈ ℕ ↔ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℕ )
42 40 41 sylibr ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
43 2 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
44 36 43 breqtrrd ⊢ ( 𝜑 → 9 < 𝐵 )
45 42 44 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℕ ∧ 9 < 𝐵 ) )