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

Theorem pntlemo 25341
 Description: Lemma for pnt 25348. 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 25331 . . . . . . . . 9 (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
1716simp1d 1093 . . . . . . . 8 (𝜑𝑍 ∈ ℝ+)
181pntrf 25297 . . . . . . . . 9 𝑅:ℝ+⟶ℝ
1918ffvelrni 6398 . . . . . . . 8 (𝑍 ∈ ℝ+ → (𝑅𝑍) ∈ ℝ)
2017, 19syl 17 . . . . . . 7 (𝜑 → (𝑅𝑍) ∈ ℝ)
2120, 17rerpdivcld 11941 . . . . . 6 (𝜑 → ((𝑅𝑍) / 𝑍) ∈ ℝ)
2221recnd 10106 . . . . 5 (𝜑 → ((𝑅𝑍) / 𝑍) ∈ ℂ)
2322abscld 14219 . . . 4 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) ∈ ℝ)
2417relogcld 24414 . . . 4 (𝜑 → (log‘𝑍) ∈ ℝ)
2523, 24remulcld 10108 . . 3 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ∈ ℝ)
267rpred 11910 . . . . . 6 (𝜑𝑈 ∈ ℝ)
27 3re 11132 . . . . . . . 8 3 ∈ ℝ
2827a1i 11 . . . . . . 7 (𝜑 → 3 ∈ ℝ)
2924, 28readdcld 10107 . . . . . 6 (𝜑 → ((log‘𝑍) + 3) ∈ ℝ)
3026, 29remulcld 10108 . . . . 5 (𝜑 → (𝑈 · ((log‘𝑍) + 3)) ∈ ℝ)
31 2re 11128 . . . . . . 7 2 ∈ ℝ
3231a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℝ)
331, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 25329 . . . . . . . . . . 11 (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))
3433simp3d 1095 . . . . . . . . . 10 (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+))
3534simp3d 1095 . . . . . . . . 9 (𝜑 → (𝑈𝐸) ∈ ℝ+)
3635rpred 11910 . . . . . . . 8 (𝜑 → (𝑈𝐸) ∈ ℝ)
371, 2, 3, 4, 5, 6pntlemd 25328 . . . . . . . . . . . 12 (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))
3837simp1d 1093 . . . . . . . . . . 11 (𝜑𝐿 ∈ ℝ+)
3933simp1d 1093 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℝ+)
40 2z 11447 . . . . . . . . . . . 12 2 ∈ ℤ
41 rpexpcl 12919 . . . . . . . . . . . 12 ((𝐸 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝐸↑2) ∈ ℝ+)
4239, 40, 41sylancl 695 . . . . . . . . . . 11 (𝜑 → (𝐸↑2) ∈ ℝ+)
4338, 42rpmulcld 11926 . . . . . . . . . 10 (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℝ+)
44 3nn0 11348 . . . . . . . . . . . . 13 3 ∈ ℕ0
45 2nn 11223 . . . . . . . . . . . . 13 2 ∈ ℕ
4644, 45decnncl 11556 . . . . . . . . . . . 12 32 ∈ ℕ
47 nnrp 11880 . . . . . . . . . . . 12 (32 ∈ ℕ → 32 ∈ ℝ+)
4846, 47ax-mp 5 . . . . . . . . . . 11 32 ∈ ℝ+
49 rpmulcl 11893 . . . . . . . . . . 11 ((32 ∈ ℝ+𝐵 ∈ ℝ+) → (32 · 𝐵) ∈ ℝ+)
5048, 3, 49sylancr 696 . . . . . . . . . 10 (𝜑 → (32 · 𝐵) ∈ ℝ+)
5143, 50rpdivcld 11927 . . . . . . . . 9 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℝ+)
5251rpred 11910 . . . . . . . 8 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℝ)
5336, 52remulcld 10108 . . . . . . 7 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) ∈ ℝ)
5453, 24remulcld 10108 . . . . . 6 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) ∈ ℝ)
5532, 54remulcld 10108 . . . . 5 (𝜑 → (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ∈ ℝ)
5630, 55resubcld 10496 . . . 4 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) ∈ ℝ)
5713rpred 11910 . . . 4 (𝜑𝐶 ∈ ℝ)
5856, 57readdcld 10107 . . 3 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶) ∈ ℝ)
597rpcnd 11912 . . . . . 6 (𝜑𝑈 ∈ ℂ)
6053recnd 10106 . . . . . 6 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) ∈ ℂ)
6124recnd 10106 . . . . . 6 (𝜑 → (log‘𝑍) ∈ ℂ)
6259, 60, 61subdird 10525 . . . . 5 (𝜑 → ((𝑈 − ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵)))) · (log‘𝑍)) = ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
6338rpcnd 11912 . . . . . . . . . . 11 (𝜑𝐿 ∈ ℂ)
6442rpcnd 11912 . . . . . . . . . . 11 (𝜑 → (𝐸↑2) ∈ ℂ)
6550rpcnne0d 11919 . . . . . . . . . . 11 (𝜑 → ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0))
66 div23 10742 . . . . . . . . . . 11 ((𝐿 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ ((32 · 𝐵) ∈ ℂ ∧ (32 · 𝐵) ≠ 0)) → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) = ((𝐿 / (32 · 𝐵)) · (𝐸↑2)))
6763, 64, 65, 66syl3anc 1366 . . . . . . . . . 10 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) = ((𝐿 / (32 · 𝐵)) · (𝐸↑2)))
689oveq1i 6700 . . . . . . . . . . . 12 (𝐸↑2) = ((𝑈 / 𝐷)↑2)
6937simp2d 1094 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ ℝ+)
7069rpcnd 11912 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ ℂ)
7169rpne0d 11915 . . . . . . . . . . . . 13 (𝜑𝐷 ≠ 0)
7259, 70, 71sqdivd 13061 . . . . . . . . . . . 12 (𝜑 → ((𝑈 / 𝐷)↑2) = ((𝑈↑2) / (𝐷↑2)))
7368, 72syl5eq 2697 . . . . . . . . . . 11 (𝜑 → (𝐸↑2) = ((𝑈↑2) / (𝐷↑2)))
7473oveq2d 6706 . . . . . . . . . 10 (𝜑 → ((𝐿 / (32 · 𝐵)) · (𝐸↑2)) = ((𝐿 / (32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))))
7538, 50rpdivcld 11927 . . . . . . . . . . . 12 (𝜑 → (𝐿 / (32 · 𝐵)) ∈ ℝ+)
7675rpcnd 11912 . . . . . . . . . . 11 (𝜑 → (𝐿 / (32 · 𝐵)) ∈ ℂ)
7759sqcld 13046 . . . . . . . . . . 11 (𝜑 → (𝑈↑2) ∈ ℂ)
78 rpexpcl 12919 . . . . . . . . . . . . 13 ((𝐷 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝐷↑2) ∈ ℝ+)
7969, 40, 78sylancl 695 . . . . . . . . . . . 12 (𝜑 → (𝐷↑2) ∈ ℝ+)
8079rpcnne0d 11919 . . . . . . . . . . 11 (𝜑 → ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0))
81 divass 10741 . . . . . . . . . . . 12 (((𝐿 / (32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0)) → (((𝐿 / (32 · 𝐵)) · (𝑈↑2)) / (𝐷↑2)) = ((𝐿 / (32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))))
82 div23 10742 . . . . . . . . . . . 12 (((𝐿 / (32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0)) → (((𝐿 / (32 · 𝐵)) · (𝑈↑2)) / (𝐷↑2)) = (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))
8381, 82eqtr3d 2687 . . . . . . . . . . 11 (((𝐿 / (32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠ 0)) → ((𝐿 / (32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))) = (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))
8476, 77, 80, 83syl3anc 1366 . . . . . . . . . 10 (𝜑 → ((𝐿 / (32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))) = (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))
8567, 74, 843eqtrd 2689 . . . . . . . . 9 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) = (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))
8685oveq2d 6706 . . . . . . . 8 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
87 df-3 11118 . . . . . . . . . . . . 13 3 = (2 + 1)
8887oveq2i 6701 . . . . . . . . . . . 12 (𝑈↑3) = (𝑈↑(2 + 1))
89 2nn0 11347 . . . . . . . . . . . . 13 2 ∈ ℕ0
90 expp1 12907 . . . . . . . . . . . . 13 ((𝑈 ∈ ℂ ∧ 2 ∈ ℕ0) → (𝑈↑(2 + 1)) = ((𝑈↑2) · 𝑈))
9159, 89, 90sylancl 695 . . . . . . . . . . . 12 (𝜑 → (𝑈↑(2 + 1)) = ((𝑈↑2) · 𝑈))
9288, 91syl5eq 2697 . . . . . . . . . . 11 (𝜑 → (𝑈↑3) = ((𝑈↑2) · 𝑈))
9377, 59mulcomd 10099 . . . . . . . . . . 11 (𝜑 → ((𝑈↑2) · 𝑈) = (𝑈 · (𝑈↑2)))
9492, 93eqtrd 2685 . . . . . . . . . 10 (𝜑 → (𝑈↑3) = (𝑈 · (𝑈↑2)))
9594oveq2d 6706 . . . . . . . . 9 (𝜑 → (𝐹 · (𝑈↑3)) = (𝐹 · (𝑈 · (𝑈↑2))))
9637simp3d 1095 . . . . . . . . . . 11 (𝜑𝐹 ∈ ℝ+)
9796rpcnd 11912 . . . . . . . . . 10 (𝜑𝐹 ∈ ℂ)
9897, 59, 77mulassd 10101 . . . . . . . . 9 (𝜑 → ((𝐹 · 𝑈) · (𝑈↑2)) = (𝐹 · (𝑈 · (𝑈↑2))))
99 1cnd 10094 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
10069rpreccld 11920 . . . . . . . . . . . . . . . 16 (𝜑 → (1 / 𝐷) ∈ ℝ+)
101100rpcnd 11912 . . . . . . . . . . . . . . 15 (𝜑 → (1 / 𝐷) ∈ ℂ)
10299, 101, 59subdird 10525 . . . . . . . . . . . . . 14 (𝜑 → ((1 − (1 / 𝐷)) · 𝑈) = ((1 · 𝑈) − ((1 / 𝐷) · 𝑈)))
10359mulid2d 10096 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝑈) = 𝑈)
10459, 70, 71divrec2d 10843 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑈 / 𝐷) = ((1 / 𝐷) · 𝑈))
1059, 104syl5req 2698 . . . . . . . . . . . . . . 15 (𝜑 → ((1 / 𝐷) · 𝑈) = 𝐸)
106103, 105oveq12d 6708 . . . . . . . . . . . . . 14 (𝜑 → ((1 · 𝑈) − ((1 / 𝐷) · 𝑈)) = (𝑈𝐸))
107102, 106eqtr2d 2686 . . . . . . . . . . . . 13 (𝜑 → (𝑈𝐸) = ((1 − (1 / 𝐷)) · 𝑈))
108107oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → ((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))))
1096oveq1i 6700 . . . . . . . . . . . . 13 (𝐹 · 𝑈) = (((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · 𝑈)
11099, 101subcld 10430 . . . . . . . . . . . . . 14 (𝜑 → (1 − (1 / 𝐷)) ∈ ℂ)
11175, 79rpdivcld 11927 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐿 / (32 · 𝐵)) / (𝐷↑2)) ∈ ℝ+)
112111rpcnd 11912 . . . . . . . . . . . . . 14 (𝜑 → ((𝐿 / (32 · 𝐵)) / (𝐷↑2)) ∈ ℂ)
113110, 112, 59mul32d 10284 . . . . . . . . . . . . 13 (𝜑 → (((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · 𝑈) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))))
114109, 113syl5eq 2697 . . . . . . . . . . . 12 (𝜑 → (𝐹 · 𝑈) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))))
115108, 114eqtr4d 2688 . . . . . . . . . . 11 (𝜑 → ((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) = (𝐹 · 𝑈))
116115oveq1d 6705 . . . . . . . . . 10 (𝜑 → (((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · (𝑈↑2)) = ((𝐹 · 𝑈) · (𝑈↑2)))
11735rpcnd 11912 . . . . . . . . . . 11 (𝜑 → (𝑈𝐸) ∈ ℂ)
118117, 112, 77mulassd 10101 . . . . . . . . . 10 (𝜑 → (((𝑈𝐸) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2))) · (𝑈↑2)) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
119116, 118eqtr3d 2687 . . . . . . . . 9 (𝜑 → ((𝐹 · 𝑈) · (𝑈↑2)) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
12095, 98, 1193eqtr2d 2691 . . . . . . . 8 (𝜑 → (𝐹 · (𝑈↑3)) = ((𝑈𝐸) · (((𝐿 / (32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))))
12186, 120eqtr4d 2688 . . . . . . 7 (𝜑 → ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) = (𝐹 · (𝑈↑3)))
122121oveq2d 6706 . . . . . 6 (𝜑 → (𝑈 − ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵)))) = (𝑈 − (𝐹 · (𝑈↑3))))
123122oveq1d 6705 . . . . 5 (𝜑 → ((𝑈 − ((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵)))) · (log‘𝑍)) = ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
12462, 123eqtr3d 2687 . . . 4 (𝜑 → ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) = ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
12526, 24remulcld 10108 . . . . 5 (𝜑 → (𝑈 · (log‘𝑍)) ∈ ℝ)
126125, 54resubcld 10496 . . . 4 (𝜑 → ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ∈ ℝ)
127124, 126eqeltrrd 2731 . . 3 (𝜑 → ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)) ∈ ℝ)
12817rpred 11910 . . . . . . . 8 (𝜑𝑍 ∈ ℝ)
12916simp2d 1094 . . . . . . . . 9 (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
130129simp1d 1093 . . . . . . . 8 (𝜑 → 1 < 𝑍)
131128, 130rplogcld 24420 . . . . . . 7 (𝜑 → (log‘𝑍) ∈ ℝ+)
13232, 131rerpdivcld 11941 . . . . . 6 (𝜑 → (2 / (log‘𝑍)) ∈ ℝ)
133 fzfid 12812 . . . . . . 7 (𝜑 → (1...(⌊‘(𝑍 / 𝑌))) ∈ Fin)
13417adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈ ℝ+)
135 elfznn 12408 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌))) → 𝑛 ∈ ℕ)
136135adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℕ)
137136nnrpd 11908 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℝ+)
138134, 137rpdivcld 11927 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 / 𝑛) ∈ ℝ+)
13918ffvelrni 6398 . . . . . . . . . . . 12 ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
140138, 139syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ)
141140, 134rerpdivcld 11941 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ)
142141recnd 10106 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ)
143142abscld 14219 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ)
144137relogcld 24414 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℝ)
145143, 144remulcld 10108 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ)
146133, 145fsumrecl 14509 . . . . . 6 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ)
147132, 146remulcld 10108 . . . . 5 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ)
148147, 57readdcld 10107 . . . 4 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶) ∈ ℝ)
14920recnd 10106 . . . . . . . . . . 11 (𝜑 → (𝑅𝑍) ∈ ℂ)
150149abscld 14219 . . . . . . . . . 10 (𝜑 → (abs‘(𝑅𝑍)) ∈ ℝ)
151150recnd 10106 . . . . . . . . 9 (𝜑 → (abs‘(𝑅𝑍)) ∈ ℂ)
152151, 61mulcld 10098 . . . . . . . 8 (𝜑 → ((abs‘(𝑅𝑍)) · (log‘𝑍)) ∈ ℂ)
153132recnd 10106 . . . . . . . . 9 (𝜑 → (2 / (log‘𝑍)) ∈ ℂ)
154140recnd 10106 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℂ)
155154abscld 14219 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℝ)
156155, 144remulcld 10108 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
157133, 156fsumrecl 14509 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
158157recnd 10106 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
159153, 158mulcld 10098 . . . . . . . 8 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) ∈ ℂ)
16017rpcnd 11912 . . . . . . . 8 (𝜑𝑍 ∈ ℂ)
16117rpne0d 11915 . . . . . . . 8 (𝜑𝑍 ≠ 0)
162152, 159, 160, 161divsubdird 10878 . . . . . . 7 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) = ((((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) − (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍)))
163151, 61, 160, 161div23d 10876 . . . . . . . . 9 (𝜑 → (((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) = (((abs‘(𝑅𝑍)) / 𝑍) · (log‘𝑍)))
164149, 160, 161absdivd 14238 . . . . . . . . . . 11 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) = ((abs‘(𝑅𝑍)) / (abs‘𝑍)))
16517rprege0d 11917 . . . . . . . . . . . . 13 (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
166 absid 14080 . . . . . . . . . . . . 13 ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → (abs‘𝑍) = 𝑍)
167165, 166syl 17 . . . . . . . . . . . 12 (𝜑 → (abs‘𝑍) = 𝑍)
168167oveq2d 6706 . . . . . . . . . . 11 (𝜑 → ((abs‘(𝑅𝑍)) / (abs‘𝑍)) = ((abs‘(𝑅𝑍)) / 𝑍))
169164, 168eqtrd 2685 . . . . . . . . . 10 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) = ((abs‘(𝑅𝑍)) / 𝑍))
170169oveq1d 6705 . . . . . . . . 9 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) = (((abs‘(𝑅𝑍)) / 𝑍) · (log‘𝑍)))
171163, 170eqtr4d 2688 . . . . . . . 8 (𝜑 → (((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) = ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)))
172153, 158, 160, 161divassd 10874 . . . . . . . . 9 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍) = ((2 / (log‘𝑍)) · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍)))
173160adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈ ℂ)
174161adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ≠ 0)
175154, 173, 174absdivd 14238 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / (abs‘𝑍)))
176167adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘𝑍) = 𝑍)
177176oveq2d 6706 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) / (abs‘𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍))
178175, 177eqtrd 2685 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍))
179178oveq1d 6705 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛)))
180155recnd 10106 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℂ)
181144recnd 10106 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℂ)
18217rpcnne0d 11919 . . . . . . . . . . . . . . 15 (𝜑 → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0))
183182adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0))
184 div23 10742 . . . . . . . . . . . . . 14 (((abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) → (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛)))
185180, 181, 183, 184syl3anc 1366 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛)))
186179, 185eqtr4d 2688 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
187186sumeq2dv 14477 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
188156recnd 10106 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
189133, 160, 188, 161fsumdivc 14562 . . . . . . . . . . 11 (𝜑 → (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
190187, 189eqtr4d 2688 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))
191190oveq2d 6706 . . . . . . . . 9 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) = ((2 / (log‘𝑍)) · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍)))
192172, 191eqtr4d 2688 . . . . . . . 8 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
193171, 192oveq12d 6708 . . . . . . 7 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) / 𝑍) − (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍)) = (((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
194162, 193eqtrd 2685 . . . . . 6 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) = (((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
195 1re 10077 . . . . . . . . 9 1 ∈ ℝ
196 rexr 10123 . . . . . . . . 9 (1 ∈ ℝ → 1 ∈ ℝ*)
197 elioopnf 12305 . . . . . . . . 9 (1 ∈ ℝ* → (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 < 𝑍)))
198195, 196, 197mp2b 10 . . . . . . . 8 (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 < 𝑍))
199128, 130, 198sylanbrc 699 . . . . . . 7 (𝜑𝑍 ∈ (1(,)+∞))
200 pntlem1.C . . . . . . 7 (𝜑 → ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) ≤ 𝐶)
201 fveq2 6229 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → (𝑅𝑧) = (𝑅𝑍))
202201fveq2d 6233 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (abs‘(𝑅𝑧)) = (abs‘(𝑅𝑍)))
203 fveq2 6229 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (log‘𝑧) = (log‘𝑍))
204202, 203oveq12d 6708 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((abs‘(𝑅𝑧)) · (log‘𝑧)) = ((abs‘(𝑅𝑍)) · (log‘𝑍)))
205203oveq2d 6706 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (2 / (log‘𝑧)) = (2 / (log‘𝑍)))
206 oveq2 6698 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑛 → (𝑧 / 𝑖) = (𝑧 / 𝑛))
207206fveq2d 6233 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 → (𝑅‘(𝑧 / 𝑖)) = (𝑅‘(𝑧 / 𝑛)))
208207fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → (abs‘(𝑅‘(𝑧 / 𝑖))) = (abs‘(𝑅‘(𝑧 / 𝑛))))
209 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → (log‘𝑖) = (log‘𝑛))
210208, 209oveq12d 6708 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → ((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = ((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)))
211210cbvsumv 14470 . . . . . . . . . . . . 13 Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = Σ𝑛 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛))
212 oveq1 6697 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑍 → (𝑧 / 𝑌) = (𝑍 / 𝑌))
213212fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑧 = 𝑍 → (⌊‘(𝑧 / 𝑌)) = (⌊‘(𝑍 / 𝑌)))
214213oveq2d 6706 . . . . . . . . . . . . . 14 (𝑧 = 𝑍 → (1...(⌊‘(𝑧 / 𝑌))) = (1...(⌊‘(𝑍 / 𝑌))))
215 simpl 472 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑧 = 𝑍)
216215oveq1d 6705 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑧 / 𝑛) = (𝑍 / 𝑛))
217216fveq2d 6233 . . . . . . . . . . . . . . . 16 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑧 / 𝑛)) = (𝑅‘(𝑍 / 𝑛)))
218217fveq2d 6233 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑧 / 𝑛))) = (abs‘(𝑅‘(𝑍 / 𝑛))))
219218oveq1d 6705 . . . . . . . . . . . . . 14 ((𝑧 = 𝑍𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))
220214, 219sumeq12rdv 14482 . . . . . . . . . . . . 13 (𝑧 = 𝑍 → Σ𝑛 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))
221211, 220syl5eq 2697 . . . . . . . . . . . 12 (𝑧 = 𝑍 → Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))
222205, 221oveq12d 6708 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖))) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))))
223204, 222oveq12d 6708 . . . . . . . . . 10 (𝑧 = 𝑍 → (((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) = (((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))))
224 id 22 . . . . . . . . . 10 (𝑧 = 𝑍𝑧 = 𝑍)
225223, 224oveq12d 6708 . . . . . . . . 9 (𝑧 = 𝑍 → ((((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) = ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍))
226225breq1d 4695 . . . . . . . 8 (𝑧 = 𝑍 → (((((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) ≤ 𝐶 ↔ ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) ≤ 𝐶))
227226rspcv 3336 . . . . . . 7 (𝑍 ∈ (1(,)+∞) → (∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) ≤ 𝐶 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) ≤ 𝐶))
228199, 200, 227sylc 65 . . . . . 6 (𝜑 → ((((abs‘(𝑅𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) ≤ 𝐶)
229194, 228eqbrtrrd 4709 . . . . 5 (𝜑 → (((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ 𝐶)
23025, 147, 57lesubadd2d 10664 . . . . 5 (𝜑 → ((((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ 𝐶 ↔ ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶)))
231229, 230mpbid 222 . . . 4 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶))
232 2cnd 11131 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
233143recnd 10106 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℂ)
234233, 181mulcld 10098 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℂ)
235133, 234fsumcl 14508 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℂ)
236131rpne0d 11915 . . . . . . 7 (𝜑 → (log‘𝑍) ≠ 0)
237232, 235, 61, 236div23d 10876 . . . . . 6 (𝜑 → ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) / (log‘𝑍)) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
23824resqcld 13075 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑍)↑2) ∈ ℝ)
23952, 238remulcld 10108 . . . . . . . . . . 11 (𝜑 → (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ)
24036, 239remulcld 10108 . . . . . . . . . 10 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ)
241 remulcl 10059 . . . . . . . . . 10 ((2 ∈ ℝ ∧ ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ) → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ∈ ℝ)
24231, 240, 241sylancr 696 . . . . . . . . 9 (𝜑 → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ∈ ℝ)
24330, 24remulcld 10108 . . . . . . . . 9 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) ∈ ℝ)
244 remulcl 10059 . . . . . . . . . 10 ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ) → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ)
24531, 146, 244sylancr 696 . . . . . . . . 9 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ)
24626adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑈 ∈ ℝ)
247246, 136nndivred 11107 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℝ)
248247, 143resubcld 10496 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ)
249248, 144remulcld 10108 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
250133, 249fsumrecl 14509 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ)
25132, 250remulcld 10108 . . . . . . . . . 10 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ∈ ℝ)
252243, 245resubcld 10496 . . . . . . . . . 10 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ∈ ℝ)
253 pntlem1.m . . . . . . . . . . . 12 𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)
254 pntlem1.n . . . . . . . . . . . 12 𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))
255 pntlem1.U . . . . . . . . . . . 12 (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)
256 pntlem1.K . . . . . . . . . . . 12 (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
2571, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 253, 254, 255, 256pntlemf 25339 . . . . . . . . . . 11 (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))
258 2pos 11150 . . . . . . . . . . . . 13 0 < 2
259258a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 < 2)
260 lemul2 10914 . . . . . . . . . . . 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‘𝑛)))))
261240, 250, 32, 259, 260syl112anc 1370 . . . . . . . . . . 11 (𝜑 → (((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))))
262257, 261mpbid 222 . . . . . . . . . 10 (𝜑 → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))
263247recnd 10106 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℂ)
264263, 233, 181subdird 10525 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
265264sumeq2dv 14477 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
266247, 144remulcld 10108 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ)
267266recnd 10106 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℂ)
268133, 267, 234fsumsub 14564 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
269265, 268eqtrd 2685 . . . . . . . . . . . . 13 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))
270269oveq2d 6706 . . . . . . . . . . . 12 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) = (2 · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
271133, 266fsumrecl 14509 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ)
272271recnd 10106 . . . . . . . . . . . . 13 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℂ)
273232, 272, 235subdid 10524 . . . . . . . . . . . 12 (𝜑 → (2 · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) = ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
274270, 273eqtrd 2685 . . . . . . . . . . 11 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) = ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
275 remulcl 10059 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ) → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ∈ ℝ)
27631, 271, 275sylancr 696 . . . . . . . . . . . 12 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ∈ ℝ)
2771, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 253, 254, 255, 256pntlemk 25340 . . . . . . . . . . . 12 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ≤ ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)))
278276, 243, 245, 277lesub1dd 10681 . . . . . . . . . . 11 (𝜑 → ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
279274, 278eqbrtrd 4707 . . . . . . . . . 10 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
280242, 251, 252, 262, 279letrd 10232 . . . . . . . . 9 (𝜑 → (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))))
281242, 243, 245, 280lesubd 10669 . . . . . . . 8 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))))
28230recnd 10106 . . . . . . . . . 10 (𝜑 → (𝑈 · ((log‘𝑍) + 3)) ∈ ℂ)
28355recnd 10106 . . . . . . . . . 10 (𝜑 → (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ∈ ℂ)
284282, 283, 61subdird 10525 . . . . . . . . 9 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍))))
28554recnd 10106 . . . . . . . . . . . 12 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) ∈ ℂ)
286232, 285, 61mulassd 10101 . . . . . . . . . . 11 (𝜑 → ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍)) = (2 · ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍))))
28760, 61, 61mulassd 10101 . . . . . . . . . . . . 13 (𝜑 → ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍)) = (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍) · (log‘𝑍))))
28861sqvald 13045 . . . . . . . . . . . . . 14 (𝜑 → ((log‘𝑍)↑2) = ((log‘𝑍) · (log‘𝑍)))
289288oveq2d 6706 . . . . . . . . . . . . 13 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍)↑2)) = (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍) · (log‘𝑍))))
29051rpcnd 11912 . . . . . . . . . . . . . 14 (𝜑 → ((𝐿 · (𝐸↑2)) / (32 · 𝐵)) ∈ ℂ)
291238recnd 10106 . . . . . . . . . . . . . 14 (𝜑 → ((log‘𝑍)↑2) ∈ ℂ)
292117, 290, 291mulassd 10101 . . . . . . . . . . . . 13 (𝜑 → (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · ((log‘𝑍)↑2)) = ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))
293287, 289, 2923eqtr2d 2691 . . . . . . . . . . . 12 (𝜑 → ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍)) = ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))
294293oveq2d 6706 . . . . . . . . . . 11 (𝜑 → (2 · ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍))) = (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))))
295286, 294eqtrd 2685 . . . . . . . . . 10 (𝜑 → ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍)) = (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2)))))
296295oveq2d 6706 . . . . . . . . 9 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − ((2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍))) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))))
297284, 296eqtrd 2685 . . . . . . . 8 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))))))
298281, 297breqtrrd 4713 . . . . . . 7 (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)))
299245, 56, 131ledivmul2d 11964 . . . . . . 7 (𝜑 → (((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) / (log‘𝑍)) ≤ ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) ↔ (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍))))
300298, 299mpbird 247 . . . . . 6 (𝜑 → ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) / (log‘𝑍)) ≤ ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
301237, 300eqbrtrrd 4709 . . . . 5 (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
302147, 56, 57, 301leadd1dd 10679 . . . 4 (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶))
30325, 148, 58, 231, 302letrd 10232 . . 3 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶))
304 remulcl 10059 . . . . . . . . 9 ((𝑈 ∈ ℝ ∧ 3 ∈ ℝ) → (𝑈 · 3) ∈ ℝ)
30526, 27, 304sylancl 695 . . . . . . . 8 (𝜑 → (𝑈 · 3) ∈ ℝ)
306305, 57readdcld 10107 . . . . . . 7 (𝜑 → ((𝑈 · 3) + 𝐶) ∈ ℝ)
30716simp3d 1095 . . . . . . . 8 (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
308307simp3d 1095 . . . . . . 7 (𝜑 → ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))
309306, 54, 125, 308leadd2dd 10680 . . . . . 6 (𝜑 → ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶)) ≤ ((𝑈 · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
31028recnd 10106 . . . . . . . . 9 (𝜑 → 3 ∈ ℂ)
31159, 61, 310adddid 10102 . . . . . . . 8 (𝜑 → (𝑈 · ((log‘𝑍) + 3)) = ((𝑈 · (log‘𝑍)) + (𝑈 · 3)))
312311oveq1d 6705 . . . . . . 7 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) = (((𝑈 · (log‘𝑍)) + (𝑈 · 3)) + 𝐶))
313125recnd 10106 . . . . . . . 8 (𝜑 → (𝑈 · (log‘𝑍)) ∈ ℂ)
31459, 310mulcld 10098 . . . . . . . 8 (𝜑 → (𝑈 · 3) ∈ ℂ)
31513rpcnd 11912 . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
316313, 314, 315addassd 10100 . . . . . . 7 (𝜑 → (((𝑈 · (log‘𝑍)) + (𝑈 · 3)) + 𝐶) = ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶)))
317312, 316eqtrd 2685 . . . . . 6 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) = ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶)))
3182852timesd 11313 . . . . . . . 8 (𝜑 → (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) = ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
319318oveq2d 6706 . . . . . . 7 (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
320313, 285, 285nppcan3d 10457 . . . . . . 7 (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + ((((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = ((𝑈 · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
321319, 320eqtrd 2685 . . . . . 6 (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = ((𝑈 · (log‘𝑍)) + (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
322309, 317, 3213brtr4d 4717 . . . . 5 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ≤ (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
32330, 57readdcld 10107 . . . . . 6 (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ∈ ℝ)
324323, 55, 126lesubaddd 10662 . . . . 5 (𝜑 → ((((𝑈 · ((log‘𝑍) + 3)) + 𝐶) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) ≤ ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) ↔ ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ≤ (((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))))
325322, 324mpbird 247 . . . 4 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) + 𝐶) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) ≤ ((𝑈 · (log‘𝑍)) − (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
326282, 315, 283addsubd 10451 . . . 4 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) + 𝐶) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) = (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶))
327325, 326, 1243brtr3d 4716 . . 3 (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))) + 𝐶) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
32825, 58, 127, 303, 327letrd 10232 . 2 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))
329 3z 11448 . . . . . . 7 3 ∈ ℤ
330 rpexpcl 12919 . . . . . . 7 ((𝑈 ∈ ℝ+ ∧ 3 ∈ ℤ) → (𝑈↑3) ∈ ℝ+)
3317, 329, 330sylancl 695 . . . . . 6 (𝜑 → (𝑈↑3) ∈ ℝ+)
33296, 331rpmulcld 11926 . . . . 5 (𝜑 → (𝐹 · (𝑈↑3)) ∈ ℝ+)
333332rpred 11910 . . . 4 (𝜑 → (𝐹 · (𝑈↑3)) ∈ ℝ)
33426, 333resubcld 10496 . . 3 (𝜑 → (𝑈 − (𝐹 · (𝑈↑3))) ∈ ℝ)
33523, 334, 131lemul1d 11953 . 2 (𝜑 → ((abs‘((𝑅𝑍) / 𝑍)) ≤ (𝑈 − (𝐹 · (𝑈↑3))) ↔ ((abs‘((𝑅𝑍) / 𝑍)) · (log‘𝑍)) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍))))
336328, 335mpbird 247 1 (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) ≤ (𝑈 − (𝐹 · (𝑈↑3))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942   class class class wbr 4685   ↦ cmpt 4762  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  +∞cpnf 10109  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304   / cdiv 10722  ℕcn 11058  2c2 11108  3c3 11109  4c4 11110  ℕ0cn0 11330  ℤcz 11415  ;cdc 11531  ℝ+crp 11870  (,)cioo 12213  [,)cico 12215  [,]cicc 12216  ...cfz 12364  ⌊cfl 12631  ↑cexp 12900  √csqrt 14017  abscabs 14018  Σcsu 14460  expce 14836  eceu 14837  logclog 24346  ψcchp 24864 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-e 14843  df-sin 14844  df-cos 14845  df-pi 14847  df-dvds 15028  df-gcd 15264  df-prm 15433  df-pc 15589  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676  df-log 24348  df-em 24764  df-vma 24869  df-chp 24870 This theorem is referenced by:  pntleme  25342
 Copyright terms: Public domain W3C validator