MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntlemo Structured version   Visualization version   GIF version

Theorem pntlemo 27558
Description: Lemma for pnt 27565. Combine all the estimates to establish a smaller eventual bound on 𝑅(𝑍) / 𝑍. (Contributed by Mario Carneiro, 14-Apr-2016.)
Hypotheses
Ref Expression
pntlem1.r 𝑅 = (π‘Ž ∈ ℝ+ ↦ ((Οˆβ€˜π‘Ž) βˆ’ π‘Ž))
pntlem1.a (πœ‘ β†’ 𝐴 ∈ ℝ+)
pntlem1.b (πœ‘ β†’ 𝐡 ∈ ℝ+)
pntlem1.l (πœ‘ β†’ 𝐿 ∈ (0(,)1))
pntlem1.d 𝐷 = (𝐴 + 1)
pntlem1.f 𝐹 = ((1 βˆ’ (1 / 𝐷)) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)))
pntlem1.u (πœ‘ β†’ π‘ˆ ∈ ℝ+)
pntlem1.u2 (πœ‘ β†’ π‘ˆ ≀ 𝐴)
pntlem1.e 𝐸 = (π‘ˆ / 𝐷)
pntlem1.k 𝐾 = (expβ€˜(𝐡 / 𝐸))
pntlem1.y (πœ‘ β†’ (π‘Œ ∈ ℝ+ ∧ 1 ≀ π‘Œ))
pntlem1.x (πœ‘ β†’ (𝑋 ∈ ℝ+ ∧ π‘Œ < 𝑋))
pntlem1.c (πœ‘ β†’ 𝐢 ∈ ℝ+)
pntlem1.w π‘Š = (((π‘Œ + (4 / (𝐿 Β· 𝐸)))↑2) + (((𝑋 Β· (𝐾↑2))↑4) + (expβ€˜(((32 Β· 𝐡) / ((π‘ˆ βˆ’ 𝐸) Β· (𝐿 Β· (𝐸↑2)))) Β· ((π‘ˆ Β· 3) + 𝐢)))))
pntlem1.z (πœ‘ β†’ 𝑍 ∈ (π‘Š[,)+∞))
pntlem1.m 𝑀 = ((βŒŠβ€˜((logβ€˜π‘‹) / (logβ€˜πΎ))) + 1)
pntlem1.n 𝑁 = (βŒŠβ€˜(((logβ€˜π‘) / (logβ€˜πΎ)) / 2))
pntlem1.U (πœ‘ β†’ βˆ€π‘§ ∈ (π‘Œ[,)+∞)(absβ€˜((π‘…β€˜π‘§) / 𝑧)) ≀ π‘ˆ)
pntlem1.K (πœ‘ β†’ βˆ€π‘¦ ∈ (𝑋(,)+∞)βˆƒπ‘§ ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝐾 Β· 𝑦)) ∧ βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
pntlem1.C (πœ‘ β†’ βˆ€π‘§ ∈ (1(,)+∞)((((absβ€˜(π‘…β€˜π‘§)) Β· (logβ€˜π‘§)) βˆ’ ((2 / (logβ€˜π‘§)) Β· Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)))) / 𝑧) ≀ 𝐢)
Assertion
Ref Expression
pntlemo (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑍)) ≀ (π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))))
Distinct variable groups:   𝑧,𝐢   𝑦,𝑧,𝑒,𝐿   𝑦,𝐾,𝑧   𝑧,𝑀   𝑧,𝑁   𝑒,𝑖,𝑦,𝑧,𝑅   𝑧,π‘ˆ   𝑧,π‘Š   𝑦,𝑋,𝑧   𝑖,π‘Œ,𝑧   𝑒,π‘Ž,𝑦,𝑧,𝐸   𝑒,𝑍,𝑧
Allowed substitution hints:   πœ‘(𝑦,𝑧,𝑒,𝑖,π‘Ž)   𝐴(𝑦,𝑧,𝑒,𝑖,π‘Ž)   𝐡(𝑦,𝑧,𝑒,𝑖,π‘Ž)   𝐢(𝑦,𝑒,𝑖,π‘Ž)   𝐷(𝑦,𝑧,𝑒,𝑖,π‘Ž)   𝑅(π‘Ž)   π‘ˆ(𝑦,𝑒,𝑖,π‘Ž)   𝐸(𝑖)   𝐹(𝑦,𝑧,𝑒,𝑖,π‘Ž)   𝐾(𝑒,𝑖,π‘Ž)   𝐿(𝑖,π‘Ž)   𝑀(𝑦,𝑒,𝑖,π‘Ž)   𝑁(𝑦,𝑒,𝑖,π‘Ž)   π‘Š(𝑦,𝑒,𝑖,π‘Ž)   𝑋(𝑒,𝑖,π‘Ž)   π‘Œ(𝑦,𝑒,π‘Ž)   𝑍(𝑦,𝑖,π‘Ž)

