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

Theorem pntpbnd2 26091
Description: Lemma for pntpbnd 26092. (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 11767 . . 3 (2 / 2) = 1
2 2re 11700 . . . . 5 2 ∈ ℝ
32a1i 11 . . . 4 (𝜑 → 2 ∈ ℝ)
4 ioossre 12788 . . . . . 6 (0(,)1) ⊆ ℝ
5 pntpbnd1.e . . . . . 6 (𝜑𝐸 ∈ (0(,)1))
64, 5sseldi 3964 . . . . 5 (𝜑𝐸 ∈ ℝ)
7 eliooord 12786 . . . . . . 7 (𝐸 ∈ (0(,)1) → (0 < 𝐸𝐸 < 1))
85, 7syl 17 . . . . . 6 (𝜑 → (0 < 𝐸𝐸 < 1))
98simpld 495 . . . . 5 (𝜑 → 0 < 𝐸)
106, 9elrpd 12418 . . . 4 (𝜑𝐸 ∈ ℝ+)
11 2rp 12384 . . . . 5 2 ∈ ℝ+
1211a1i 11 . . . 4 (𝜑 → 2 ∈ ℝ+)
13 pntpbnd1.c . . . . . . . . 9 𝐶 = (𝐴 + 2)
1413oveq1i 7155 . . . . . . . 8 (𝐶𝐴) = ((𝐴 + 2) − 𝐴)
15 pntpbnd1.1 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ+)
1615rpcnd 12423 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
17 2cn 11701 . . . . . . . . 9 2 ∈ ℂ
18 pncan2 10882 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝐴 + 2) − 𝐴) = 2)
1916, 17, 18sylancl 586 . . . . . . . 8 (𝜑 → ((𝐴 + 2) − 𝐴) = 2)
2014, 19syl5eq 2868 . . . . . . 7 (𝜑 → (𝐶𝐴) = 2)
2120oveq1d 7160 . . . . . 6 (𝜑 → ((𝐶𝐴) / 𝐸) = (2 / 𝐸))
22 rpaddcl 12401 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (𝐴 + 2) ∈ ℝ+)
2315, 11, 22sylancl 586 . . . . . . . . 9 (𝜑 → (𝐴 + 2) ∈ ℝ+)
2413, 23eqeltrid 2917 . . . . . . . 8 (𝜑𝐶 ∈ ℝ+)
2524rpcnd 12423 . . . . . . 7 (𝜑𝐶 ∈ ℂ)
266recnd 10658 . . . . . . 7 (𝜑𝐸 ∈ ℂ)
2710rpne0d 12426 . . . . . . 7 (𝜑𝐸 ≠ 0)
2825, 16, 26, 27divsubdird 11444 . . . . . 6 (𝜑 → ((𝐶𝐴) / 𝐸) = ((𝐶 / 𝐸) − (𝐴 / 𝐸)))
2921, 28eqtr3d 2858 . . . . 5 (𝜑 → (2 / 𝐸) = ((𝐶 / 𝐸) − (𝐴 / 𝐸)))
3024, 10rpdivcld 12438 . . . . . . 7 (𝜑 → (𝐶 / 𝐸) ∈ ℝ+)
3130rpred 12421 . . . . . 6 (𝜑 → (𝐶 / 𝐸) ∈ ℝ)
3215rpred 12421 . . . . . . 7 (𝜑𝐴 ∈ ℝ)
3332, 10rerpdivcld 12452 . . . . . 6 (𝜑 → (𝐴 / 𝐸) ∈ ℝ)
34 resubcl 10939 . . . . . . . 8 (((𝐶 / 𝐸) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝐶 / 𝐸) − 2) ∈ ℝ)
3531, 2, 34sylancl 586 . . . . . . 7 (𝜑 → ((𝐶 / 𝐸) − 2) ∈ ℝ)
36 pntpbnd1.k . . . . . . . . . . . 12 (𝜑𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))
3731reefcld 15431 . . . . . . . . . . . . 13 (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ)
38 elicopnf 12823 . . . . . . . . . . . . 13 ((exp‘(𝐶 / 𝐸)) ∈ ℝ → (𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾)))
3937, 38syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾)))
4036, 39mpbid 233 . . . . . . . . . . 11 (𝜑 → (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾))
4140simpld 495 . . . . . . . . . 10 (𝜑𝐾 ∈ ℝ)
42 0red 10633 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℝ)
43 1re 10630 . . . . . . . . . . . 12 1 ∈ ℝ
4443a1i 11 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℝ)
45 0lt1 11151 . . . . . . . . . . . 12 0 < 1
4645a1i 11 . . . . . . . . . . 11 (𝜑 → 0 < 1)
47 efgt1 15459 . . . . . . . . . . . . 13 ((𝐶 / 𝐸) ∈ ℝ+ → 1 < (exp‘(𝐶 / 𝐸)))
4830, 47syl 17 . . . . . . . . . . . 12 (𝜑 → 1 < (exp‘(𝐶 / 𝐸)))
4940simprd 496 . . . . . . . . . . . 12 (𝜑 → (exp‘(𝐶 / 𝐸)) ≤ 𝐾)
5044, 37, 41, 48, 49ltletrd 10789 . . . . . . . . . . 11 (𝜑 → 1 < 𝐾)
5142, 44, 41, 46, 50lttrd 10790 . . . . . . . . . 10 (𝜑 → 0 < 𝐾)
5241, 51elrpd 12418 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ+)
5352relogcld 25133 . . . . . . . 8 (𝜑 → (log‘𝐾) ∈ ℝ)
54 resubcl 10939 . . . . . . . 8 (((log‘𝐾) ∈ ℝ ∧ 2 ∈ ℝ) → ((log‘𝐾) − 2) ∈ ℝ)
5553, 2, 54sylancl 586 . . . . . . 7 (𝜑 → ((log‘𝐾) − 2) ∈ ℝ)
5652reeflogd 25134 . . . . . . . . . 10 (𝜑 → (exp‘(log‘𝐾)) = 𝐾)
5749, 56breqtrrd 5086 . . . . . . . . 9 (𝜑 → (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾)))
58 efle 15461 . . . . . . . . . 10 (((𝐶 / 𝐸) ∈ ℝ ∧ (log‘𝐾) ∈ ℝ) → ((𝐶 / 𝐸) ≤ (log‘𝐾) ↔ (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾))))
5931, 53, 58syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐶 / 𝐸) ≤ (log‘𝐾) ↔ (exp‘(𝐶 / 𝐸)) ≤ (exp‘(log‘𝐾))))
6057, 59mpbird 258 . . . . . . . 8 (𝜑 → (𝐶 / 𝐸) ≤ (log‘𝐾))
6131, 53, 3, 60lesub1dd 11245 . . . . . . 7 (𝜑 → ((𝐶 / 𝐸) − 2) ≤ ((log‘𝐾) − 2))
62 fzfid 13331 . . . . . . . . 9 (𝜑 → (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) ∈ Fin)
63 ioossre 12788 . . . . . . . . . . . . . . 15 (𝑋(,)+∞) ⊆ ℝ
64 pntpbnd1.y . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ (𝑋(,)+∞))
6563, 64sseldi 3964 . . . . . . . . . . . . . 14 (𝜑𝑌 ∈ ℝ)
66 pntpbnd1.x . . . . . . . . . . . . . . . . 17 𝑋 = (exp‘(2 / 𝐸))
67 rerpdivcl 12409 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℝ ∧ 𝐸 ∈ ℝ+) → (2 / 𝐸) ∈ ℝ)
682, 10, 67sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2 / 𝐸) ∈ ℝ)
6968reefcld 15431 . . . . . . . . . . . . . . . . 17 (𝜑 → (exp‘(2 / 𝐸)) ∈ ℝ)
7066, 69eqeltrid 2917 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℝ)
71 efgt0 15446 . . . . . . . . . . . . . . . . . 18 ((2 / 𝐸) ∈ ℝ → 0 < (exp‘(2 / 𝐸)))
7268, 71syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < (exp‘(2 / 𝐸)))
7372, 66breqtrrdi 5100 . . . . . . . . . . . . . . . 16 (𝜑 → 0 < 𝑋)
7470rexrd 10680 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ ℝ*)
75 elioopnf 12821 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ ℝ* → (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌)))
7674, 75syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌)))
7764, 76mpbid 233 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌))
7877simprd 496 . . . . . . . . . . . . . . . 16 (𝜑𝑋 < 𝑌)
7942, 70, 65, 73, 78lttrd 10790 . . . . . . . . . . . . . . 15 (𝜑 → 0 < 𝑌)
8042, 65, 79ltled 10777 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ 𝑌)
81 flge0nn0 13180 . . . . . . . . . . . . . 14 ((𝑌 ∈ ℝ ∧ 0 ≤ 𝑌) → (⌊‘𝑌) ∈ ℕ0)
8265, 80, 81syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (⌊‘𝑌) ∈ ℕ0)
83 nn0p1nn 11925 . . . . . . . . . . . . 13 ((⌊‘𝑌) ∈ ℕ0 → ((⌊‘𝑌) + 1) ∈ ℕ)
8482, 83syl 17 . . . . . . . . . . . 12 (𝜑 → ((⌊‘𝑌) + 1) ∈ ℕ)
85 elfzuz 12894 . . . . . . . . . . . 12 (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑛 ∈ (ℤ‘((⌊‘𝑌) + 1)))
86 eluznn 12307 . . . . . . . . . . . 12 ((((⌊‘𝑌) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑌) + 1))) → 𝑛 ∈ ℕ)
8784, 85, 86syl2an 595 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℕ)
8887peano2nnd 11644 . . . . . . . . . 10 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℕ)
8988nnrecred 11677 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℝ)
9062, 89fsumrecl 15081 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ∈ ℝ)
9153recnd 10658 . . . . . . . . . 10 (𝜑 → (log‘𝐾) ∈ ℂ)
92 2cnd 11704 . . . . . . . . . 10 (𝜑 → 2 ∈ ℂ)
9365, 79elrpd 12418 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ+)
9493relogcld 25133 . . . . . . . . . . 11 (𝜑 → (log‘𝑌) ∈ ℝ)
9594recnd 10658 . . . . . . . . . 10 (𝜑 → (log‘𝑌) ∈ ℂ)
9691, 92, 95pnpcan2d 11024 . . . . . . . . 9 (𝜑 → (((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) = ((log‘𝐾) − 2))
9752, 93relogmuld 25135 . . . . . . . . . . 11 (𝜑 → (log‘(𝐾 · 𝑌)) = ((log‘𝐾) + (log‘𝑌)))
9853, 94readdcld 10659 . . . . . . . . . . . . 13 (𝜑 → ((log‘𝐾) + (log‘𝑌)) ∈ ℝ)
9997, 98eqeltrd 2913 . . . . . . . . . . . 12 (𝜑 → (log‘(𝐾 · 𝑌)) ∈ ℝ)
100 fzfid 13331 . . . . . . . . . . . . . 14 (𝜑 → (0...(⌊‘𝑌)) ∈ Fin)
101 elfznn0 12990 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (0...(⌊‘𝑌)) → 𝑛 ∈ ℕ0)
102101adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (0...(⌊‘𝑌))) → 𝑛 ∈ ℕ0)
103 nn0p1nn 11925 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ)
104102, 103syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (0...(⌊‘𝑌))) → (𝑛 + 1) ∈ ℕ)
105104nnrecred 11677 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (0...(⌊‘𝑌))) → (1 / (𝑛 + 1)) ∈ ℝ)
106100, 105fsumrecl 15081 . . . . . . . . . . . . 13 (𝜑 → Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) ∈ ℝ)
107106, 90readdcld 10659 . . . . . . . . . . . 12 (𝜑 → (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ∈ ℝ)
108 readdcl 10609 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (2 + (log‘𝑌)) ∈ ℝ)
1092, 94, 108sylancr 587 . . . . . . . . . . . . 13 (𝜑 → (2 + (log‘𝑌)) ∈ ℝ)
110109, 90readdcld 10659 . . . . . . . . . . . 12 (𝜑 → ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ∈ ℝ)
11141, 65remulcld 10660 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐾 · 𝑌) ∈ ℝ)
11265recnd 10658 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑌 ∈ ℂ)
113112mulid2d 10648 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 · 𝑌) = 𝑌)
11444, 41, 50ltled 10777 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ≤ 𝐾)
115 lemul1 11481 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ (𝑌 ∈ ℝ ∧ 0 < 𝑌)) → (1 ≤ 𝐾 ↔ (1 · 𝑌) ≤ (𝐾 · 𝑌)))
11644, 41, 65, 79, 115syl112anc 1366 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1 ≤ 𝐾 ↔ (1 · 𝑌) ≤ (𝐾 · 𝑌)))
117114, 116mpbid 233 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 · 𝑌) ≤ (𝐾 · 𝑌))
118113, 117eqbrtrrd 5082 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑌 ≤ (𝐾 · 𝑌))
11942, 65, 111, 80, 118letrd 10786 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (𝐾 · 𝑌))
120 flge0nn0 13180 . . . . . . . . . . . . . . . . . 18 (((𝐾 · 𝑌) ∈ ℝ ∧ 0 ≤ (𝐾 · 𝑌)) → (⌊‘(𝐾 · 𝑌)) ∈ ℕ0)
121111, 119, 120syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℕ0)
122 nn0p1nn 11925 . . . . . . . . . . . . . . . . 17 ((⌊‘(𝐾 · 𝑌)) ∈ ℕ0 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℕ)
123121, 122syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℕ)
124123nnrpd 12419 . . . . . . . . . . . . . . 15 (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℝ+)
125124relogcld 25133 . . . . . . . . . . . . . 14 (𝜑 → (log‘((⌊‘(𝐾 · 𝑌)) + 1)) ∈ ℝ)
126 1zzd 12002 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
127111flcld 13158 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℤ)
128127peano2zd 12079 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℤ)
129 elfznn 12926 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1)) → 𝑘 ∈ ℕ)
130129adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))) → 𝑘 ∈ ℕ)
131 nnrecre 11668 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
132131recnd 10658 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℂ)
133130, 132syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))) → (1 / 𝑘) ∈ ℂ)
134 oveq2 7153 . . . . . . . . . . . . . . . . 17 (𝑘 = (𝑛 + 1) → (1 / 𝑘) = (1 / (𝑛 + 1)))
135126, 126, 128, 133, 134fsumshftm 15126 . . . . . . . . . . . . . . . 16 (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) = Σ𝑛 ∈ ((1 − 1)...(((⌊‘(𝐾 · 𝑌)) + 1) − 1))(1 / (𝑛 + 1)))
136 1m1e0 11698 . . . . . . . . . . . . . . . . . . 19 (1 − 1) = 0
137136a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 − 1) = 0)
138127zcnd 12077 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℂ)
139 ax-1cn 10584 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
140 pncan 10881 . . . . . . . . . . . . . . . . . . 19 (((⌊‘(𝐾 · 𝑌)) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘(𝐾 · 𝑌)) + 1) − 1) = (⌊‘(𝐾 · 𝑌)))
141138, 139, 140sylancl 586 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((⌊‘(𝐾 · 𝑌)) + 1) − 1) = (⌊‘(𝐾 · 𝑌)))
142137, 141oveq12d 7163 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 − 1)...(((⌊‘(𝐾 · 𝑌)) + 1) − 1)) = (0...(⌊‘(𝐾 · 𝑌))))
143142sumeq1d 15048 . . . . . . . . . . . . . . . 16 (𝜑 → Σ𝑛 ∈ ((1 − 1)...(((⌊‘(𝐾 · 𝑌)) + 1) − 1))(1 / (𝑛 + 1)) = Σ𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))
144 reflcl 13156 . . . . . . . . . . . . . . . . . . . 20 (𝑌 ∈ ℝ → (⌊‘𝑌) ∈ ℝ)
14565, 144syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘𝑌) ∈ ℝ)
146145ltp1d 11559 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘𝑌) < ((⌊‘𝑌) + 1))
147 fzdisj 12924 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑌) < ((⌊‘𝑌) + 1) → ((0...(⌊‘𝑌)) ∩ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) = ∅)
148146, 147syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0...(⌊‘𝑌)) ∩ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) = ∅)
149 flwordi 13172 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ ℝ ∧ (𝐾 · 𝑌) ∈ ℝ ∧ 𝑌 ≤ (𝐾 · 𝑌)) → (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌)))
15065, 111, 118, 149syl3anc 1363 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌)))
151 elfz2nn0 12988 . . . . . . . . . . . . . . . . . . 19 ((⌊‘𝑌) ∈ (0...(⌊‘(𝐾 · 𝑌))) ↔ ((⌊‘𝑌) ∈ ℕ0 ∧ (⌊‘(𝐾 · 𝑌)) ∈ ℕ0 ∧ (⌊‘𝑌) ≤ (⌊‘(𝐾 · 𝑌))))
15282, 121, 150, 151syl3anbrc 1335 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘𝑌) ∈ (0...(⌊‘(𝐾 · 𝑌))))
153 fzsplit 12923 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑌) ∈ (0...(⌊‘(𝐾 · 𝑌))) → (0...(⌊‘(𝐾 · 𝑌))) = ((0...(⌊‘𝑌)) ∪ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))))
154152, 153syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (0...(⌊‘(𝐾 · 𝑌))) = ((0...(⌊‘𝑌)) ∪ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))))
155 fzfid 13331 . . . . . . . . . . . . . . . . 17 (𝜑 → (0...(⌊‘(𝐾 · 𝑌))) ∈ Fin)
156 elfznn0 12990 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌))) → 𝑛 ∈ ℕ0)
157156adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℕ0)
158157, 103syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℕ)
159158nnrecred 11677 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℝ)
160159recnd 10658 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℂ)
161148, 154, 155, 160fsumsplit 15087 . . . . . . . . . . . . . . . 16 (𝜑 → Σ𝑛 ∈ (0...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) = (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
162135, 143, 1613eqtrd 2860 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) = (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
163162, 107eqeltrd 2913 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) ∈ ℝ)
164 fllep1 13161 . . . . . . . . . . . . . . . 16 ((𝐾 · 𝑌) ∈ ℝ → (𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1))
165111, 164syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1))
16652, 93rpmulcld 12437 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 · 𝑌) ∈ ℝ+)
167166, 124logled 25137 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐾 · 𝑌) ≤ ((⌊‘(𝐾 · 𝑌)) + 1) ↔ (log‘(𝐾 · 𝑌)) ≤ (log‘((⌊‘(𝐾 · 𝑌)) + 1))))
168165, 167mpbid 233 . . . . . . . . . . . . . 14 (𝜑 → (log‘(𝐾 · 𝑌)) ≤ (log‘((⌊‘(𝐾 · 𝑌)) + 1)))
169 emre 25511 . . . . . . . . . . . . . . . . 17 γ ∈ ℝ
170169a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → γ ∈ ℝ)
171163, 125resubcld 11057 . . . . . . . . . . . . . . . 16 (𝜑 → (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ ℝ)
172 0re 10632 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
173 emgt0 25512 . . . . . . . . . . . . . . . . . 18 0 < γ
174172, 169, 173ltleii 10752 . . . . . . . . . . . . . . . . 17 0 ≤ γ
175174a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ γ)
176 harmonicbnd 25509 . . . . . . . . . . . . . . . . . 18 (((⌊‘(𝐾 · 𝑌)) + 1) ∈ ℕ → (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ (γ[,]1))
177123, 176syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ (γ[,]1))
178169, 43elicc2i 12792 . . . . . . . . . . . . . . . . . 18 ((Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ (γ[,]1) ↔ ((Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∈ ℝ ∧ γ ≤ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ∧ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ≤ 1))
179178simp2bi 1138 . . . . . . . . . . . . . . . . 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 10786 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))))
182163, 125subge0d 11219 . . . . . . . . . . . . . . 15 (𝜑 → (0 ≤ (Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘) − (log‘((⌊‘(𝐾 · 𝑌)) + 1))) ↔ (log‘((⌊‘(𝐾 · 𝑌)) + 1)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘)))
183181, 182mpbid 233 . . . . . . . . . . . . . 14 (𝜑 → (log‘((⌊‘(𝐾 · 𝑌)) + 1)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘))
18499, 125, 163, 168, 183letrd 10786 . . . . . . . . . . . . 13 (𝜑 → (log‘(𝐾 · 𝑌)) ≤ Σ𝑘 ∈ (1...((⌊‘(𝐾 · 𝑌)) + 1))(1 / 𝑘))
185184, 162breqtrd 5084 . . . . . . . . . . . 12 (𝜑 → (log‘(𝐾 · 𝑌)) ≤ (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
18665flcld 13158 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌊‘𝑌) ∈ ℤ)
187186peano2zd 12079 . . . . . . . . . . . . . . . 16 (𝜑 → ((⌊‘𝑌) + 1) ∈ ℤ)
188 elfznn 12926 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (1...((⌊‘𝑌) + 1)) → 𝑘 ∈ ℕ)
189188adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...((⌊‘𝑌) + 1))) → 𝑘 ∈ ℕ)
190189, 132syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...((⌊‘𝑌) + 1))) → (1 / 𝑘) ∈ ℂ)
191126, 126, 187, 190, 134fsumshftm 15126 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) = Σ𝑛 ∈ ((1 − 1)...(((⌊‘𝑌) + 1) − 1))(1 / (𝑛 + 1)))
192145recnd 10658 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘𝑌) ∈ ℂ)
193 pncan 10881 . . . . . . . . . . . . . . . . . 18 (((⌊‘𝑌) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑌) + 1) − 1) = (⌊‘𝑌))
194192, 139, 193sylancl 586 . . . . . . . . . . . . . . . . 17 (𝜑 → (((⌊‘𝑌) + 1) − 1) = (⌊‘𝑌))
195137, 194oveq12d 7163 . . . . . . . . . . . . . . . 16 (𝜑 → ((1 − 1)...(((⌊‘𝑌) + 1) − 1)) = (0...(⌊‘𝑌)))
196195sumeq1d 15048 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑛 ∈ ((1 − 1)...(((⌊‘𝑌) + 1) − 1))(1 / (𝑛 + 1)) = Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)))
197191, 196eqtrd 2856 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) = Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)))
198197, 106eqeltrd 2913 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ∈ ℝ)
19984nnrpd 12419 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘𝑌) + 1) ∈ ℝ+)
200199relogcld 25133 . . . . . . . . . . . . . . . 16 (𝜑 → (log‘((⌊‘𝑌) + 1)) ∈ ℝ)
201 readdcl 10609 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ (log‘((⌊‘𝑌) + 1)) ∈ ℝ) → (1 + (log‘((⌊‘𝑌) + 1))) ∈ ℝ)
20243, 200, 201sylancr 587 . . . . . . . . . . . . . . 15 (𝜑 → (1 + (log‘((⌊‘𝑌) + 1))) ∈ ℝ)
203 harmonicbnd 25509 . . . . . . . . . . . . . . . . . 18 (((⌊‘𝑌) + 1) ∈ ℕ → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈ (γ[,]1))
20484, 203syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈ (γ[,]1))
205169, 43elicc2i 12792 . . . . . . . . . . . . . . . . . 18 ((Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈ (γ[,]1) ↔ ((Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∈ ℝ ∧ γ ≤ (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ∧ (Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ≤ 1))
206205simp3bi 1139 . . . . . . . . . . . . . . . . 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 11226 . . . . . . . . . . . . . . . 16 (𝜑 → ((Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) − (log‘((⌊‘𝑌) + 1))) ≤ 1 ↔ Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ≤ (1 + (log‘((⌊‘𝑌) + 1)))))
209207, 208mpbid 233 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ≤ (1 + (log‘((⌊‘𝑌) + 1))))
210 readdcl 10609 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℝ ∧ (log‘𝑌) ∈ ℝ) → (1 + (log‘𝑌)) ∈ ℝ)
21143, 94, 210sylancr 587 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 + (log‘𝑌)) ∈ ℝ)
212 peano2re 10802 . . . . . . . . . . . . . . . . . . . . 21 ((⌊‘𝑌) ∈ ℝ → ((⌊‘𝑌) + 1) ∈ ℝ)
213145, 212syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((⌊‘𝑌) + 1) ∈ ℝ)
2143, 65remulcld 10660 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 · 𝑌) ∈ ℝ)
215 epr 15551 . . . . . . . . . . . . . . . . . . . . . 22 e ∈ ℝ+
216 rpmulcl 12402 . . . . . . . . . . . . . . . . . . . . . 22 ((e ∈ ℝ+𝑌 ∈ ℝ+) → (e · 𝑌) ∈ ℝ+)
217215, 93, 216sylancr 587 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (e · 𝑌) ∈ ℝ+)
218217rpred 12421 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (e · 𝑌) ∈ ℝ)
219 flle 13159 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 ∈ ℝ → (⌊‘𝑌) ≤ 𝑌)
22065, 219syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (⌊‘𝑌) ≤ 𝑌)
22112, 10rpdivcld 12438 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (2 / 𝐸) ∈ ℝ+)
222 efgt1 15459 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 / 𝐸) ∈ ℝ+ → 1 < (exp‘(2 / 𝐸)))
223221, 222syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 1 < (exp‘(2 / 𝐸)))
224223, 66breqtrrdi 5100 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 < 𝑋)
22544, 70, 65, 224, 78lttrd 10790 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 < 𝑌)
22644, 65, 225ltled 10777 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 ≤ 𝑌)
227145, 44, 65, 65, 220, 226le2addd 11248 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((⌊‘𝑌) + 1) ≤ (𝑌 + 𝑌))
2281122timesd 11869 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 · 𝑌) = (𝑌 + 𝑌))
229227, 228breqtrrd 5086 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((⌊‘𝑌) + 1) ≤ (2 · 𝑌))
230 ere 15432 . . . . . . . . . . . . . . . . . . . . . . 23 e ∈ ℝ
231 egt2lt3 15549 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 < e ∧ e < 3)
232231simpli 484 . . . . . . . . . . . . . . . . . . . . . . 23 2 < e
2332, 230, 232ltleii 10752 . . . . . . . . . . . . . . . . . . . . . 22 2 ≤ e
234233a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ≤ e)
235230a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → e ∈ ℝ)
236 lemul1 11481 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℝ ∧ e ∈ ℝ ∧ (𝑌 ∈ ℝ ∧ 0 < 𝑌)) → (2 ≤ e ↔ (2 · 𝑌) ≤ (e · 𝑌)))
2373, 235, 65, 79, 236syl112anc 1366 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 ≤ e ↔ (2 · 𝑌) ≤ (e · 𝑌)))
238234, 237mpbid 233 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 · 𝑌) ≤ (e · 𝑌))
239213, 214, 218, 229, 238letrd 10786 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((⌊‘𝑌) + 1) ≤ (e · 𝑌))
240199, 217logled 25137 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((⌊‘𝑌) + 1) ≤ (e · 𝑌) ↔ (log‘((⌊‘𝑌) + 1)) ≤ (log‘(e · 𝑌))))
241239, 240mpbid 233 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘((⌊‘𝑌) + 1)) ≤ (log‘(e · 𝑌)))
242 relogmul 25102 . . . . . . . . . . . . . . . . . . . 20 ((e ∈ ℝ+𝑌 ∈ ℝ+) → (log‘(e · 𝑌)) = ((log‘e) + (log‘𝑌)))
243215, 93, 242sylancr 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (log‘(e · 𝑌)) = ((log‘e) + (log‘𝑌)))
244 loge 25097 . . . . . . . . . . . . . . . . . . . 20 (log‘e) = 1
245244oveq1i 7155 . . . . . . . . . . . . . . . . . . 19 ((log‘e) + (log‘𝑌)) = (1 + (log‘𝑌))
246243, 245syl6eq 2872 . . . . . . . . . . . . . . . . . 18 (𝜑 → (log‘(e · 𝑌)) = (1 + (log‘𝑌)))
247241, 246breqtrd 5084 . . . . . . . . . . . . . . . . 17 (𝜑 → (log‘((⌊‘𝑌) + 1)) ≤ (1 + (log‘𝑌)))
248200, 211, 44, 247leadd2dd 11244 . . . . . . . . . . . . . . . 16 (𝜑 → (1 + (log‘((⌊‘𝑌) + 1))) ≤ (1 + (1 + (log‘𝑌))))
249 df-2 11689 . . . . . . . . . . . . . . . . . 18 2 = (1 + 1)
250249oveq1i 7155 . . . . . . . . . . . . . . . . 17 (2 + (log‘𝑌)) = ((1 + 1) + (log‘𝑌))
251139a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℂ)
252251, 251, 95addassd 10652 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 + 1) + (log‘𝑌)) = (1 + (1 + (log‘𝑌))))
253250, 252syl5eq 2868 . . . . . . . . . . . . . . . 16 (𝜑 → (2 + (log‘𝑌)) = (1 + (1 + (log‘𝑌))))
254248, 253breqtrrd 5086 . . . . . . . . . . . . . . 15 (𝜑 → (1 + (log‘((⌊‘𝑌) + 1))) ≤ (2 + (log‘𝑌)))
255198, 202, 109, 209, 254letrd 10786 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ (1...((⌊‘𝑌) + 1))(1 / 𝑘) ≤ (2 + (log‘𝑌)))
256197, 255eqbrtrrd 5082 . . . . . . . . . . . . 13 (𝜑 → Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) ≤ (2 + (log‘𝑌)))
257106, 109, 90, 256leadd1dd 11243 . . . . . . . . . . . 12 (𝜑 → (Σ𝑛 ∈ (0...(⌊‘𝑌))(1 / (𝑛 + 1)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
25899, 107, 110, 185, 257letrd 10786 . . . . . . . . . . 11 (𝜑 → (log‘(𝐾 · 𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
25997, 258eqbrtrrd 5082 . . . . . . . . . 10 (𝜑 → ((log‘𝐾) + (log‘𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))))
26098, 109, 90lesubadd2d 11228 . . . . . . . . . 10 (𝜑 → ((((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ↔ ((log‘𝐾) + (log‘𝑌)) ≤ ((2 + (log‘𝑌)) + Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))))
261259, 260mpbird 258 . . . . . . . . 9 (𝜑 → (((log‘𝐾) + (log‘𝑌)) − (2 + (log‘𝑌))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))
26296, 261eqbrtrrd 5082 . . . . . . . 8 (𝜑 → ((log‘𝐾) − 2) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)))
26389recnd 10658 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (1 / (𝑛 + 1)) ∈ ℂ)
26462, 26, 263fsummulc2 15129 . . . . . . . . . 10 (𝜑 → (𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))))
2656adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ∈ ℝ)
266265recnd 10658 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ∈ ℂ)
26788nncnd 11643 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℂ)
26888nnne0d 11676 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ≠ 0)
269266, 267, 268divrecd 11408 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) = (𝐸 · (1 / (𝑛 + 1))))
270265, 88nndivred 11680 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) ∈ ℝ)
271269, 270eqeltrrd 2914 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 · (1 / (𝑛 + 1))) ∈ ℝ)
27262, 271fsumrecl 15081 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ∈ ℝ)
27387nnrpd 12419 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℝ+)
274 pntpbnd.r . . . . . . . . . . . . . . . . . 18 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
275274pntrf 26067 . . . . . . . . . . . . . . . . 17 𝑅:ℝ+⟶ℝ
276275ffvelrni 6843 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℝ+ → (𝑅𝑛) ∈ ℝ)
277273, 276syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅𝑛) ∈ ℝ)
27887, 88nnmulcld 11679 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
279277, 278nndivred 11680 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
280279recnd 10658 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
281280abscld 14786 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ)
28262, 281fsumrecl 15081 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ)
283277, 87nndivred 11680 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅𝑛) / 𝑛) ∈ ℝ)
284283recnd 10658 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅𝑛) / 𝑛) ∈ ℂ)
285284abscld 14786 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅𝑛) / 𝑛)) ∈ ℝ)
28688nnrpd 12419 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℝ+)
287 pntpbnd1.3 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸))
288287adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸))
289 elfzle1 12900 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → ((⌊‘𝑌) + 1) ≤ 𝑛)
290289adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) + 1) ≤ 𝑛)
29165adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑌 ∈ ℝ)
292291flcld 13158 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (⌊‘𝑌) ∈ ℤ)
29387nnzd 12075 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℤ)
294 zltp1le 12021 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘𝑌) ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((⌊‘𝑌) < 𝑛 ↔ ((⌊‘𝑌) + 1) ≤ 𝑛))
295292, 293, 294syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) < 𝑛 ↔ ((⌊‘𝑌) + 1) ≤ 𝑛))
296290, 295mpbird 258 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (⌊‘𝑌) < 𝑛)
297 fllt 13166 . . . . . . . . . . . . . . . . . . 19 ((𝑌 ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑌 < 𝑛 ↔ (⌊‘𝑌) < 𝑛))
298291, 293, 297syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑌 < 𝑛 ↔ (⌊‘𝑌) < 𝑛))
299296, 298mpbird 258 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑌 < 𝑛)
300 elfzle2 12901 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑛 ≤ (⌊‘(𝐾 · 𝑌)))
301300adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≤ (⌊‘(𝐾 · 𝑌)))
302111adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐾 · 𝑌) ∈ ℝ)
303 flge 13165 . . . . . . . . . . . . . . . . . . 19 (((𝐾 · 𝑌) ∈ ℝ ∧ 𝑛 ∈ ℤ) → (𝑛 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (⌊‘(𝐾 · 𝑌))))
304302, 293, 303syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (⌊‘(𝐾 · 𝑌))))
305301, 304mpbird 258 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≤ (𝐾 · 𝑌))
306 breq2 5062 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑛 → (𝑌 < 𝑦𝑌 < 𝑛))
307 breq1 5061 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑛 → (𝑦 ≤ (𝐾 · 𝑌) ↔ 𝑛 ≤ (𝐾 · 𝑌)))
308306, 307anbi12d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑛 → ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ↔ (𝑌 < 𝑛𝑛 ≤ (𝐾 · 𝑌))))
309 fveq2 6664 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑛 → (𝑅𝑦) = (𝑅𝑛))
310 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑛𝑦 = 𝑛)
311309, 310oveq12d 7163 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑛 → ((𝑅𝑦) / 𝑦) = ((𝑅𝑛) / 𝑛))
312311fveq2d 6668 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑛 → (abs‘((𝑅𝑦) / 𝑦)) = (abs‘((𝑅𝑛) / 𝑛)))
313312breq1d 5068 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑛 → ((abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸 ↔ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸))
314308, 313anbi12d 630 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑛 → (((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸) ↔ ((𝑌 < 𝑛𝑛 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸)))
315314rspcev 3622 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ ((𝑌 < 𝑛𝑛 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸)) → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸))
316315expr 457 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ ∧ (𝑌 < 𝑛𝑛 ≤ (𝐾 · 𝑌))) → ((abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸 → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸)))
31787, 299, 305, 316syl12anc 832 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸 → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸)))
318288, 317mtod 199 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸)
319285, 265letrid 10781 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸𝐸 ≤ (abs‘((𝑅𝑛) / 𝑛))))
320319ord 858 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (¬ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝐸𝐸 ≤ (abs‘((𝑅𝑛) / 𝑛))))
321318, 320mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝐸 ≤ (abs‘((𝑅𝑛) / 𝑛)))
322265, 285, 286, 321lediv1dd 12479 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 / (𝑛 + 1)) ≤ ((abs‘((𝑅𝑛) / 𝑛)) / (𝑛 + 1)))
323284, 267, 268absdivd 14805 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(((𝑅𝑛) / 𝑛) / (𝑛 + 1))) = ((abs‘((𝑅𝑛) / 𝑛)) / (abs‘(𝑛 + 1))))
324277recnd 10658 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅𝑛) ∈ ℂ)
32587nncnd 11643 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℂ)
32687nnne0d 11676 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ≠ 0)
327324, 325, 267, 326, 268divdiv1d 11436 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (((𝑅𝑛) / 𝑛) / (𝑛 + 1)) = ((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
328327fveq2d 6668 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(((𝑅𝑛) / 𝑛) / (𝑛 + 1))) = (abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
329286rprege0d 12428 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑛 + 1) ∈ ℝ ∧ 0 ≤ (𝑛 + 1)))
330 absid 14646 . . . . . . . . . . . . . . . 16 (((𝑛 + 1) ∈ ℝ ∧ 0 ≤ (𝑛 + 1)) → (abs‘(𝑛 + 1)) = (𝑛 + 1))
331329, 330syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘(𝑛 + 1)) = (𝑛 + 1))
332331oveq2d 7161 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅𝑛) / 𝑛)) / (abs‘(𝑛 + 1))) = ((abs‘((𝑅𝑛) / 𝑛)) / (𝑛 + 1)))
333323, 328, 3323eqtr3rd 2865 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((abs‘((𝑅𝑛) / 𝑛)) / (𝑛 + 1)) = (abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
334322, 269, 3333brtr3d 5089 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝐸 · (1 / (𝑛 + 1))) ≤ (abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
33562, 271, 281, 334fsumle 15144 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
336 pntpbnd1.2 . . . . . . . . . . . 12 (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴)
337274, 5, 66, 64, 15, 336, 13, 36, 287pntpbnd1 26090 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴)
338272, 282, 32, 335, 337letrd 10786 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝐸 · (1 / (𝑛 + 1))) ≤ 𝐴)
339264, 338eqbrtrd 5080 . . . . . . . . 9 (𝜑 → (𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ 𝐴)
34090, 32, 10lemuldiv2d 12471 . . . . . . . . 9 (𝜑 → ((𝐸 · Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1))) ≤ 𝐴 ↔ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ≤ (𝐴 / 𝐸)))
341339, 340mpbid 233 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(1 / (𝑛 + 1)) ≤ (𝐴 / 𝐸))
34255, 90, 33, 262, 341letrd 10786 . . . . . . 7 (𝜑 → ((log‘𝐾) − 2) ≤ (𝐴 / 𝐸))
34335, 55, 33, 61, 342letrd 10786 . . . . . 6 (𝜑 → ((𝐶 / 𝐸) − 2) ≤ (𝐴 / 𝐸))
34431, 3, 33, 343subled 11232 . . . . 5 (𝜑 → ((𝐶 / 𝐸) − (𝐴 / 𝐸)) ≤ 2)
34529, 344eqbrtrd 5080 . . . 4 (𝜑 → (2 / 𝐸) ≤ 2)
3463, 10, 12, 345lediv23d 12489 . . 3 (𝜑 → (2 / 2) ≤ 𝐸)
3471, 346eqbrtrrid 5094 . 2 (𝜑 → 1 ≤ 𝐸)
3488simprd 496 . . 3 (𝜑𝐸 < 1)
349 ltnle 10709 . . . 4 ((𝐸 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐸 < 1 ↔ ¬ 1 ≤ 𝐸))
3506, 43, 349sylancl 586 . . 3 (𝜑 → (𝐸 < 1 ↔ ¬ 1 ≤ 𝐸))
351348, 350mpbid 233 . 2 (𝜑 → ¬ 1 ≤ 𝐸)
352347, 351pm2.65i 195 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wral 3138  wrex 3139  cun 3933  cin 3934  c0 4290   class class class wbr 5058  cmpt 5138  cfv 6349  (class class class)co 7145  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  +∞cpnf 10661  *cxr 10663   < clt 10664  cle 10665  cmin 10859   / cdiv 11286  cn 11627  2c2 11681  3c3 11682  0cn0 11886  cz 11970  cuz 12232  +crp 12379  (,)cioo 12728  [,)cico 12730  [,]cicc 12731  ...cfz 12882  cfl 13150  abscabs 14583  Σcsu 15032  expce 15405  eceu 15406  logclog 25065  γcem 25497  ψcchp 25598
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-inf2 9093  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-iin 4915  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7569  df-1st 7680  df-2nd 7681  df-supp 7822  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-2o 8094  df-oadd 8097  df-er 8279  df-map 8398  df-pm 8399  df-ixp 8451  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-fsupp 8823  df-fi 8864  df-sup 8895  df-inf 8896  df-oi 8963  df-dju 9319  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-xnn0 11957  df-z 11971  df-dec 12088  df-uz 12233  df-q 12338  df-rp 12380  df-xneg 12497  df-xadd 12498  df-xmul 12499  df-ioo 12732  df-ioc 12733  df-ico 12734  df-icc 12735  df-fz 12883  df-fzo 13024  df-fl 13152  df-mod 13228  df-seq 13360  df-exp 13420  df-fac 13624  df-bc 13653  df-hash 13681  df-shft 14416  df-cj 14448  df-re 14449  df-im 14450  df-sqrt 14584  df-abs 14585  df-limsup 14818  df-clim 14835  df-rlim 14836  df-sum 15033  df-ef 15411  df-e 15412  df-sin 15413  df-cos 15414  df-tan 15415  df-pi 15416  df-dvds 15598  df-gcd 15834  df-prm 16006  df-pc 16164  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-ress 16481  df-plusg 16568  df-mulr 16569  df-starv 16570  df-sca 16571  df-vsca 16572  df-ip 16573  df-tset 16574  df-ple 16575  df-ds 16577  df-unif 16578  df-hom 16579  df-cco 16580  df-rest 16686  df-topn 16687  df-0g 16705  df-gsum 16706  df-topgen 16707  df-pt 16708  df-prds 16711  df-xrs 16765  df-qtop 16770  df-imas 16771  df-xps 16773  df-mre 16847  df-mrc 16848  df-acs 16850  df-mgm 17842  df-sgrp 17891  df-mnd 17902  df-submnd 17947  df-mulg 18165  df-cntz 18387  df-cmn 18839  df-psmet 20467  df-xmet 20468  df-met 20469  df-bl 20470  df-mopn 20471  df-fbas 20472  df-fg 20473  df-cnfld 20476  df-top 21432  df-topon 21449  df-topsp 21471  df-bases 21484  df-cld 21557  df-ntr 21558  df-cls 21559  df-nei 21636  df-lp 21674  df-perf 21675  df-cn 21765  df-cnp 21766  df-haus 21853  df-cmp 21925  df-tx 22100  df-hmeo 22293  df-fil 22384  df-fm 22476  df-flim 22477  df-flf 22478  df-xms 22859  df-ms 22860  df-tms 22861  df-cncf 23415  df-limc 24393  df-dv 24394  df-ulm 24894  df-log 25067  df-atan 25372  df-em 25498  df-vma 25603  df-chp 25604
This theorem is referenced by:  pntpbnd  26092
  Copyright terms: Public domain W3C validator