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

Theorem pntpbnd2 26495
Description: Lemma for pntpbnd 26496. (Contributed by Mario Carneiro, 11-Apr-2016.)
Hypotheses
Ref Expression
pntpbnd.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
pntpbnd1.e (𝜑𝐸 ∈ (0(,)1))
pntpbnd1.x 𝑋 = (exp‘(2 / 𝐸))
pntpbnd1.y (𝜑𝑌 ∈ (𝑋(,)+∞))
pntpbnd1.1 (𝜑𝐴 ∈ ℝ+)
pntpbnd1.2 (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴)
pntpbnd1.c 𝐶 = (𝐴 + 2)
pntpbnd1.k (𝜑𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))
pntpbnd1.3 (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸))
Assertion
Ref Expression
pntpbnd2 ¬ 𝜑
Distinct variable groups:   𝑖,𝑗,𝑦,𝐾   𝑅,𝑖,𝑗,𝑦   𝑖,𝑎,𝑗,𝑦,𝐴   𝑦,𝐸   𝑖,𝑌,𝑗,𝑦
Allowed substitution hints:   𝜑(𝑦,𝑖,𝑗,𝑎)   𝐶(𝑦,𝑖,𝑗,𝑎)   𝑅(𝑎)   𝐸(𝑖,𝑗,𝑎)   𝐾(𝑎)   𝑋(𝑦,𝑖,𝑗,𝑎)   𝑌(𝑎)

