Metamath Proof Explorer

Theorem pntlemk

Description: Lemma for pnt . Evaluate the naive part of the estimate. (Contributed by Mario Carneiro, 14-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 ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
pntlem1.K ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
Assertion pntlemk ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ) ≤ ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( 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 pntlem1.K ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
20 2re ⊢ 2 ∈ ℝ
21 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ∈ Fin )
22 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) → 𝑛 ∈ ℕ )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ∈ ℕ )
24 23 nnrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑛 ∈ ℝ+ )
25 24 relogcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
26 25 23 nndivred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
27 21 26 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
28 remulcl ⊢ ( ( 2 ∈ ℝ ∧ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
29 20 27 28 sylancr ⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
30 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 ‘ 𝑍 ) ) ) ) )
31 30 simp1d ⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
32 31 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ )
33 peano2re ⊢ ( ( log ‘ 𝑍 ) ∈ ℝ → ( ( log ‘ 𝑍 ) + 1 ) ∈ ℝ )
34 32 33 syl ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) + 1 ) ∈ ℝ )
35 34 resqcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) + 1 ) ↑ 2 ) ∈ ℝ )
36 3re ⊢ 3 ∈ ℝ
37 readdcl ⊢ ( ( ( log ‘ 𝑍 ) ∈ ℝ ∧ 3 ∈ ℝ ) → ( ( log ‘ 𝑍 ) + 3 ) ∈ ℝ )
38 32 36 37 sylancl ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) + 3 ) ∈ ℝ )
39 38 32 remulcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) + 3 ) · ( log ‘ 𝑍 ) ) ∈ ℝ )
40 31 rpred ⊢ ( 𝜑 → 𝑍 ∈ ℝ )
41 11 simpld ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
42 40 41 rerpdivcld ⊢ ( 𝜑 → ( 𝑍 / 𝑌 ) ∈ ℝ )
43 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
44 31 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ∈ ℝ+ )
45 44 rpred ⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ∈ ℝ )
46 ere ⊢ e ∈ ℝ
47 46 a1i ⊢ ( 𝜑 → e ∈ ℝ )
48 1re ⊢ 1 ∈ ℝ
49 1lt2 ⊢ 1 < 2
50 egt2lt3 ⊢ ( 2 < e ∧ e < 3 )
51 50 simpli ⊢ 2 < e
52 48 20 46 lttri ⊢ ( ( 1 < 2 ∧ 2 < e ) → 1 < e )
53 49 51 52 mp2an ⊢ 1 < e
54 48 46 53 ltleii ⊢ 1 ≤ e
55 54 a1i ⊢ ( 𝜑 → 1 ≤ e )
56 30 simp2d ⊢ ( 𝜑 → ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) )
57 56 simp2d ⊢ ( 𝜑 → e ≤ ( √ ‘ 𝑍 ) )
58 43 47 45 55 57 letrd ⊢ ( 𝜑 → 1 ≤ ( √ ‘ 𝑍 ) )
59 56 simp3d ⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) )
60 43 45 42 58 59 letrd ⊢ ( 𝜑 → 1 ≤ ( 𝑍 / 𝑌 ) )
61 flge1nn ⊢ ( ( ( 𝑍 / 𝑌 ) ∈ ℝ ∧ 1 ≤ ( 𝑍 / 𝑌 ) ) → ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ℕ )
62 42 60 61 syl2anc ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ℕ )
63 62 nnrpd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ℝ+ )
64 63 relogcld ⊢ ( 𝜑 → ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ∈ ℝ )
65 64 43 readdcld ⊢ ( 𝜑 → ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ∈ ℝ )
66 65 resqcld ⊢ ( 𝜑 → ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) ∈ ℝ )
67 logdivbnd ⊢ ( ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ℕ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ ( ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) / 2 ) )
68 62 67 syl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ ( ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) / 2 ) )
69 20 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
70 2pos ⊢ 0 < 2
71 70 a1i ⊢ ( 𝜑 → 0 < 2 )
72 lemuldiv2 ⊢ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ∧ ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) ↔ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ ( ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) / 2 ) ) )
73 27 66 69 71 72 syl112anc ⊢ ( 𝜑 → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) ↔ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ ( ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) / 2 ) ) )
74 68 73 mpbird ⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) )
75 reflcl ⊢ ( ( 𝑍 / 𝑌 ) ∈ ℝ → ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ℝ )
76 42 75 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ℝ )
77 flle ⊢ ( ( 𝑍 / 𝑌 ) ∈ ℝ → ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ≤ ( 𝑍 / 𝑌 ) )
78 42 77 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ≤ ( 𝑍 / 𝑌 ) )
79 11 simprd ⊢ ( 𝜑 → 1 ≤ 𝑌 )
80 1rp ⊢ 1 ∈ ℝ+
81 80 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
82 81 41 31 lediv2d ⊢ ( 𝜑 → ( 1 ≤ 𝑌 ↔ ( 𝑍 / 𝑌 ) ≤ ( 𝑍 / 1 ) ) )
83 79 82 mpbid ⊢ ( 𝜑 → ( 𝑍 / 𝑌 ) ≤ ( 𝑍 / 1 ) )
84 40 recnd ⊢ ( 𝜑 → 𝑍 ∈ ℂ )
85 84 div1d ⊢ ( 𝜑 → ( 𝑍 / 1 ) = 𝑍 )
86 83 85 breqtrd ⊢ ( 𝜑 → ( 𝑍 / 𝑌 ) ≤ 𝑍 )
87 76 42 40 78 86 letrd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ≤ 𝑍 )
88 63 31 logled ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ≤ 𝑍 ↔ ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ≤ ( log ‘ 𝑍 ) ) )
89 87 88 mpbid ⊢ ( 𝜑 → ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ≤ ( log ‘ 𝑍 ) )
90 64 32 43 89 leadd1dd ⊢ ( 𝜑 → ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ≤ ( ( log ‘ 𝑍 ) + 1 ) )
91 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
92 log1 ⊢ ( log ‘ 1 ) = 0
93 62 nnge1d ⊢ ( 𝜑 → 1 ≤ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) )
94 logleb ⊢ ( ( 1 ∈ ℝ+ ∧ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ∈ ℝ+ ) → ( 1 ≤ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ↔ ( log ‘ 1 ) ≤ ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) )
95 80 63 94 sylancr ⊢ ( 𝜑 → ( 1 ≤ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ↔ ( log ‘ 1 ) ≤ ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) )
96 93 95 mpbid ⊢ ( 𝜑 → ( log ‘ 1 ) ≤ ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
97 92 96 eqbrtrrid ⊢ ( 𝜑 → 0 ≤ ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) )
98 64 lep1d ⊢ ( 𝜑 → ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ≤ ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) )
99 91 64 65 97 98 letrd ⊢ ( 𝜑 → 0 ≤ ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) )
100 91 65 34 99 90 letrd ⊢ ( 𝜑 → 0 ≤ ( ( log ‘ 𝑍 ) + 1 ) )
101 65 34 99 100 le2sqd ⊢ ( 𝜑 → ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ≤ ( ( log ‘ 𝑍 ) + 1 ) ↔ ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) ≤ ( ( ( log ‘ 𝑍 ) + 1 ) ↑ 2 ) ) )
102 90 101 mpbid ⊢ ( 𝜑 → ( ( ( log ‘ ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) + 1 ) ↑ 2 ) ≤ ( ( ( log ‘ 𝑍 ) + 1 ) ↑ 2 ) )
103 29 66 35 74 102 letrd ⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( ( ( log ‘ 𝑍 ) + 1 ) ↑ 2 ) )
104 32 resqcld ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) ↑ 2 ) ∈ ℝ )
105 69 32 remulcld ⊢ ( 𝜑 → ( 2 · ( log ‘ 𝑍 ) ) ∈ ℝ )
106 104 105 readdcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) ↑ 2 ) + ( 2 · ( log ‘ 𝑍 ) ) ) ∈ ℝ )
107 loge ⊢ ( log ‘ e ) = 1
108 44 rpge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ 𝑍 ) )
109 45 45 108 58 lemulge12d ⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ≤ ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) )
110 31 rprege0d ⊢ ( 𝜑 → ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) )
111 remsqsqrt ⊢ ( ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) → ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) = 𝑍 )
112 110 111 syl ⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) = 𝑍 )
113 109 112 breqtrd ⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ≤ 𝑍 )
114 47 45 40 57 113 letrd ⊢ ( 𝜑 → e ≤ 𝑍 )
115 epr ⊢ e ∈ ℝ+
116 logleb ⊢ ( ( e ∈ ℝ+ ∧ 𝑍 ∈ ℝ+ ) → ( e ≤ 𝑍 ↔ ( log ‘ e ) ≤ ( log ‘ 𝑍 ) ) )
117 115 31 116 sylancr ⊢ ( 𝜑 → ( e ≤ 𝑍 ↔ ( log ‘ e ) ≤ ( log ‘ 𝑍 ) ) )
118 114 117 mpbid ⊢ ( 𝜑 → ( log ‘ e ) ≤ ( log ‘ 𝑍 ) )
119 107 118 eqbrtrrid ⊢ ( 𝜑 → 1 ≤ ( log ‘ 𝑍 ) )
120 43 32 106 119 leadd2dd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) ↑ 2 ) + ( 2 · ( log ‘ 𝑍 ) ) ) + 1 ) ≤ ( ( ( ( log ‘ 𝑍 ) ↑ 2 ) + ( 2 · ( log ‘ 𝑍 ) ) ) + ( log ‘ 𝑍 ) ) )
121 32 recnd ⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℂ )
122 binom21 ⊢ ( ( log ‘ 𝑍 ) ∈ ℂ → ( ( ( log ‘ 𝑍 ) + 1 ) ↑ 2 ) = ( ( ( ( log ‘ 𝑍 ) ↑ 2 ) + ( 2 · ( log ‘ 𝑍 ) ) ) + 1 ) )
123 121 122 syl ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) + 1 ) ↑ 2 ) = ( ( ( ( log ‘ 𝑍 ) ↑ 2 ) + ( 2 · ( log ‘ 𝑍 ) ) ) + 1 ) )
124 121 sqvald ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) ↑ 2 ) = ( ( log ‘ 𝑍 ) · ( log ‘ 𝑍 ) ) )
125 df-3 ⊢ 3 = ( 2 + 1 )
126 125 oveq1i ⊢ ( 3 · ( log ‘ 𝑍 ) ) = ( ( 2 + 1 ) · ( log ‘ 𝑍 ) )
127 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
128 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
129 127 128 121 adddird ⊢ ( 𝜑 → ( ( 2 + 1 ) · ( log ‘ 𝑍 ) ) = ( ( 2 · ( log ‘ 𝑍 ) ) + ( 1 · ( log ‘ 𝑍 ) ) ) )
130 126 129 syl5eq ⊢ ( 𝜑 → ( 3 · ( log ‘ 𝑍 ) ) = ( ( 2 · ( log ‘ 𝑍 ) ) + ( 1 · ( log ‘ 𝑍 ) ) ) )
131 121 mulid2d ⊢ ( 𝜑 → ( 1 · ( log ‘ 𝑍 ) ) = ( log ‘ 𝑍 ) )
132 131 oveq2d ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝑍 ) ) + ( 1 · ( log ‘ 𝑍 ) ) ) = ( ( 2 · ( log ‘ 𝑍 ) ) + ( log ‘ 𝑍 ) ) )
133 130 132 eqtr2d ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝑍 ) ) + ( log ‘ 𝑍 ) ) = ( 3 · ( log ‘ 𝑍 ) ) )
134 124 133 oveq12d ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) ↑ 2 ) + ( ( 2 · ( log ‘ 𝑍 ) ) + ( log ‘ 𝑍 ) ) ) = ( ( ( log ‘ 𝑍 ) · ( log ‘ 𝑍 ) ) + ( 3 · ( log ‘ 𝑍 ) ) ) )
135 121 sqcld ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) ↑ 2 ) ∈ ℂ )
136 2cn ⊢ 2 ∈ ℂ
137 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( log ‘ 𝑍 ) ∈ ℂ ) → ( 2 · ( log ‘ 𝑍 ) ) ∈ ℂ )
138 136 121 137 sylancr ⊢ ( 𝜑 → ( 2 · ( log ‘ 𝑍 ) ) ∈ ℂ )
139 135 138 121 addassd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) ↑ 2 ) + ( 2 · ( log ‘ 𝑍 ) ) ) + ( log ‘ 𝑍 ) ) = ( ( ( log ‘ 𝑍 ) ↑ 2 ) + ( ( 2 · ( log ‘ 𝑍 ) ) + ( log ‘ 𝑍 ) ) ) )
140 3cn ⊢ 3 ∈ ℂ
141 140 a1i ⊢ ( 𝜑 → 3 ∈ ℂ )
142 121 141 121 adddird ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) + 3 ) · ( log ‘ 𝑍 ) ) = ( ( ( log ‘ 𝑍 ) · ( log ‘ 𝑍 ) ) + ( 3 · ( log ‘ 𝑍 ) ) ) )
143 134 139 142 3eqtr4rd ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) + 3 ) · ( log ‘ 𝑍 ) ) = ( ( ( ( log ‘ 𝑍 ) ↑ 2 ) + ( 2 · ( log ‘ 𝑍 ) ) ) + ( log ‘ 𝑍 ) ) )
144 120 123 143 3brtr4d ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) + 1 ) ↑ 2 ) ≤ ( ( ( log ‘ 𝑍 ) + 3 ) · ( log ‘ 𝑍 ) ) )
145 29 35 39 103 144 letrd ⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( ( ( log ‘ 𝑍 ) + 3 ) · ( log ‘ 𝑍 ) ) )
146 29 39 7 lemul2d ⊢ ( 𝜑 → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( ( ( log ‘ 𝑍 ) + 3 ) · ( log ‘ 𝑍 ) ) ↔ ( 𝑈 · ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ) ≤ ( 𝑈 · ( ( ( log ‘ 𝑍 ) + 3 ) · ( log ‘ 𝑍 ) ) ) ) )
147 145 146 mpbid ⊢ ( 𝜑 → ( 𝑈 · ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ) ≤ ( 𝑈 · ( ( ( log ‘ 𝑍 ) + 3 ) · ( log ‘ 𝑍 ) ) ) )
148 7 rpred ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
149 148 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑈 ∈ ℝ )
150 149 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → 𝑈 ∈ ℂ )
151 25 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
152 24 rpcnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
153 div23 ⊢ ( ( 𝑈 ∈ ℂ ∧ ( log ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑈 · ( log ‘ 𝑛 ) ) / 𝑛 ) = ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) )
154 divass ⊢ ( ( 𝑈 ∈ ℂ ∧ ( log ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑈 · ( log ‘ 𝑛 ) ) / 𝑛 ) = ( 𝑈 · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
155 153 154 eqtr3d ⊢ ( ( 𝑈 ∈ ℂ ∧ ( log ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) = ( 𝑈 · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
156 150 151 152 155 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) = ( 𝑈 · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
157 156 sumeq2dv ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( 𝑈 · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
158 148 recnd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
159 26 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ) → ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
160 21 158 159 fsummulc2 ⊢ ( 𝜑 → ( 𝑈 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( 𝑈 · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
161 157 160 eqtr4d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) = ( 𝑈 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
162 161 oveq2d ⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( 2 · ( 𝑈 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ) )
163 27 recnd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
164 127 158 163 mul12d ⊢ ( 𝜑 → ( 2 · ( 𝑈 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ) = ( 𝑈 · ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ) )
165 162 164 eqtrd ⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( 𝑈 · ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ) )
166 38 recnd ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) + 3 ) ∈ ℂ )
167 158 166 121 mulassd ⊢ ( 𝜑 → ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) = ( 𝑈 · ( ( ( log ‘ 𝑍 ) + 3 ) · ( log ‘ 𝑍 ) ) ) )
168 147 165 167 3brtr4d ⊢ ( 𝜑 → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑍 / 𝑌 ) ) ) ( ( 𝑈 / 𝑛 ) · ( log ‘ 𝑛 ) ) ) ≤ ( ( 𝑈 · ( ( log ‘ 𝑍 ) + 3 ) ) · ( log ‘ 𝑍 ) ) )