Metamath Proof Explorer

Theorem aks6d1c7lem1

Description: The last set of inequalities of Claim 7 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf . (Contributed by metakunt, 12-May-2025)

Ref Expression
Hypotheses aks6d1c7lem1.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c7lem1.2 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c7lem1.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks6d1c7lem1.4 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c7lem1.5 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c7lem1.6 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
aks6d1c7lem1.7 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
aks6d1c7lem1.8 ⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
aks6d1c7lem1.9 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
aks6d1c7lem1.10 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
Assertion aks6d1c7lem1 ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c7lem1.1 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2 aks6d1c7lem1.2 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
3 aks6d1c7lem1.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
4 aks6d1c7lem1.4 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
5 aks6d1c7lem1.5 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
6 aks6d1c7lem1.6 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
7 aks6d1c7lem1.7 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
8 aks6d1c7lem1.8 ⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
9 aks6d1c7lem1.9 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
10 aks6d1c7lem1.10 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
11 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
12 3 11 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
13 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
14 3re ⊢ 3 ∈ ℝ
15 14 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
16 12 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
17 3pos ⊢ 0 < 3
18 17 a1i ⊢ ( 𝜑 → 0 < 3 )
19 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
20 3 19 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
21 13 15 16 18 20 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
22 12 21 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
23 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
24 22 23 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
25 24 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
26 8 a1i ⊢ ( 𝜑 → 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
27 eqid ⊢ ( ℤ/nℤ ‘ 𝑅 ) = ( ℤ/nℤ ‘ 𝑅 )
28 24 1 4 2 5 6 7 27 hashscontpowcl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )
29 26 28 eqeltrd ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
30 29 nn0red ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
31 29 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐷 )
32 30 31 resqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝐷 ) ∈ ℝ )
33 32 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ∈ ℤ )
34 30 31 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ 𝐷 ) )
35 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
36 flge ⊢ ( ( ( √ ‘ 𝐷 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( √ ‘ 𝐷 ) ↔ 0 ≤ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) )
37 32 35 36 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( √ ‘ 𝐷 ) ↔ 0 ≤ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) )
38 34 37 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) )
39 33 38 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) )
40 elnn0z ⊢ ( ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) )
41 39 40 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ∈ ℕ0 )
42 25 41 reexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) ∈ ℝ )
43 2re ⊢ 2 ∈ ℝ
44 43 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
45 2pos ⊢ 0 < 2
46 45 a1i ⊢ ( 𝜑 → 0 < 2 )
47 24 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
48 1ne2 ⊢ 1 ≠ 2
49 48 necomi ⊢ 2 ≠ 1
50 49 a1i ⊢ ( 𝜑 → 2 ≠ 1 )
51 44 46 25 47 50 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
52 26 30 eqeltrrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ )
53 31 26 breqtrd ⊢ ( 𝜑 → 0 ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
54 52 53 resqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℝ )
55 51 54 remulcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℝ )
56 55 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℤ )
57 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
58 0le1 ⊢ 0 ≤ 1
59 58 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
60 44 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
61 13 46 gtned ⊢ ( 𝜑 → 2 ≠ 0 )
62 logbid1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 2 ) = 1 )
63 60 61 50 62 syl3anc ⊢ ( 𝜑 → ( 2 logb 2 ) = 1 )
64 63 eqcomd ⊢ ( 𝜑 → 1 = ( 2 logb 2 ) )
65 2z ⊢ 2 ∈ ℤ
66 65 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
67 44 leidd ⊢ ( 𝜑 → 2 ≤ 2 )
68 1nn0 ⊢ 1 ∈ ℕ0
69 43 68 nn0addge1i ⊢ 2 ≤ ( 2 + 1 )
70 2p1e3 ⊢ ( 2 + 1 ) = 3
71 69 70 breqtri ⊢ 2 ≤ 3
72 71 a1i ⊢ ( 𝜑 → 2 ≤ 3 )
73 44 15 16 72 20 letrd ⊢ ( 𝜑 → 2 ≤ 𝑁 )
74 66 67 44 46 16 21 73 logblebd ⊢ ( 𝜑 → ( 2 logb 2 ) ≤ ( 2 logb 𝑁 ) )
75 64 74 eqbrtrd ⊢ ( 𝜑 → 1 ≤ ( 2 logb 𝑁 ) )
76 13 57 51 59 75 letrd ⊢ ( 𝜑 → 0 ≤ ( 2 logb 𝑁 ) )
77 52 53 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
78 51 54 76 77 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
79 flge ⊢ ( ( ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ↔ 0 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
80 55 35 79 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ↔ 0 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
81 78 80 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
82 56 81 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
83 elnn0z ⊢ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
84 82 83 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℕ0 )
85 68 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
86 84 85 nn0addcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ∈ ℕ0 )
87 2 phicld ⊢ ( 𝜑 → ( ϕ ‘ 𝑅 ) ∈ ℕ )
88 87 nnred ⊢ ( 𝜑 → ( ϕ ‘ 𝑅 ) ∈ ℝ )
89 87 nnnn0d ⊢ ( 𝜑 → ( ϕ ‘ 𝑅 ) ∈ ℕ0 )
90 89 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ϕ ‘ 𝑅 ) )
91 88 90 resqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ϕ ‘ 𝑅 ) ) ∈ ℝ )
92 91 51 remulcld ⊢ ( 𝜑 → ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ )
93 92 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ )
94 88 90 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ ( ϕ ‘ 𝑅 ) ) )
95 91 51 94 76 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
96 flge ⊢ ( ( ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ↔ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
97 92 35 96 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ↔ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
98 95 97 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) )
99 93 98 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
100 elnn0z ⊢ ( ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
101 99 100 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℕ0 )
102 86 101 nn0addcld ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) ∈ ℕ0 )
103 56 peano2zd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ∈ ℤ )
104 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
105 104 znegcld ⊢ ( 𝜑 → - 1 ∈ ℤ )
106 103 105 zaddcld ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) ∈ ℤ )
107 bccl ⊢ ( ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) ∈ ℕ0 ∧ ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) ∈ ℤ ) → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) ) ∈ ℕ0 )
108 102 106 107 syl2anc ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) ) ∈ ℕ0 )
109 108 nn0red ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) ) ∈ ℝ )
110 28 101 nn0addcld ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) ∈ ℕ0 )
111 28 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℤ )
112 111 105 zaddcld ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + - 1 ) ∈ ℤ )
113 bccl ⊢ ( ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) ∈ ℕ0 ∧ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + - 1 ) ∈ ℤ ) → ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + - 1 ) ) ∈ ℕ0 )
114 110 112 113 syl2anc ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + - 1 ) ) ∈ ℕ0 )
115 114 nn0red ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + - 1 ) ) ∈ ℝ )
116 54 51 remulcld ⊢ ( 𝜑 → ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ )
117 116 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ )
118 54 51 77 76 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) )
119 flge ⊢ ( ( ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ↔ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) )
120 116 35 119 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ↔ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) )
121 118 120 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) )
122 117 121 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) )
123 elnn0z ⊢ ( ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) )
124 122 123 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℕ0 )
125 86 124 nn0addcld ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) ∈ ℕ0 )
126 bccl ⊢ ( ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) ∈ ℕ0 ∧ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℤ ) → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ∈ ℕ0 )
127 125 56 126 syl2anc ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ∈ ℕ0 )
128 127 nn0red ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ∈ ℝ )
129 bccl ⊢ ( ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) ∈ ℕ0 ∧ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℤ ) → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ∈ ℕ0 )
130 102 56 129 syl2anc ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ∈ ℕ0 )
131 130 nn0red ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ∈ ℝ )
132 44 86 reexpcld ⊢ ( 𝜑 → ( 2 ↑ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) ∈ ℝ )
133 2nn0 ⊢ 2 ∈ ℕ0
134 133 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
135 134 84 nn0mulcld ⊢ ( 𝜑 → ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ∈ ℕ0 )
136 135 85 nn0addcld ⊢ ( 𝜑 → ( ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) ∈ ℕ0 )
137 bccl ⊢ ( ( ( ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) ∈ ℕ0 ∧ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℤ ) → ( ( ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ∈ ℕ0 )
138 136 56 137 syl2anc ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ∈ ℕ0 )
139 138 nn0red ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ∈ ℝ )
140 13 44 46 ltled ⊢ ( 𝜑 → 0 ≤ 2 )
141 44 140 55 recxpcld ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℝ )
142 reflcl ⊢ ( ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℝ → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℝ )
143 55 142 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℝ )
144 143 57 readdcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ∈ ℝ )
145 44 140 144 recxpcld ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) ∈ ℝ )
146 1le2 ⊢ 1 ≤ 2
147 146 a1i ⊢ ( 𝜑 → 1 ≤ 2 )
148 57 44 16 147 73 letrd ⊢ ( 𝜑 → 1 ≤ 𝑁 )
149 reflcl ⊢ ( ( √ ‘ 𝐷 ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ∈ ℝ )
150 32 149 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ∈ ℝ )
151 26 fveq2d ⊢ ( 𝜑 → ( √ ‘ 𝐷 ) = ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
152 151 fveq2d ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝐷 ) ) = ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
153 flle ⊢ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
154 54 153 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
155 152 154 eqbrtrd ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
156 16 148 150 54 155 cxplead ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) ≤ ( 𝑁 ↑𝑐 ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
157 16 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
158 13 21 gtned ⊢ ( 𝜑 → 𝑁 ≠ 0 )
159 157 158 33 cxpexpzd ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) = ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) )
160 61 50 nelprd ⊢ ( 𝜑 → ¬ 2 ∈ { 0 , 1 } )
161 60 160 eldifd ⊢ ( 𝜑 → 2 ∈ ( ℂ ∖ { 0 , 1 } ) )
162 158 neneqd ⊢ ( 𝜑 → ¬ 𝑁 = 0 )
163 elsng ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ { 0 } ↔ 𝑁 = 0 ) )
164 24 163 syl ⊢ ( 𝜑 → ( 𝑁 ∈ { 0 } ↔ 𝑁 = 0 ) )
165 162 164 mtbird ⊢ ( 𝜑 → ¬ 𝑁 ∈ { 0 } )
166 157 165 eldifd ⊢ ( 𝜑 → 𝑁 ∈ ( ℂ ∖ { 0 } ) )
167 cxplogb ⊢ ( ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑁 ∈ ( ℂ ∖ { 0 } ) ) → ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) = 𝑁 )
168 161 166 167 syl2anc ⊢ ( 𝜑 → ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) = 𝑁 )
169 168 eqcomd ⊢ ( 𝜑 → 𝑁 = ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) )
170 169 oveq1d ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
171 156 159 170 3brtr3d ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) ≤ ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
172 44 46 elrpd ⊢ ( 𝜑 → 2 ∈ ℝ+ )
173 54 recnd ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℂ )
174 cxpmul ⊢ ( ( 2 ∈ ℝ+ ∧ ( 2 logb 𝑁 ) ∈ ℝ ∧ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℂ ) → ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) = ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
175 172 51 173 174 syl3anc ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) = ( ( 2 ↑𝑐 ( 2 logb 𝑁 ) ) ↑𝑐 ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
176 171 175 breqtrrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) ≤ ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
177 fllep1 ⊢ ( ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℝ → ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ≤ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) )
178 55 177 syl ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ≤ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) )
179 57 44 147 50 leneltd ⊢ ( 𝜑 → 1 < 2 )
180 86 nn0red ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ∈ ℝ )
181 44 179 55 180 cxpled ⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ≤ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ↔ ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ≤ ( 2 ↑𝑐 ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) ) )
182 178 181 mpbid ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ≤ ( 2 ↑𝑐 ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) )
183 42 141 145 176 182 letrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) ≤ ( 2 ↑𝑐 ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) )
184 cxpexpz ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ∈ ℤ ) → ( 2 ↑𝑐 ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) = ( 2 ↑ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) )
185 60 61 103 184 syl3anc ⊢ ( 𝜑 → ( 2 ↑𝑐 ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) = ( 2 ↑ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) )
186 183 185 breqtrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) ≤ ( 2 ↑ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) )
187 51 51 jca ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ∈ ℝ ∧ ( 2 logb 𝑁 ) ∈ ℝ ) )
188 remulcl ⊢ ( ( ( 2 logb 𝑁 ) ∈ ℝ ∧ ( 2 logb 𝑁 ) ∈ ℝ ) → ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ∈ ℝ )
189 187 188 syl ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ∈ ℝ )
190 reflcl ⊢ ( ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ∈ ℝ → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ) ∈ ℝ )
191 189 190 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ) ∈ ℝ )
192 84 nn0red ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℝ )
193 44 46 15 18 50 relogbcld ⊢ ( 𝜑 → ( 2 logb 3 ) ∈ ℝ )
194 193 resqcld ⊢ ( 𝜑 → ( ( 2 logb 3 ) ↑ 2 ) ∈ ℝ )
195 51 recnd ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℂ )
196 195 sqvald ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) = ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) )
197 196 189 eqeltrd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ )
198 3lexlogpow2ineq2 ⊢ ( 2 < ( ( 2 logb 3 ) ↑ 2 ) ∧ ( ( 2 logb 3 ) ↑ 2 ) < 3 )
199 198 simpli ⊢ 2 < ( ( 2 logb 3 ) ↑ 2 )
200 199 a1i ⊢ ( 𝜑 → 2 < ( ( 2 logb 3 ) ↑ 2 ) )
201 44 194 200 ltled ⊢ ( 𝜑 → 2 ≤ ( ( 2 logb 3 ) ↑ 2 ) )
202 15 44 61 redivcld ⊢ ( 𝜑 → ( 3 / 2 ) ∈ ℝ )
203 2rp ⊢ 2 ∈ ℝ+
204 203 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
205 13 15 18 ltled ⊢ ( 𝜑 → 0 ≤ 3 )
206 15 204 205 divge0d ⊢ ( 𝜑 → 0 ≤ ( 3 / 2 ) )
207 3lexlogpow2ineq1 ⊢ ( ( 3 / 2 ) < ( 2 logb 3 ) ∧ ( 2 logb 3 ) < ( 5 / 3 ) )
208 207 simpli ⊢ ( 3 / 2 ) < ( 2 logb 3 )
209 208 a1i ⊢ ( 𝜑 → ( 3 / 2 ) < ( 2 logb 3 ) )
210 202 193 209 ltled ⊢ ( 𝜑 → ( 3 / 2 ) ≤ ( 2 logb 3 ) )
211 13 202 193 206 210 letrd ⊢ ( 𝜑 → 0 ≤ ( 2 logb 3 ) )
212 66 67 15 18 16 21 20 logblebd ⊢ ( 𝜑 → ( 2 logb 3 ) ≤ ( 2 logb 𝑁 ) )
213 193 51 134 211 212 leexp1ad ⊢ ( 𝜑 → ( ( 2 logb 3 ) ↑ 2 ) ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) )
214 44 194 197 201 213 letrd ⊢ ( 𝜑 → 2 ≤ ( ( 2 logb 𝑁 ) ↑ 2 ) )
215 214 196 breqtrd ⊢ ( 𝜑 → 2 ≤ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) )
216 flge ⊢ ( ( ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ∈ ℝ ∧ 2 ∈ ℤ ) → ( 2 ≤ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ↔ 2 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ) ) )
217 189 66 216 syl2anc ⊢ ( 𝜑 → ( 2 ≤ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ↔ 2 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ) ) )
218 215 217 mpbid ⊢ ( 𝜑 → 2 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ) )
219 51 51 remulcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ∈ ℝ )
220 24 1 4 2 5 6 7 27 10 aks6d1c3 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
221 173 sqvald ⊢ ( 𝜑 → ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ↑ 2 ) = ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
222 28 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℂ )
223 222 msqsqrtd ⊢ ( 𝜑 → ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
224 221 223 eqtr2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) = ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ↑ 2 ) )
225 220 224 breqtrd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ↑ 2 ) )
226 51 54 76 77 lt2sqd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) < ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ↔ ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ↑ 2 ) ) )
227 225 226 mpbird ⊢ ( 𝜑 → ( 2 logb 𝑁 ) < ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
228 51 54 227 ltled ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
229 51 54 51 76 228 lemul2ad ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ≤ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
230 flwordi ⊢ ( ( ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ∈ ℝ ∧ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℝ ∧ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ≤ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
231 219 55 229 230 syl3anc ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( 2 logb 𝑁 ) ) ) ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
232 44 191 192 218 231 letrd ⊢ ( 𝜑 → 2 ≤ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
233 56 232 2ap1caineq ⊢ ( 𝜑 → ( 2 ↑ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) < ( ( ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
234 42 132 139 186 233 lelttrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
235 84 nn0cnd ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ∈ ℂ )
236 235 2timesd ⊢ ( 𝜑 → ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) = ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
237 236 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) = ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) )
238 237 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) = ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
239 234 238 breqtrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
240 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
241 235 235 240 addassd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) = ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) )
242 86 nn0cnd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ∈ ℂ )
243 235 242 addcomd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ) = ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
244 241 243 eqtrd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) = ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
245 244 oveq1d ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) + 1 ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) = ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
246 239 245 breqtrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
247 195 173 mulcomd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) )
248 247 fveq2d ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) = ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) )
249 248 oveq2d ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) = ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) )
250 249 oveq1d ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) = ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
251 246 250 breqtrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
252 124 nn0red ⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℝ )
253 101 nn0red ⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ∈ ℝ )
254 8 29 eqeltrrid ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )
255 254 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ )
256 254 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
257 255 256 resqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℝ )
258 257 51 remulcld ⊢ ( 𝜑 → ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ )
259 24 1 4 2 5 6 7 aks6d1c4 ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ϕ ‘ 𝑅 ) )
260 52 53 88 90 sqrtled ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ϕ ‘ 𝑅 ) ↔ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ≤ ( √ ‘ ( ϕ ‘ 𝑅 ) ) ) )
261 259 260 mpbid ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ≤ ( √ ‘ ( ϕ ‘ 𝑅 ) ) )
262 257 91 51 76 261 lemul1ad ⊢ ( 𝜑 → ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
263 flwordi ⊢ ( ( ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ ∧ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ∈ ℝ ∧ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ≤ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) → ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) )
264 258 92 262 263 syl3anc ⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) )
265 252 253 144 264 leadd2dd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) ≤ ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) )
266 125 102 56 265 bcled ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) ≤ ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
267 42 128 131 251 266 ltletrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) )
268 235 240 pncand ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) − 1 ) = ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
269 268 eqcomd ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) = ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) − 1 ) )
270 242 240 negsubd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) = ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) − 1 ) )
271 270 eqcomd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) − 1 ) = ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) )
272 269 271 eqtrd ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) = ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) )
273 272 oveq2d ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) ) = ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) ) )
274 267 273 breqtrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) ) )
275 2 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
276 27 zncrng ⊢ ( 𝑅 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing )
277 275 276 syl ⊢ ( 𝜑 → ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing )
278 crngring ⊢ ( ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing → ( ℤ/nℤ ‘ 𝑅 ) ∈ Ring )
279 7 zrhrhm ⊢ ( ( ℤ/nℤ ‘ 𝑅 ) ∈ Ring → 𝐿 ∈ ( ℤring RingHom ( ℤ/nℤ ‘ 𝑅 ) ) )
280 zringbas ⊢ ℤ = ( Base ‘ ℤring )
281 eqid ⊢ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) )
282 280 281 rhmf ⊢ ( 𝐿 ∈ ( ℤring RingHom ( ℤ/nℤ ‘ 𝑅 ) ) → 𝐿 : ℤ ⟶ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
283 277 278 279 282 4syl ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
284 283 ffnd ⊢ ( 𝜑 → 𝐿 Fn ℤ )
285 24 1 4 6 aks6d1c2p1 ⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ )
286 nnssz ⊢ ℕ ⊆ ℤ
287 286 a1i ⊢ ( 𝜑 → ℕ ⊆ ℤ )
288 285 287 fssd ⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℤ )
289 frn ⊢ ( 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℤ → ran 𝐸 ⊆ ℤ )
290 288 289 syl ⊢ ( 𝜑 → ran 𝐸 ⊆ ℤ )
291 285 ffnd ⊢ ( 𝜑 → 𝐸 Fn ( ℕ0 × ℕ0 ) )
292 fnima ⊢ ( 𝐸 Fn ( ℕ0 × ℕ0 ) → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) = ran 𝐸 )
293 291 292 syl ⊢ ( 𝜑 → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) = ran 𝐸 )
294 293 sseq1d ⊢ ( 𝜑 → ( ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℤ ↔ ran 𝐸 ⊆ ℤ ) )
295 290 294 mpbird ⊢ ( 𝜑 → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℤ )
296 vex ⊢ 𝑘 ∈ V
297 vex ⊢ 𝑙 ∈ V
298 296 297 op1std ⊢ ( 𝑣 = ⟨ 𝑘 , 𝑙 ⟩ → ( 1st ‘ 𝑣 ) = 𝑘 )
299 298 oveq2d ⊢ ( 𝑣 = ⟨ 𝑘 , 𝑙 ⟩ → ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) = ( 𝑃 ↑ 𝑘 ) )
300 296 297 op2ndd ⊢ ( 𝑣 = ⟨ 𝑘 , 𝑙 ⟩ → ( 2nd ‘ 𝑣 ) = 𝑙 )
301 300 oveq2d ⊢ ( 𝑣 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) )
302 299 301 oveq12d ⊢ ( 𝑣 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) = ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
303 302 mpompt ⊢ ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ) = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
304 303 eqcomi ⊢ ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) )
305 6 304 eqtri ⊢ 𝐸 = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) )
306 305 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝑣 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) ) )
307 c0ex ⊢ 0 ∈ V
308 307 307 op1std ⊢ ( 𝑣 = ⟨ 0 , 0 ⟩ → ( 1st ‘ 𝑣 ) = 0 )
309 308 adantl ⊢ ( ( 𝜑 ∧ 𝑣 = ⟨ 0 , 0 ⟩ ) → ( 1st ‘ 𝑣 ) = 0 )
310 309 oveq2d ⊢ ( ( 𝜑 ∧ 𝑣 = ⟨ 0 , 0 ⟩ ) → ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) = ( 𝑃 ↑ 0 ) )
311 307 307 op2ndd ⊢ ( 𝑣 = ⟨ 0 , 0 ⟩ → ( 2nd ‘ 𝑣 ) = 0 )
312 311 adantl ⊢ ( ( 𝜑 ∧ 𝑣 = ⟨ 0 , 0 ⟩ ) → ( 2nd ‘ 𝑣 ) = 0 )
313 312 oveq2d ⊢ ( ( 𝜑 ∧ 𝑣 = ⟨ 0 , 0 ⟩ ) → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) = ( ( 𝑁 / 𝑃 ) ↑ 0 ) )
314 310 313 oveq12d ⊢ ( ( 𝜑 ∧ 𝑣 = ⟨ 0 , 0 ⟩ ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) = ( ( 𝑃 ↑ 0 ) · ( ( 𝑁 / 𝑃 ) ↑ 0 ) ) )
315 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
316 1 315 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
317 316 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
318 317 exp0d ⊢ ( 𝜑 → ( 𝑃 ↑ 0 ) = 1 )
319 316 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
320 157 317 319 divcld ⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∈ ℂ )
321 320 exp0d ⊢ ( 𝜑 → ( ( 𝑁 / 𝑃 ) ↑ 0 ) = 1 )
322 318 321 oveq12d ⊢ ( 𝜑 → ( ( 𝑃 ↑ 0 ) · ( ( 𝑁 / 𝑃 ) ↑ 0 ) ) = ( 1 · 1 ) )
323 240 mulridd ⊢ ( 𝜑 → ( 1 · 1 ) = 1 )
324 322 323 eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ↑ 0 ) · ( ( 𝑁 / 𝑃 ) ↑ 0 ) ) = 1 )
325 324 adantr ⊢ ( ( 𝜑 ∧ 𝑣 = ⟨ 0 , 0 ⟩ ) → ( ( 𝑃 ↑ 0 ) · ( ( 𝑁 / 𝑃 ) ↑ 0 ) ) = 1 )
326 314 325 eqtrd ⊢ ( ( 𝜑 ∧ 𝑣 = ⟨ 0 , 0 ⟩ ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑣 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑣 ) ) ) = 1 )
327 0nn0 ⊢ 0 ∈ ℕ0
328 327 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
329 328 328 opelxpd ⊢ ( 𝜑 → ⟨ 0 , 0 ⟩ ∈ ( ℕ0 × ℕ0 ) )
330 1nn ⊢ 1 ∈ ℕ
331 330 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
332 306 326 329 331 fvmptd ⊢ ( 𝜑 → ( 𝐸 ‘ ⟨ 0 , 0 ⟩ ) = 1 )
333 ssidd ⊢ ( 𝜑 → ( ℕ0 × ℕ0 ) ⊆ ( ℕ0 × ℕ0 ) )
334 fnfvima ⊢ ( ( 𝐸 Fn ( ℕ0 × ℕ0 ) ∧ ( ℕ0 × ℕ0 ) ⊆ ( ℕ0 × ℕ0 ) ∧ ⟨ 0 , 0 ⟩ ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ ⟨ 0 , 0 ⟩ ) ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
335 291 333 329 334 syl3anc ⊢ ( 𝜑 → ( 𝐸 ‘ ⟨ 0 , 0 ⟩ ) ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
336 332 335 eqeltrrd ⊢ ( 𝜑 → 1 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
337 fnfvima ⊢ ( ( 𝐿 Fn ℤ ∧ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℤ ∧ 1 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ( 𝐿 ‘ 1 ) ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
338 284 295 336 337 syl3anc ⊢ ( 𝜑 → ( 𝐿 ‘ 1 ) ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
339 7 a1i ⊢ ( 𝜑 → 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
340 fvexd ⊢ ( 𝜑 → ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ∈ V )
341 339 340 eqeltrd ⊢ ( 𝜑 → 𝐿 ∈ V )
342 341 imaexd ⊢ ( 𝜑 → ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ V )
343 338 342 hashelne0d ⊢ ( 𝜑 → ¬ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) = 0 )
344 343 neqned ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≠ 0 )
345 28 344 jca ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 ∧ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≠ 0 ) )
346 elnnne0 ⊢ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ ↔ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 ∧ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≠ 0 ) )
347 345 346 sylibr ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ )
348 347 nnrpd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ+ )
349 348 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℝ+ )
350 51 54 349 227 ltmul1dd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) < ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
351 52 53 52 53 sqrtmuld ⊢ ( 𝜑 → ( √ ‘ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) · ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
352 351 eqcomd ⊢ ( 𝜑 → ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( √ ‘ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) · ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
353 350 352 breqtrd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) < ( √ ‘ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) · ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
354 351 223 eqtrd ⊢ ( 𝜑 → ( √ ‘ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) · ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
355 353 354 breqtrd ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) < ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
356 fllt ⊢ ( ( ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℝ ∧ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℤ ) → ( ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) < ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ↔ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) < ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
357 55 111 356 syl2anc ⊢ ( 𝜑 → ( ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) < ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ↔ ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) < ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
358 355 357 mpbid ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) < ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
359 56 111 zltp1led ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) < ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ↔ ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
360 358 359 mpbid ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
361 57 renegcld ⊢ ( 𝜑 → - 1 ∈ ℝ )
362 df-neg ⊢ - 1 = ( 0 − 1 )
363 362 a1i ⊢ ( 𝜑 → - 1 = ( 0 − 1 ) )
364 13 lem1d ⊢ ( 𝜑 → ( 0 − 1 ) ≤ 0 )
365 363 364 eqbrtrd ⊢ ( 𝜑 → - 1 ≤ 0 )
366 361 13 253 365 98 letrd ⊢ ( 𝜑 → - 1 ≤ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) )
367 86 28 101 105 360 366 bcle2d ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) + 1 ) + - 1 ) ) ≤ ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + - 1 ) ) )
368 42 109 115 274 367 ltletrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + - 1 ) ) )
369 222 240 negsubd ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + - 1 ) = ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) − 1 ) )
370 369 oveq2d ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + - 1 ) ) = ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) − 1 ) ) )
371 368 370 breqtrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) − 1 ) ) )
372 9 eqcomi ⊢ ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) = 𝐴
373 372 a1i ⊢ ( 𝜑 → ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) = 𝐴 )
374 373 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) = ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + 𝐴 ) )
375 374 oveq1d ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) ) ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) − 1 ) ) = ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + 𝐴 ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) − 1 ) ) )
376 371 375 breqtrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + 𝐴 ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) − 1 ) ) )
377 26 eqcomd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) = 𝐷 )
378 377 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + 𝐴 ) = ( 𝐷 + 𝐴 ) )
379 377 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) − 1 ) = ( 𝐷 − 1 ) )
380 378 379 oveq12d ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) + 𝐴 ) C ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) − 1 ) ) = ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) )
381 376 380 breqtrd ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( √ ‘ 𝐷 ) ) ) < ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) )