Proof of Theorem pntpbnd2
Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2div2e1 11996 . . 3 (2 / 2) = 1
2 2re 11929 . . . . 5 2 ∈ ℝ
32a1i 11 . . . 4 (𝜑 → 2 ∈ ℝ)
4 ioossre 13021 . . . . . 6 (0(,)1) ⊆ ℝ
5 pntpbnd1.e . . . . . 6 (𝜑𝐸 ∈ (0(,)1))
64, 5sselid 3913 . . . . 5 (𝜑𝐸 ∈ ℝ)
7 eliooord 13019 . . . . . . 7 (𝐸 ∈ (0(,)1) → (0 < 𝐸𝐸 < 1))
85, 7syl 17 . . . . . 6 (𝜑 → (0 < 𝐸𝐸 < 1))
98simpld 498 . . . . 5 (𝜑 → 0 < 𝐸)
106, 9elrpd 12650 . . . 4 (𝜑𝐸 ∈ ℝ+)
11 2rp 12616 . . . . 5 2 ∈ ℝ+
1211a1i 11 . . . 4 (𝜑 → 2 ∈ ℝ+)
13 pntpbnd1.c . . . . . . . . 9 𝐶 = (𝐴 + 2)
1413oveq1i 7242 . . . . . . . 8 (𝐶𝐴) = ((𝐴 + 2) − 𝐴)
15 pntpbnd1.1 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ+)
1615rpcnd 12655 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
17 2cn 11930 . . . . . . . . 9 2 ∈ ℂ
18 pncan2 11110 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝐴 + 2) − 𝐴) = 2)
1916, 17, 18sylancl 589 . . . . . . . 8 (𝜑 → ((𝐴 + 2) − 𝐴) = 2)
2014, 19syl5eq 2791 . . . . . . 7 (𝜑 → (𝐶𝐴) = 2)
2120oveq1d 7247 . . . . . 6 (𝜑 → ((𝐶𝐴) / 𝐸) = (2 / 𝐸))
22 rpaddcl 12633 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (𝐴 + 2) ∈ ℝ+)
2315, 11, 22sylancl 589 . . . . . . . . 9 (𝜑 → (𝐴 + 2) ∈ ℝ+)
2413, 23eqeltrid 2843 . . . . . . . 8 (𝜑𝐶 ∈ ℝ+)
2524rpcnd 12655 . . . . . . 7 (𝜑𝐶 ∈ ℂ)
266recnd 10886 . . . . . . 7 (𝜑𝐸 ∈ ℂ)
2710rpne0d 12658 . . . . . . 7 (𝜑𝐸 ≠ 0)
2825, 16, 26, 27divsubdird 11672 . . . . . 6 (𝜑 → ((𝐶𝐴) / 𝐸) = ((𝐶 / 𝐸) − (𝐴 / 𝐸)))
2921, 28eqtr3d 2780 . . . . 5 (𝜑 → (2 / 𝐸) = ((𝐶 / 𝐸) − (𝐴 / 𝐸)))
3024, 10rpdivcld 12670 . . . . . . 7 (𝜑 → (𝐶 / 𝐸) ∈ ℝ+)
3130rpred 12653 . . . . . 6 (𝜑 → (𝐶 / 𝐸) ∈ ℝ)
3215rpred 12653 . . . . . . 7 (𝜑𝐴 ∈ ℝ)
3332, 10rerpdivcld 12684 . . . . . 6 (𝜑 → (𝐴 / 𝐸) ∈ ℝ)
34 resubcl 11167 . . . . . . . 8 (((𝐶 / 𝐸) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝐶 / 𝐸) − 2) ∈ ℝ)
3531, 2, 34sylancl 589 . . . . . . 7 (𝜑 → ((𝐶 / 𝐸) − 2) ∈ ℝ)
36 pntpbnd1.k . . . . . . . . . . . 12 (𝜑𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))
3731reefcld 15677 . . . . . . . . . . . . 13 (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ)
38 elicopnf 13058 . . . . . . . . . . . . 13 ((exp‘(𝐶 / 𝐸)) ∈ ℝ → (𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾)))
3937, 38syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾)))
4036, 39mpbid 235 . . . . . . . . . . 11 (𝜑 → (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾))
4140simpld 498 . . . . . . . . . 10 (𝜑𝐾 ∈ ℝ)
42 0red 10861 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℝ)
43 1re 10858 . . . . . . . . . . . 12 1 ∈ ℝ
4443a1i 11 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℝ)
45 0lt1 11379 . . . . . . . . . . . 12 0 < 1
4645a1i 11 . . . . . . . . . . 11 (𝜑 → 0 < 1)
47 efgt1 15705 . . . . . . . . . . . . 13 ((𝐶 / 𝐸) ∈ ℝ+ → 1 < (exp‘(𝐶 / 𝐸)))
4830, 47syl 17 . . . . . . . . . . . 12 (𝜑 → 1 < (exp‘(𝐶 / 𝐸)))
4940simprd 499 . . . . . . . . . . . 12 (𝜑 → (exp‘(𝐶 / 𝐸)) ≤ 𝐾)
5044, 37, 41, 48, 49ltletrd 11017 . . . . . . . . . . 11 (𝜑 → 1 < 𝐾)
5142, 44, 41, 46, 50lttrd 11018 . . . . . . . . . 10 (𝜑 → 0 < 𝐾)
5241, 51elrpd 12650 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ+)
5352relogcld 25538 . . . . . . . 8 (𝜑 → (log‘𝐾) ∈ ℝ)
54 resubcl 11167 . . . . . . . 8 (((log‘𝐾) ∈ ℝ ∧ 2 ∈ ℝ) → ((log‘𝐾) − 2) ∈ ℝ)
5553, 2, 54sylancl 589 . . . . . . 7 (𝜑 → ((log‘𝐾) − 2) ∈ ℝ)
5652reeflogd 25539 . . . . . . . . . 10 (𝜑 → (exp‘(log‘𝐾)) = 𝐾)
5749, 56breqtrrd 5096 . . . . . . . . 9 (𝜑 → (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾)))
58 efle 15707 . . . . . . . . . 10 (((𝐶 / 𝐸) ∈ ℝ ∧ (log‘𝐾) ∈ ℝ) → ((𝐶 / 𝐸) ≤ (log‘𝐾) ↔ (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾))))
5931, 53, 58syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝐶 / 𝐸) ≤ (log‘𝐾) ↔ (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾))))
6057, 59mpbird 260 . . . . . . . 8 (𝜑 → (𝐶 / 𝐸) ≤ (log‘𝐾))
6131, 53, 3, 60lesub1dd 11473 . . . . . . 7 (𝜑 → ((𝐶 / 𝐸) − 2) ≤ ((log‘𝐾) − 2))
62 fzfid 13573 . . . . . . . . 9 (𝜑 → (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) ∈ Fin)
63 ioossre 13021 . . . . . . . . . . . . . . 15 (𝑋(,)+∞) ⊆ ℝ
64 pntpbnd1.y . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ (𝑋(,)+∞))
6563, 64sselid 3913 . . . . . . . . . . . . . 14 (𝜑𝑌 ∈ ℝ)
66 pntpbnd1.x . . . . . . . . . . . . . . . . 17 𝑋 = (exp‘(2 / 𝐸))
67 rerpdivcl 12641 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ ∧ 𝐸 ∈ ℝ+) → (2 / 𝐸) ∈ ℝ)
682, 10, 67sylancr 590 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2 / 𝐸) ∈ ℝ)
6968reefcld 15677 . . . . . . . . . . . . . . . . 17 (𝜑 → (exp‘(2 / 𝐸)) ∈ ℝ)
7066, 69eqeltrid 2843 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℝ)
71 efgt0 15692 . . . . . . . . . . . . . . . . . 18 ((2 / 𝐸) ∈ ℝ → 0 < (exp‘(2 / 𝐸)))
7268, 71syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < (exp‘(2 / 𝐸)))
7372, 66breqtrrdi 5110 . . . . . . . . . . . . . . . 16 (𝜑 → 0 < 𝑋)
7470rexrd 10908 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ ℝ*)
75 elioopnf 13056 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ ℝ* → (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌)))
7674, 75syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌)))
7764, 76mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌))
7877simprd 499 . . . . . . . . . . . . . . . 16 (𝜑𝑋 < 𝑌)
7942, 70, 65, 73, 78lttrd 11018 . . . . . . . . . . . . . . 15 (𝜑 → 0 < 𝑌)
8042, 65, 79ltled 11005 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ 𝑌)
81 flge0nn0 13420 . . . . . . . . . . . . . 14 ((𝑌 ∈ ℝ ∧ 0 ≤ 𝑌) → (⌊‘𝑌) ∈ ℕ0)
8265, 80, 81syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → (⌊‘𝑌) ∈ ℕ0)
83 nn0p1nn 12154 . . . . . . . . . . . . 13 ((⌊‘𝑌) ∈ ℕ0 → ((⌊‘𝑌) + 1) ∈ ℕ)
8482, 83syl 17 . . . . . . . . . . . 12 (𝜑 → ((⌊‘𝑌) + 1) ∈ ℕ)
85 elfzuz 13133 . . . . . . . . . . . 12 (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑛 ∈ (ℤ‘((⌊‘𝑌) + 1)))
86 eluznn 12539 . . . . . . . . . . . 12 ((((⌊‘𝑌) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑌) + 1))) → 𝑛 ∈ ℕ)
8784, 85, 86syl2an 599 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℕ)
8887peano2nnd 11872 . . . . . . . . . 10 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℕ)
8988nnrecred 11906 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℝ)
9062, 89fsumrecl 15326 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ∈ ℝ)
9153recnd 10886 . . . . . . . . . 10 (𝜑 → (log‘𝐾) ∈ ℂ)
92 2cnd 11933 . . . . . . . . . 10 (𝜑 → 2 ∈ ℂ)
9365, 79elrpd 12650 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ+)
9493relogcld 25538 . . . . . . . . . . 11 (𝜑 → (log‘𝑌) ∈ ℝ)
9594recnd 10886 . . . . . . . . . 10 (𝜑 → (log‘𝑌) ∈ ℂ)
9691, 92, 95pnpcan2d 11252 . . . . . . . . 9 (𝜑 → (((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) = ((log‘𝐾) − 2))
9752, 93relogmuld 25540 . . . . . . . . . . 11 (𝜑 → (log‘(𝐾 · 𝑌)) = ((log‘𝐾) + (log‘𝑌)))
9853, 94readdcld 10887 . . . . . . . . . . . . 13 (𝜑 → ((log‘𝐾) + (log‘𝑌)) ∈ ℝ)
9997, 98eqeltrd 2839 . . . . . . . . . . . 12 (𝜑 → (log‘(𝐾 · 𝑌)) ∈ ℝ)
100 fzfid 13573 . . . . . . . . . . . . . 14 (𝜑 → (0...(⌊‘𝑌)) ∈ Fin)
101 elfznn0 13230 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (0...(⌊‘𝑌)) → 𝑛 ∈ ℕ0)
102101adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (0...(⌊‘𝑌))) → 𝑛 ∈ ℕ0)
103 nn0p1nn 12154 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ)
104102, 103syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (0...(⌊‘𝑌))) → (𝑛 + 1) ∈ ℕ)
105104nnrecred 11906 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (0...(⌊‘𝑌))) → (1 / (𝑛 + 1)) ∈ ℝ)
106100, 105fsumrecl 15326 . . . . . . . . . . . . 13 (𝜑 → Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) ∈ ℝ)
107106, 90readdcld 10887 . . . . . . . . . . . 12 (𝜑 → (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ∈ ℝ)
108 readdcl 10837 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (2 + (log‘𝑌)) ∈ ℝ)
1092, 94, 108sylancr 590 . . . . . . . . . . . . 13 (𝜑 → (2 + (log‘𝑌)) ∈ ℝ)
110109, 90readdcld 10887 . . . . . . . . . . . 12 (𝜑 → ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ∈ ℝ)
11141, 65remulcld 10888 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐾 · 𝑌) ∈ ℝ)
11265recnd 10886 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑌 ∈ ℂ)
113112mulid2d 10876 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 · 𝑌) = 𝑌)
11444, 41, 50ltled 11005 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ≤ 𝐾)
115 lemul1 11709 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ (𝑌 ∈ ℝ ∧ 0 < 𝑌)) → (1 ≤ 𝐾 ↔ (1 · 𝑌) ≤ (𝐾 · 𝑌)))
11644, 41, 65, 79, 115syl112anc 1376 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1 ≤ 𝐾 ↔ (1 · 𝑌) ≤ (𝐾 · 𝑌)))
117114, 116mpbid 235 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 · 𝑌) ≤ (𝐾 · 𝑌))
118113, 117eqbrtrrd 5092 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑌 ≤ (𝐾 · 𝑌))
11942, 65, 111, 80, 118letrd 11014 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (𝐾 · 𝑌))
120 flge0nn0 13420 . . . . . . . . . . . . . . . . . 18 (((𝐾 · 𝑌) ∈ ℝ ∧ 0 ≤ (𝐾 · 𝑌)) → (⌊‘(𝐾 · 𝑌)) ∈ ℕ0)
121111, 119, 120syl2anc 587 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℕ0)
122 nn0p1nn 12154 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝐾 · 𝑌)) ∈ ℕ0 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℕ)
123121, 122syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℕ)
124123nnrpd 12651 . . . . . . . . . . . . . . 15 (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℝ+)
125124relogcld 25538 . . . . . . . . . . . . . 14 (𝜑 → (log‘((⌊‘(𝐾 · 𝑌)) + 1)) ∈ ℝ)
126 1zzd 12233 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
127111flcld 13398 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℤ)
128127peano2zd 12310 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℤ)
129 elfznn 13166 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1)) → 𝑘 ∈ ℕ)
130129adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))) → 𝑘 ∈ ℕ)
131 nnrecre 11897 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
132131recnd 10886 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℂ)
133130, 132syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))) → (1 / 𝑘) ∈ ℂ)
134 oveq2 7240 . . . . . . . . . . . . . . . . 17 (𝑘 = (𝑛 + 1) → (1 / 𝑘) = (1 / (𝑛 + 1)))
135126, 126, 128, 133, 134fsumshftm 15373 . . . . . . . . . . . . . . . 16 (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) = Σ𝑛 ∈ ((1 − 1)...(((⌊‘(𝐾 · 𝑌)) + 1) − 1))(1 / (𝑛 + 1)))
136 1m1e0 11927 . . . . . . . . . . . . . . . . . . 19 (1 − 1) = 0
137136a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 − 1) = 0)
138127zcnd 12308 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℂ)
139 ax-1cn 10812 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
140 pncan 11109 . . . . . . . . . . . . . . . . . . 19 (((⌊‘(𝐾 · 𝑌)) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘(𝐾 · 𝑌)) + 1) − 1) = (⌊‘(𝐾 · 𝑌)))
141138, 139, 140sylancl 589 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((⌊‘(𝐾 · 𝑌)) + 1) − 1) = (⌊‘(𝐾 · 𝑌)))
142137, 141oveq12d 7250 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 − 1)...(((⌊‘(𝐾 · 𝑌)) + 1) − 1)) = (0...(⌊‘(𝐾 · 𝑌))))
143142sumeq1d 15293 . . . . . . . . . . . . . . . 16 (𝜑 → Σ𝑛 ∈ ((1 − 1)...(((⌊‘(𝐾 · 𝑌)) + 1) − 1))(1 / (𝑛 + 1)) = Σ𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))
144 reflcl 13396 . . . . . . . . . . . . . . . . . . . 20 (𝑌 ∈ ℝ → (⌊‘𝑌) ∈ ℝ)
14565, 144syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘𝑌) ∈ ℝ)
146145ltp1d 11787 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘𝑌) < ((⌊‘𝑌) + 1))
147 fzdisj 13164 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑌) < ((⌊‘𝑌) + 1) → ((0...(⌊‘𝑌)) ∩ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) = ∅)
148146, 147syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0...(⌊‘𝑌)) ∩ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) = ∅)
149 flwordi 13412 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ ℝ ∧ (𝐾 · 𝑌) ∈ ℝ ∧ 𝑌 ≤ (𝐾 · 𝑌)) → (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌)))
15065, 111, 118, 149syl3anc 1373 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌)))
151 elfz2nn0 13228 . . . . . . . . . . . . . . . . . . 19 ((⌊‘𝑌) ∈ (0...(⌊‘(𝐾 · 𝑌))) ↔ ((⌊‘𝑌) ∈ ℕ0 ∧ (⌊‘(𝐾 · 𝑌)) ∈ ℕ0 ∧ (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌))))
15282, 121, 150, 151syl3anbrc 1345 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘𝑌) ∈ (0...(⌊‘(𝐾 · 𝑌))))
153 fzsplit 13163 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑌) ∈ (0...(⌊‘(𝐾 · 𝑌))) → (0...(⌊‘(𝐾 · 𝑌))) = ((0...(⌊‘𝑌)) ∪ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))))
154152, 153syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (0...(⌊‘(𝐾 · 𝑌))) = ((0...(⌊‘𝑌)) ∪ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))))
155 fzfid 13573 . . . . . . . . . . . . . . . . 17 (𝜑 → (0...(⌊‘(𝐾 · 𝑌))) ∈ Fin)
156 elfznn0 13230 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌))) → 𝑛 ∈ ℕ0)
157156adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℕ0)
158157, 103syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℕ)
159158nnrecred 11906 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℝ)
160159recnd 10886 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℂ)
161148, 154, 155, 160fsumsplit 15333 . . . . . . . . . . . . . . . 16 (𝜑 → Σ𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) = (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
162135, 143, 1613eqtrd 2782 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) = (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
163162, 107eqeltrd 2839 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) ∈ ℝ)
164 fllep1 13401 . . . . . . . . . . . . . . . 16 ((𝐾 · 𝑌) ∈ ℝ → (𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1))
165111, 164syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1))
16652, 93rpmulcld 12669 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 · 𝑌) ∈ ℝ+)
167166, 124logled 25542 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1) ↔ (log‘(𝐾 · 𝑌)) ≤ (log‘((⌊‘(𝐾 · 𝑌)) + 1))))
168165, 167mpbid 235 . . . . . . . . . . . . . 14 (𝜑 → (log‘(𝐾 · 𝑌)) ≤ (log‘((⌊‘(𝐾 · 𝑌)) + 1)))
169 emre 25915 . . . . . . . . . . . . . . . . 17 γ ∈ ℝ
170169a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → γ ∈ ℝ)
171163, 125resubcld 11285 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ ℝ)
172 0re 10860 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
173 emgt0 25916 . . . . . . . . . . . . . . . . . 18 0 < γ
174172, 169, 173ltleii 10980 . . . . . . . . . . . . . . . . 17 0 ≤ γ
175174a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ γ)
176 harmonicbnd 25913 . . . . . . . . . . . . . . . . . 18 (((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℕ → (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ (γ[,]1))
177123, 176syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ (γ[,]1))
178169, 43elicc2i 13026 . . . . . . . . . . . . . . . . . 18 ((Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ (γ[,]1) ↔ ((Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ ℝ ∧ γ ≤ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∧ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ≤ 1))
179178simp2bi 1148 . . . . . . . . . . . . . . . . 17 ((Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ (γ[,]1) → γ ≤ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))))
180177, 179syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → γ ≤ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))))
18142, 170, 171, 175, 180letrd 11014 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))))
182163, 125subge0d 11447 . . . . . . . . . . . . . . 15 (𝜑 → (0 ≤ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ↔ (log‘((⌊‘(𝐾 · 𝑌)) + 1)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘)))
183181, 182mpbid 235 . . . . . . . . . . . . . 14 (𝜑 → (log‘((⌊‘(𝐾 · 𝑌)) + 1)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘))
18499, 125, 163, 168, 183letrd 11014 . . . . . . . . . . . . 13 (𝜑 → (log‘(𝐾 · 𝑌)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘))
185184, 162breqtrd 5094 . . . . . . . . . . . 12 (𝜑 → (log‘(𝐾 · 𝑌)) ≤ (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
18665flcld 13398 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘𝑌) ∈ ℤ)
187186peano2zd 12310 . . . . . . . . . . . . . . . 16 (𝜑 → ((⌊‘𝑌) + 1) ∈ ℤ)
188 elfznn 13166 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (1...((⌊‘𝑌) + 1)) → 𝑘 ∈ ℕ)
189188adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...((⌊‘𝑌) + 1))) → 𝑘 ∈ ℕ)
190189, 132syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...((⌊‘𝑌) + 1))) → (1 / 𝑘) ∈ ℂ)
191126, 126, 187, 190, 134fsumshftm 15373 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) = Σ𝑛 ∈ ((1 − 1)...(((⌊‘𝑌) + 1) − 1))(1 / (𝑛 + 1)))
192145recnd 10886 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘𝑌) ∈ ℂ)
193 pncan 11109 . . . . . . . . . . . . . . . . . 18 (((⌊‘𝑌) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑌) + 1) − 1) = (⌊‘𝑌))
194192, 139, 193sylancl 589 . . . . . . . . . . . . . . . . 17 (𝜑 → (((⌊‘𝑌) + 1) − 1) = (⌊‘𝑌))
195137, 194oveq12d 7250 . . . . . . . . . . . . . . . 16 (𝜑 → ((1 − 1)...(((⌊‘𝑌) + 1) − 1)) = (0...(⌊‘𝑌)))
196195sumeq1d 15293 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑛 ∈ ((1 − 1)...(((⌊‘𝑌) + 1) − 1))(1 / (𝑛 + 1)) = Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)))
197191, 196eqtrd 2778 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) = Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)))
198197, 106eqeltrd 2839 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ∈ ℝ)
19984nnrpd 12651 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘𝑌) + 1) ∈ ℝ+)
200199relogcld 25538 . . . . . . . . . . . . . . . 16 (𝜑 → (log‘((⌊‘𝑌) + 1)) ∈ ℝ)
201 readdcl 10837 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ (log‘((⌊‘𝑌) + 1)) ∈ ℝ) → (1 + (log‘((⌊‘𝑌) + 1))) ∈ ℝ)
20243, 200, 201sylancr 590 . . . . . . . . . . . . . . 15 (𝜑 → (1 + (log‘((⌊‘𝑌) + 1))) ∈ ℝ)
203 harmonicbnd 25913 . . . . . . . . . . . . . . . . . 18 (((⌊‘𝑌) + 1) ∈ ℕ → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈ (γ[,]1))
20484, 203syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈ (γ[,]1))
205169, 43elicc2i 13026 . . . . . . . . . . . . . . . . . 18 ((Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈ (γ[,]1) ↔ ((Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈ ℝ ∧ γ ≤ (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∧ (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ≤ 1))
206205simp3bi 1149 . . . . . . . . . . . . . . . . 17 ((Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈ (γ[,]1) → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ≤ 1)
207204, 206syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ≤ 1)
208198, 200, 44lesubaddd 11454 . . . . . . . . . . . . . . . 16 (𝜑 → ((Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ≤ 1 ↔ Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ≤ (1 + (log‘((⌊‘𝑌) + 1)))))
209207, 208mpbid 235 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ≤ (1 + (log‘((⌊‘𝑌) + 1))))
210 readdcl 10837 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (1 + (log‘𝑌)) ∈ ℝ)
21143, 94, 210sylancr 590 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 + (log‘𝑌)) ∈ ℝ)
212 peano2re 11030 . . . . . . . . . . . . . . . . . . . . 21 ((⌊‘𝑌) ∈ ℝ → ((⌊‘𝑌) + 1) ∈ ℝ)
213145, 212syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((⌊‘𝑌) + 1) ∈ ℝ)
2143, 65remulcld 10888 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 · 𝑌) ∈ ℝ)
215 epr 15797 . . . . . . . . . . . . . . . . . . . . . 22 e ∈ ℝ+
216 rpmulcl 12634 . . . . . . . . . . . . . . . . . . . . . 22 ((e ∈ ℝ+𝑌 ∈ ℝ+) → (e · 𝑌) ∈ ℝ+)
217215, 93, 216sylancr 590 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (e · 𝑌) ∈ ℝ+)
218217rpred 12653 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (e · 𝑌) ∈ ℝ)
219 flle 13399 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 ∈ ℝ → (⌊‘𝑌) ≤ 𝑌)
22065, 219syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (⌊‘𝑌) ≤ 𝑌)
22112, 10rpdivcld 12670 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (2 / 𝐸) ∈ ℝ+)
222 efgt1 15705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 / 𝐸) ∈ ℝ+ → 1 < (exp‘(2 / 𝐸)))
223221, 222syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 1 < (exp‘(2 / 𝐸)))
224223, 66breqtrrdi 5110 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 < 𝑋)
22544, 70, 65, 224, 78lttrd 11018 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 < 𝑌)
22644, 65, 225ltled 11005 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 ≤ 𝑌)
227145, 44, 65, 65, 220, 226le2addd 11476 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((⌊‘𝑌) + 1) ≤ (𝑌 + 𝑌))
2281122timesd 12098 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 · 𝑌) = (𝑌 + 𝑌))
229227, 228breqtrrd 5096 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((⌊‘𝑌) + 1) ≤ (2 · 𝑌))
230 ere 15678 . . . . . . . . . . . . . . . . . . . . . . 23 e ∈ ℝ
231 egt2lt3 15795 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 < e ∧ e < 3)
232231simpli 487 . . . . . . . . . . . . . . . . . . . . . . 23 2 < e
2332, 230, 232ltleii 10980 . . . . . . . . . . . . . . . . . . . . . 22 2 ≤ e
234233a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ≤ e)
235230a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → e ∈ ℝ)
236 lemul1 11709 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℝ ∧ e ∈ ℝ ∧ (𝑌 ∈ ℝ ∧ 0 < 𝑌)) → (2 ≤ e ↔ (2 · 𝑌) ≤ (e · 𝑌)))
2373, 235, 65, 79, 236syl112anc 1376 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 ≤ e ↔ (2 · 𝑌) ≤ (e · 𝑌)))
238234, 237mpbid 235 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 · 𝑌) ≤ (e · 𝑌))
239213, 214, 218, 229, 238letrd 11014 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((⌊‘𝑌) + 1) ≤ (e · 𝑌))
240199, 217logled 25542 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((⌊‘𝑌) + 1) ≤ (e · 𝑌) ↔ (log‘((⌊‘𝑌) + 1)) ≤ (log‘(e · 𝑌))))
241239, 240mpbid 235 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((⌊‘𝑌) + 1)) ≤ (log‘(e · 𝑌)))
242 relogmul 25507 . . . . . . . . . . . . . . . . . . . 20 ((e ∈ ℝ+𝑌 ∈ ℝ+) → (log‘(e · 𝑌)) = ((log‘e) + (log‘𝑌)))
243215, 93, 242sylancr 590 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (log‘(e · 𝑌)) = ((log‘e) + (log‘𝑌)))
244 loge 25502 . . . . . . . . . . . . . . . . . . . 20 (log‘e) = 1
245244oveq1i 7242 . . . . . . . . . . . . . . . . . . 19 ((log‘e) + (log‘𝑌)) = (1 + (log‘𝑌))
246243, 245eqtrdi 2795 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘(e · 𝑌)) = (1 + (log‘𝑌)))
247241, 246breqtrd 5094 . . . . . . . . . . . . . . . . 17 (𝜑 → (log‘((⌊‘𝑌) + 1)) ≤ (1 + (log‘𝑌)))
248200, 211, 44, 247leadd2dd 11472 . . . . . . . . . . . . . . . 16 (𝜑 → (1 + (log‘((⌊‘𝑌) + 1))) ≤ (1 + (1 + (log‘𝑌))))
249 df-2 11918 . . . . . . . . . . . . . . . . . 18 2 = (1 + 1)
250249oveq1i 7242 . . . . . . . . . . . . . . . . 17 (2 + (log‘𝑌)) = ((1 + 1) + (log‘𝑌))
251139a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℂ)
252251, 251, 95addassd 10880 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + 1) + (log‘𝑌)) = (1 + (1 + (log‘𝑌))))
253250, 252syl5eq 2791 . . . . . . . . . . . . . . . 16 (𝜑 → (2 + (log‘𝑌)) = (1 + (1 + (log‘𝑌))))
254248, 253breqtrrd 5096 . . . . . . . . . . . . . . 15 (𝜑 → (1 + (log‘((⌊‘𝑌) + 1))) ≤ (2 + (log‘𝑌)))
255198, 202, 109, 209, 254letrd 11014 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ≤ (2 + (log‘𝑌)))
256197, 255eqbrtrrd 5092 . . . . . . . . . . . . 13 (𝜑 → Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) ≤ (2 + (log‘𝑌)))
257106, 109, 90, 256leadd1dd 11471 . . . . . . . . . . . 12 (𝜑 → (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
25899, 107, 110, 185, 257letrd 11014 . . . . . . . . . . 11 (𝜑 → (log‘(𝐾 · 𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
25997, 258eqbrtrrd 5092 . . . . . . . . . 10 (𝜑 → ((log‘𝐾) + (log‘𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
26098, 109, 90lesubadd2d 11456 . . . . . . . . . 10 (𝜑 → ((((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ↔ ((log‘𝐾) + (log‘𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))))
261259, 260mpbird 260 . . . . . . . . 9 (𝜑 → (((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))
26296, 261eqbrtrrd 5092 . . . . . . . 8 (𝜑 → ((log‘𝐾) − 2) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))
26389recnd 10886 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℂ)
26462, 26, 263fsummulc2 15376 . . . . . . . . . 10 (𝜑 → (𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))))
2656adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ∈ ℝ)
266265recnd 10886 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ∈ ℂ)
26788nncnd 11871 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℂ)
26888nnne0d 11905 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ≠ 0)
269266, 267, 268divrecd 11636 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) = (𝐸 · (1 / (𝑛 + 1))))
270265, 88nndivred 11909 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) ∈ ℝ)
271269, 270eqeltrrd 2840 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 · (1 / (𝑛 + 1))) ∈ ℝ)
27262, 271fsumrecl 15326 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ∈ ℝ)
27387nnrpd 12651 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℝ+)
274 pntpbnd.r . . . . . . . . . . . . . . . . . 18 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
275274pntrf 26471 . . . . . . . . . . . . . . . . 17 𝑅:ℝ+⟶ℝ
276275ffvelrni 6922 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℝ+ → (𝑅𝑛) ∈ ℝ)
277273, 276syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅𝑛) ∈ ℝ)
27887, 88nnmulcld 11908 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
279277, 278nndivred 11909 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
280279recnd 10886 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
281280abscld 15028 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ)
28262, 281fsumrecl 15326 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ)
283277, 87nndivred 11909 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅𝑛) / 𝑛) ∈ ℝ)
284283recnd 10886 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅𝑛) / 𝑛) ∈ ℂ)
285284abscld 15028 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅𝑛) / 𝑛)) ∈ ℝ)
28688nnrpd 12651 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℝ+)
287 pntpbnd1.3 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸))
288287adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸))
289 elfzle1 13140 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → ((⌊‘𝑌) + 1) ≤ 𝑛)
290289adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) + 1) ≤ 𝑛)
29165adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑌 ∈ ℝ)
292291flcld 13398 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (⌊‘𝑌) ∈ ℤ)
29387nnzd 12306 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℤ)
294 zltp1le 12252 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘𝑌) ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((⌊‘𝑌) < 𝑛 ↔ ((⌊‘𝑌) + 1) ≤ 𝑛))
295292, 293, 294syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) < 𝑛 ↔ ((⌊‘𝑌) + 1) ≤ 𝑛))
296290, 295mpbird 260 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (⌊‘𝑌) < 𝑛)
297 fllt 13406 . . . . . . . . . . . . . . . . . . 19 ((𝑌 ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑌 < 𝑛 ↔ (⌊‘𝑌) < 𝑛))
298291, 293, 297syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑌 < 𝑛 ↔ (⌊‘𝑌) < 𝑛))
299296, 298mpbird 260 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑌 < 𝑛)
300 elfzle2 13141 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑛 ≤ (⌊‘(𝐾 · 𝑌)))
301300adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≤ (⌊‘(𝐾 · 𝑌)))
302111adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐾 · 𝑌) ∈ ℝ)
303 flge 13405 . . . . . . . . . . . . . . . . . . 19 (((𝐾 · 𝑌) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (⌊‘(𝐾 · 𝑌))))
304302, 293, 303syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (⌊‘(𝐾 · 𝑌))))
305301, 304mpbird 260 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≤ (𝐾 · 𝑌))
306 breq2 5072 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑛 → (𝑌 < 𝑦𝑌 < 𝑛))
307 breq1 5071 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑛 → (𝑦 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (𝐾 · 𝑌)))
308306, 307anbi12d 634 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑛 → ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ↔ (𝑌 < 𝑛𝑛 ≤ (𝐾 · 𝑌))))
309 fveq2 6736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑛 → (𝑅𝑦) = (𝑅𝑛))
310 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑛𝑦 = 𝑛)
311309, 310oveq12d 7250 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑛 → ((𝑅𝑦) / 𝑦) = ((𝑅𝑛) / 𝑛))
312311fveq2d 6740 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑛 → (abs‘((𝑅𝑦) / 𝑦)) = (abs‘((𝑅𝑛) / 𝑛)))
313312breq1d 5078 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑛 → ((abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸 ↔ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸))
314308, 313anbi12d 634 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑛 → (((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸) ↔ ((𝑌 < 𝑛𝑛 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸)))
315314rspcev 3550 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ ((𝑌 < 𝑛𝑛 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸)) → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸))
316315expr 460 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ (𝑌 < 𝑛𝑛 ≤ (𝐾 · 𝑌))) → ((abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸 → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸)))
31787, 299, 305, 316syl12anc 837 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸 → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸)))
318288, 317mtod 201 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸)
319285, 265letrid 11009 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸𝐸 ≤ (abs‘((𝑅𝑛) / 𝑛))))
320319ord 864 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (¬ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸𝐸 ≤ (abs‘((𝑅𝑛) / 𝑛))))
321318, 320mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ≤ (abs‘((𝑅𝑛) / 𝑛)))
322265, 285, 286, 321lediv1dd 12711 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) ≤ ((abs‘((𝑅𝑛) / 𝑛)) / (𝑛 + 1)))
323284, 267, 268absdivd 15047 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(((𝑅𝑛) / 𝑛) / (𝑛 + 1))) = ((abs‘((𝑅𝑛) / 𝑛)) / (abs‘(𝑛 + 1))))
324277recnd 10886 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅𝑛) ∈ ℂ)
32587nncnd 11871 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℂ)
32687nnne0d 11905 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≠ 0)
327324, 325, 267, 326, 268divdiv1d 11664 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (((𝑅𝑛) / 𝑛) / (𝑛 + 1)) = ((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
328327fveq2d 6740 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(((𝑅𝑛) / 𝑛) / (𝑛 + 1))) = (abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
329286rprege0d 12660 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑛 + 1) ∈ ℝ ∧ 0 ≤ (𝑛 + 1)))
330 absid 14888 . . . . . . . . . . . . . . . 16 (((𝑛 + 1) ∈ ℝ ∧ 0 ≤ (𝑛 + 1)) → (abs‘(𝑛 + 1)) = (𝑛 + 1))
331329, 330syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(𝑛 + 1)) = (𝑛 + 1))
332331oveq2d 7248 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅𝑛) / 𝑛)) / (abs‘(𝑛 + 1))) = ((abs‘((𝑅𝑛) / 𝑛)) / (𝑛 + 1)))
333323, 328, 3323eqtr3rd 2787 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅𝑛) / 𝑛)) / (𝑛 + 1)) = (abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
334322, 269, 3333brtr3d 5099 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 · (1 / (𝑛 + 1))) ≤ (abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
33562, 271, 281, 334fsumle 15391 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
336 pntpbnd1.2 . . . . . . . . . . . 12 (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴)
337274, 5, 66, 64, 15, 336, 13, 36, 287pntpbnd1 26494 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴)
338272, 282, 32, 335, 337letrd 11014 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ≤ 𝐴)
339264, 338eqbrtrd 5090 . . . . . . . . 9 (𝜑 → (𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ 𝐴)
34090, 32, 10lemuldiv2d 12703 . . . . . . . . 9 (𝜑 → ((𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ 𝐴 ↔ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ≤ (𝐴 / 𝐸)))
341339, 340mpbid 235 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ≤ (𝐴 / 𝐸))
34255, 90, 33, 262, 341letrd 11014 . . . . . . 7 (𝜑 → ((log‘𝐾) − 2) ≤ (𝐴 / 𝐸))
34335, 55, 33, 61, 342letrd 11014 . . . . . 6 (𝜑 → ((𝐶 / 𝐸) − 2) ≤ (𝐴 / 𝐸))
34431, 3, 33, 343subled 11460 . . . . 5 (𝜑 → ((𝐶 / 𝐸) − (𝐴 / 𝐸)) ≤ 2)
34529, 344eqbrtrd 5090 . . . 4 (𝜑 → (2 / 𝐸) ≤ 2)
3463, 10, 12, 345lediv23d 12721 . . 3 (𝜑 → (2 / 2) ≤ 𝐸)
3471, 346eqbrtrrid 5104 . 2 (𝜑 → 1 ≤ 𝐸)
3488simprd 499 . . 3 (𝜑𝐸 < 1)
349 ltnle 10937 . . . 4 ((𝐸 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐸 < 1 ↔ ¬ 1 ≤ 𝐸))
3506, 43, 349sylancl 589 . . 3 (𝜑 → (𝐸 < 1 ↔ ¬ 1 ≤ 𝐸))
351348, 350mpbid 235 . 2 (𝜑 → ¬ 1 ≤ 𝐸)
352347, 351pm2.65i 197 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wcel 2111  wral 3062  wrex 3063  cun 3879  cin 3880  c0 4252   class class class wbr 5068  cmpt 5150  cfv 6398  (class class class)co 7232  cc 10752  cr 10753  0cc0 10754  1c1 10755   + caddc 10757   · cmul 10759  +∞cpnf 10889  *cxr 10891   < clt 10892  cle 10893  cmin 11087   / cdiv 11514  cn 11855  2c2 11910  3c3 11911  0cn0 12115  cz 12201  cuz 12463  +crp 12611  (,)cioo 12960  [,)cico 12962  [,]cicc 12963  ...cfz 13120  cfl 13390  abscabs 14825  Σcsu 15277  expce 15651  eceu 15652  logclog 25470  γcem 25901  ψcchp 26002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5194  ax-sep 5207  ax-nul 5214  ax-pow 5273  ax-pr 5337  ax-un 7542  ax-inf2 9281  ax-cnex 10810  ax-resscn 10811  ax-1cn 10812  ax-icn 10813  ax-addcl 10814  ax-addrcl 10815  ax-mulcl 10816  ax-mulrcl 10817  ax-mulcom 10818  ax-addass 10819  ax-mulass 10820  ax-distr 10821  ax-i2m1 10822  ax-1ne0 10823  ax-1rid 10824  ax-rnegex 10825  ax-rrecex 10826  ax-cnre 10827  ax-pre-lttri 10828  ax-pre-lttrn 10829  ax-pre-ltadd 10830  ax-pre-mulgt0 10831  ax-pre-sup 10832  ax-addf 10833  ax-mulf 10834
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3423  df-sbc 3710  df-csb 3827  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4253  df-if 4455  df-pw 4530  df-sn 4557  df-pr 4559  df-tp 4561  df-op 4563  df-uni 4835  df-int 4875  df-iun 4921  df-iin 4922  df-br 5069  df-opab 5131  df-mpt 5151  df-tr 5177  df-id 5470  df-eprel 5475  df-po 5483  df-so 5484  df-fr 5524  df-se 5525  df-we 5526  df-xp 5572  df-rel 5573  df-cnv 5574  df-co 5575  df-dm 5576  df-rn 5577  df-res 5578  df-ima 5579  df-pred 6176  df-ord 6234  df-on 6235  df-lim 6236  df-suc 6237  df-iota 6356  df-fun 6400  df-fn 6401  df-f 6402  df-f1 6403  df-fo 6404  df-f1o 6405  df-fv 6406  df-isom 6407  df-riota 7189  df-ov 7235  df-oprab 7236  df-mpo 7237  df-of 7488  df-om 7664  df-1st 7780  df-2nd 7781  df-supp 7925  df-wrecs 8068  df-recs 8129  df-rdg 8167  df-1o 8223  df-2o 8224  df-oadd 8227  df-er 8412  df-map 8531  df-pm 8532  df-ixp 8600  df-en 8648  df-dom 8649  df-sdom 8650  df-fin 8651  df-fsupp 9011  df-fi 9052  df-sup 9083  df-inf 9084  df-oi 9151  df-dju 9542  df-card 9580  df-pnf 10894  df-mnf 10895  df-xr 10896  df-ltxr 10897  df-le 10898  df-sub 11089  df-neg 11090  df-div 11515  df-nn 11856  df-2 11918  df-3 11919  df-4 11920  df-5 11921  df-6 11922  df-7 11923  df-8 11924  df-9 11925  df-n0 12116  df-xnn0 12188  df-z 12202  df-dec 12319  df-uz 12464  df-q 12570  df-rp 12612  df-xneg 12729  df-xadd 12730  df-xmul 12731  df-ioo 12964  df-ioc 12965  df-ico 12966  df-icc 12967  df-fz 13121  df-fzo 13264  df-fl 13392  df-mod 13470  df-seq 13602  df-exp 13663  df-fac 13868  df-bc 13897  df-hash 13925  df-shft 14658  df-cj 14690  df-re 14691  df-im 14692  df-sqrt 14826  df-abs 14827  df-limsup 15060  df-clim 15077  df-rlim 15078  df-sum 15278  df-ef 15657  df-e 15658  df-sin 15659  df-cos 15660  df-tan 15661  df-pi 15662  df-dvds 15844  df-gcd 16082  df-prm 16257  df-pc 16418  df-struct 16728  df-sets 16745  df-slot 16763  df-ndx 16773  df-base 16789  df-ress 16813  df-plusg 16843  df-mulr 16844  df-starv 16845  df-sca 16846  df-vsca 16847  df-ip 16848  df-tset 16849  df-ple 16850  df-ds 16852  df-unif 16853  df-hom 16854  df-cco 16855  df-rest 16955  df-topn 16956  df-0g 16974  df-gsum 16975  df-topgen 16976  df-pt 16977  df-prds 16980  df-xrs 17035  df-qtop 17040  df-imas 17041  df-xps 17043  df-mre 17117  df-mrc 17118  df-acs 17120  df-mgm 18142  df-sgrp 18191  df-mnd 18202  df-submnd 18247  df-mulg 18517  df-cntz 18739  df-cmn 19200  df-psmet 20383  df-xmet 20384  df-met 20385  df-bl 20386  df-mopn 20387  df-fbas 20388  df-fg 20389  df-cnfld 20392  df-top 21818  df-topon 21835  df-topsp 21857  df-bases 21870  df-cld 21943  df-ntr 21944  df-cls 21945  df-nei 22022  df-lp 22060  df-perf 22061  df-cn 22151  df-cnp 22152  df-haus 22239  df-cmp 22311  df-tx 22486  df-hmeo 22679  df-fil 22770  df-fm 22862  df-flim 22863  df-flf 22864  df-xms 23245  df-ms 23246  df-tms 23247  df-cncf 23802  df-limc 24790  df-dv 24791  df-ulm 25296  df-log 25472  df-atan 25777  df-em 25902  df-vma 26007  df-chp 26008
This theorem is referenced by:  pntpbnd  26496
  Copyright terms: Public domain W3C validator