Metamath Proof Explorer

Theorem pntlemn

Description: Lemma for pnt . The "naive" base bound, which we will slightly improve. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Hypotheses pntlem1.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
pntlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
pntlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
pntlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
pntlem1.d ⊢ 𝐷 = ( 𝐴 + 1 )
pntlem1.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
pntlem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
pntlem1.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
pntlem1.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
pntlem1.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
pntlem1.y ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
pntlem1.x ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
pntlem1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
pntlem1.w ⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
pntlem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
pntlem1.m ⊢ 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
pntlem1.n ⊢ 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
pntlem1.U ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
Assertion pntlemn ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 0 ≤ ( ( ( 𝑈 / 𝐽 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) ) · ( log ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 pntlem1.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 pntlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3 pntlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4 pntlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
5 pntlem1.d ⊢ 𝐷 = ( 𝐴 + 1 )
6 pntlem1.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
7 pntlem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
8 pntlem1.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
9 pntlem1.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
10 pntlem1.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
11 pntlem1.y ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
12 pntlem1.x ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
13 pntlem1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
14 pntlem1.w ⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
15 pntlem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
16 pntlem1.m ⊢ 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
17 pntlem1.n ⊢ 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
18 pntlem1.U ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
19 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝑈 ∈ ℝ+ )
20 19 rpred ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝑈 ∈ ℝ )
21 simprl ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝐽 ∈ ℕ )
22 20 21 nndivred ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 𝑈 / 𝐽 ) ∈ ℝ )
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pntlemb ⊢ ( 𝜑 → ( 𝑍 ∈ ℝ+ ∧ ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) ∧ ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )
24 23 simp1d ⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
25 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝑍 ∈ ℝ+ )
26 21 nnrpd ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝐽 ∈ ℝ+ )
27 25 26 rpdivcld ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 𝑍 / 𝐽 ) ∈ ℝ+ )
28 1 pntrf ⊢ 𝑅 : ℝ+ ⟶ ℝ
29 28 ffvelrni ⊢ ( ( 𝑍 / 𝐽 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) ∈ ℝ )
30 27 29 syl ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) ∈ ℝ )
31 30 25 rerpdivcld ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ∈ ℝ )
32 31 recnd ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ∈ ℂ )
33 32 abscld ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) ∈ ℝ )
34 22 33 resubcld ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( 𝑈 / 𝐽 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) ) ∈ ℝ )
35 26 relogcld ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( log ‘ 𝐽 ) ∈ ℝ )
36 30 recnd ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) ∈ ℂ )
37 25 rpcnne0d ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) )
38 26 rpcnne0d ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 𝐽 ∈ ℂ ∧ 𝐽 ≠ 0 ) )
39 divdiv2 ⊢ ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) ∈ ℂ ∧ ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) ∧ ( 𝐽 ∈ ℂ ∧ 𝐽 ≠ 0 ) ) → ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / ( 𝑍 / 𝐽 ) ) = ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) · 𝐽 ) / 𝑍 ) )
40 36 37 38 39 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / ( 𝑍 / 𝐽 ) ) = ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) · 𝐽 ) / 𝑍 ) )
41 21 nncnd ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝐽 ∈ ℂ )
42 div23 ⊢ ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) ) → ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) · 𝐽 ) / 𝑍 ) = ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) · 𝐽 ) )
43 36 41 37 42 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) · 𝐽 ) / 𝑍 ) = ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) · 𝐽 ) )
44 40 43 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / ( 𝑍 / 𝐽 ) ) = ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) · 𝐽 ) )
45 44 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / ( 𝑍 / 𝐽 ) ) ) = ( abs ‘ ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) · 𝐽 ) ) )
46 32 41 absmuld ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( abs ‘ ( ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) · 𝐽 ) ) = ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) · ( abs ‘ 𝐽 ) ) )
47 26 rprege0d ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 𝐽 ∈ ℝ ∧ 0 ≤ 𝐽 ) )
48 absid ⊢ ( ( 𝐽 ∈ ℝ ∧ 0 ≤ 𝐽 ) → ( abs ‘ 𝐽 ) = 𝐽 )
49 47 48 syl ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( abs ‘ 𝐽 ) = 𝐽 )
50 49 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) · ( abs ‘ 𝐽 ) ) = ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) · 𝐽 ) )
51 45 46 50 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / ( 𝑍 / 𝐽 ) ) ) = ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) · 𝐽 ) )
52 fveq2 ⊢ ( 𝑧 = ( 𝑍 / 𝐽 ) → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) )
53 id ⊢ ( 𝑧 = ( 𝑍 / 𝐽 ) → 𝑧 = ( 𝑍 / 𝐽 ) )
54 52 53 oveq12d ⊢ ( 𝑧 = ( 𝑍 / 𝐽 ) → ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) = ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / ( 𝑍 / 𝐽 ) ) )
55 54 fveq2d ⊢ ( 𝑧 = ( 𝑍 / 𝐽 ) → ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) = ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / ( 𝑍 / 𝐽 ) ) ) )
56 55 breq1d ⊢ ( 𝑧 = ( 𝑍 / 𝐽 ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 ↔ ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / ( 𝑍 / 𝐽 ) ) ) ≤ 𝑈 ) )
57 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
58 27 rpred ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 𝑍 / 𝐽 ) ∈ ℝ )
59 simprr ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝐽 ≤ ( 𝑍 / 𝑌 ) )
60 26 rpred ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝐽 ∈ ℝ )
61 25 rpred ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝑍 ∈ ℝ )
62 11 simpld ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝑌 ∈ ℝ+ )
64 60 61 63 lemuldiv2d ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( 𝑌 · 𝐽 ) ≤ 𝑍 ↔ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) )
65 59 64 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 𝑌 · 𝐽 ) ≤ 𝑍 )
66 63 rpred ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝑌 ∈ ℝ )
67 66 61 26 lemuldivd ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( 𝑌 · 𝐽 ) ≤ 𝑍 ↔ 𝑌 ≤ ( 𝑍 / 𝐽 ) ) )
68 65 67 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 𝑌 ≤ ( 𝑍 / 𝐽 ) )
69 elicopnf ⊢ ( 𝑌 ∈ ℝ → ( ( 𝑍 / 𝐽 ) ∈ ( 𝑌 [,) +∞ ) ↔ ( ( 𝑍 / 𝐽 ) ∈ ℝ ∧ 𝑌 ≤ ( 𝑍 / 𝐽 ) ) ) )
70 66 69 syl ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( 𝑍 / 𝐽 ) ∈ ( 𝑌 [,) +∞ ) ↔ ( ( 𝑍 / 𝐽 ) ∈ ℝ ∧ 𝑌 ≤ ( 𝑍 / 𝐽 ) ) ) )
71 58 68 70 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 𝑍 / 𝐽 ) ∈ ( 𝑌 [,) +∞ ) )
72 56 57 71 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / ( 𝑍 / 𝐽 ) ) ) ≤ 𝑈 )
73 51 72 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) · 𝐽 ) ≤ 𝑈 )
74 33 20 26 lemuldivd ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) · 𝐽 ) ≤ 𝑈 ↔ ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) ≤ ( 𝑈 / 𝐽 ) ) )
75 73 74 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) ≤ ( 𝑈 / 𝐽 ) )
76 22 33 subge0d ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 0 ≤ ( ( 𝑈 / 𝐽 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) ) ↔ ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) ≤ ( 𝑈 / 𝐽 ) ) )
77 75 76 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 0 ≤ ( ( 𝑈 / 𝐽 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) ) )
78 log1 ⊢ ( log ‘ 1 ) = 0
79 nnge1 ⊢ ( 𝐽 ∈ ℕ → 1 ≤ 𝐽 )
80 79 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 1 ≤ 𝐽 )
81 1rp ⊢ 1 ∈ ℝ+
82 logleb ⊢ ( ( 1 ∈ ℝ+ ∧ 𝐽 ∈ ℝ+ ) → ( 1 ≤ 𝐽 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐽 ) ) )
83 81 26 82 sylancr ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( 1 ≤ 𝐽 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐽 ) ) )
84 80 83 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → ( log ‘ 1 ) ≤ ( log ‘ 𝐽 ) )
85 78 84 eqbrtrrid ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 0 ≤ ( log ‘ 𝐽 ) )
86 34 35 77 85 mulge0d ⊢ ( ( 𝜑 ∧ ( 𝐽 ∈ ℕ ∧ 𝐽 ≤ ( 𝑍 / 𝑌 ) ) ) → 0 ≤ ( ( ( 𝑈 / 𝐽 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝐽 ) ) / 𝑍 ) ) ) · ( log ‘ 𝐽 ) ) )