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

Theorem pntlemo 27633
Description: Lemma for pnt 27640. 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 27623 . . . . . . . . 9 (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
1716simp1d 1139 . . . . . . . 8 (𝜑𝑍 ∈ ℝ+)
181pntrf 27589 . . . . . . . . 9 𝑅:ℝ+⟶ℝ
1918ffvelcdmi 7089 . . . . . . . 8 (𝑍 ∈ ℝ+ → (𝑅𝑍) ∈ ℝ)
2017, 19syl 17 . . . . . . 7 (𝜑 → (𝑅𝑍) ∈ ℝ)
2120, 17rerpdivcld 13095 . . . . . 6 (𝜑 → ((𝑅𝑍) / 𝑍) ∈ ℝ)
2221recnd 11283 . . . . 5 (𝜑 → ((𝑅𝑍) / 𝑍) ∈ ℂ)
2322abscld 15436 . . . 4 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) ∈ ℝ)
2417relogcld 26647 . . . 4 (𝜑 → (log‘𝑍) ∈ ℝ)
2523, 24remulcld 11285 . . 3 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ∈ ℝ)
267rpred 13064 . . . . . 6 (𝜑𝑈 ∈ ℝ)
27 3re 12338 . . . . . . . 8 3 ∈ ℝ
2827a1i 11 . . . . . . 7 (𝜑 → 3 ∈ ℝ)
2924, 28readdcld 11284 . . . . . 6 (𝜑 → ((log‘𝑍) + 3) ∈ ℝ)
3026, 29remulcld 11285 . . . . 5 (𝜑 → (𝑈 · ((log‘𝑍) + 3)) ∈ ℝ)
31 2re 12332 . . . . . . 7 2 ∈ ℝ
3231a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℝ)
331, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 27621 . . . . . . . . . . 11 (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))
3433simp3d 1141 . . . . . . . . . 10 (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+))
3534simp3d 1141 . . . . . . . . 9 (𝜑 → (𝑈𝐸) ∈ ℝ+)
3635rpred 13064 . . . . . . . 8 (𝜑 → (𝑈𝐸) ∈ ℝ)
371, 2, 3, 4, 5, 6pntlemd 27620 . . . . . . . . . . . 12 (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))
3837simp1d 1139 . . . . . . . . . . 11 (𝜑𝐿 ∈ ℝ+)
3933simp1d 1139 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℝ+)
40 2z 12640 . . . . . . . . . . . 12 2 ∈ ℤ
41 rpexpcl 14094 . . . . . . . . . . . 12 ((𝐸 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝐸↑2) ∈ ℝ+)
4239, 40, 41sylancl 584 . . . . . . . . . . 11 (𝜑 → (𝐸↑2) ∈ ℝ+)
4338, 42rpmulcld 13080 . . . . . . . . . 10 (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℝ+)
44 3nn0 12536 . . . . . . . . . . . . 13 3 ∈ ℕ0
45 2nn 12331 . . . . . . . . . . . . 13 2 ∈ ℕ
4644, 45decnncl 12743 . . . . . . . . . . . 12 32 ∈ ℕ
47 nnrp 13033 . . . . . . . . . . . 12 (32 ∈ ℕ → 32 ∈ ℝ+)
4846, 47ax-mp 5 . . . . . . . . . . 11 32 ∈ ℝ+
49 rpmulcl 13045 . . . . . . . . . . 11 ((32 ∈ ℝ+𝐵 ∈ ℝ+) → (32 · 𝐵) ∈ ℝ+)
5048, 3, 49sylancr 585 . . . . . . . . . 10 (𝜑 → (32 · 𝐵) ∈ ℝ+)
5143, 50rpdivcld 13081 . . . . . . . . 9 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℝ+)
5251rpred 13064 . . . . . . . 8 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℝ)
5336, 52remulcld 11285 . . . . . . 7 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) ∈ ℝ)
5453, 24remulcld 11285 . . . . . 6 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) ∈ ℝ)
5532, 54remulcld 11285 . . . . 5 (𝜑 → (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ∈ ℝ)
5630, 55resubcld 11683 . . . 4 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) ∈ ℝ)
5713rpred 13064 . . . 4 (𝜑𝐶 ∈ ℝ)
5856, 57readdcld 11284 . . 3 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶) ∈ ℝ)
597rpcnd 13066 . . . . . 6 (𝜑𝑈 ∈ ℂ)
6053recnd 11283 . . . . . 6 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) ∈ ℂ)
6124recnd 11283 . . . . . 6 (𝜑 → (log‘𝑍) ∈ ℂ)
6259, 60, 61subdird 11712 . . . . 5 (𝜑 → ((𝑈 − ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵)))) · (log‘𝑍)) = ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
6338rpcnd 13066 . . . . . . . . . . 11 (𝜑𝐿 ∈ ℂ)
6442rpcnd 13066 . . . . . . . . . . 11 (𝜑 → (𝐸↑2) ∈ ℂ)
6550rpcnne0d 13073 . . . . . . . . . . 11 (𝜑 → ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0))
66 div23 11933 . . . . . . . . . . 11 ((𝐿 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0)) → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) = ((𝐿 / (32 · 𝐵)) · (𝐸↑2)))
6763, 64, 65, 66syl3anc 1368 . . . . . . . . . 10 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) = ((𝐿 / (32 · 𝐵)) · (𝐸↑2)))
689oveq1i 7426 . . . . . . . . . . . 12 (𝐸↑2) = ((𝑈 / 𝐷)↑2)
6937simp2d 1140 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ ℝ+)
7069rpcnd 13066 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ ℂ)
7169rpne0d 13069 . . . . . . . . . . . . 13 (𝜑𝐷 ≠ 0)
7259, 70, 71sqdivd 14172 . . . . . . . . . . . 12 (𝜑 → ((𝑈 / 𝐷)↑2) = ((𝑈↑2) / (𝐷↑2)))
7368, 72eqtrid 2778 . . . . . . . . . . 11 (𝜑 → (𝐸↑2) = ((𝑈↑2) / (𝐷↑2)))
7473oveq2d 7432 . . . . . . . . . 10 (𝜑 → ((𝐿 / (32 · 𝐵)) · (𝐸↑2)) = ((𝐿 / (32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))))
7538, 50rpdivcld 13081 . . . . . . . . . . . 12 (𝜑 → (𝐿 / (32 · 𝐵)) ∈ ℝ+)
7675rpcnd 13066 . . . . . . . . . . 11 (𝜑 → (𝐿 / (32 · 𝐵)) ∈ ℂ)
7759sqcld 14157 . . . . . . . . . . 11 (𝜑 → (𝑈↑2) ∈ ℂ)
78 rpexpcl 14094 . . . . . . . . . . . . 13 ((𝐷 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝐷↑2) ∈ ℝ+)
7969, 40, 78sylancl 584 . . . . . . . . . . . 12 (𝜑 → (𝐷↑2) ∈ ℝ+)
8079rpcnne0d 13073 . . . . . . . . . . 11 (𝜑 → ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0))
81 divass 11932 . . . . . . . . . . . 12 (((𝐿 / (32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0)) → (((𝐿 / (32 · 𝐵)) · (𝑈↑2)) / (𝐷↑2)) = ((𝐿 / (32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))))
82 div23 11933 . . . . . . . . . . . 12 (((𝐿 / (32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0)) → (((𝐿 / (32 · 𝐵)) · (𝑈↑2)) / (𝐷↑2)) = (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))
8381, 82eqtr3d 2768 . . . . . . . . . . 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 2770 . . . . . . . . 9 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) = (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))
8685oveq2d 7432 . . . . . . . 8 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
87 df-3 12322 . . . . . . . . . . . . 13 3 = (2 + 1)
8887oveq2i 7427 . . . . . . . . . . . 12 (𝑈↑3) = (𝑈↑(2 + 1))
89 2nn0 12535 . . . . . . . . . . . . 13 2 ∈ ℕ0
90 expp1 14082 . . . . . . . . . . . . 13 ((𝑈 ∈ ℂ ∧ 2 ∈ ℕ0) → (𝑈↑(2 + 1)) = ((𝑈↑2) · 𝑈))
9159, 89, 90sylancl 584 . . . . . . . . . . . 12 (𝜑 → (𝑈↑(2 + 1)) = ((𝑈↑2) · 𝑈))
9288, 91eqtrid 2778 . . . . . . . . . . 11 (𝜑 → (𝑈↑3) = ((𝑈↑2) · 𝑈))
9377, 59mulcomd 11276 . . . . . . . . . . 11 (𝜑 → ((𝑈↑2) · 𝑈) = (𝑈 · (𝑈↑2)))
9492, 93eqtrd 2766 . . . . . . . . . 10 (𝜑 → (𝑈↑3) = (𝑈 · (𝑈↑2)))
9594oveq2d 7432 . . . . . . . . 9 (𝜑 → (𝐹 · (𝑈↑3)) = (𝐹 · (𝑈 · (𝑈↑2))))
9637simp3d 1141 . . . . . . . . . . 11 (𝜑𝐹 ∈ ℝ+)
9796rpcnd 13066 . . . . . . . . . 10 (𝜑𝐹 ∈ ℂ)
9897, 59, 77mulassd 11278 . . . . . . . . 9 (𝜑 → ((𝐹 · 𝑈) · (𝑈↑2)) = (𝐹 · (𝑈 · (𝑈↑2))))
99 1cnd 11250 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
10069rpreccld 13074 . . . . . . . . . . . . . . . 16 (𝜑 → (1 / 𝐷) ∈ ℝ+)
101100rpcnd 13066 . . . . . . . . . . . . . . 15 (𝜑 → (1 / 𝐷) ∈ ℂ)
10299, 101, 59subdird 11712 . . . . . . . . . . . . . 14 (𝜑 → ((1 − (1 / 𝐷)) · 𝑈) = ((1 · 𝑈) − ((1 / 𝐷) · 𝑈)))
10359mullidd 11273 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝑈) = 𝑈)
10459, 70, 71divrec2d 12039 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑈 / 𝐷) = ((1 / 𝐷) · 𝑈))
1059, 104eqtr2id 2779 . . . . . . . . . . . . . . 15 (𝜑 → ((1 / 𝐷) · 𝑈) = 𝐸)
106103, 105oveq12d 7434 . . . . . . . . . . . . . 14 (𝜑 → ((1 · 𝑈) − ((1 / 𝐷) · 𝑈)) = (𝑈𝐸))
107102, 106eqtr2d 2767 . . . . . . . . . . . . 13 (𝜑 → (𝑈𝐸) = ((1 − (1 / 𝐷)) · 𝑈))
108107oveq1d 7431 . . . . . . . . . . . 12 (𝜑 → ((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))))
1096oveq1i 7426 . . . . . . . . . . . . 13 (𝐹 · 𝑈) = (((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · 𝑈)
11099, 101subcld 11612 . . . . . . . . . . . . . 14 (𝜑 → (1 − (1 / 𝐷)) ∈ ℂ)
11175, 79rpdivcld 13081 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐿 / (32 · 𝐵)) / (𝐷↑2)) ∈ ℝ+)
112111rpcnd 13066 . . . . . . . . . . . . . 14 (𝜑 → ((𝐿 / (32 · 𝐵)) / (𝐷↑2)) ∈ ℂ)
113110, 112, 59mul32d 11465 . . . . . . . . . . . . 13 (𝜑 → (((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · 𝑈) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))))
114109, 113eqtrid 2778 . . . . . . . . . . . 12 (𝜑 → (𝐹 · 𝑈) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))))
115108, 114eqtr4d 2769 . . . . . . . . . . 11 (𝜑 → ((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) = (𝐹 · 𝑈))
116115oveq1d 7431 . . . . . . . . . 10 (𝜑 → (((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · (𝑈↑2)) = ((𝐹 · 𝑈) · (𝑈↑2)))
11735rpcnd 13066 . . . . . . . . . . 11 (𝜑 → (𝑈𝐸) ∈ ℂ)
118117, 112, 77mulassd 11278 . . . . . . . . . 10 (𝜑 → (((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · (𝑈↑2)) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
119116, 118eqtr3d 2768 . . . . . . . . 9 (𝜑 → ((𝐹 · 𝑈) · (𝑈↑2)) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
12095, 98, 1193eqtr2d 2772 . . . . . . . 8 (𝜑 → (𝐹 · (𝑈↑3)) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
12186, 120eqtr4d 2769 . . . . . . 7 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) = (𝐹 · (𝑈↑3)))
122121oveq2d 7432 . . . . . 6 (𝜑 → (𝑈 − ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵)))) = (𝑈 − (𝐹 · (𝑈↑3))))
123122oveq1d 7431 . . . . 5 (𝜑 → ((𝑈 − ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵)))) · (log‘𝑍)) = ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
12462, 123eqtr3d 2768 . . . 4 (𝜑 → ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) = ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
12526, 24remulcld 11285 . . . . 5 (𝜑 → (𝑈 · (log‘𝑍)) ∈ ℝ)
126125, 54resubcld 11683 . . . 4 (𝜑 → ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ∈ ℝ)
127124, 126eqeltrrd 2827 . . 3 (𝜑 → ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)) ∈ ℝ)
12817rpred 13064 . . . . . . . 8 (𝜑𝑍 ∈ ℝ)
12916simp2d 1140 . . . . . . . . 9 (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
130129simp1d 1139 . . . . . . . 8 (𝜑 → 1 < 𝑍)
131128, 130rplogcld 26653 . . . . . . 7 (𝜑 → (log‘𝑍) ∈ ℝ+)
13232, 131rerpdivcld 13095 . . . . . 6 (𝜑 → (2 / (log‘𝑍)) ∈ ℝ)
133 fzfid 13987 . . . . . . 7 (𝜑 → (1...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
13417adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈ ℝ+)
135 elfznn 13578 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ∈ ℕ)
136135adantl 480 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℕ)
137136nnrpd 13062 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℝ+)
138134, 137rpdivcld 13081 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 / 𝑛) ∈ ℝ+)
13918ffvelcdmi 7089 . . . . . . . . . . . 12 ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
140138, 139syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
141140, 134rerpdivcld 13095 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
142141recnd 11283 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
143142abscld 15436 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
144137relogcld 26647 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℝ)
145143, 144remulcld 11285 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ)
146133, 145fsumrecl 15733 . . . . . 6 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ)
147132, 146remulcld 11285 . . . . 5 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ)
148147, 57readdcld 11284 . . . 4 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶) ∈ ℝ)
14920recnd 11283 . . . . . . . . . . 11 (𝜑 → (𝑅𝑍) ∈ ℂ)
150149abscld 15436 . . . . . . . . . 10 (𝜑 → (abs‘(𝑅𝑍)) ∈ ℝ)
151150recnd 11283 . . . . . . . . 9 (𝜑 → (abs‘(𝑅𝑍)) ∈ ℂ)
152151, 61mulcld 11275 . . . . . . . 8 (𝜑 → ((abs‘(𝑅𝑍)) · (log‘𝑍)) ∈ ℂ)
153132recnd 11283 . . . . . . . . 9 (𝜑 → (2 / (log‘𝑍)) ∈ ℂ)
154140recnd 11283 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℂ)
155154abscld 15436 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℝ)
156155, 144remulcld 11285 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
157133, 156fsumrecl 15733 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
158157recnd 11283 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
159153, 158mulcld 11275 . . . . . . . 8 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) ∈ ℂ)
16017rpcnd 13066 . . . . . . . 8 (𝜑𝑍 ∈ ℂ)
16117rpne0d 13069 . . . . . . . 8 (𝜑𝑍 ≠ 0)
162152, 159, 160, 161divsubdird 12074 . . . . . . 7 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) = ((((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) − (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍)))
163151, 61, 160, 161div23d 12072 . . . . . . . . 9 (𝜑 → (((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) = (((abs‘(𝑅𝑍)) / 𝑍) · (log‘𝑍)))
164149, 160, 161absdivd 15455 . . . . . . . . . . 11 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) = ((abs‘(𝑅𝑍)) / (abs‘𝑍)))
16517rprege0d 13071 . . . . . . . . . . . . 13 (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
166 absid 15296 . . . . . . . . . . . . 13 ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → (abs‘𝑍) = 𝑍)
167165, 166syl 17 . . . . . . . . . . . 12 (𝜑 → (abs‘𝑍) = 𝑍)
168167oveq2d 7432 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝑅𝑍)) / (abs‘𝑍)) = ((abs‘(𝑅𝑍)) / 𝑍))
169164, 168eqtrd 2766 . . . . . . . . . 10 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) = ((abs‘(𝑅𝑍)) / 𝑍))
170169oveq1d 7431 . . . . . . . . 9 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) = (((abs‘(𝑅𝑍)) / 𝑍) · (log‘𝑍)))
171163, 170eqtr4d 2769 . . . . . . . 8 (𝜑 → (((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) = ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)))
172153, 158, 160, 161divassd 12070 . . . . . . . . 9 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍) = ((2 / (log‘𝑍)) · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍)))
173160adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈ ℂ)
174161adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ≠ 0)
175154, 173, 174absdivd 15455 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / (abs‘𝑍)))
176167adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘𝑍) = 𝑍)
177176oveq2d 7432 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) / (abs‘𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍))
178175, 177eqtrd 2766 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍))
179178oveq1d 7431 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛)))
180155recnd 11283 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℂ)
181144recnd 11283 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℂ)
18217rpcnne0d 13073 . . . . . . . . . . . . . . 15 (𝜑 → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0))
183182adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0))
184 div23 11933 . . . . . . . . . . . . . 14 (((abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) → (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛)))
185180, 181, 183, 184syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛)))
186179, 185eqtr4d 2769 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
187186sumeq2dv 15702 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
188156recnd 11283 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
189133, 160, 188, 161fsumdivc 15785 . . . . . . . . . . 11 (𝜑 → (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
190187, 189eqtr4d 2769 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
191190oveq2d 7432 . . . . . . . . 9 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) = ((2 / (log‘𝑍)) · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍)))
192172, 191eqtr4d 2769 . . . . . . . 8 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
193171, 192oveq12d 7434 . . . . . . 7 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) − (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍)) = (((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
194162, 193eqtrd 2766 . . . . . 6 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) = (((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
195 2fveq3 6898 . . . . . . . . . . 11 (𝑧 = 𝑍 → (abs‘(𝑅𝑧)) = (abs‘(𝑅𝑍)))
196 fveq2 6893 . . . . . . . . . . 11 (𝑧 = 𝑍 → (log‘𝑧) = (log‘𝑍))
197195, 196oveq12d 7434 . . . . . . . . . 10 (𝑧 = 𝑍 → ((abs‘(𝑅𝑧)) · (log‘𝑧)) = ((abs‘(𝑅𝑍)) · (log‘𝑍)))
198196oveq2d 7432 . . . . . . . . . . 11 (𝑧 = 𝑍 → (2 / (log‘𝑧)) = (2 / (log‘𝑍)))
199 oveq2 7424 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 → (𝑧 / 𝑖) = (𝑧 / 𝑛))
200199fveq2d 6897 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → (𝑅‘(𝑧 / 𝑖)) = (𝑅‘(𝑧 / 𝑛)))
201200fveq2d 6897 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (abs‘(𝑅‘(𝑧 / 𝑖))) = (abs‘(𝑅‘(𝑧 / 𝑛))))
202 fveq2 6893 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (log‘𝑖) = (log‘𝑛))
203201, 202oveq12d 7434 . . . . . . . . . . . . 13 (𝑖 = 𝑛 → ((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = ((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))
204203cbvsumv 15695 . . . . . . . . . . . 12 Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = Σ𝑛 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛))
205 fvoveq1 7439 . . . . . . . . . . . . . 14 (𝑧 = 𝑍 → (⌊‘(𝑧 / 𝑌)) = (⌊‘(𝑍 / 𝑌)))
206205oveq2d 7432 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → (1...(⌊‘(𝑧 / 𝑌))) = (1...(⌊‘(𝑍 / 𝑌))))
207 simpl 481 . . . . . . . . . . . . . . . 16 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑧 = 𝑍)
208207fvoveq1d 7438 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑧 / 𝑛)) = (𝑅‘(𝑍 / 𝑛)))
209208fveq2d 6897 . . . . . . . . . . . . . 14 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑧 / 𝑛))) = (abs‘(𝑅‘(𝑍 / 𝑛))))
210209oveq1d 7431 . . . . . . . . . . . . 13 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))
211206, 210sumeq12rdv 15706 . . . . . . . . . . . 12 (𝑧 = 𝑍 → Σ𝑛 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))
212204, 211eqtrid 2778 . . . . . . . . . . 11 (𝑧 = 𝑍 → Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))
213198, 212oveq12d 7434 . . . . . . . . . 10 (𝑧 = 𝑍 → ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖))) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))))
214197, 213oveq12d 7434 . . . . . . . . 9 (𝑧 = 𝑍 → (((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) = (((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))))
215 id 22 . . . . . . . . 9 (𝑧 = 𝑍𝑧 = 𝑍)
216214, 215oveq12d 7434 . . . . . . . 8 (𝑧 = 𝑍 → ((((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) = ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍))
217216breq1d 5155 . . . . . . 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 11255 . . . . . . . . 9 1 ∈ ℝ
220 rexr 11301 . . . . . . . . 9 (1 ∈ ℝ → 1 ∈ ℝ*)
221 elioopnf 13468 . . . . . . . . 9 (1 ∈ ℝ* → (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 < 𝑍)))
222219, 220, 221mp2b 10 . . . . . . . 8 (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 < 𝑍))
223128, 130, 222sylanbrc 581 . . . . . . 7 (𝜑𝑍 ∈ (1(,)+∞))
224217, 218, 223rspcdva 3608 . . . . . 6 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) ≤ 𝐶)
225194, 224eqbrtrrd 5169 . . . . 5 (𝜑 → (((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ 𝐶)
22625, 147, 57lesubadd2d 11854 . . . . 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 12336 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
229143recnd 11283 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℂ)
230229, 181mulcld 11275 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℂ)
231133, 230fsumcl 15732 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℂ)
232131rpne0d 13069 . . . . . . 7 (𝜑 → (log‘𝑍) ≠ 0)
233228, 231, 61, 232div23d 12072 . . . . . 6 (𝜑 → ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) / (log‘𝑍)) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
23424resqcld 14138 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑍)↑2) ∈ ℝ)
23552, 234remulcld 11285 . . . . . . . . . . 11 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ)
23636, 235remulcld 11285 . . . . . . . . . 10 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ)
237 remulcl 11234 . . . . . . . . . 10 ((2 ∈ ℝ ∧ ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ) → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ∈ ℝ)
23831, 236, 237sylancr 585 . . . . . . . . 9 (𝜑 → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ∈ ℝ)
23930, 24remulcld 11285 . . . . . . . . 9 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) ∈ ℝ)
240 remulcl 11234 . . . . . . . . . 10 ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ) → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ)
24131, 146, 240sylancr 585 . . . . . . . . 9 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ)
24226adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑈 ∈ ℝ)
243242, 136nndivred 12312 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℝ)
244243, 143resubcld 11683 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
245244, 144remulcld 11285 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
246133, 245fsumrecl 15733 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
24732, 246remulcld 11285 . . . . . . . . . 10 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ∈ ℝ)
248239, 241resubcld 11683 . . . . . . . . . 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 27631 . . . . . . . . . . 11 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
254 2pos 12361 . . . . . . . . . . . . 13 0 < 2
255254a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 < 2)
256 lemul2 12112 . . . . . . . . . . . 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 11283 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℂ)
260259, 229, 181subdird 11712 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
261260sumeq2dv 15702 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
262243, 144remulcld 11285 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ)
263262recnd 11283 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℂ)
264133, 263, 230fsumsub 15787 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
265261, 264eqtrd 2766 . . . . . . . . . . . . 13 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
266265oveq2d 7432 . . . . . . . . . . . 12 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) = (2 · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
267133, 262fsumrecl 15733 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ)
268267recnd 11283 . . . . . . . . . . . . 13 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℂ)
269228, 268, 231subdid 11711 . . . . . . . . . . . 12 (𝜑 → (2 · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) = ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
270266, 269eqtrd 2766 . . . . . . . . . . 11 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) = ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
271 remulcl 11234 . . . . . . . . . . . . 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 27632 . . . . . . . . . . . 12 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ≤ ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)))
274272, 239, 241, 273lesub1dd 11871 . . . . . . . . . . 11 (𝜑 → ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
275270, 274eqbrtrd 5167 . . . . . . . . . 10 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
276238, 247, 248, 258, 275letrd 11412 . . . . . . . . 9 (𝜑 → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
277238, 239, 241, 276lesubd 11859 . . . . . . . 8 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))))
27830recnd 11283 . . . . . . . . . 10 (𝜑 → (𝑈 · ((log‘𝑍) + 3)) ∈ ℂ)
27955recnd 11283 . . . . . . . . . 10 (𝜑 → (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ∈ ℂ)
280278, 279, 61subdird 11712 . . . . . . . . 9 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍))))
28154recnd 11283 . . . . . . . . . . . 12 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) ∈ ℂ)
282228, 281, 61mulassd 11278 . . . . . . . . . . 11 (𝜑 → ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍)) = (2 · ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍))))
28360, 61, 61mulassd 11278 . . . . . . . . . . . . 13 (𝜑 → ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍)) = (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍) · (log‘𝑍))))
28461sqvald 14156 . . . . . . . . . . . . . 14 (𝜑 → ((log‘𝑍)↑2) = ((log‘𝑍) · (log‘𝑍)))
285284oveq2d 7432 . . . . . . . . . . . . 13 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍)↑2)) = (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍) · (log‘𝑍))))
28651rpcnd 13066 . . . . . . . . . . . . . 14 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℂ)
287234recnd 11283 . . . . . . . . . . . . . 14 (𝜑 → ((log‘𝑍)↑2) ∈ ℂ)
288117, 286, 287mulassd 11278 . . . . . . . . . . . . 13 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍)↑2)) = ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))
289283, 285, 2883eqtr2d 2772 . . . . . . . . . . . 12 (𝜑 → ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍)) = ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))
290289oveq2d 7432 . . . . . . . . . . 11 (𝜑 → (2 · ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍))) = (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))))
291282, 290eqtrd 2766 . . . . . . . . . 10 (𝜑 → ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍)) = (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))))
292291oveq2d 7432 . . . . . . . . 9 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍))) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))))
293280, 292eqtrd 2766 . . . . . . . 8 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))))
294277, 293breqtrrd 5173 . . . . . . 7 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)))
295241, 56, 131ledivmul2d 13118 . . . . . . 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 5169 . . . . 5 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
298147, 56, 57, 297leadd1dd 11869 . . . 4 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶))
29925, 148, 58, 227, 298letrd 11412 . . 3 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶))
300 remulcl 11234 . . . . . . . . 9 ((𝑈 ∈ ℝ ∧ 3 ∈ ℝ) → (𝑈 · 3) ∈ ℝ)
30126, 27, 300sylancl 584 . . . . . . . 8 (𝜑 → (𝑈 · 3) ∈ ℝ)
302301, 57readdcld 11284 . . . . . . 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 11870 . . . . . 6 (𝜑 → ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶)) ≤ ((𝑈 · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
30628recnd 11283 . . . . . . . . 9 (𝜑 → 3 ∈ ℂ)
30759, 61, 306adddid 11279 . . . . . . . 8 (𝜑 → (𝑈 · ((log‘𝑍) + 3)) = ((𝑈 · (log‘𝑍)) + (𝑈 · 3)))
308307oveq1d 7431 . . . . . . 7 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) = (((𝑈 · (log‘𝑍)) + (𝑈 · 3)) + 𝐶))
309125recnd 11283 . . . . . . . 8 (𝜑 → (𝑈 · (log‘𝑍)) ∈ ℂ)
31059, 306mulcld 11275 . . . . . . . 8 (𝜑 → (𝑈 · 3) ∈ ℂ)
31113rpcnd 13066 . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
312309, 310, 311addassd 11277 . . . . . . 7 (𝜑 → (((𝑈 · (log‘𝑍)) + (𝑈 · 3)) + 𝐶) = ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶)))
313308, 312eqtrd 2766 . . . . . 6 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) = ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶)))
3142812timesd 12501 . . . . . . . 8 (𝜑 → (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) = ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
315314oveq2d 7432 . . . . . . 7 (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
316309, 281, 281nppcan3d 11639 . . . . . . 7 (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = ((𝑈 · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
317315, 316eqtrd 2766 . . . . . 6 (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = ((𝑈 · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
318305, 313, 3173brtr4d 5177 . . . . 5 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ≤ (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
31930, 57readdcld 11284 . . . . . 6 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ∈ ℝ)
320319, 55, 126lesubaddd 11852 . . . . 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 11633 . . . 4 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) + 𝐶) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶))
323321, 322, 1243brtr3d 5176 . . 3 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
32425, 58, 127, 299, 323letrd 11412 . 2 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
325 3z 12641 . . . . . . 7 3 ∈ ℤ
326 rpexpcl 14094 . . . . . . 7 ((𝑈 ∈ ℝ+ ∧ 3 ∈ ℤ) → (𝑈↑3) ∈ ℝ+)
3277, 325, 326sylancl 584 . . . . . 6 (𝜑 → (𝑈↑3) ∈ ℝ+)
32896, 327rpmulcld 13080 . . . . 5 (𝜑 → (𝐹 · (𝑈↑3)) ∈ ℝ+)
329328rpred 13064 . . . 4 (𝜑 → (𝐹 · (𝑈↑3)) ∈ ℝ)
33026, 329resubcld 11683 . . 3 (𝜑 → (𝑈 − (𝐹 · (𝑈↑3))) ∈ ℝ)
33123, 330, 131lemul1d 13107 . 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 1534  wcel 2099  wne 2930  wral 3051  wrex 3060   class class class wbr 5145  cmpt 5228  cfv 6546  (class class class)co 7416  cc 11147  cr 11148  0cc0 11149  1c1 11150   + caddc 11152   · cmul 11154  +∞cpnf 11286  *cxr 11288   < clt 11289  cle 11290  cmin 11485   / cdiv 11912  cn 12258  2c2 12313  3c3 12314  4c4 12315  0cn0 12518  cz 12604  cdc 12723  +crp 13022  (,)cioo 13372  [,)cico 13374  [,]cicc 13375  ...cfz 13532  cfl 13804  cexp 14075  csqrt 15233  abscabs 15234  Σcsu 15685  expce 16058  eceu 16059  logclog 26578  ψcchp 27118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-inf2 9677  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227  ax-addf 11228
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-om 7869  df-1st 7995  df-2nd 7996  df-supp 8167  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-oadd 8492  df-er 8726  df-map 8849  df-pm 8850  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9399  df-fi 9447  df-sup 9478  df-inf 9479  df-oi 9546  df-dju 9937  df-card 9975  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12519  df-xnn0 12591  df-z 12605  df-dec 12724  df-uz 12869  df-q 12979  df-rp 13023  df-xneg 13140  df-xadd 13141  df-xmul 13142  df-ioo 13376  df-ioc 13377  df-ico 13378  df-icc 13379  df-fz 13533  df-fzo 13676  df-fl 13806  df-mod 13884  df-seq 14016  df-exp 14076  df-fac 14286  df-bc 14315  df-hash 14343  df-shft 15067  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-limsup 15468  df-clim 15485  df-rlim 15486  df-sum 15686  df-ef 16064  df-e 16065  df-sin 16066  df-cos 16067  df-tan 16068  df-pi 16069  df-dvds 16252  df-gcd 16490  df-prm 16668  df-pc 16834  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-starv 17276  df-sca 17277  df-vsca 17278  df-ip 17279  df-tset 17280  df-ple 17281  df-ds 17283  df-unif 17284  df-hom 17285  df-cco 17286  df-rest 17432  df-topn 17433  df-0g 17451  df-gsum 17452  df-topgen 17453  df-pt 17454  df-prds 17457  df-xrs 17512  df-qtop 17517  df-imas 17518  df-xps 17520  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-submnd 18769  df-mulg 19058  df-cntz 19307  df-cmn 19776  df-psmet 21331  df-xmet 21332  df-met 21333  df-bl 21334  df-mopn 21335  df-fbas 21336  df-fg 21337  df-cnfld 21340  df-top 22884  df-topon 22901  df-topsp 22923  df-bases 22937  df-cld 23011  df-ntr 23012  df-cls 23013  df-nei 23090  df-lp 23128  df-perf 23129  df-cn 23219  df-cnp 23220  df-haus 23307  df-cmp 23379  df-tx 23554  df-hmeo 23747  df-fil 23838  df-fm 23930  df-flim 23931  df-flf 23932  df-xms 24314  df-ms 24315  df-tms 24316  df-cncf 24886  df-limc 25883  df-dv 25884  df-ulm 26403  df-log 26580  df-atan 26892  df-em 27018  df-vma 27123  df-chp 27124
This theorem is referenced by:  pntleme  27634
  Copyright terms: Public domain W3C validator