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

Theorem pntlemo 26978
Description: Lemma for pnt 26985. 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 26968 . . . . . . . . 9 (πœ‘ β†’ (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≀ (βˆšβ€˜π‘) ∧ (βˆšβ€˜π‘) ≀ (𝑍 / π‘Œ)) ∧ ((4 / (𝐿 Β· 𝐸)) ≀ (βˆšβ€˜π‘) ∧ (((logβ€˜π‘‹) / (logβ€˜πΎ)) + 2) ≀ (((logβ€˜π‘) / (logβ€˜πΎ)) / 4) ∧ ((π‘ˆ Β· 3) + 𝐢) ≀ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))))
1716simp1d 1143 . . . . . . . 8 (πœ‘ β†’ 𝑍 ∈ ℝ+)
181pntrf 26934 . . . . . . . . 9 𝑅:ℝ+βŸΆβ„
1918ffvelcdmi 7038 . . . . . . . 8 (𝑍 ∈ ℝ+ β†’ (π‘…β€˜π‘) ∈ ℝ)
2017, 19syl 17 . . . . . . 7 (πœ‘ β†’ (π‘…β€˜π‘) ∈ ℝ)
2120, 17rerpdivcld 12996 . . . . . 6 (πœ‘ β†’ ((π‘…β€˜π‘) / 𝑍) ∈ ℝ)
2221recnd 11191 . . . . 5 (πœ‘ β†’ ((π‘…β€˜π‘) / 𝑍) ∈ β„‚)
2322abscld 15330 . . . 4 (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑍)) ∈ ℝ)
2417relogcld 26001 . . . 4 (πœ‘ β†’ (logβ€˜π‘) ∈ ℝ)
2523, 24remulcld 11193 . . 3 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) ∈ ℝ)
267rpred 12965 . . . . . 6 (πœ‘ β†’ π‘ˆ ∈ ℝ)
27 3re 12241 . . . . . . . 8 3 ∈ ℝ
2827a1i 11 . . . . . . 7 (πœ‘ β†’ 3 ∈ ℝ)
2924, 28readdcld 11192 . . . . . 6 (πœ‘ β†’ ((logβ€˜π‘) + 3) ∈ ℝ)
3026, 29remulcld 11193 . . . . 5 (πœ‘ β†’ (π‘ˆ Β· ((logβ€˜π‘) + 3)) ∈ ℝ)
31 2re 12235 . . . . . . 7 2 ∈ ℝ
3231a1i 11 . . . . . 6 (πœ‘ β†’ 2 ∈ ℝ)
331, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 26966 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (π‘ˆ βˆ’ 𝐸) ∈ ℝ+)))
3433simp3d 1145 . . . . . . . . . 10 (πœ‘ β†’ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (π‘ˆ βˆ’ 𝐸) ∈ ℝ+))
3534simp3d 1145 . . . . . . . . 9 (πœ‘ β†’ (π‘ˆ βˆ’ 𝐸) ∈ ℝ+)
3635rpred 12965 . . . . . . . 8 (πœ‘ β†’ (π‘ˆ βˆ’ 𝐸) ∈ ℝ)
371, 2, 3, 4, 5, 6pntlemd 26965 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+))
3837simp1d 1143 . . . . . . . . . . 11 (πœ‘ β†’ 𝐿 ∈ ℝ+)
3933simp1d 1143 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐸 ∈ ℝ+)
40 2z 12543 . . . . . . . . . . . 12 2 ∈ β„€
41 rpexpcl 13995 . . . . . . . . . . . 12 ((𝐸 ∈ ℝ+ ∧ 2 ∈ β„€) β†’ (𝐸↑2) ∈ ℝ+)
4239, 40, 41sylancl 587 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸↑2) ∈ ℝ+)
4338, 42rpmulcld 12981 . . . . . . . . . 10 (πœ‘ β†’ (𝐿 Β· (𝐸↑2)) ∈ ℝ+)
44 3nn0 12439 . . . . . . . . . . . . 13 3 ∈ β„•0
45 2nn 12234 . . . . . . . . . . . . 13 2 ∈ β„•
4644, 45decnncl 12646 . . . . . . . . . . . 12 32 ∈ β„•
47 nnrp 12934 . . . . . . . . . . . 12 (32 ∈ β„• β†’ 32 ∈ ℝ+)
4846, 47ax-mp 5 . . . . . . . . . . 11 32 ∈ ℝ+
49 rpmulcl 12946 . . . . . . . . . . 11 ((32 ∈ ℝ+ ∧ 𝐡 ∈ ℝ+) β†’ (32 Β· 𝐡) ∈ ℝ+)
5048, 3, 49sylancr 588 . . . . . . . . . 10 (πœ‘ β†’ (32 Β· 𝐡) ∈ ℝ+)
5143, 50rpdivcld 12982 . . . . . . . . 9 (πœ‘ β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) ∈ ℝ+)
5251rpred 12965 . . . . . . . 8 (πœ‘ β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) ∈ ℝ)
5336, 52remulcld 11193 . . . . . . 7 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) ∈ ℝ)
5453, 24remulcld 11193 . . . . . 6 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) ∈ ℝ)
5532, 54remulcld 11193 . . . . 5 (πœ‘ β†’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) ∈ ℝ)
5630, 55resubcld 11591 . . . 4 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) ∈ ℝ)
5713rpred 12965 . . . 4 (πœ‘ β†’ 𝐢 ∈ ℝ)
5856, 57readdcld 11192 . . 3 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) + 𝐢) ∈ ℝ)
597rpcnd 12967 . . . . . 6 (πœ‘ β†’ π‘ˆ ∈ β„‚)
6053recnd 11191 . . . . . 6 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) ∈ β„‚)
6124recnd 11191 . . . . . 6 (πœ‘ β†’ (logβ€˜π‘) ∈ β„‚)
6259, 60, 61subdird 11620 . . . . 5 (πœ‘ β†’ ((π‘ˆ βˆ’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)))) Β· (logβ€˜π‘)) = ((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
6338rpcnd 12967 . . . . . . . . . . 11 (πœ‘ β†’ 𝐿 ∈ β„‚)
6442rpcnd 12967 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸↑2) ∈ β„‚)
6550rpcnne0d 12974 . . . . . . . . . . 11 (πœ‘ β†’ ((32 Β· 𝐡) ∈ β„‚ ∧ (32 Β· 𝐡) β‰  0))
66 div23 11840 . . . . . . . . . . 11 ((𝐿 ∈ β„‚ ∧ (𝐸↑2) ∈ β„‚ ∧ ((32 Β· 𝐡) ∈ β„‚ ∧ (32 Β· 𝐡) β‰  0)) β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) = ((𝐿 / (32 Β· 𝐡)) Β· (𝐸↑2)))
6763, 64, 65, 66syl3anc 1372 . . . . . . . . . 10 (πœ‘ β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) = ((𝐿 / (32 Β· 𝐡)) Β· (𝐸↑2)))
689oveq1i 7371 . . . . . . . . . . . 12 (𝐸↑2) = ((π‘ˆ / 𝐷)↑2)
6937simp2d 1144 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 ∈ ℝ+)
7069rpcnd 12967 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 ∈ β„‚)
7169rpne0d 12970 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 β‰  0)
7259, 70, 71sqdivd 14073 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘ˆ / 𝐷)↑2) = ((π‘ˆβ†‘2) / (𝐷↑2)))
7368, 72eqtrid 2785 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸↑2) = ((π‘ˆβ†‘2) / (𝐷↑2)))
7473oveq2d 7377 . . . . . . . . . 10 (πœ‘ β†’ ((𝐿 / (32 Β· 𝐡)) Β· (𝐸↑2)) = ((𝐿 / (32 Β· 𝐡)) Β· ((π‘ˆβ†‘2) / (𝐷↑2))))
7538, 50rpdivcld 12982 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐿 / (32 Β· 𝐡)) ∈ ℝ+)
7675rpcnd 12967 . . . . . . . . . . 11 (πœ‘ β†’ (𝐿 / (32 Β· 𝐡)) ∈ β„‚)
7759sqcld 14058 . . . . . . . . . . 11 (πœ‘ β†’ (π‘ˆβ†‘2) ∈ β„‚)
78 rpexpcl 13995 . . . . . . . . . . . . 13 ((𝐷 ∈ ℝ+ ∧ 2 ∈ β„€) β†’ (𝐷↑2) ∈ ℝ+)
7969, 40, 78sylancl 587 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐷↑2) ∈ ℝ+)
8079rpcnne0d 12974 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐷↑2) ∈ β„‚ ∧ (𝐷↑2) β‰  0))
81 divass 11839 . . . . . . . . . . . 12 (((𝐿 / (32 Β· 𝐡)) ∈ β„‚ ∧ (π‘ˆβ†‘2) ∈ β„‚ ∧ ((𝐷↑2) ∈ β„‚ ∧ (𝐷↑2) β‰  0)) β†’ (((𝐿 / (32 Β· 𝐡)) Β· (π‘ˆβ†‘2)) / (𝐷↑2)) = ((𝐿 / (32 Β· 𝐡)) Β· ((π‘ˆβ†‘2) / (𝐷↑2))))
82 div23 11840 . . . . . . . . . . . 12 (((𝐿 / (32 Β· 𝐡)) ∈ β„‚ ∧ (π‘ˆβ†‘2) ∈ β„‚ ∧ ((𝐷↑2) ∈ β„‚ ∧ (𝐷↑2) β‰  0)) β†’ (((𝐿 / (32 Β· 𝐡)) Β· (π‘ˆβ†‘2)) / (𝐷↑2)) = (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2)))
8381, 82eqtr3d 2775 . . . . . . . . . . 11 (((𝐿 / (32 Β· 𝐡)) ∈ β„‚ ∧ (π‘ˆβ†‘2) ∈ β„‚ ∧ ((𝐷↑2) ∈ β„‚ ∧ (𝐷↑2) β‰  0)) β†’ ((𝐿 / (32 Β· 𝐡)) Β· ((π‘ˆβ†‘2) / (𝐷↑2))) = (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2)))
8476, 77, 80, 83syl3anc 1372 . . . . . . . . . 10 (πœ‘ β†’ ((𝐿 / (32 Β· 𝐡)) Β· ((π‘ˆβ†‘2) / (𝐷↑2))) = (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2)))
8567, 74, 843eqtrd 2777 . . . . . . . . 9 (πœ‘ β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) = (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2)))
8685oveq2d 7377 . . . . . . . 8 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2))))
87 df-3 12225 . . . . . . . . . . . . 13 3 = (2 + 1)
8887oveq2i 7372 . . . . . . . . . . . 12 (π‘ˆβ†‘3) = (π‘ˆβ†‘(2 + 1))
89 2nn0 12438 . . . . . . . . . . . . 13 2 ∈ β„•0
90 expp1 13983 . . . . . . . . . . . . 13 ((π‘ˆ ∈ β„‚ ∧ 2 ∈ β„•0) β†’ (π‘ˆβ†‘(2 + 1)) = ((π‘ˆβ†‘2) Β· π‘ˆ))
9159, 89, 90sylancl 587 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘ˆβ†‘(2 + 1)) = ((π‘ˆβ†‘2) Β· π‘ˆ))
9288, 91eqtrid 2785 . . . . . . . . . . 11 (πœ‘ β†’ (π‘ˆβ†‘3) = ((π‘ˆβ†‘2) Β· π‘ˆ))
9377, 59mulcomd 11184 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘ˆβ†‘2) Β· π‘ˆ) = (π‘ˆ Β· (π‘ˆβ†‘2)))
9492, 93eqtrd 2773 . . . . . . . . . 10 (πœ‘ β†’ (π‘ˆβ†‘3) = (π‘ˆ Β· (π‘ˆβ†‘2)))
9594oveq2d 7377 . . . . . . . . 9 (πœ‘ β†’ (𝐹 Β· (π‘ˆβ†‘3)) = (𝐹 Β· (π‘ˆ Β· (π‘ˆβ†‘2))))
9637simp3d 1145 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 ∈ ℝ+)
9796rpcnd 12967 . . . . . . . . . 10 (πœ‘ β†’ 𝐹 ∈ β„‚)
9897, 59, 77mulassd 11186 . . . . . . . . 9 (πœ‘ β†’ ((𝐹 Β· π‘ˆ) Β· (π‘ˆβ†‘2)) = (𝐹 Β· (π‘ˆ Β· (π‘ˆβ†‘2))))
99 1cnd 11158 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 1 ∈ β„‚)
10069rpreccld 12975 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (1 / 𝐷) ∈ ℝ+)
101100rpcnd 12967 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1 / 𝐷) ∈ β„‚)
10299, 101, 59subdird 11620 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1 βˆ’ (1 / 𝐷)) Β· π‘ˆ) = ((1 Β· π‘ˆ) βˆ’ ((1 / 𝐷) Β· π‘ˆ)))
10359mulid2d 11181 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1 Β· π‘ˆ) = π‘ˆ)
10459, 70, 71divrec2d 11943 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π‘ˆ / 𝐷) = ((1 / 𝐷) Β· π‘ˆ))
1059, 104eqtr2id 2786 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((1 / 𝐷) Β· π‘ˆ) = 𝐸)
106103, 105oveq12d 7379 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1 Β· π‘ˆ) βˆ’ ((1 / 𝐷) Β· π‘ˆ)) = (π‘ˆ βˆ’ 𝐸))
107102, 106eqtr2d 2774 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘ˆ βˆ’ 𝐸) = ((1 βˆ’ (1 / 𝐷)) Β· π‘ˆ))
108107oveq1d 7376 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) = (((1 βˆ’ (1 / 𝐷)) Β· π‘ˆ) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))))
1096oveq1i 7371 . . . . . . . . . . . . 13 (𝐹 Β· π‘ˆ) = (((1 βˆ’ (1 / 𝐷)) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) Β· π‘ˆ)
11099, 101subcld 11520 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 βˆ’ (1 / 𝐷)) ∈ β„‚)
11175, 79rpdivcld 12982 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) ∈ ℝ+)
112111rpcnd 12967 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) ∈ β„‚)
113110, 112, 59mul32d 11373 . . . . . . . . . . . . 13 (πœ‘ β†’ (((1 βˆ’ (1 / 𝐷)) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) Β· π‘ˆ) = (((1 βˆ’ (1 / 𝐷)) Β· π‘ˆ) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))))
114109, 113eqtrid 2785 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹 Β· π‘ˆ) = (((1 βˆ’ (1 / 𝐷)) Β· π‘ˆ) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))))
115108, 114eqtr4d 2776 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) = (𝐹 Β· π‘ˆ))
116115oveq1d 7376 . . . . . . . . . 10 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) Β· (π‘ˆβ†‘2)) = ((𝐹 Β· π‘ˆ) Β· (π‘ˆβ†‘2)))
11735rpcnd 12967 . . . . . . . . . . 11 (πœ‘ β†’ (π‘ˆ βˆ’ 𝐸) ∈ β„‚)
118117, 112, 77mulassd 11186 . . . . . . . . . 10 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 / (32 Β· 𝐡)) / (𝐷↑2))) Β· (π‘ˆβ†‘2)) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2))))
119116, 118eqtr3d 2775 . . . . . . . . 9 (πœ‘ β†’ ((𝐹 Β· π‘ˆ) Β· (π‘ˆβ†‘2)) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2))))
12095, 98, 1193eqtr2d 2779 . . . . . . . 8 (πœ‘ β†’ (𝐹 Β· (π‘ˆβ†‘3)) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 / (32 Β· 𝐡)) / (𝐷↑2)) Β· (π‘ˆβ†‘2))))
12186, 120eqtr4d 2776 . . . . . . 7 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) = (𝐹 Β· (π‘ˆβ†‘3)))
122121oveq2d 7377 . . . . . 6 (πœ‘ β†’ (π‘ˆ βˆ’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)))) = (π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))))
123122oveq1d 7376 . . . . 5 (πœ‘ β†’ ((π‘ˆ βˆ’ ((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)))) Β· (logβ€˜π‘)) = ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘)))
12462, 123eqtr3d 2775 . . . 4 (πœ‘ β†’ ((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) = ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘)))
12526, 24remulcld 11193 . . . . 5 (πœ‘ β†’ (π‘ˆ Β· (logβ€˜π‘)) ∈ ℝ)
126125, 54resubcld 11591 . . . 4 (πœ‘ β†’ ((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) ∈ ℝ)
127124, 126eqeltrrd 2835 . . 3 (πœ‘ β†’ ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘)) ∈ ℝ)
12817rpred 12965 . . . . . . . 8 (πœ‘ β†’ 𝑍 ∈ ℝ)
12916simp2d 1144 . . . . . . . . 9 (πœ‘ β†’ (1 < 𝑍 ∧ e ≀ (βˆšβ€˜π‘) ∧ (βˆšβ€˜π‘) ≀ (𝑍 / π‘Œ)))
130129simp1d 1143 . . . . . . . 8 (πœ‘ β†’ 1 < 𝑍)
131128, 130rplogcld 26007 . . . . . . 7 (πœ‘ β†’ (logβ€˜π‘) ∈ ℝ+)
13232, 131rerpdivcld 12996 . . . . . 6 (πœ‘ β†’ (2 / (logβ€˜π‘)) ∈ ℝ)
133 fzfid 13887 . . . . . . 7 (πœ‘ β†’ (1...(βŒŠβ€˜(𝑍 / π‘Œ))) ∈ Fin)
13417adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑍 ∈ ℝ+)
135 elfznn 13479 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ))) β†’ 𝑛 ∈ β„•)
136135adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑛 ∈ β„•)
137136nnrpd 12963 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑛 ∈ ℝ+)
138134, 137rpdivcld 12982 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (𝑍 / 𝑛) ∈ ℝ+)
13918ffvelcdmi 7038 . . . . . . . . . . . 12 ((𝑍 / 𝑛) ∈ ℝ+ β†’ (π‘…β€˜(𝑍 / 𝑛)) ∈ ℝ)
140138, 139syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (π‘…β€˜(𝑍 / 𝑛)) ∈ ℝ)
141140, 134rerpdivcld 12996 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((π‘…β€˜(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
142141recnd 11191 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((π‘…β€˜(𝑍 / 𝑛)) / 𝑍) ∈ β„‚)
143142abscld 15330 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
144137relogcld 26001 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (logβ€˜π‘›) ∈ ℝ)
145143, 144remulcld 11193 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) ∈ ℝ)
146133, 145fsumrecl 15627 . . . . . 6 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) ∈ ℝ)
147132, 146remulcld 11193 . . . . 5 (πœ‘ β†’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ∈ ℝ)
148147, 57readdcld 11192 . . . 4 (πœ‘ β†’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) + 𝐢) ∈ ℝ)
14920recnd 11191 . . . . . . . . . . 11 (πœ‘ β†’ (π‘…β€˜π‘) ∈ β„‚)
150149abscld 15330 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜(π‘…β€˜π‘)) ∈ ℝ)
151150recnd 11191 . . . . . . . . 9 (πœ‘ β†’ (absβ€˜(π‘…β€˜π‘)) ∈ β„‚)
152151, 61mulcld 11183 . . . . . . . 8 (πœ‘ β†’ ((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) ∈ β„‚)
153132recnd 11191 . . . . . . . . 9 (πœ‘ β†’ (2 / (logβ€˜π‘)) ∈ β„‚)
154140recnd 11191 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (π‘…β€˜(𝑍 / 𝑛)) ∈ β„‚)
155154abscld 15330 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜(π‘…β€˜(𝑍 / 𝑛))) ∈ ℝ)
156155, 144remulcld 11193 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) ∈ ℝ)
157133, 156fsumrecl 15627 . . . . . . . . . 10 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) ∈ ℝ)
158157recnd 11191 . . . . . . . . 9 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) ∈ β„‚)
159153, 158mulcld 11183 . . . . . . . 8 (πœ‘ β†’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))) ∈ β„‚)
16017rpcnd 12967 . . . . . . . 8 (πœ‘ β†’ 𝑍 ∈ β„‚)
16117rpne0d 12970 . . . . . . . 8 (πœ‘ β†’ 𝑍 β‰  0)
162152, 159, 160, 161divsubdird 11978 . . . . . . 7 (πœ‘ β†’ ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))) / 𝑍) = ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) / 𝑍) βˆ’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))) / 𝑍)))
163151, 61, 160, 161div23d 11976 . . . . . . . . 9 (πœ‘ β†’ (((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) / 𝑍) = (((absβ€˜(π‘…β€˜π‘)) / 𝑍) Β· (logβ€˜π‘)))
164149, 160, 161absdivd 15349 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑍)) = ((absβ€˜(π‘…β€˜π‘)) / (absβ€˜π‘)))
16517rprege0d 12972 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑍 ∈ ℝ ∧ 0 ≀ 𝑍))
166 absid 15190 . . . . . . . . . . . . 13 ((𝑍 ∈ ℝ ∧ 0 ≀ 𝑍) β†’ (absβ€˜π‘) = 𝑍)
167165, 166syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (absβ€˜π‘) = 𝑍)
168167oveq2d 7377 . . . . . . . . . . 11 (πœ‘ β†’ ((absβ€˜(π‘…β€˜π‘)) / (absβ€˜π‘)) = ((absβ€˜(π‘…β€˜π‘)) / 𝑍))
169164, 168eqtrd 2773 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑍)) = ((absβ€˜(π‘…β€˜π‘)) / 𝑍))
170169oveq1d 7376 . . . . . . . . 9 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) = (((absβ€˜(π‘…β€˜π‘)) / 𝑍) Β· (logβ€˜π‘)))
171163, 170eqtr4d 2776 . . . . . . . 8 (πœ‘ β†’ (((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) / 𝑍) = ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)))
172153, 158, 160, 161divassd 11974 . . . . . . . . 9 (πœ‘ β†’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))) / 𝑍) = ((2 / (logβ€˜π‘)) Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍)))
173160adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑍 ∈ β„‚)
174161adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑍 β‰  0)
175154, 173, 174absdivd 15349 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) = ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / (absβ€˜π‘)))
176167adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜π‘) = 𝑍)
177176oveq2d 7377 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / (absβ€˜π‘)) = ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / 𝑍))
178175, 177eqtrd 2773 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) = ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / 𝑍))
179178oveq1d 7376 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) = (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / 𝑍) Β· (logβ€˜π‘›)))
180155recnd 11191 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜(π‘…β€˜(𝑍 / 𝑛))) ∈ β„‚)
181144recnd 11191 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (logβ€˜π‘›) ∈ β„‚)
18217rpcnne0d 12974 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑍 ∈ β„‚ ∧ 𝑍 β‰  0))
183182adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (𝑍 ∈ β„‚ ∧ 𝑍 β‰  0))
184 div23 11840 . . . . . . . . . . . . . 14 (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) ∈ β„‚ ∧ (logβ€˜π‘›) ∈ β„‚ ∧ (𝑍 ∈ β„‚ ∧ 𝑍 β‰  0)) β†’ (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍) = (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / 𝑍) Β· (logβ€˜π‘›)))
185180, 181, 183, 184syl3anc 1372 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍) = (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) / 𝑍) Β· (logβ€˜π‘›)))
186179, 185eqtr4d 2776 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) = (((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍))
187186sumeq2dv 15596 . . . . . . . . . . 11 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍))
188156recnd 11191 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) ∈ β„‚)
189133, 160, 188, 161fsumdivc 15679 . . . . . . . . . . 11 (πœ‘ β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍))
190187, 189eqtr4d 2776 . . . . . . . . . 10 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) = (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍))
191190oveq2d 7377 . . . . . . . . 9 (πœ‘ β†’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) = ((2 / (logβ€˜π‘)) Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)) / 𝑍)))
192172, 191eqtr4d 2776 . . . . . . . 8 (πœ‘ β†’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))) / 𝑍) = ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
193171, 192oveq12d 7379 . . . . . . 7 (πœ‘ β†’ ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) / 𝑍) βˆ’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))) / 𝑍)) = (((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
194162, 193eqtrd 2773 . . . . . 6 (πœ‘ β†’ ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))) / 𝑍) = (((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
195 2fveq3 6851 . . . . . . . . . . 11 (𝑧 = 𝑍 β†’ (absβ€˜(π‘…β€˜π‘§)) = (absβ€˜(π‘…β€˜π‘)))
196 fveq2 6846 . . . . . . . . . . 11 (𝑧 = 𝑍 β†’ (logβ€˜π‘§) = (logβ€˜π‘))
197195, 196oveq12d 7379 . . . . . . . . . 10 (𝑧 = 𝑍 β†’ ((absβ€˜(π‘…β€˜π‘§)) Β· (logβ€˜π‘§)) = ((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)))
198196oveq2d 7377 . . . . . . . . . . 11 (𝑧 = 𝑍 β†’ (2 / (logβ€˜π‘§)) = (2 / (logβ€˜π‘)))
199 oveq2 7369 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 β†’ (𝑧 / 𝑖) = (𝑧 / 𝑛))
200199fveq2d 6850 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 β†’ (π‘…β€˜(𝑧 / 𝑖)) = (π‘…β€˜(𝑧 / 𝑛)))
201200fveq2d 6850 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 β†’ (absβ€˜(π‘…β€˜(𝑧 / 𝑖))) = (absβ€˜(π‘…β€˜(𝑧 / 𝑛))))
202 fveq2 6846 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 β†’ (logβ€˜π‘–) = (logβ€˜π‘›))
203201, 202oveq12d 7379 . . . . . . . . . . . . 13 (𝑖 = 𝑛 β†’ ((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)) = ((absβ€˜(π‘…β€˜(𝑧 / 𝑛))) Β· (logβ€˜π‘›)))
204203cbvsumv 15589 . . . . . . . . . . . 12 Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑛))) Β· (logβ€˜π‘›))
205 fvoveq1 7384 . . . . . . . . . . . . . 14 (𝑧 = 𝑍 β†’ (βŒŠβ€˜(𝑧 / π‘Œ)) = (βŒŠβ€˜(𝑍 / π‘Œ)))
206205oveq2d 7377 . . . . . . . . . . . . 13 (𝑧 = 𝑍 β†’ (1...(βŒŠβ€˜(𝑧 / π‘Œ))) = (1...(βŒŠβ€˜(𝑍 / π‘Œ))))
207 simpl 484 . . . . . . . . . . . . . . . 16 ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ 𝑧 = 𝑍)
208207fvoveq1d 7383 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (π‘…β€˜(𝑧 / 𝑛)) = (π‘…β€˜(𝑍 / 𝑛)))
209208fveq2d 6850 . . . . . . . . . . . . . 14 ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜(π‘…β€˜(𝑧 / 𝑛))) = (absβ€˜(π‘…β€˜(𝑍 / 𝑛))))
210209oveq1d 7376 . . . . . . . . . . . . 13 ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜(π‘…β€˜(𝑧 / 𝑛))) Β· (logβ€˜π‘›)) = ((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))
211206, 210sumeq12rdv 15600 . . . . . . . . . . . 12 (𝑧 = 𝑍 β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑛))) Β· (logβ€˜π‘›)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))
212204, 211eqtrid 2785 . . . . . . . . . . 11 (𝑧 = 𝑍 β†’ Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))
213198, 212oveq12d 7379 . . . . . . . . . 10 (𝑧 = 𝑍 β†’ ((2 / (logβ€˜π‘§)) Β· Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–))) = ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›))))
214197, 213oveq12d 7379 . . . . . . . . 9 (𝑧 = 𝑍 β†’ (((absβ€˜(π‘…β€˜π‘§)) Β· (logβ€˜π‘§)) βˆ’ ((2 / (logβ€˜π‘§)) Β· Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)))) = (((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))))
215 id 22 . . . . . . . . 9 (𝑧 = 𝑍 β†’ 𝑧 = 𝑍)
216214, 215oveq12d 7379 . . . . . . . 8 (𝑧 = 𝑍 β†’ ((((absβ€˜(π‘…β€˜π‘§)) Β· (logβ€˜π‘§)) βˆ’ ((2 / (logβ€˜π‘§)) Β· Σ𝑖 ∈ (1...(βŒŠβ€˜(𝑧 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑧 / 𝑖))) Β· (logβ€˜π‘–)))) / 𝑧) = ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))) / 𝑍))
217216breq1d 5119 . . . . . . 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 11163 . . . . . . . . 9 1 ∈ ℝ
220 rexr 11209 . . . . . . . . 9 (1 ∈ ℝ β†’ 1 ∈ ℝ*)
221 elioopnf 13369 . . . . . . . . 9 (1 ∈ ℝ* β†’ (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 < 𝑍)))
222219, 220, 221mp2b 10 . . . . . . . 8 (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 < 𝑍))
223128, 130, 222sylanbrc 584 . . . . . . 7 (πœ‘ β†’ 𝑍 ∈ (1(,)+∞))
224217, 218, 223rspcdva 3584 . . . . . 6 (πœ‘ β†’ ((((absβ€˜(π‘…β€˜π‘)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜(π‘…β€˜(𝑍 / 𝑛))) Β· (logβ€˜π‘›)))) / 𝑍) ≀ 𝐢)
225194, 224eqbrtrrd 5133 . . . . 5 (πœ‘ β†’ (((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) βˆ’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))) ≀ 𝐢)
22625, 147, 57lesubadd2d 11762 . . . . 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 12239 . . . . . . 7 (πœ‘ β†’ 2 ∈ β„‚)
229143recnd 11191 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) ∈ β„‚)
230229, 181mulcld 11183 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) ∈ β„‚)
231133, 230fsumcl 15626 . . . . . . 7 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) ∈ β„‚)
232131rpne0d 12970 . . . . . . 7 (πœ‘ β†’ (logβ€˜π‘) β‰  0)
233228, 231, 61, 232div23d 11976 . . . . . 6 (πœ‘ β†’ ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) / (logβ€˜π‘)) = ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
23424resqcld 14039 . . . . . . . . . . . 12 (πœ‘ β†’ ((logβ€˜π‘)↑2) ∈ ℝ)
23552, 234remulcld 11193 . . . . . . . . . . 11 (πœ‘ β†’ (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)) ∈ ℝ)
23636, 235remulcld 11193 . . . . . . . . . 10 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))) ∈ ℝ)
237 remulcl 11144 . . . . . . . . . 10 ((2 ∈ ℝ ∧ ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))) ∈ ℝ) β†’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))) ∈ ℝ)
23831, 236, 237sylancr 588 . . . . . . . . 9 (πœ‘ β†’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))) ∈ ℝ)
23930, 24remulcld 11193 . . . . . . . . 9 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) ∈ ℝ)
240 remulcl 11144 . . . . . . . . . 10 ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)) ∈ ℝ) β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ∈ ℝ)
24131, 146, 240sylancr 588 . . . . . . . . 9 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ∈ ℝ)
24226adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ π‘ˆ ∈ ℝ)
243242, 136nndivred 12215 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (π‘ˆ / 𝑛) ∈ ℝ)
244243, 143resubcld 11591 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
245244, 144remulcld 11193 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) ∈ ℝ)
246133, 245fsumrecl 15627 . . . . . . . . . . 11 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) ∈ ℝ)
24732, 246remulcld 11193 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›))) ∈ ℝ)
248239, 241resubcld 11591 . . . . . . . . . 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 26976 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)))
254 2pos 12264 . . . . . . . . . . . . 13 0 < 2
255254a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < 2)
256 lemul2 12016 . . . . . . . . . . . 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 1375 . . . . . . . . . . 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 11191 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (π‘ˆ / 𝑛) ∈ β„‚)
260259, 229, 181subdird 11620 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ (((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) = (((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
261260sumeq2dv 15596 . . . . . . . . . . . . . 14 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
262243, 144remulcld 11193 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) ∈ ℝ)
263262recnd 11191 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))) β†’ ((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) ∈ β„‚)
264133, 263, 230fsumsub 15681 . . . . . . . . . . . . . 14 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ ((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) = (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
265261, 264eqtrd 2773 . . . . . . . . . . . . 13 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›)) = (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))))
266265oveq2d 7377 . . . . . . . . . . . 12 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›))) = (2 Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
267133, 262fsumrecl 15627 . . . . . . . . . . . . . 14 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) ∈ ℝ)
268267recnd 11191 . . . . . . . . . . . . 13 (πœ‘ β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) ∈ β„‚)
269228, 268, 231subdid 11619 . . . . . . . . . . . 12 (πœ‘ β†’ (2 Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))) = ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
270266, 269eqtrd 2773 . . . . . . . . . . 11 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›))) = ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
271 remulcl 11144 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›)) ∈ ℝ) β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) ∈ ℝ)
27231, 267, 271sylancr 588 . . . . . . . . . . . 12 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) ∈ ℝ)
2731, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 249, 250, 251, 252pntlemk 26977 . . . . . . . . . . . 12 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) ≀ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)))
274272, 239, 241, 273lesub1dd 11779 . . . . . . . . . . 11 (πœ‘ β†’ ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((π‘ˆ / 𝑛) Β· (logβ€˜π‘›))) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
275270, 274eqbrtrd 5131 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))(((π‘ˆ / 𝑛) βˆ’ (absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍))) Β· (logβ€˜π‘›))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
276238, 247, 248, 258, 275letrd 11320 . . . . . . . . 9 (πœ‘ β†’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›)))))
277238, 239, 241, 276lesubd 11767 . . . . . . . 8 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))))))
27830recnd 11191 . . . . . . . . . 10 (πœ‘ β†’ (π‘ˆ Β· ((logβ€˜π‘) + 3)) ∈ β„‚)
27955recnd 11191 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) ∈ β„‚)
280278, 279, 61subdird 11620 . . . . . . . . 9 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) Β· (logβ€˜π‘)) = (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ ((2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) Β· (logβ€˜π‘))))
28154recnd 11191 . . . . . . . . . . . 12 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) ∈ β„‚)
282228, 281, 61mulassd 11186 . . . . . . . . . . 11 (πœ‘ β†’ ((2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) Β· (logβ€˜π‘)) = (2 Β· ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) Β· (logβ€˜π‘))))
28360, 61, 61mulassd 11186 . . . . . . . . . . . . 13 (πœ‘ β†’ ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) Β· (logβ€˜π‘)) = (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· ((logβ€˜π‘) Β· (logβ€˜π‘))))
28461sqvald 14057 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((logβ€˜π‘)↑2) = ((logβ€˜π‘) Β· (logβ€˜π‘)))
285284oveq2d 7377 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· ((logβ€˜π‘)↑2)) = (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· ((logβ€˜π‘) Β· (logβ€˜π‘))))
28651rpcnd 12967 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) ∈ β„‚)
287234recnd 11191 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((logβ€˜π‘)↑2) ∈ β„‚)
288117, 286, 287mulassd 11186 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· ((logβ€˜π‘)↑2)) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))))
289283, 285, 2883eqtr2d 2779 . . . . . . . . . . . 12 (πœ‘ β†’ ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) Β· (logβ€˜π‘)) = ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))))
290289oveq2d 7377 . . . . . . . . . . 11 (πœ‘ β†’ (2 Β· ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) Β· (logβ€˜π‘))) = (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))))
291282, 290eqtrd 2773 . . . . . . . . . 10 (πœ‘ β†’ ((2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) Β· (logβ€˜π‘)) = (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2)))))
292291oveq2d 7377 . . . . . . . . 9 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ ((2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) Β· (logβ€˜π‘))) = (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))))))
293280, 292eqtrd 2773 . . . . . . . 8 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) Β· (logβ€˜π‘)) = (((π‘ˆ Β· ((logβ€˜π‘) + 3)) Β· (logβ€˜π‘)) βˆ’ (2 Β· ((π‘ˆ βˆ’ 𝐸) Β· (((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡)) Β· ((logβ€˜π‘)↑2))))))
294277, 293breqtrrd 5137 . . . . . . 7 (πœ‘ β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) Β· (logβ€˜π‘)))
295241, 56, 131ledivmul2d 13019 . . . . . . 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 257 . . . . . 6 (πœ‘ β†’ ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) / (logβ€˜π‘)) ≀ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))))
297233, 296eqbrtrrd 5133 . . . . 5 (πœ‘ β†’ ((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) ≀ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))))
298147, 56, 57, 297leadd1dd 11777 . . . 4 (πœ‘ β†’ (((2 / (logβ€˜π‘)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜(𝑍 / π‘Œ)))((absβ€˜((π‘…β€˜(𝑍 / 𝑛)) / 𝑍)) Β· (logβ€˜π‘›))) + 𝐢) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) + 𝐢))
29925, 148, 58, 227, 298letrd 11320 . . 3 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) ≀ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) + 𝐢))
300 remulcl 11144 . . . . . . . . 9 ((π‘ˆ ∈ ℝ ∧ 3 ∈ ℝ) β†’ (π‘ˆ Β· 3) ∈ ℝ)
30126, 27, 300sylancl 587 . . . . . . . 8 (πœ‘ β†’ (π‘ˆ Β· 3) ∈ ℝ)
302301, 57readdcld 11192 . . . . . . 7 (πœ‘ β†’ ((π‘ˆ Β· 3) + 𝐢) ∈ ℝ)
30316simp3d 1145 . . . . . . . 8 (πœ‘ β†’ ((4 / (𝐿 Β· 𝐸)) ≀ (βˆšβ€˜π‘) ∧ (((logβ€˜π‘‹) / (logβ€˜πΎ)) + 2) ≀ (((logβ€˜π‘) / (logβ€˜πΎ)) / 4) ∧ ((π‘ˆ Β· 3) + 𝐢) ≀ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
304303simp3d 1145 . . . . . . 7 (πœ‘ β†’ ((π‘ˆ Β· 3) + 𝐢) ≀ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))
305302, 54, 125, 304leadd2dd 11778 . . . . . 6 (πœ‘ β†’ ((π‘ˆ Β· (logβ€˜π‘)) + ((π‘ˆ Β· 3) + 𝐢)) ≀ ((π‘ˆ Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
30628recnd 11191 . . . . . . . . 9 (πœ‘ β†’ 3 ∈ β„‚)
30759, 61, 306adddid 11187 . . . . . . . 8 (πœ‘ β†’ (π‘ˆ Β· ((logβ€˜π‘) + 3)) = ((π‘ˆ Β· (logβ€˜π‘)) + (π‘ˆ Β· 3)))
308307oveq1d 7376 . . . . . . 7 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) = (((π‘ˆ Β· (logβ€˜π‘)) + (π‘ˆ Β· 3)) + 𝐢))
309125recnd 11191 . . . . . . . 8 (πœ‘ β†’ (π‘ˆ Β· (logβ€˜π‘)) ∈ β„‚)
31059, 306mulcld 11183 . . . . . . . 8 (πœ‘ β†’ (π‘ˆ Β· 3) ∈ β„‚)
31113rpcnd 12967 . . . . . . . 8 (πœ‘ β†’ 𝐢 ∈ β„‚)
312309, 310, 311addassd 11185 . . . . . . 7 (πœ‘ β†’ (((π‘ˆ Β· (logβ€˜π‘)) + (π‘ˆ Β· 3)) + 𝐢) = ((π‘ˆ Β· (logβ€˜π‘)) + ((π‘ˆ Β· 3) + 𝐢)))
313308, 312eqtrd 2773 . . . . . 6 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) = ((π‘ˆ Β· (logβ€˜π‘)) + ((π‘ˆ Β· 3) + 𝐢)))
3142812timesd 12404 . . . . . . . 8 (πœ‘ β†’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) = ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
315314oveq2d 7377 . . . . . . 7 (πœ‘ β†’ (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) = (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))))
316309, 281, 281nppcan3d 11547 . . . . . . 7 (πœ‘ β†’ (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + ((((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) = ((π‘ˆ Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
317315, 316eqtrd 2773 . . . . . 6 (πœ‘ β†’ (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) = ((π‘ˆ Β· (logβ€˜π‘)) + (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
318305, 313, 3173brtr4d 5141 . . . . 5 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) ≀ (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))))
31930, 57readdcld 11192 . . . . . 6 (πœ‘ β†’ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) ∈ ℝ)
320319, 55, 126lesubaddd 11760 . . . . 5 (πœ‘ β†’ ((((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) ≀ ((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) ↔ ((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) ≀ (((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))) + (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))))
321318, 320mpbird 257 . . . 4 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) ≀ ((π‘ˆ Β· (logβ€˜π‘)) βˆ’ (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘))))
322278, 311, 279addsubd 11541 . . . 4 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) + 𝐢) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) = (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) + 𝐢))
323321, 322, 1243brtr3d 5140 . . 3 (πœ‘ β†’ (((π‘ˆ Β· ((logβ€˜π‘) + 3)) βˆ’ (2 Β· (((π‘ˆ βˆ’ 𝐸) Β· ((𝐿 Β· (𝐸↑2)) / (32 Β· 𝐡))) Β· (logβ€˜π‘)))) + 𝐢) ≀ ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘)))
32425, 58, 127, 299, 323letrd 11320 . 2 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) ≀ ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘)))
325 3z 12544 . . . . . . 7 3 ∈ β„€
326 rpexpcl 13995 . . . . . . 7 ((π‘ˆ ∈ ℝ+ ∧ 3 ∈ β„€) β†’ (π‘ˆβ†‘3) ∈ ℝ+)
3277, 325, 326sylancl 587 . . . . . 6 (πœ‘ β†’ (π‘ˆβ†‘3) ∈ ℝ+)
32896, 327rpmulcld 12981 . . . . 5 (πœ‘ β†’ (𝐹 Β· (π‘ˆβ†‘3)) ∈ ℝ+)
329328rpred 12965 . . . 4 (πœ‘ β†’ (𝐹 Β· (π‘ˆβ†‘3)) ∈ ℝ)
33026, 329resubcld 11591 . . 3 (πœ‘ β†’ (π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) ∈ ℝ)
33123, 330, 131lemul1d 13008 . 2 (πœ‘ β†’ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) ≀ (π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) ↔ ((absβ€˜((π‘…β€˜π‘) / 𝑍)) Β· (logβ€˜π‘)) ≀ ((π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))) Β· (logβ€˜π‘))))
332324, 331mpbird 257 1 (πœ‘ β†’ (absβ€˜((π‘…β€˜π‘) / 𝑍)) ≀ (π‘ˆ βˆ’ (𝐹 Β· (π‘ˆβ†‘3))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070   class class class wbr 5109   ↦ cmpt 5192  β€˜cfv 6500  (class class class)co 7361  β„‚cc 11057  β„cr 11058  0cc0 11059  1c1 11060   + caddc 11062   Β· cmul 11064  +∞cpnf 11194  β„*cxr 11196   < clt 11197   ≀ cle 11198   βˆ’ cmin 11393   / cdiv 11820  β„•cn 12161  2c2 12216  3c3 12217  4c4 12218  β„•0cn0 12421  β„€cz 12507  cdc 12626  β„+crp 12923  (,)cioo 13273  [,)cico 13275  [,]cicc 13276  ...cfz 13433  βŒŠcfl 13704  β†‘cexp 13976  βˆšcsqrt 15127  abscabs 15128  Ξ£csu 15579  expce 15952  eceu 15953  logclog 25933  Οˆcchp 26465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137  ax-addf 11138  ax-mulf 11139
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-iin 4961  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7621  df-om 7807  df-1st 7925  df-2nd 7926  df-supp 8097  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-2o 8417  df-oadd 8420  df-er 8654  df-map 8773  df-pm 8774  df-ixp 8842  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-fsupp 9312  df-fi 9355  df-sup 9386  df-inf 9387  df-oi 9454  df-dju 9845  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-4 12226  df-5 12227  df-6 12228  df-7 12229  df-8 12230  df-9 12231  df-n0 12422  df-xnn0 12494  df-z 12508  df-dec 12627  df-uz 12772  df-q 12882  df-rp 12924  df-xneg 13041  df-xadd 13042  df-xmul 13043  df-ioo 13277  df-ioc 13278  df-ico 13279  df-icc 13280  df-fz 13434  df-fzo 13577  df-fl 13706  df-mod 13784  df-seq 13916  df-exp 13977  df-fac 14183  df-bc 14212  df-hash 14240  df-shft 14961  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-limsup 15362  df-clim 15379  df-rlim 15380  df-sum 15580  df-ef 15958  df-e 15959  df-sin 15960  df-cos 15961  df-tan 15962  df-pi 15963  df-dvds 16145  df-gcd 16383  df-prm 16556  df-pc 16717  df-struct 17027  df-sets 17044  df-slot 17062  df-ndx 17074  df-base 17092  df-ress 17121  df-plusg 17154  df-mulr 17155  df-starv 17156  df-sca 17157  df-vsca 17158  df-ip 17159  df-tset 17160  df-ple 17161  df-ds 17163  df-unif 17164  df-hom 17165  df-cco 17166  df-rest 17312  df-topn 17313  df-0g 17331  df-gsum 17332  df-topgen 17333  df-pt 17334  df-prds 17337  df-xrs 17392  df-qtop 17397  df-imas 17398  df-xps 17400  df-mre 17474  df-mrc 17475  df-acs 17477  df-mgm 18505  df-sgrp 18554  df-mnd 18565  df-submnd 18610  df-mulg 18881  df-cntz 19105  df-cmn 19572  df-psmet 20811  df-xmet 20812  df-met 20813  df-bl 20814  df-mopn 20815  df-fbas 20816  df-fg 20817  df-cnfld 20820  df-top 22266  df-topon 22283  df-topsp 22305  df-bases 22319  df-cld 22393  df-ntr 22394  df-cls 22395  df-nei 22472  df-lp 22510  df-perf 22511  df-cn 22601  df-cnp 22602  df-haus 22689  df-cmp 22761  df-tx 22936  df-hmeo 23129  df-fil 23220  df-fm 23312  df-flim 23313  df-flf 23314  df-xms 23696  df-ms 23697  df-tms 23698  df-cncf 24264  df-limc 25253  df-dv 25254  df-ulm 25759  df-log 25935  df-atan 26240  df-em 26365  df-vma 26470  df-chp 26471
This theorem is referenced by:  pntleme  26979
  Copyright terms: Public domain W3C validator