Proof of Theorem pntlemo
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 pntlem1.r . . . . . . . . . 10 𝑅 = (π‘Ž ∈ ℝ+ ↦ ((Οˆβ€˜π‘Ž) βˆ’ π‘Ž))
2 pntlem1.a . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ ℝ+)
3 pntlem1.b . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ ℝ+)
4 pntlem1.l . . . . . . . . . 10 (πœ‘ β†’ 𝐿 ∈ (0(,)1))
5 pntlem1.d . . . . . . . . . 10 𝐷 = (𝐴 + 1)
6 pntlem1.f . . . . . . . . . 10 𝐹 = ((1 βˆ’ (1 / 𝐷)) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)))
7 pntlem1.u . . . . . . . . . 10 (πœ‘ β†’ π‘ˆ ∈ ℝ+)
8 pntlem1.u2 . . . . . . . . . 10 (πœ‘ β†’ π‘ˆ ≀ 𝐴)
9 pntlem1.e . . . . . . . . . 10 𝐸 = (π‘ˆ / 𝐷)
10 pntlem1.k . . . . . . . . . 10 𝐾 = (expβ€˜(𝐡 / 𝐸))
11 pntlem1.y . . . . . . . . . 10 (πœ‘ β†’ (π‘Œ ∈ ℝ+ ∧ 1 ≀ π‘Œ))
12 pntlem1.x . . . . . . . . . 10 (πœ‘ β†’ (𝑋 ∈ ℝ+ ∧ π‘Œ < 𝑋))
13 pntlem1.c . . . . . . . . . 10 (πœ‘ β†’ 𝐢 ∈ ℝ+)
14 pntlem1.w . . . . . . . . . 10 π‘Š = (((π‘Œ + (4 / (𝐿 Β· 𝐸)))↑2) + (((𝑋 Β· (𝐾↑2))↑4) + (expβ€˜(((32 Β· 𝐡) / ((π‘ˆ βˆ’ 𝐸) Β· (𝐿 Β· (𝐸↑2)))) Β· ((π‘ˆ Β· 3) + 𝐢)))))
15 pntlem1.z . . . . . . . . . 10 (πœ‘ β†’ 𝑍 ∈ (π‘Š[,)+∞))
161, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15pntlemb 27548 . . . . . . . . 9 (πœ‘ β†’ (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≀ (βˆšβ€˜π‘) ∧ (βˆšβ€˜π‘) ≀ (𝑍 / π‘Œ)) ∧ ((4 / (𝐿 Β· 𝐸)) ≀ (βˆšβ€˜π‘) ∧ (((logβ€˜π‘‹) / (logβ€˜πΎ)) + 2) ≀ (((logβ€˜π‘) / (logβ€˜πΎ)) / 4) ∧ ((π‘ˆ Β· 3) + 𝐢) ≀ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))))
1716simp1d 1139 . . . . . . . 8 (πœ‘ β†’ 𝑍 ∈ ℝ+)
181pntrf 27514 . . . . . . . . 9 𝑅:ℝ+βŸΆβ„
1918ffvelcdmi 7096 . . . . . . . 8 (𝑍 ∈ ℝ+ β†’ (π‘…β€˜π‘) ∈ ℝ)
2017, 19syl 17 . . . . . . 7 (πœ‘ β†’ (π‘…β€˜π‘) ∈ ℝ)
2120, 17rerpdivcld 13085 . . . . . 6 (πœ‘ β†’ ((π‘…β€˜π‘) / 𝑍) ∈ ℝ)
2221recnd 11278 . . . . 5 (πœ‘ β†’ ((π‘…β€˜π‘) / 𝑍) ∈ β„‚)
2322abscld 15421 . . . 4 (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑍)) ∈ ℝ)
2417relogcld 26575 . . . 4 (πœ‘ β†’ (logβ€˜π‘) ∈ ℝ)
2523, 24remulcld 11280 . . 3 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) ∈ ℝ)
267rpred 13054 . . . . . 6 (πœ‘ β†’ π‘ˆ ∈ ℝ)
27 3re 12328 . . . . . . . 8 3 ∈ ℝ
2827a1i 11 . . . . . . 7 (πœ‘ β†’ 3 ∈ ℝ)
2924, 28readdcld 11279 . . . . . 6 (πœ‘ β†’ ((logβ€˜π‘) + 3) ∈ ℝ)
3026, 29remulcld 11280 . . . . 5 (πœ‘ β†’ (π‘ˆ Β· ((logβ€˜π‘) + 3)) ∈ ℝ)
31 2re 12322 . . . . . . 7 2 ∈ ℝ
3231a1i 11 . . . . . 6 (πœ‘ β†’ 2 ∈ ℝ)
331, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 27546 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (π‘ˆ βˆ’ 𝐸) ∈ ℝ+)))
3433simp3d 1141 . . . . . . . . . 10 (πœ‘ β†’ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (π‘ˆ βˆ’ 𝐸) ∈ ℝ+))
3534simp3d 1141 . . . . . . . . 9 (πœ‘ β†’ (π‘ˆ βˆ’ 𝐸) ∈ ℝ+)
3635rpred 13054 . . . . . . . 8 (πœ‘ β†’ (π‘ˆ βˆ’ 𝐸) ∈ ℝ)
371, 2, 3, 4, 5, 6pntlemd 27545 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+))
3837simp1d 1139 . . . . . . . . . . 11 (πœ‘ β†’ 𝐿 ∈ ℝ+)
3933simp1d 1139 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐸 ∈ ℝ+)
40 2z 12630 . . . . . . . . . . . 12 2 ∈ β„€
41 rpexpcl 14083 . . . . . . . . . . . 12 ((𝐸 ∈ ℝ+ ∧ 2 ∈ β„€) β†’ (𝐸↑2) ∈ ℝ+)
4239, 40, 41sylancl 584 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸↑2) ∈ ℝ+)
4338, 42rpmulcld 13070 . . . . . . . . . 10 (πœ‘ β†’ (𝐿 Β· (𝐸↑2)) ∈ ℝ+)
44 3nn0 12526 . . . . . . . . . . . . 13 3 ∈ β„•0
45 2nn 12321 . . . . . . . . . . . . 13 2 ∈ β„•
4644, 45decnncl 12733 . . . . . . . . . . . 12 32 ∈ β„•
47 nnrp 13023 . . . . . . . . . . . 12 (32 ∈ β„• β†’ 32 ∈ ℝ+)
4846, 47ax-mp 5 . . . . . . . . . . 11 32 ∈ ℝ+
49 rpmulcl 13035 . . . . . . . . . . 11 ((32 ∈ ℝ+ ∧ 𝐡 ∈ ℝ+) β†’ (32 Β· 𝐡) ∈ ℝ+)
5048, 3, 49sylancr 585 . . . . . . . . . 10 (πœ‘ β†’ (32 Β· 𝐡) ∈ ℝ+)
5143, 50rpdivcld 13071 . . . . . . . . 9 (πœ‘ β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) ∈ ℝ+)
5251rpred 13054 . . . . . . . 8 (πœ‘ β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) ∈ ℝ)
5336, 52remulcld 11280 . . . . . . 7 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) ∈ ℝ)
5453, 24remulcld 11280 . . . . . 6 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) ∈ ℝ)
5532, 54remulcld 11280 . . . . 5 (πœ‘ β†’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) ∈ ℝ)
5630, 55resubcld 11678 . . . 4 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) ∈ ℝ)
5713rpred 13054 . . . 4 (πœ‘ β†’ 𝐢 ∈ ℝ)
5856, 57readdcld 11279 . . 3 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) + 𝐢) ∈ ℝ)
597rpcnd 13056 . . . . . 6 (πœ‘ β†’ π‘ˆ ∈ β„‚)
6053recnd 11278 . . . . . 6 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) ∈ β„‚)
6124recnd 11278 . . . . . 6 (πœ‘ β†’ (logβ€˜π‘) ∈ β„‚)
6259, 60, 61subdird 11707 . . . . 5 (πœ‘ β†’ ((π‘ˆ βˆ’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)))) Β· (logβ€˜π‘)) = ((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
6338rpcnd 13056 . . . . . . . . . . 11 (πœ‘ β†’ 𝐿 ∈ β„‚)
6442rpcnd 13056 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸↑2) ∈ β„‚)
6550rpcnne0d 13063 . . . . . . . . . . 11 (πœ‘ β†’ ((32 Β· 𝐡) ∈ β„‚ ∧ (32 Β· 𝐡) β‰  0))
66 div23 11927 . . . . . . . . . . 11 ((𝐿 ∈ β„‚ ∧ (𝐸↑2) ∈ β„‚ ∧ ((32 Β· 𝐡) ∈ β„‚ ∧ (32 Β· 𝐡) β‰  0)) β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) = ((𝐿 / (32 Β· 𝐡)) Β· (𝐸↑2)))
6763, 64, 65, 66syl3anc 1368 . . . . . . . . . 10 (πœ‘ β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) = ((𝐿 / (32 Β· 𝐡)) Β· (𝐸↑2)))
689oveq1i 7434 . . . . . . . . . . . 12 (𝐸↑2) = ((π‘ˆ / 𝐷)↑2)
6937simp2d 1140 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 ∈ ℝ+)
7069rpcnd 13056 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 ∈ β„‚)
7169rpne0d 13059 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 β‰  0)
7259, 70, 71sqdivd 14161 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘ˆ / 𝐷)↑2) = ((π‘ˆβ†‘2) / (𝐷↑2)))
7368, 72eqtrid 2779 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸↑2) = ((π‘ˆβ†‘2) / (𝐷↑2)))
7473oveq2d 7440 . . . . . . . . . 10 (πœ‘ β†’ ((𝐿 / (32 Β· 𝐡)) Β· (𝐸↑2)) = ((𝐿 / (32 Β· 𝐡)) Β· ((π‘ˆβ†‘2) / (𝐷↑2))))
7538, 50rpdivcld 13071 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐿 / (32 Β· 𝐡)) ∈ ℝ+)
7675rpcnd 13056 . . . . . . . . . . 11 (πœ‘ β†’ (𝐿 / (32 Β· 𝐡)) ∈ β„‚)
7759sqcld 14146 . . . . . . . . . . 11 (πœ‘ β†’ (π‘ˆβ†‘2) ∈ β„‚)
78 rpexpcl 14083 . . . . . . . . . . . . 13 ((𝐷 ∈ ℝ+ ∧ 2 ∈ β„€) β†’ (𝐷↑2) ∈ ℝ+)
7969, 40, 78sylancl 584 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐷↑2) ∈ ℝ+)
8079rpcnne0d 13063 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐷↑2) ∈ β„‚ ∧ (𝐷↑2) β‰  0))
81 divass 11926 . . . . . . . . . . . 12 (((𝐿 / (32 Β· 𝐡)) ∈ β„‚ ∧ (π‘ˆβ†‘2) ∈ β„‚ ∧ ((𝐷↑2) ∈ β„‚ ∧ (𝐷↑2) β‰  0)) β†’ (((𝐿 / (32 Β· 𝐡)) Β· (π‘ˆβ†‘2)) / (𝐷↑2)) = ((𝐿 / (32 Β· 𝐡)) Β· ((π‘ˆβ†‘2) / (𝐷↑2))))
82 div23 11927 . . . . . . . . . . . 12 (((𝐿 / (32 Β· 𝐡)) ∈ β„‚ ∧ (π‘ˆβ†‘2) ∈ β„‚ ∧ ((𝐷↑2) ∈ β„‚ ∧ (𝐷↑2) β‰  0)) β†’ (((𝐿 / (32 Β· 𝐡)) Β· (π‘ˆβ†‘2)) / (𝐷↑2)) = (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2)))
8381, 82eqtr3d 2769 . . . . . . . . . . 11 (((𝐿 / (32 Β· 𝐡)) ∈ β„‚ ∧ (π‘ˆβ†‘2) ∈ β„‚ ∧ ((𝐷↑2) ∈ β„‚ ∧ (𝐷↑2) β‰  0)) β†’ ((𝐿 / (32 Β· 𝐡)) Β· ((π‘ˆβ†‘2) / (𝐷↑2))) = (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2)))
8476, 77, 80, 83syl3anc 1368 . . . . . . . . . 10 (πœ‘ β†’ ((𝐿 / (32 Β· 𝐡)) Β· ((π‘ˆβ†‘2) / (𝐷↑2))) = (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2)))
8567, 74, 843eqtrd 2771 . . . . . . . . 9 (πœ‘ β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) = (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2)))
8685oveq2d 7440 . . . . . . . 8 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2))))
87 df-3 12312 . . . . . . . . . . . . 13 3 = (2 + 1)
8887oveq2i 7435 . . . . . . . . . . . 12 (π‘ˆβ†‘3) = (π‘ˆβ†‘(2 + 1))
89 2nn0 12525 . . . . . . . . . . . . 13 2 ∈ β„•0
90 expp1 14071 . . . . . . . . . . . . 13 ((π‘ˆ ∈ β„‚ ∧ 2 ∈ β„•0) β†’ (π‘ˆβ†‘(2 + 1)) = ((π‘ˆβ†‘2) Β· π‘ˆ))
9159, 89, 90sylancl 584 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘ˆβ†‘(2 + 1)) = ((π‘ˆβ†‘2) Β· π‘ˆ))
9288, 91eqtrid 2779 . . . . . . . . . . 11 (πœ‘ β†’ (π‘ˆβ†‘3) = ((π‘ˆβ†‘2) Β· π‘ˆ))
9377, 59mulcomd 11271 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘ˆβ†‘2) Β· π‘ˆ) = (π‘ˆ Β· (π‘ˆβ†‘2)))
9492, 93eqtrd 2767 . . . . . . . . . 10 (πœ‘ β†’ (π‘ˆβ†‘3) = (π‘ˆ Β· (π‘ˆβ†‘2)))
9594oveq2d 7440 . . . . . . . . 9 (πœ‘ β†’ (𝐹 Β· (π‘ˆβ†‘3)) = (𝐹 Β· (π‘ˆ Β· (π‘ˆβ†‘2))))
9637simp3d 1141 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 ∈ ℝ+)
9796rpcnd 13056 . . . . . . . . . 10 (πœ‘ β†’ 𝐹 ∈ β„‚)
9897, 59, 77mulassd 11273 . . . . . . . . 9 (πœ‘ β†’ ((𝐹 Β· π‘ˆ) Β· (π‘ˆβ†‘2)) = (𝐹 Β· (π‘ˆ Β· (π‘ˆβ†‘2))))
99 1cnd 11245 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 1 ∈ β„‚)
10069rpreccld 13064 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (1 / 𝐷) ∈ ℝ+)
101100rpcnd 13056 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1 / 𝐷) ∈ β„‚)
10299, 101, 59subdird 11707 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1 βˆ’ (1 / 𝐷)) Β· π‘ˆ) = ((1 Β· π‘ˆ) βˆ’ ((1 / 𝐷) Β· π‘ˆ)))
10359mullidd 11268 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1 Β· π‘ˆ) = π‘ˆ)
10459, 70, 71divrec2d 12030 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π‘ˆ / 𝐷) = ((1 / 𝐷) Β· π‘ˆ))
1059, 104eqtr2id 2780 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((1 / 𝐷) Β· π‘ˆ) = 𝐸)
106103, 105oveq12d 7442 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1 Β· π‘ˆ) βˆ’ ((1 / 𝐷) Β· π‘ˆ)) = (π‘ˆ βˆ’ 𝐸))
107102, 106eqtr2d 2768 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘ˆ βˆ’ 𝐸) = ((1 βˆ’ (1 / 𝐷)) Β· π‘ˆ))
108107oveq1d 7439 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) = (((1 βˆ’ (1 / 𝐷)) Β· π‘ˆ) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))))
1096oveq1i 7434 . . . . . . . . . . . . 13 (𝐹 Β· π‘ˆ) = (((1 βˆ’ (1 / 𝐷)) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) Β· π‘ˆ)
11099, 101subcld 11607 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 βˆ’ (1 / 𝐷)) ∈ β„‚)
11175, 79rpdivcld 13071 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) ∈ ℝ+)
112111rpcnd 13056 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) ∈ β„‚)
113110, 112, 59mul32d 11460 . . . . . . . . . . . . 13 (πœ‘ β†’ (((1 βˆ’ (1 / 𝐷)) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) Β· π‘ˆ) = (((1 βˆ’ (1 / 𝐷)) Β· π‘ˆ) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))))
114109, 113eqtrid 2779 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹 Β· π‘ˆ) = (((1 βˆ’ (1 / 𝐷)) Β· π‘ˆ) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))))
115108, 114eqtr4d 2770 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) = (𝐹 Β· π‘ˆ))
116115oveq1d 7439 . . . . . . . . . 10 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) Β· (π‘ˆβ†‘2)) = ((𝐹 Β· π‘ˆ) Β· (π‘ˆβ†‘2)))
11735rpcnd 13056 . . . . . . . . . . 11 (πœ‘ β†’ (π‘ˆ βˆ’ 𝐸) ∈ β„‚)
118117, 112, 77mulassd 11273 . . . . . . . . . 10 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) Β· (π‘ˆβ†‘2)) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2))))
119116, 118eqtr3d 2769 . . . . . . . . 9 (πœ‘ β†’ ((𝐹 Β· π‘ˆ) Β· (π‘ˆβ†‘2)) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2))))
12095, 98, 1193eqtr2d 2773 . . . . . . . 8 (πœ‘ β†’ (𝐹 Β· (π‘ˆβ†‘3)) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2))))
12186, 120eqtr4d 2770 . . . . . . 7 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) = (𝐹 Β· (π‘ˆβ†‘3)))
122121oveq2d 7440 . . . . . 6 (πœ‘ β†’ (π‘ˆ βˆ’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)))) = (π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))))
123122oveq1d 7439 . . . . 5 (πœ‘ β†’ ((π‘ˆ βˆ’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)))) Β· (logβ€˜π‘)) = ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘)))
12462, 123eqtr3d 2769 . . . 4 (πœ‘ β†’ ((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) = ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘)))
12526, 24remulcld 11280 . . . . 5 (πœ‘ β†’ (π‘ˆ Β· (logβ€˜π‘)) ∈ ℝ)
126125, 54resubcld 11678 . . . 4 (πœ‘ β†’ ((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) ∈ ℝ)
127124, 126eqeltrrd 2829 . . 3 (πœ‘ β†’ ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘)) ∈ ℝ)
12817rpred 13054 . . . . . . . 8 (πœ‘ β†’ 𝑍 ∈ ℝ)
12916simp2d 1140 . . . . . . . . 9 (πœ‘ β†’ (1 < 𝑍 ∧ e ≀ (βˆšβ€˜π‘) ∧ (βˆšβ€˜π‘) ≀ (𝑍 / π‘Œ)))
130129simp1d 1139 . . . . . . . 8 (πœ‘ β†’ 1 < 𝑍)
131128, 130rplogcld 26581 . . . . . . 7 (πœ‘ β†’ (logβ€˜π‘) ∈ ℝ+)
13232, 131rerpdivcld 13085 . . . . . 6 (πœ‘ β†’ (2 / (logβ€˜π‘)) ∈ ℝ)
133 fzfid 13976 . . . . . . 7 (πœ‘ β†’ (1...(βŒŠβ€˜(𝑍 / π‘Œ))) ∈ Fin)
13417adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑍 ∈ ℝ+)
135 elfznn 13568 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ))) β†’ 𝑛 ∈ β„•)
136135adantl 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑛 ∈ β„•)
137136nnrpd 13052 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑛 ∈ ℝ+)
138134, 137rpdivcld 13071 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (𝑍 / 𝑛) ∈ ℝ+)
13918ffvelcdmi 7096 . . . . . . . . . . . 12 ((𝑍 / 𝑛) ∈ ℝ+ β†’ (π‘…β€˜(𝑍 / 𝑛)) ∈ ℝ)
140138, 139syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (π‘…β€˜(𝑍 / 𝑛)) ∈ ℝ)
141140, 134rerpdivcld 13085 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((π‘…β€˜(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
142141recnd 11278 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((π‘…β€˜(𝑍 / 𝑛)) / 𝑍) ∈ β„‚)
143142abscld 15421 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
144137relogcld 26575 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (logβ€˜π‘›) ∈ ℝ)
145143, 144remulcld 11280 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) ∈ ℝ)
146133, 145fsumrecl 15718 . . . . . 6 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) ∈ ℝ)
147132, 146remulcld 11280 . . . . 5 (πœ‘ β†’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ∈ ℝ)
148147, 57readdcld 11279 . . . 4 (πœ‘ β†’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) + 𝐢) ∈ ℝ)
14920recnd 11278 . . . . . . . . . . 11 (πœ‘ β†’ (π‘…β€˜π‘) ∈ β„‚)
150149abscld 15421 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜(π‘…β€˜π‘)) ∈ ℝ)
151150recnd 11278 . . . . . . . . 9 (πœ‘ β†’ (absβ€˜(π‘…β€˜π‘)) ∈ β„‚)
152151, 61mulcld 11270 . . . . . . . 8 (πœ‘ β†’ ((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) ∈ β„‚)
153132recnd 11278 . . . . . . . . 9 (πœ‘ β†’ (2 / (logβ€˜π‘)) ∈ β„‚)
154140recnd 11278 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (π‘…β€˜(𝑍 / 𝑛)) ∈ β„‚)
155154abscld 15421 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜(π‘…β€˜(𝑍 / 𝑛))) ∈ ℝ)
156155, 144remulcld 11280 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) ∈ ℝ)
157133, 156fsumrecl 15718 . . . . . . . . . 10 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) ∈ ℝ)
158157recnd 11278 . . . . . . . . 9 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) ∈ β„‚)
159153, 158mulcld 11270 . . . . . . . 8 (πœ‘ β†’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))) ∈ β„‚)
16017rpcnd 13056 . . . . . . . 8 (πœ‘ β†’ 𝑍 ∈ β„‚)
16117rpne0d 13059 . . . . . . . 8 (πœ‘ β†’ 𝑍 β‰  0)
162152, 159, 160, 161divsubdird 12065 . . . . . . 7 (πœ‘ β†’ ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))) / 𝑍) = ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) / 𝑍) βˆ’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))) / 𝑍)))
163151, 61, 160, 161div23d 12063 . . . . . . . . 9 (πœ‘ β†’ (((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) / 𝑍) = (((absβ€˜(π‘…β€˜π‘)) / 𝑍) Β· (logβ€˜π‘)))
164149, 160, 161absdivd 15440 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑍)) = ((absβ€˜(π‘…β€˜π‘)) / (absβ€˜π‘)))
16517rprege0d 13061 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑍 ∈ ℝ ∧ 0 ≀ 𝑍))
166 absid 15281 . . . . . . . . . . . . 13 ((𝑍 ∈ ℝ ∧ 0 ≀ 𝑍) β†’ (absβ€˜π‘) = 𝑍)
167165, 166syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (absβ€˜π‘) = 𝑍)
168167oveq2d 7440 . . . . . . . . . . 11 (πœ‘ β†’ ((absβ€˜(π‘…β€˜π‘)) / (absβ€˜π‘)) = ((absβ€˜(π‘…β€˜π‘)) / 𝑍))
169164, 168eqtrd 2767 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑍)) = ((absβ€˜(π‘…β€˜π‘)) / 𝑍))
170169oveq1d 7439 . . . . . . . . 9 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) = (((absβ€˜(π‘…β€˜π‘)) / 𝑍) Β· (logβ€˜π‘)))
171163, 170eqtr4d 2770 . . . . . . . 8 (πœ‘ β†’ (((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) / 𝑍) = ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)))
172153, 158, 160, 161divassd 12061 . . . . . . . . 9 (πœ‘ β†’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))) / 𝑍) = ((2 / (logβ€˜π‘)) Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍)))
173160adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑍 ∈ β„‚)
174161adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑍 β‰  0)
175154, 173, 174absdivd 15440 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) = ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / (absβ€˜π‘)))
176167adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜π‘) = 𝑍)
177176oveq2d 7440 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / (absβ€˜π‘)) = ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / 𝑍))
178175, 177eqtrd 2767 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) = ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / 𝑍))
179178oveq1d 7439 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) = (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / 𝑍) Β· (logβ€˜π‘›)))
180155recnd 11278 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜(π‘…β€˜(𝑍 / 𝑛))) ∈ β„‚)
181144recnd 11278 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (logβ€˜π‘›) ∈ β„‚)
18217rpcnne0d 13063 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑍 ∈ β„‚ ∧ 𝑍 β‰  0))
183182adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (𝑍 ∈ β„‚ ∧ 𝑍 β‰  0))
184 div23 11927 . . . . . . . . . . . . . 14 (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) ∈ β„‚ ∧ (logβ€˜π‘›) ∈ β„‚ ∧ (𝑍 ∈ β„‚ ∧ 𝑍 β‰  0)) β†’ (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍) = (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / 𝑍) Β· (logβ€˜π‘›)))
185180, 181, 183, 184syl3anc 1368 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍) = (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / 𝑍) Β· (logβ€˜π‘›)))
186179, 185eqtr4d 2770 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) = (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍))
187186sumeq2dv 15687 . . . . . . . . . . 11 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍))
188156recnd 11278 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) ∈ β„‚)
189133, 160, 188, 161fsumdivc 15770 . . . . . . . . . . 11 (πœ‘ β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍))
190187, 189eqtr4d 2770 . . . . . . . . . 10 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) = (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍))
191190oveq2d 7440 . . . . . . . . 9 (πœ‘ β†’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) = ((2 / (logβ€˜π‘)) Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍)))
192172, 191eqtr4d 2770 . . . . . . . 8 (πœ‘ β†’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))) / 𝑍) = ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
193171, 192oveq12d 7442 . . . . . . 7 (πœ‘ β†’ ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) / 𝑍) βˆ’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))) / 𝑍)) = (((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
194162, 193eqtrd 2767 . . . . . 6 (πœ‘ β†’ ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))) / 𝑍) = (((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
195 2fveq3 6905 . . . . . . . . . . 11 (𝑧 = 𝑍 β†’ (absβ€˜(π‘…β€˜π‘§)) = (absβ€˜(π‘…β€˜π‘)))
196 fveq2 6900 . . . . . . . . . . 11 (𝑧 = 𝑍 β†’ (logβ€˜π‘§) = (logβ€˜π‘))
197195, 196oveq12d 7442 . . . . . . . . . 10 (𝑧 = 𝑍 β†’ ((absβ€˜(π‘…β€˜π‘§)) Β· (logβ€˜π‘§)) = ((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)))
198196oveq2d 7440 . . . . . . . . . . 11 (𝑧 = 𝑍 β†’ (2 / (logβ€˜π‘§)) = (2 / (logβ€˜π‘)))
199 oveq2 7432 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 β†’ (𝑧 / 𝑖) = (𝑧 / 𝑛))
200199fveq2d 6904 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 β†’ (π‘…β€˜(𝑧 / 𝑖)) = (π‘…β€˜(𝑧 / 𝑛)))
201200fveq2d 6904 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 β†’ (absβ€˜(π‘…β€˜(𝑧 / 𝑖))) = (absβ€˜(π‘…β€˜(𝑧 / 𝑛))))
202 fveq2 6900 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 β†’ (logβ€˜π‘–) = (logβ€˜π‘›))
203201, 202oveq12d 7442 . . . . . . . . . . . . 13 (𝑖 = 𝑛 β†’ ((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)) = ((absβ€˜(π‘…β€˜(𝑧 / 𝑛))) Β· (logβ€˜π‘›)))
204203cbvsumv 15680 . . . . . . . . . . . 12 Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑛))) Β· (logβ€˜π‘›))
205 fvoveq1 7447 . . . . . . . . . . . . . 14 (𝑧 = 𝑍 β†’ (βŒŠβ€˜(𝑧 / π‘Œ)) = (βŒŠβ€˜(𝑍 / π‘Œ)))
206205oveq2d 7440 . . . . . . . . . . . . 13 (𝑧 = 𝑍 β†’ (1...(βŒŠβ€˜(𝑧 / π‘Œ))) = (1...(βŒŠβ€˜(𝑍 / π‘Œ))))
207 simpl 481 . . . . . . . . . . . . . . . 16 ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑧 = 𝑍)
208207fvoveq1d 7446 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (π‘…β€˜(𝑧 / 𝑛)) = (π‘…β€˜(𝑍 / 𝑛)))
209208fveq2d 6904 . . . . . . . . . . . . . 14 ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜(π‘…β€˜(𝑧 / 𝑛))) = (absβ€˜(π‘…β€˜(𝑍 / 𝑛))))
210209oveq1d 7439 . . . . . . . . . . . . 13 ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜(π‘…β€˜(𝑧 / 𝑛))) Β· (logβ€˜π‘›)) = ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))
211206, 210sumeq12rdv 15691 . . . . . . . . . . . 12 (𝑧 = 𝑍 β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑛))) Β· (logβ€˜π‘›)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))
212204, 211eqtrid 2779 . . . . . . . . . . 11 (𝑧 = 𝑍 β†’ Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))
213198, 212oveq12d 7442 . . . . . . . . . 10 (𝑧 = 𝑍 β†’ ((2 / (logβ€˜π‘§)) Β· Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–))) = ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))))
214197, 213oveq12d 7442 . . . . . . . . 9 (𝑧 = 𝑍 β†’ (((absβ€˜(π‘…β€˜π‘§)) Β· (logβ€˜π‘§)) βˆ’ ((2 / (logβ€˜π‘§)) Β· Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)))) = (((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))))
215 id 22 . . . . . . . . 9 (𝑧 = 𝑍 β†’ 𝑧 = 𝑍)
216214, 215oveq12d 7442 . . . . . . . 8 (𝑧 = 𝑍 β†’ ((((absβ€˜(π‘…β€˜π‘§)) Β· (logβ€˜π‘§)) βˆ’ ((2 / (logβ€˜π‘§)) Β· Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)))) / 𝑧) = ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))) / 𝑍))
217216breq1d 5160 . . . . . . 7 (𝑧 = 𝑍 β†’ (((((absβ€˜(π‘…β€˜π‘§)) Β· (logβ€˜π‘§)) βˆ’ ((2 / (logβ€˜π‘§)) Β· Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)))) / 𝑧) ≀ 𝐢 ↔ ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))) / 𝑍) ≀ 𝐢))
218 pntlem1.C . . . . . . 7 (πœ‘ β†’ βˆ€π‘§ ∈ (1(,)+∞)((((absβ€˜(π‘…β€˜π‘§)) Β· (logβ€˜π‘§)) βˆ’ ((2 / (logβ€˜π‘§)) Β· Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)))) / 𝑧) ≀ 𝐢)
219 1re 11250 . . . . . . . . 9 1 ∈ ℝ
220 rexr 11296 . . . . . . . . 9 (1 ∈ ℝ β†’ 1 ∈ ℝ*)
221 elioopnf 13458 . . . . . . . . 9 (1 ∈ ℝ* β†’ (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 < 𝑍)))
222219, 220, 221mp2b 10 . . . . . . . 8 (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 < 𝑍))
223128, 130, 222sylanbrc 581 . . . . . . 7 (πœ‘ β†’ 𝑍 ∈ (1(,)+∞))
224217, 218, 223rspcdva 3610 . . . . . 6 (πœ‘ β†’ ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))) / 𝑍) ≀ 𝐢)
225194, 224eqbrtrrd 5174 . . . . 5 (πœ‘ β†’ (((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))) ≀ 𝐢)
22625, 147, 57lesubadd2d 11849 . . . . 5 (πœ‘ β†’ ((((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))) ≀ 𝐢 ↔ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) ≀ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) + 𝐢)))
227225, 226mpbid 231 . . . 4 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) ≀ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) + 𝐢))
228 2cnd 12326 . . . . . . 7 (πœ‘ β†’ 2 ∈ β„‚)
229143recnd 11278 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) ∈ β„‚)
230229, 181mulcld 11270 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) ∈ β„‚)
231133, 230fsumcl 15717 . . . . . . 7 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) ∈ β„‚)
232131rpne0d 13059 . . . . . . 7 (πœ‘ β†’ (logβ€˜π‘) β‰  0)
233228, 231, 61, 232div23d 12063 . . . . . 6 (πœ‘ β†’ ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) / (logβ€˜π‘)) = ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
23424resqcld 14127 . . . . . . . . . . . 12 (πœ‘ β†’ ((logβ€˜π‘)↑2) ∈ ℝ)
23552, 234remulcld 11280 . . . . . . . . . . 11 (πœ‘ β†’ (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)) ∈ ℝ)
23636, 235remulcld 11280 . . . . . . . . . 10 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))) ∈ ℝ)
237 remulcl 11229 . . . . . . . . . 10 ((2 ∈ ℝ ∧ ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))) ∈ ℝ) β†’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))) ∈ ℝ)
23831, 236, 237sylancr 585 . . . . . . . . 9 (πœ‘ β†’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))) ∈ ℝ)
23930, 24remulcld 11280 . . . . . . . . 9 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) ∈ ℝ)
240 remulcl 11229 . . . . . . . . . 10 ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) ∈ ℝ) β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ∈ ℝ)
24131, 146, 240sylancr 585 . . . . . . . . 9 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ∈ ℝ)
24226adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ π‘ˆ ∈ ℝ)
243242, 136nndivred 12302 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (π‘ˆ / 𝑛) ∈ ℝ)
244243, 143resubcld 11678 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
245244, 144remulcld 11280 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) ∈ ℝ)
246133, 245fsumrecl 15718 . . . . . . . . . . 11 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) ∈ ℝ)
24732, 246remulcld 11280 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›))) ∈ ℝ)
248239, 241resubcld 11678 . . . . . . . . . 10 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))) ∈ ℝ)
249 pntlem1.m . . . . . . . . . . . 12 𝑀 = ((βŒŠβ€˜((logβ€˜π‘‹) / (logβ€˜πΎ))) + 1)
250 pntlem1.n . . . . . . . . . . . 12 𝑁 = (βŒŠβ€˜(((logβ€˜π‘) / (logβ€˜πΎ)) / 2))
251 pntlem1.U . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘§ ∈ (π‘Œ[,)+∞)(absβ€˜((π‘…β€˜π‘§) / 𝑧)) ≀ π‘ˆ)
252 pntlem1.K . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘¦ ∈ (𝑋(,)+∞)βˆƒπ‘§ ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 Β· 𝐸)) Β· 𝑧) < (𝐾 Β· 𝑦)) ∧ βˆ€π‘’ ∈ (𝑧[,]((1 + (𝐿 Β· 𝐸)) Β· 𝑧))(absβ€˜((π‘…β€˜π‘’) / 𝑒)) ≀ 𝐸))
2531, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 249, 250, 251, 252pntlemf 27556 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)))
254 2pos 12351 . . . . . . . . . . . . 13 0 < 2
255254a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < 2)
256 lemul2 12103 . . . . . . . . . . . 12 ((((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))) ∈ ℝ ∧ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ (((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) ↔ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))) ≀ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)))))
257236, 246, 32, 255, 256syl112anc 1371 . . . . . . . . . . 11 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) ↔ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))) ≀ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)))))
258253, 257mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))) ≀ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›))))
259243recnd 11278 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (π‘ˆ / 𝑛) ∈ β„‚)
260259, 229, 181subdird 11707 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) = (((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
261260sumeq2dv 15687 . . . . . . . . . . . . . 14 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
262243, 144remulcld 11280 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) ∈ ℝ)
263262recnd 11278 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) ∈ β„‚)
264133, 263, 230fsumsub 15772 . . . . . . . . . . . . . 14 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) = (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
265261, 264eqtrd 2767 . . . . . . . . . . . . 13 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) = (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
266265oveq2d 7440 . . . . . . . . . . . 12 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›))) = (2 Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
267133, 262fsumrecl 15718 . . . . . . . . . . . . . 14 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) ∈ ℝ)
268267recnd 11278 . . . . . . . . . . . . 13 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) ∈ β„‚)
269228, 268, 231subdid 11706 . . . . . . . . . . . 12 (πœ‘ β†’ (2 Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))) = ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
270266, 269eqtrd 2767 . . . . . . . . . . 11 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›))) = ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
271 remulcl 11229 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) ∈ ℝ) β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) ∈ ℝ)
27231, 267, 271sylancr 585 . . . . . . . . . . . 12 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) ∈ ℝ)
2731, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 249, 250, 251, 252pntlemk 27557 . . . . . . . . . . . 12 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) ≀ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)))
274272, 239, 241, 273lesub1dd 11866 . . . . . . . . . . 11 (πœ‘ β†’ ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
275270, 274eqbrtrd 5172 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
276238, 247, 248, 258, 275letrd 11407 . . . . . . . . 9 (πœ‘ β†’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
277238, 239, 241, 276lesubd 11854 . . . . . . . 8 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))))))
27830recnd 11278 . . . . . . . . . 10 (πœ‘ β†’ (π‘ˆ Β· ((logβ€˜π‘) + 3)) ∈ β„‚)
27955recnd 11278 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) ∈ β„‚)
280278, 279, 61subdird 11707 . . . . . . . . 9 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) Β· (logβ€˜π‘)) = (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ ((2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) Β· (logβ€˜π‘))))
28154recnd 11278 . . . . . . . . . . . 12 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) ∈ β„‚)
282228, 281, 61mulassd 11273 . . . . . . . . . . 11 (πœ‘ β†’ ((2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) Β· (logβ€˜π‘)) = (2 Β· ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) Β· (logβ€˜π‘))))
28360, 61, 61mulassd 11273 . . . . . . . . . . . . 13 (πœ‘ β†’ ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) Β· (logβ€˜π‘)) = (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· ((logβ€˜π‘) Β· (logβ€˜π‘))))
28461sqvald 14145 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((logβ€˜π‘)↑2) = ((logβ€˜π‘) Β· (logβ€˜π‘)))
285284oveq2d 7440 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· ((logβ€˜π‘)↑2)) = (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· ((logβ€˜π‘) Β· (logβ€˜π‘))))
28651rpcnd 13056 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) ∈ β„‚)
287234recnd 11278 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((logβ€˜π‘)↑2) ∈ β„‚)
288117, 286, 287mulassd 11273 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· ((logβ€˜π‘)↑2)) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))))
289283, 285, 2883eqtr2d 2773 . . . . . . . . . . . 12 (πœ‘ β†’ ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) Β· (logβ€˜π‘)) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))))
290289oveq2d 7440 . . . . . . . . . . 11 (πœ‘ β†’ (2 Β· ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) Β· (logβ€˜π‘))) = (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))))
291282, 290eqtrd 2767 . . . . . . . . . 10 (πœ‘ β†’ ((2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) Β· (logβ€˜π‘)) = (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))))
292291oveq2d 7440 . . . . . . . . 9 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ ((2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) Β· (logβ€˜π‘))) = (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))))))
293280, 292eqtrd 2767 . . . . . . . 8 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) Β· (logβ€˜π‘)) = (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))))))
294277, 293breqtrrd 5178 . . . . . . 7 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) Β· (logβ€˜π‘)))
295241, 56, 131ledivmul2d 13108 . . . . . . 7 (πœ‘ β†’ (((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) / (logβ€˜π‘)) ≀ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) ↔ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) Β· (logβ€˜π‘))))
296294, 295mpbird 256 . . . . . 6 (πœ‘ β†’ ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) / (logβ€˜π‘)) ≀ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))))
297233, 296eqbrtrrd 5174 . . . . 5 (πœ‘ β†’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ≀ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))))
298147, 56, 57, 297leadd1dd 11864 . . . 4 (πœ‘ β†’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) + 𝐢) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) + 𝐢))
29925, 148, 58, 227, 298letrd 11407 . . 3 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) + 𝐢))
300 remulcl 11229 . . . . . . . . 9 ((π‘ˆ ∈ ℝ ∧ 3 ∈ ℝ) β†’ (π‘ˆ Β· 3) ∈ ℝ)
30126, 27, 300sylancl 584 . . . . . . . 8 (πœ‘ β†’ (π‘ˆ Β· 3) ∈ ℝ)
302301, 57readdcld 11279 . . . . . . 7 (πœ‘ β†’ ((π‘ˆ Β· 3) + 𝐢) ∈ ℝ)
30316simp3d 1141 . . . . . . . 8 (πœ‘ β†’ ((4 / (𝐿 Β· 𝐸)) ≀ (βˆšβ€˜π‘) ∧ (((logβ€˜π‘‹) / (logβ€˜πΎ)) + 2) ≀ (((logβ€˜π‘) / (logβ€˜πΎ)) / 4) ∧ ((π‘ˆ Β· 3) + 𝐢) ≀ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
304303simp3d 1141 . . . . . . 7 (πœ‘ β†’ ((π‘ˆ Β· 3) + 𝐢) ≀ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))
305302, 54, 125, 304leadd2dd 11865 . . . . . 6 (πœ‘ β†’ ((π‘ˆ Β· (logβ€˜π‘)) + ((π‘ˆ Β· 3) + 𝐢)) ≀ ((π‘ˆ Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
30628recnd 11278 . . . . . . . . 9 (πœ‘ β†’ 3 ∈ β„‚)
30759, 61, 306adddid 11274 . . . . . . . 8 (πœ‘ β†’ (π‘ˆ Β· ((logβ€˜π‘) + 3)) = ((π‘ˆ Β· (logβ€˜π‘)) + (π‘ˆ Β· 3)))
308307oveq1d 7439 . . . . . . 7 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) = (((π‘ˆ Β· (logβ€˜π‘)) + (π‘ˆ Β· 3)) + 𝐢))
309125recnd 11278 . . . . . . . 8 (πœ‘ β†’ (π‘ˆ Β· (logβ€˜π‘)) ∈ β„‚)
31059, 306mulcld 11270 . . . . . . . 8 (πœ‘ β†’ (π‘ˆ Β· 3) ∈ β„‚)
31113rpcnd 13056 . . . . . . . 8 (πœ‘ β†’ 𝐢 ∈ β„‚)
312309, 310, 311addassd 11272 . . . . . . 7 (πœ‘ β†’ (((π‘ˆ Β· (logβ€˜π‘)) + (π‘ˆ Β· 3)) + 𝐢) = ((π‘ˆ Β· (logβ€˜π‘)) + ((π‘ˆ Β· 3) + 𝐢)))
313308, 312eqtrd 2767 . . . . . 6 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) = ((π‘ˆ Β· (logβ€˜π‘)) + ((π‘ˆ Β· 3) + 𝐢)))
3142812timesd 12491 . . . . . . . 8 (πœ‘ β†’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) = ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
315314oveq2d 7440 . . . . . . 7 (πœ‘ β†’ (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) = (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))))
316309, 281, 281nppcan3d 11634 . . . . . . 7 (πœ‘ β†’ (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) = ((π‘ˆ Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
317315, 316eqtrd 2767 . . . . . 6 (πœ‘ β†’ (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) = ((π‘ˆ Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
318305, 313, 3173brtr4d 5182 . . . . 5 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) ≀ (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))))
31930, 57readdcld 11279 . . . . . 6 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) ∈ ℝ)
320319, 55, 126lesubaddd 11847 . . . . 5 (πœ‘ β†’ ((((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) ≀ ((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) ↔ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) ≀ (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))))
321318, 320mpbird 256 . . . 4 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) ≀ ((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
322278, 311, 279addsubd 11628 . . . 4 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) = (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) + 𝐢))
323321, 322, 1243brtr3d 5181 . . 3 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) + 𝐢) ≀ ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘)))
32425, 58, 127, 299, 323letrd 11407 . 2 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) ≀ ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘)))
325 3z 12631 . . . . . . 7 3 ∈ β„€
326 rpexpcl 14083 . . . . . . 7 ((π‘ˆ ∈ ℝ+ ∧ 3 ∈ β„€) β†’ (π‘ˆβ†‘3) ∈ ℝ+)
3277, 325, 326sylancl 584 . . . . . 6 (πœ‘ β†’ (π‘ˆβ†‘3) ∈ ℝ+)
32896, 327rpmulcld 13070 . . . . 5 (πœ‘ β†’ (𝐹 Β· (π‘ˆβ†‘3)) ∈ ℝ+)
329328rpred 13054 . . . 4 (πœ‘ β†’ (𝐹 Β· (π‘ˆβ†‘3)) ∈ ℝ)
33026, 329resubcld 11678 . . 3 (πœ‘ β†’ (π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) ∈ ℝ)
33123, 330, 131lemul1d 13097 . 2 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) ≀ (π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) ↔ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) ≀ ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘))))
332324, 331mpbird 256 1 (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑍)) ≀ (π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2936  βˆ€wral 3057  βˆƒwrex 3066   class class class wbr 5150   ↦ cmpt 5233  β€˜cfv 6551  (class class class)co 7424  β„‚cc 11142  β„cr 11143  0cc0 11144  1c1 11145   + caddc 11147   Β· cmul 11149  +∞cpnf 11281  β„*cxr 11283   < clt 11284   ≀ cle 11285   βˆ’ cmin 11480   / cdiv 11907  β„•cn 12248  2c2 12303  3c3 12304  4c4 12305  β„•0cn0 12508  β„€cz 12594  cdc 12713  β„+crp 13012  (,)cioo 13362  [,)cico 13364  [,]cicc 13365  ...cfz 13522  βŒŠcfl 13793  β†‘cexp 14064  βˆšcsqrt 15218  abscabs 15219  Ξ£csu 15670  expce 16043  eceu 16044  logclog 26506  Οˆcchp 27043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-inf2 9670  ax-cnex 11200  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-addrcl 11205  ax-mulcl 11206  ax-mulrcl 11207  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-i2m1 11212  ax-1ne0 11213  ax-1rid 11214  ax-rnegex 11215  ax-rrecex 11216  ax-cnre 11217  ax-pre-lttri 11218  ax-pre-lttrn 11219  ax-pre-ltadd 11220  ax-pre-mulgt0 11221  ax-pre-sup 11222  ax-addf 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4911  df-int 4952  df-iun 5000  df-iin 5001  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-se 5636  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-isom 6560  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7689  df-om 7875  df-1st 7997  df-2nd 7998  df-supp 8170  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-1o 8491  df-2o 8492  df-oadd 8495  df-er 8729  df-map 8851  df-pm 8852  df-ixp 8921  df-en 8969  df-dom 8970  df-sdom 8971  df-fin 8972  df-fsupp 9392  df-fi 9440  df-sup 9471  df-inf 9472  df-oi 9539  df-dju 9930  df-card 9968  df-pnf 11286  df-mnf 11287  df-xr 11288  df-ltxr 11289  df-le 11290  df-sub 11482  df-neg 11483  df-div 11908  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316  df-8 12317  df-9 12318  df-n0 12509  df-xnn0 12581  df-z 12595  df-dec 12714  df-uz 12859  df-q 12969  df-rp 13013  df-xneg 13130  df-xadd 13131  df-xmul 13132  df-ioo 13366  df-ioc 13367  df-ico 13368  df-icc 13369  df-fz 13523  df-fzo 13666  df-fl 13795  df-mod 13873  df-seq 14005  df-exp 14065  df-fac 14271  df-bc 14300  df-hash 14328  df-shft 15052  df-cj 15084  df-re 15085  df-im 15086  df-sqrt 15220  df-abs 15221  df-limsup 15453  df-clim 15470  df-rlim 15471  df-sum 15671  df-ef 16049  df-e 16050  df-sin 16051  df-cos 16052  df-tan 16053  df-pi 16054  df-dvds 16237  df-gcd 16475  df-prm 16648  df-pc 16811  df-struct 17121  df-sets 17138  df-slot 17156  df-ndx 17168  df-base 17186  df-ress 17215  df-plusg 17251  df-mulr 17252  df-starv 17253  df-sca 17254  df-vsca 17255  df-ip 17256  df-tset 17257  df-ple 17258  df-ds 17260  df-unif 17261  df-hom 17262  df-cco 17263  df-rest 17409  df-topn 17410  df-0g 17428  df-gsum 17429  df-topgen 17430  df-pt 17431  df-prds 17434  df-xrs 17489  df-qtop 17494  df-imas 17495  df-xps 17497  df-mre 17571  df-mrc 17572  df-acs 17574  df-mgm 18605  df-sgrp 18684  df-mnd 18700  df-submnd 18746  df-mulg 19029  df-cntz 19273  df-cmn 19742  df-psmet 21276  df-xmet 21277  df-met 21278  df-bl 21279  df-mopn 21280  df-fbas 21281  df-fg 21282  df-cnfld 21285  df-top 22814  df-topon 22831  df-topsp 22853  df-bases 22867  df-cld 22941  df-ntr 22942  df-cls 22943  df-nei 23020  df-lp 23058  df-perf 23059  df-cn 23149  df-cnp 23150  df-haus 23237  df-cmp 23309  df-tx 23484  df-hmeo 23677  df-fil 23768  df-fm 23860  df-flim 23861  df-flf 23862  df-xms 24244  df-ms 24245  df-tms 24246  df-cncf 24816  df-limc 25813  df-dv 25814  df-ulm 26331  df-log 26508  df-atan 26817  df-em 26943  df-vma 27048  df-chp 27049
This theorem is referenced by:  pntleme  27559
  Copyright terms: Public domain W3C validator