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

Theorem pntlemo 25516
Description: Lemma for pnt 25523. 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 25506 . . . . . . . . 9 (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
1716simp1d 1137 . . . . . . . 8 (𝜑𝑍 ∈ ℝ+)
181pntrf 25472 . . . . . . . . 9 𝑅:ℝ+⟶ℝ
1918ffvelrni 6522 . . . . . . . 8 (𝑍 ∈ ℝ+ → (𝑅𝑍) ∈ ℝ)
2017, 19syl 17 . . . . . . 7 (𝜑 → (𝑅𝑍) ∈ ℝ)
2120, 17rerpdivcld 12116 . . . . . 6 (𝜑 → ((𝑅𝑍) / 𝑍) ∈ ℝ)
2221recnd 10280 . . . . 5 (𝜑 → ((𝑅𝑍) / 𝑍) ∈ ℂ)
2322abscld 14394 . . . 4 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) ∈ ℝ)
2417relogcld 24589 . . . 4 (𝜑 → (log‘𝑍) ∈ ℝ)
2523, 24remulcld 10282 . . 3 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ∈ ℝ)
267rpred 12085 . . . . . 6 (𝜑𝑈 ∈ ℝ)
27 3re 11306 . . . . . . . 8 3 ∈ ℝ
2827a1i 11 . . . . . . 7 (𝜑 → 3 ∈ ℝ)
2924, 28readdcld 10281 . . . . . 6 (𝜑 → ((log‘𝑍) + 3) ∈ ℝ)
3026, 29remulcld 10282 . . . . 5 (𝜑 → (𝑈 · ((log‘𝑍) + 3)) ∈ ℝ)
31 2re 11302 . . . . . . 7 2 ∈ ℝ
3231a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℝ)
331, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 25504 . . . . . . . . . . 11 (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))
3433simp3d 1139 . . . . . . . . . 10 (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+))
3534simp3d 1139 . . . . . . . . 9 (𝜑 → (𝑈𝐸) ∈ ℝ+)
3635rpred 12085 . . . . . . . 8 (𝜑 → (𝑈𝐸) ∈ ℝ)
371, 2, 3, 4, 5, 6pntlemd 25503 . . . . . . . . . . . 12 (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))
3837simp1d 1137 . . . . . . . . . . 11 (𝜑𝐿 ∈ ℝ+)
3933simp1d 1137 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℝ+)
40 2z 11621 . . . . . . . . . . . 12 2 ∈ ℤ
41 rpexpcl 13093 . . . . . . . . . . . 12 ((𝐸 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝐸↑2) ∈ ℝ+)
4239, 40, 41sylancl 697 . . . . . . . . . . 11 (𝜑 → (𝐸↑2) ∈ ℝ+)
4338, 42rpmulcld 12101 . . . . . . . . . 10 (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℝ+)
44 3nn0 11522 . . . . . . . . . . . . 13 3 ∈ ℕ0
45 2nn 11397 . . . . . . . . . . . . 13 2 ∈ ℕ
4644, 45decnncl 11730 . . . . . . . . . . . 12 32 ∈ ℕ
47 nnrp 12055 . . . . . . . . . . . 12 (32 ∈ ℕ → 32 ∈ ℝ+)
4846, 47ax-mp 5 . . . . . . . . . . 11 32 ∈ ℝ+
49 rpmulcl 12068 . . . . . . . . . . 11 ((32 ∈ ℝ+𝐵 ∈ ℝ+) → (32 · 𝐵) ∈ ℝ+)
5048, 3, 49sylancr 698 . . . . . . . . . 10 (𝜑 → (32 · 𝐵) ∈ ℝ+)
5143, 50rpdivcld 12102 . . . . . . . . 9 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℝ+)
5251rpred 12085 . . . . . . . 8 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℝ)
5336, 52remulcld 10282 . . . . . . 7 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) ∈ ℝ)
5453, 24remulcld 10282 . . . . . 6 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) ∈ ℝ)
5532, 54remulcld 10282 . . . . 5 (𝜑 → (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ∈ ℝ)
5630, 55resubcld 10670 . . . 4 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) ∈ ℝ)
5713rpred 12085 . . . 4 (𝜑𝐶 ∈ ℝ)
5856, 57readdcld 10281 . . 3 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶) ∈ ℝ)
597rpcnd 12087 . . . . . 6 (𝜑𝑈 ∈ ℂ)
6053recnd 10280 . . . . . 6 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) ∈ ℂ)
6124recnd 10280 . . . . . 6 (𝜑 → (log‘𝑍) ∈ ℂ)
6259, 60, 61subdird 10699 . . . . 5 (𝜑 → ((𝑈 − ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵)))) · (log‘𝑍)) = ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
6338rpcnd 12087 . . . . . . . . . . 11 (𝜑𝐿 ∈ ℂ)
6442rpcnd 12087 . . . . . . . . . . 11 (𝜑 → (𝐸↑2) ∈ ℂ)
6550rpcnne0d 12094 . . . . . . . . . . 11 (𝜑 → ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0))
66 div23 10916 . . . . . . . . . . 11 ((𝐿 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0)) → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) = ((𝐿 / (32 · 𝐵)) · (𝐸↑2)))
6763, 64, 65, 66syl3anc 1477 . . . . . . . . . 10 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) = ((𝐿 / (32 · 𝐵)) · (𝐸↑2)))
689oveq1i 6824 . . . . . . . . . . . 12 (𝐸↑2) = ((𝑈 / 𝐷)↑2)
6937simp2d 1138 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ ℝ+)
7069rpcnd 12087 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ ℂ)
7169rpne0d 12090 . . . . . . . . . . . . 13 (𝜑𝐷 ≠ 0)
7259, 70, 71sqdivd 13235 . . . . . . . . . . . 12 (𝜑 → ((𝑈 / 𝐷)↑2) = ((𝑈↑2) / (𝐷↑2)))
7368, 72syl5eq 2806 . . . . . . . . . . 11 (𝜑 → (𝐸↑2) = ((𝑈↑2) / (𝐷↑2)))
7473oveq2d 6830 . . . . . . . . . 10 (𝜑 → ((𝐿 / (32 · 𝐵)) · (𝐸↑2)) = ((𝐿 / (32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))))
7538, 50rpdivcld 12102 . . . . . . . . . . . 12 (𝜑 → (𝐿 / (32 · 𝐵)) ∈ ℝ+)
7675rpcnd 12087 . . . . . . . . . . 11 (𝜑 → (𝐿 / (32 · 𝐵)) ∈ ℂ)
7759sqcld 13220 . . . . . . . . . . 11 (𝜑 → (𝑈↑2) ∈ ℂ)
78 rpexpcl 13093 . . . . . . . . . . . . 13 ((𝐷 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝐷↑2) ∈ ℝ+)
7969, 40, 78sylancl 697 . . . . . . . . . . . 12 (𝜑 → (𝐷↑2) ∈ ℝ+)
8079rpcnne0d 12094 . . . . . . . . . . 11 (𝜑 → ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0))
81 divass 10915 . . . . . . . . . . . 12 (((𝐿 / (32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0)) → (((𝐿 / (32 · 𝐵)) · (𝑈↑2)) / (𝐷↑2)) = ((𝐿 / (32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))))
82 div23 10916 . . . . . . . . . . . 12 (((𝐿 / (32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0)) → (((𝐿 / (32 · 𝐵)) · (𝑈↑2)) / (𝐷↑2)) = (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))
8381, 82eqtr3d 2796 . . . . . . . . . . 11 (((𝐿 / (32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0)) → ((𝐿 / (32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))) = (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))
8476, 77, 80, 83syl3anc 1477 . . . . . . . . . 10 (𝜑 → ((𝐿 / (32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))) = (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))
8567, 74, 843eqtrd 2798 . . . . . . . . 9 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) = (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))
8685oveq2d 6830 . . . . . . . 8 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
87 df-3 11292 . . . . . . . . . . . . 13 3 = (2 + 1)
8887oveq2i 6825 . . . . . . . . . . . 12 (𝑈↑3) = (𝑈↑(2 + 1))
89 2nn0 11521 . . . . . . . . . . . . 13 2 ∈ ℕ0
90 expp1 13081 . . . . . . . . . . . . 13 ((𝑈 ∈ ℂ ∧ 2 ∈ ℕ0) → (𝑈↑(2 + 1)) = ((𝑈↑2) · 𝑈))
9159, 89, 90sylancl 697 . . . . . . . . . . . 12 (𝜑 → (𝑈↑(2 + 1)) = ((𝑈↑2) · 𝑈))
9288, 91syl5eq 2806 . . . . . . . . . . 11 (𝜑 → (𝑈↑3) = ((𝑈↑2) · 𝑈))
9377, 59mulcomd 10273 . . . . . . . . . . 11 (𝜑 → ((𝑈↑2) · 𝑈) = (𝑈 · (𝑈↑2)))
9492, 93eqtrd 2794 . . . . . . . . . 10 (𝜑 → (𝑈↑3) = (𝑈 · (𝑈↑2)))
9594oveq2d 6830 . . . . . . . . 9 (𝜑 → (𝐹 · (𝑈↑3)) = (𝐹 · (𝑈 · (𝑈↑2))))
9637simp3d 1139 . . . . . . . . . . 11 (𝜑𝐹 ∈ ℝ+)
9796rpcnd 12087 . . . . . . . . . 10 (𝜑𝐹 ∈ ℂ)
9897, 59, 77mulassd 10275 . . . . . . . . 9 (𝜑 → ((𝐹 · 𝑈) · (𝑈↑2)) = (𝐹 · (𝑈 · (𝑈↑2))))
99 1cnd 10268 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
10069rpreccld 12095 . . . . . . . . . . . . . . . 16 (𝜑 → (1 / 𝐷) ∈ ℝ+)
101100rpcnd 12087 . . . . . . . . . . . . . . 15 (𝜑 → (1 / 𝐷) ∈ ℂ)
10299, 101, 59subdird 10699 . . . . . . . . . . . . . 14 (𝜑 → ((1 − (1 / 𝐷)) · 𝑈) = ((1 · 𝑈) − ((1 / 𝐷) · 𝑈)))
10359mulid2d 10270 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝑈) = 𝑈)
10459, 70, 71divrec2d 11017 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑈 / 𝐷) = ((1 / 𝐷) · 𝑈))
1059, 104syl5req 2807 . . . . . . . . . . . . . . 15 (𝜑 → ((1 / 𝐷) · 𝑈) = 𝐸)
106103, 105oveq12d 6832 . . . . . . . . . . . . . 14 (𝜑 → ((1 · 𝑈) − ((1 / 𝐷) · 𝑈)) = (𝑈𝐸))
107102, 106eqtr2d 2795 . . . . . . . . . . . . 13 (𝜑 → (𝑈𝐸) = ((1 − (1 / 𝐷)) · 𝑈))
108107oveq1d 6829 . . . . . . . . . . . 12 (𝜑 → ((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))))
1096oveq1i 6824 . . . . . . . . . . . . 13 (𝐹 · 𝑈) = (((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · 𝑈)
11099, 101subcld 10604 . . . . . . . . . . . . . 14 (𝜑 → (1 − (1 / 𝐷)) ∈ ℂ)
11175, 79rpdivcld 12102 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐿 / (32 · 𝐵)) / (𝐷↑2)) ∈ ℝ+)
112111rpcnd 12087 . . . . . . . . . . . . . 14 (𝜑 → ((𝐿 / (32 · 𝐵)) / (𝐷↑2)) ∈ ℂ)
113110, 112, 59mul32d 10458 . . . . . . . . . . . . 13 (𝜑 → (((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · 𝑈) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))))
114109, 113syl5eq 2806 . . . . . . . . . . . 12 (𝜑 → (𝐹 · 𝑈) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))))
115108, 114eqtr4d 2797 . . . . . . . . . . 11 (𝜑 → ((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) = (𝐹 · 𝑈))
116115oveq1d 6829 . . . . . . . . . 10 (𝜑 → (((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · (𝑈↑2)) = ((𝐹 · 𝑈) · (𝑈↑2)))
11735rpcnd 12087 . . . . . . . . . . 11 (𝜑 → (𝑈𝐸) ∈ ℂ)
118117, 112, 77mulassd 10275 . . . . . . . . . 10 (𝜑 → (((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · (𝑈↑2)) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
119116, 118eqtr3d 2796 . . . . . . . . 9 (𝜑 → ((𝐹 · 𝑈) · (𝑈↑2)) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
12095, 98, 1193eqtr2d 2800 . . . . . . . 8 (𝜑 → (𝐹 · (𝑈↑3)) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
12186, 120eqtr4d 2797 . . . . . . 7 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) = (𝐹 · (𝑈↑3)))
122121oveq2d 6830 . . . . . 6 (𝜑 → (𝑈 − ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵)))) = (𝑈 − (𝐹 · (𝑈↑3))))
123122oveq1d 6829 . . . . 5 (𝜑 → ((𝑈 − ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵)))) · (log‘𝑍)) = ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
12462, 123eqtr3d 2796 . . . 4 (𝜑 → ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) = ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
12526, 24remulcld 10282 . . . . 5 (𝜑 → (𝑈 · (log‘𝑍)) ∈ ℝ)
126125, 54resubcld 10670 . . . 4 (𝜑 → ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ∈ ℝ)
127124, 126eqeltrrd 2840 . . 3 (𝜑 → ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)) ∈ ℝ)
12817rpred 12085 . . . . . . . 8 (𝜑𝑍 ∈ ℝ)
12916simp2d 1138 . . . . . . . . 9 (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
130129simp1d 1137 . . . . . . . 8 (𝜑 → 1 < 𝑍)
131128, 130rplogcld 24595 . . . . . . 7 (𝜑 → (log‘𝑍) ∈ ℝ+)
13232, 131rerpdivcld 12116 . . . . . 6 (𝜑 → (2 / (log‘𝑍)) ∈ ℝ)
133 fzfid 12986 . . . . . . 7 (𝜑 → (1...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
13417adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈ ℝ+)
135 elfznn 12583 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ∈ ℕ)
136135adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℕ)
137136nnrpd 12083 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℝ+)
138134, 137rpdivcld 12102 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 / 𝑛) ∈ ℝ+)
13918ffvelrni 6522 . . . . . . . . . . . 12 ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
140138, 139syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
141140, 134rerpdivcld 12116 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
142141recnd 10280 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
143142abscld 14394 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
144137relogcld 24589 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℝ)
145143, 144remulcld 10282 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ)
146133, 145fsumrecl 14684 . . . . . 6 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ)
147132, 146remulcld 10282 . . . . 5 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ)
148147, 57readdcld 10281 . . . 4 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶) ∈ ℝ)
14920recnd 10280 . . . . . . . . . . 11 (𝜑 → (𝑅𝑍) ∈ ℂ)
150149abscld 14394 . . . . . . . . . 10 (𝜑 → (abs‘(𝑅𝑍)) ∈ ℝ)
151150recnd 10280 . . . . . . . . 9 (𝜑 → (abs‘(𝑅𝑍)) ∈ ℂ)
152151, 61mulcld 10272 . . . . . . . 8 (𝜑 → ((abs‘(𝑅𝑍)) · (log‘𝑍)) ∈ ℂ)
153132recnd 10280 . . . . . . . . 9 (𝜑 → (2 / (log‘𝑍)) ∈ ℂ)
154140recnd 10280 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℂ)
155154abscld 14394 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℝ)
156155, 144remulcld 10282 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
157133, 156fsumrecl 14684 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
158157recnd 10280 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
159153, 158mulcld 10272 . . . . . . . 8 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) ∈ ℂ)
16017rpcnd 12087 . . . . . . . 8 (𝜑𝑍 ∈ ℂ)
16117rpne0d 12090 . . . . . . . 8 (𝜑𝑍 ≠ 0)
162152, 159, 160, 161divsubdird 11052 . . . . . . 7 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) = ((((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) − (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍)))
163151, 61, 160, 161div23d 11050 . . . . . . . . 9 (𝜑 → (((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) = (((abs‘(𝑅𝑍)) / 𝑍) · (log‘𝑍)))
164149, 160, 161absdivd 14413 . . . . . . . . . . 11 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) = ((abs‘(𝑅𝑍)) / (abs‘𝑍)))
16517rprege0d 12092 . . . . . . . . . . . . 13 (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
166 absid 14255 . . . . . . . . . . . . 13 ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → (abs‘𝑍) = 𝑍)
167165, 166syl 17 . . . . . . . . . . . 12 (𝜑 → (abs‘𝑍) = 𝑍)
168167oveq2d 6830 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝑅𝑍)) / (abs‘𝑍)) = ((abs‘(𝑅𝑍)) / 𝑍))
169164, 168eqtrd 2794 . . . . . . . . . 10 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) = ((abs‘(𝑅𝑍)) / 𝑍))
170169oveq1d 6829 . . . . . . . . 9 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) = (((abs‘(𝑅𝑍)) / 𝑍) · (log‘𝑍)))
171163, 170eqtr4d 2797 . . . . . . . 8 (𝜑 → (((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) = ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)))
172153, 158, 160, 161divassd 11048 . . . . . . . . 9 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍) = ((2 / (log‘𝑍)) · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍)))
173160adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈ ℂ)
174161adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ≠ 0)
175154, 173, 174absdivd 14413 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / (abs‘𝑍)))
176167adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘𝑍) = 𝑍)
177176oveq2d 6830 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) / (abs‘𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍))
178175, 177eqtrd 2794 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍))
179178oveq1d 6829 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛)))
180155recnd 10280 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℂ)
181144recnd 10280 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℂ)
18217rpcnne0d 12094 . . . . . . . . . . . . . . 15 (𝜑 → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0))
183182adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0))
184 div23 10916 . . . . . . . . . . . . . 14 (((abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) → (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛)))
185180, 181, 183, 184syl3anc 1477 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛)))
186179, 185eqtr4d 2797 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
187186sumeq2dv 14652 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
188156recnd 10280 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
189133, 160, 188, 161fsumdivc 14737 . . . . . . . . . . 11 (𝜑 → (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
190187, 189eqtr4d 2797 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
191190oveq2d 6830 . . . . . . . . 9 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) = ((2 / (log‘𝑍)) · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍)))
192172, 191eqtr4d 2797 . . . . . . . 8 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
193171, 192oveq12d 6832 . . . . . . 7 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) − (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍)) = (((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
194162, 193eqtrd 2794 . . . . . 6 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) = (((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
195 fveq2 6353 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (𝑅𝑧) = (𝑅𝑍))
196195fveq2d 6357 . . . . . . . . . . 11 (𝑧 = 𝑍 → (abs‘(𝑅𝑧)) = (abs‘(𝑅𝑍)))
197 fveq2 6353 . . . . . . . . . . 11 (𝑧 = 𝑍 → (log‘𝑧) = (log‘𝑍))
198196, 197oveq12d 6832 . . . . . . . . . 10 (𝑧 = 𝑍 → ((abs‘(𝑅𝑧)) · (log‘𝑧)) = ((abs‘(𝑅𝑍)) · (log‘𝑍)))
199197oveq2d 6830 . . . . . . . . . . 11 (𝑧 = 𝑍 → (2 / (log‘𝑧)) = (2 / (log‘𝑍)))
200 oveq2 6822 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 → (𝑧 / 𝑖) = (𝑧 / 𝑛))
201200fveq2d 6357 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → (𝑅‘(𝑧 / 𝑖)) = (𝑅‘(𝑧 / 𝑛)))
202201fveq2d 6357 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (abs‘(𝑅‘(𝑧 / 𝑖))) = (abs‘(𝑅‘(𝑧 / 𝑛))))
203 fveq2 6353 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (log‘𝑖) = (log‘𝑛))
204202, 203oveq12d 6832 . . . . . . . . . . . . 13 (𝑖 = 𝑛 → ((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = ((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))
205204cbvsumv 14645 . . . . . . . . . . . 12 Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = Σ𝑛 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛))
206 oveq1 6821 . . . . . . . . . . . . . . 15 (𝑧 = 𝑍 → (𝑧 / 𝑌) = (𝑍 / 𝑌))
207206fveq2d 6357 . . . . . . . . . . . . . 14 (𝑧 = 𝑍 → (⌊‘(𝑧 / 𝑌)) = (⌊‘(𝑍 / 𝑌)))
208207oveq2d 6830 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → (1...(⌊‘(𝑧 / 𝑌))) = (1...(⌊‘(𝑍 / 𝑌))))
209 simpl 474 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑧 = 𝑍)
210209oveq1d 6829 . . . . . . . . . . . . . . . 16 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑧 / 𝑛) = (𝑍 / 𝑛))
211210fveq2d 6357 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑧 / 𝑛)) = (𝑅‘(𝑍 / 𝑛)))
212211fveq2d 6357 . . . . . . . . . . . . . 14 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑧 / 𝑛))) = (abs‘(𝑅‘(𝑍 / 𝑛))))
213212oveq1d 6829 . . . . . . . . . . . . 13 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))
214208, 213sumeq12rdv 14657 . . . . . . . . . . . 12 (𝑧 = 𝑍 → Σ𝑛 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))
215205, 214syl5eq 2806 . . . . . . . . . . 11 (𝑧 = 𝑍 → Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))
216199, 215oveq12d 6832 . . . . . . . . . 10 (𝑧 = 𝑍 → ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖))) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))))
217198, 216oveq12d 6832 . . . . . . . . 9 (𝑧 = 𝑍 → (((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) = (((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))))
218 id 22 . . . . . . . . 9 (𝑧 = 𝑍𝑧 = 𝑍)
219217, 218oveq12d 6832 . . . . . . . 8 (𝑧 = 𝑍 → ((((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) = ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍))
220219breq1d 4814 . . . . . . 7 (𝑧 = 𝑍 → (((((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) ≤ 𝐶 ↔ ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) ≤ 𝐶))
221 pntlem1.C . . . . . . 7 (𝜑 → ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) ≤ 𝐶)
222 1re 10251 . . . . . . . . 9 1 ∈ ℝ
223 rexr 10297 . . . . . . . . 9 (1 ∈ ℝ → 1 ∈ ℝ*)
224 elioopnf 12480 . . . . . . . . 9 (1 ∈ ℝ* → (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 < 𝑍)))
225222, 223, 224mp2b 10 . . . . . . . 8 (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 < 𝑍))
226128, 130, 225sylanbrc 701 . . . . . . 7 (𝜑𝑍 ∈ (1(,)+∞))
227220, 221, 226rspcdva 3455 . . . . . 6 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) ≤ 𝐶)
228194, 227eqbrtrrd 4828 . . . . 5 (𝜑 → (((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ 𝐶)
22925, 147, 57lesubadd2d 10838 . . . . 5 (𝜑 → ((((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ 𝐶 ↔ ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶)))
230228, 229mpbid 222 . . . 4 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶))
231 2cnd 11305 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
232143recnd 10280 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℂ)
233232, 181mulcld 10272 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℂ)
234133, 233fsumcl 14683 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℂ)
235131rpne0d 12090 . . . . . . 7 (𝜑 → (log‘𝑍) ≠ 0)
236231, 234, 61, 235div23d 11050 . . . . . 6 (𝜑 → ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) / (log‘𝑍)) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
23724resqcld 13249 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑍)↑2) ∈ ℝ)
23852, 237remulcld 10282 . . . . . . . . . . 11 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ)
23936, 238remulcld 10282 . . . . . . . . . 10 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ)
240 remulcl 10233 . . . . . . . . . 10 ((2 ∈ ℝ ∧ ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ) → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ∈ ℝ)
24131, 239, 240sylancr 698 . . . . . . . . 9 (𝜑 → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ∈ ℝ)
24230, 24remulcld 10282 . . . . . . . . 9 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) ∈ ℝ)
243 remulcl 10233 . . . . . . . . . 10 ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ) → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ)
24431, 146, 243sylancr 698 . . . . . . . . 9 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ)
24526adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑈 ∈ ℝ)
246245, 136nndivred 11281 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℝ)
247246, 143resubcld 10670 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
248247, 144remulcld 10282 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
249133, 248fsumrecl 14684 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
25032, 249remulcld 10282 . . . . . . . . . 10 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ∈ ℝ)
251242, 244resubcld 10670 . . . . . . . . . 10 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ∈ ℝ)
252 pntlem1.m . . . . . . . . . . . 12 𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)
253 pntlem1.n . . . . . . . . . . . 12 𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))
254 pntlem1.U . . . . . . . . . . . 12 (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)
255 pntlem1.K . . . . . . . . . . . 12 (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
2561, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 252, 253, 254, 255pntlemf 25514 . . . . . . . . . . 11 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
257 2pos 11324 . . . . . . . . . . . . 13 0 < 2
258257a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 < 2)
259 lemul2 11088 . . . . . . . . . . . 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‘𝑛)))))
260239, 249, 32, 258, 259syl112anc 1481 . . . . . . . . . . 11 (𝜑 → (((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
261256, 260mpbid 222 . . . . . . . . . 10 (𝜑 → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
262246recnd 10280 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℂ)
263262, 232, 181subdird 10699 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
264263sumeq2dv 14652 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
265246, 144remulcld 10282 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ)
266265recnd 10280 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℂ)
267133, 266, 233fsumsub 14739 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
268264, 267eqtrd 2794 . . . . . . . . . . . . 13 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
269268oveq2d 6830 . . . . . . . . . . . 12 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) = (2 · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
270133, 265fsumrecl 14684 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ)
271270recnd 10280 . . . . . . . . . . . . 13 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℂ)
272231, 271, 234subdid 10698 . . . . . . . . . . . 12 (𝜑 → (2 · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) = ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
273269, 272eqtrd 2794 . . . . . . . . . . 11 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) = ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
274 remulcl 10233 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ) → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ∈ ℝ)
27531, 270, 274sylancr 698 . . . . . . . . . . . 12 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ∈ ℝ)
2761, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 252, 253, 254, 255pntlemk 25515 . . . . . . . . . . . 12 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ≤ ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)))
277275, 242, 244, 276lesub1dd 10855 . . . . . . . . . . 11 (𝜑 → ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
278273, 277eqbrtrd 4826 . . . . . . . . . 10 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
279241, 250, 251, 261, 278letrd 10406 . . . . . . . . 9 (𝜑 → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
280241, 242, 244, 279lesubd 10843 . . . . . . . 8 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))))
28130recnd 10280 . . . . . . . . . 10 (𝜑 → (𝑈 · ((log‘𝑍) + 3)) ∈ ℂ)
28255recnd 10280 . . . . . . . . . 10 (𝜑 → (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ∈ ℂ)
283281, 282, 61subdird 10699 . . . . . . . . 9 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍))))
28454recnd 10280 . . . . . . . . . . . 12 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) ∈ ℂ)
285231, 284, 61mulassd 10275 . . . . . . . . . . 11 (𝜑 → ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍)) = (2 · ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍))))
28660, 61, 61mulassd 10275 . . . . . . . . . . . . 13 (𝜑 → ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍)) = (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍) · (log‘𝑍))))
28761sqvald 13219 . . . . . . . . . . . . . 14 (𝜑 → ((log‘𝑍)↑2) = ((log‘𝑍) · (log‘𝑍)))
288287oveq2d 6830 . . . . . . . . . . . . 13 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍)↑2)) = (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍) · (log‘𝑍))))
28951rpcnd 12087 . . . . . . . . . . . . . 14 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℂ)
290237recnd 10280 . . . . . . . . . . . . . 14 (𝜑 → ((log‘𝑍)↑2) ∈ ℂ)
291117, 289, 290mulassd 10275 . . . . . . . . . . . . 13 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍)↑2)) = ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))
292286, 288, 2913eqtr2d 2800 . . . . . . . . . . . 12 (𝜑 → ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍)) = ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))
293292oveq2d 6830 . . . . . . . . . . 11 (𝜑 → (2 · ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍))) = (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))))
294285, 293eqtrd 2794 . . . . . . . . . 10 (𝜑 → ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍)) = (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))))
295294oveq2d 6830 . . . . . . . . 9 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍))) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))))
296283, 295eqtrd 2794 . . . . . . . 8 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))))
297280, 296breqtrrd 4832 . . . . . . 7 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)))
298244, 56, 131ledivmul2d 12139 . . . . . . 7 (𝜑 → (((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) / (log‘𝑍)) ≤ ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) ↔ (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍))))
299297, 298mpbird 247 . . . . . 6 (𝜑 → ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) / (log‘𝑍)) ≤ ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
300236, 299eqbrtrrd 4828 . . . . 5 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
301147, 56, 57, 300leadd1dd 10853 . . . 4 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶))
30225, 148, 58, 230, 301letrd 10406 . . 3 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶))
303 remulcl 10233 . . . . . . . . 9 ((𝑈 ∈ ℝ ∧ 3 ∈ ℝ) → (𝑈 · 3) ∈ ℝ)
30426, 27, 303sylancl 697 . . . . . . . 8 (𝜑 → (𝑈 · 3) ∈ ℝ)
305304, 57readdcld 10281 . . . . . . 7 (𝜑 → ((𝑈 · 3) + 𝐶) ∈ ℝ)
30616simp3d 1139 . . . . . . . 8 (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
307306simp3d 1139 . . . . . . 7 (𝜑 → ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))
308305, 54, 125, 307leadd2dd 10854 . . . . . 6 (𝜑 → ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶)) ≤ ((𝑈 · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
30928recnd 10280 . . . . . . . . 9 (𝜑 → 3 ∈ ℂ)
31059, 61, 309adddid 10276 . . . . . . . 8 (𝜑 → (𝑈 · ((log‘𝑍) + 3)) = ((𝑈 · (log‘𝑍)) + (𝑈 · 3)))
311310oveq1d 6829 . . . . . . 7 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) = (((𝑈 · (log‘𝑍)) + (𝑈 · 3)) + 𝐶))
312125recnd 10280 . . . . . . . 8 (𝜑 → (𝑈 · (log‘𝑍)) ∈ ℂ)
31359, 309mulcld 10272 . . . . . . . 8 (𝜑 → (𝑈 · 3) ∈ ℂ)
31413rpcnd 12087 . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
315312, 313, 314addassd 10274 . . . . . . 7 (𝜑 → (((𝑈 · (log‘𝑍)) + (𝑈 · 3)) + 𝐶) = ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶)))
316311, 315eqtrd 2794 . . . . . 6 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) = ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶)))
3172842timesd 11487 . . . . . . . 8 (𝜑 → (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) = ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
318317oveq2d 6830 . . . . . . 7 (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
319312, 284, 284nppcan3d 10631 . . . . . . 7 (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = ((𝑈 · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
320318, 319eqtrd 2794 . . . . . 6 (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = ((𝑈 · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
321308, 316, 3203brtr4d 4836 . . . . 5 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ≤ (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
32230, 57readdcld 10281 . . . . . 6 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ∈ ℝ)
323322, 55, 126lesubaddd 10836 . . . . 5 (𝜑 → ((((𝑈 · ((log‘𝑍) + 3)) + 𝐶) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) ≤ ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ↔ ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ≤ (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))))
324321, 323mpbird 247 . . . 4 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) + 𝐶) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) ≤ ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
325281, 314, 282addsubd 10625 . . . 4 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) + 𝐶) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶))
326324, 325, 1243brtr3d 4835 . . 3 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
32725, 58, 127, 302, 326letrd 10406 . 2 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
328 3z 11622 . . . . . . 7 3 ∈ ℤ
329 rpexpcl 13093 . . . . . . 7 ((𝑈 ∈ ℝ+ ∧ 3 ∈ ℤ) → (𝑈↑3) ∈ ℝ+)
3307, 328, 329sylancl 697 . . . . . 6 (𝜑 → (𝑈↑3) ∈ ℝ+)
33196, 330rpmulcld 12101 . . . . 5 (𝜑 → (𝐹 · (𝑈↑3)) ∈ ℝ+)
332331rpred 12085 . . . 4 (𝜑 → (𝐹 · (𝑈↑3)) ∈ ℝ)
33326, 332resubcld 10670 . . 3 (𝜑 → (𝑈 − (𝐹 · (𝑈↑3))) ∈ ℝ)
33423, 333, 131lemul1d 12128 . 2 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) ≤ (𝑈 − (𝐹 · (𝑈↑3))) ↔ ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍))))
335327, 334mpbird 247 1 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) ≤ (𝑈 − (𝐹 · (𝑈↑3))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051   class class class wbr 4804  cmpt 4881  cfv 6049  (class class class)co 6814  cc 10146  cr 10147  0cc0 10148  1c1 10149   + caddc 10151   · cmul 10153  +∞cpnf 10283  *cxr 10285   < clt 10286  cle 10287  cmin 10478   / cdiv 10896  cn 11232  2c2 11282  3c3 11283  4c4 11284  0cn0 11504  cz 11589  cdc 11705  +crp 12045  (,)cioo 12388  [,)cico 12390  [,]cicc 12391  ...cfz 12539  cfl 12805  cexp 13074  csqrt 14192  abscabs 14193  Σcsu 14635  expce 15011  eceu 15012  logclog 24521  ψcchp 25039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-inf2 8713  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226  ax-addf 10227  ax-mulf 10228
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-of 7063  df-om 7232  df-1st 7334  df-2nd 7335  df-supp 7465  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-2o 7731  df-oadd 7734  df-er 7913  df-map 8027  df-pm 8028  df-ixp 8077  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-fsupp 8443  df-fi 8484  df-sup 8515  df-inf 8516  df-oi 8582  df-card 8975  df-cda 9202  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-5 11294  df-6 11295  df-7 11296  df-8 11297  df-9 11298  df-n0 11505  df-z 11590  df-dec 11706  df-uz 11900  df-q 12002  df-rp 12046  df-xneg 12159  df-xadd 12160  df-xmul 12161  df-ioo 12392  df-ioc 12393  df-ico 12394  df-icc 12395  df-fz 12540  df-fzo 12680  df-fl 12807  df-mod 12883  df-seq 13016  df-exp 13075  df-fac 13275  df-bc 13304  df-hash 13332  df-shft 14026  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-limsup 14421  df-clim 14438  df-rlim 14439  df-sum 14636  df-ef 15017  df-e 15018  df-sin 15019  df-cos 15020  df-pi 15022  df-dvds 15203  df-gcd 15439  df-prm 15608  df-pc 15764  df-struct 16081  df-ndx 16082  df-slot 16083  df-base 16085  df-sets 16086  df-ress 16087  df-plusg 16176  df-mulr 16177  df-starv 16178  df-sca 16179  df-vsca 16180  df-ip 16181  df-tset 16182  df-ple 16183  df-ds 16186  df-unif 16187  df-hom 16188  df-cco 16189  df-rest 16305  df-topn 16306  df-0g 16324  df-gsum 16325  df-topgen 16326  df-pt 16327  df-prds 16330  df-xrs 16384  df-qtop 16389  df-imas 16390  df-xps 16392  df-mre 16468  df-mrc 16469  df-acs 16471  df-mgm 17463  df-sgrp 17505  df-mnd 17516  df-submnd 17557  df-mulg 17762  df-cntz 17970  df-cmn 18415  df-psmet 19960  df-xmet 19961  df-met 19962  df-bl 19963  df-mopn 19964  df-fbas 19965  df-fg 19966  df-cnfld 19969  df-top 20921  df-topon 20938  df-topsp 20959  df-bases 20972  df-cld 21045  df-ntr 21046  df-cls 21047  df-nei 21124  df-lp 21162  df-perf 21163  df-cn 21253  df-cnp 21254  df-haus 21341  df-tx 21587  df-hmeo 21780  df-fil 21871  df-fm 21963  df-flim 21964  df-flf 21965  df-xms 22346  df-ms 22347  df-tms 22348  df-cncf 22902  df-limc 23849  df-dv 23850  df-log 24523  df-em 24939  df-vma 25044  df-chp 25045
This theorem is referenced by:  pntleme  25517
  Copyright terms: Public domain W3C validator