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

Theorem logfacbnd3 25400
Description: Show the stronger statement log(𝑥!) = 𝑥log𝑥𝑥 + 𝑂(log𝑥) alluded to in logfacrlim 25401. (Contributed by Mario Carneiro, 20-May-2016.)
Assertion
Ref Expression
logfacbnd3 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1))

Proof of Theorem logfacbnd3
Dummy variables 𝑥 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 476 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ+)
21rprege0d 12188 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
3 flge0nn0 12940 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0)
42, 3syl 17 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0)
5 faccl 13388 . . . . . . . . . 10 ((⌊‘𝐴) ∈ ℕ0 → (!‘(⌊‘𝐴)) ∈ ℕ)
64, 5syl 17 . . . . . . . . 9 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (!‘(⌊‘𝐴)) ∈ ℕ)
76nnrpd 12179 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (!‘(⌊‘𝐴)) ∈ ℝ+)
8 relogcl 24759 . . . . . . . 8 ((!‘(⌊‘𝐴)) ∈ ℝ+ → (log‘(!‘(⌊‘𝐴))) ∈ ℝ)
97, 8syl 17 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) ∈ ℝ)
10 rpre 12145 . . . . . . . . 9 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
1110adantr 474 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ)
12 relogcl 24759 . . . . . . . . . 10 (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
1312adantr 474 . . . . . . . . 9 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℝ)
14 peano2rem 10690 . . . . . . . . 9 ((log‘𝐴) ∈ ℝ → ((log‘𝐴) − 1) ∈ ℝ)
1513, 14syl 17 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((log‘𝐴) − 1) ∈ ℝ)
1611, 15remulcld 10407 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (𝐴 · ((log‘𝐴) − 1)) ∈ ℝ)
179, 16resubcld 10803 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℝ)
1817recnd 10405 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ)
1918abscld 14583 . . . 4 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ∈ ℝ)
20 peano2rem 10690 . . . 4 ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ∈ ℝ → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ∈ ℝ)
2119, 20syl 17 . . 3 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ∈ ℝ)
22 ax-1cn 10330 . . . . 5 1 ∈ ℂ
23 subcl 10621 . . . . 5 ((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈ ℂ) → (((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈ ℂ)
2418, 22, 23sylancl 580 . . . 4 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈ ℂ)
2524abscld 14583 . . 3 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ∈ ℝ)
26 abs1 14444 . . . . 5 (abs‘1) = 1
2726oveq2i 6933 . . . 4 ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) = ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1)
28 abs2dif 14479 . . . . 5 ((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈ ℂ) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) ≤ (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)))
2918, 22, 28sylancl 580 . . . 4 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) ≤ (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)))
3027, 29syl5eqbrr 4922 . . 3 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤ (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)))
31 fveq2 6446 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (⌊‘𝑥) = (⌊‘𝐴))
3231oveq2d 6938 . . . . . . . . . . 11 (𝑥 = 𝐴 → (1...(⌊‘𝑥)) = (1...(⌊‘𝐴)))
3332sumeq1d 14839 . . . . . . . . . 10 (𝑥 = 𝐴 → Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
34 id 22 . . . . . . . . . . 11 (𝑥 = 𝐴𝑥 = 𝐴)
35 fveq2 6446 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (log‘𝑥) = (log‘𝐴))
3635oveq1d 6937 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((log‘𝑥) − 1) = ((log‘𝐴) − 1))
3734, 36oveq12d 6940 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝑥 · ((log‘𝑥) − 1)) = (𝐴 · ((log‘𝐴) − 1)))
3833, 37oveq12d 6940 . . . . . . . . 9 (𝑥 = 𝐴 → (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1))))
39 eqid 2778 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))
40 ovex 6954 . . . . . . . . 9 𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) ∈ V
4138, 39, 40fvmpt3i 6547 . . . . . . . 8 (𝐴 ∈ ℝ+ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1))))
4241adantr 474 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1))))
43 logfac 24784 . . . . . . . . 9 ((⌊‘𝐴) ∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
444, 43syl 17 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
4544oveq1d 6937 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1))))
4642, 45eqtr4d 2817 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = ((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))))
47 1rp 12141 . . . . . . 7 1 ∈ ℝ+
48 fveq2 6446 . . . . . . . . . . . . . 14 (𝑥 = 1 → (⌊‘𝑥) = (⌊‘1))
49 1z 11759 . . . . . . . . . . . . . . 15 1 ∈ ℤ
50 flid 12928 . . . . . . . . . . . . . . 15 (1 ∈ ℤ → (⌊‘1) = 1)
5149, 50ax-mp 5 . . . . . . . . . . . . . 14 (⌊‘1) = 1
5248, 51syl6eq 2830 . . . . . . . . . . . . 13 (𝑥 = 1 → (⌊‘𝑥) = 1)
5352oveq2d 6938 . . . . . . . . . . . 12 (𝑥 = 1 → (1...(⌊‘𝑥)) = (1...1))
5453sumeq1d 14839 . . . . . . . . . . 11 (𝑥 = 1 → Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...1)(log‘𝑛))
55 0cn 10368 . . . . . . . . . . . 12 0 ∈ ℂ
56 fveq2 6446 . . . . . . . . . . . . . 14 (𝑛 = 1 → (log‘𝑛) = (log‘1))
57 log1 24769 . . . . . . . . . . . . . 14 (log‘1) = 0
5856, 57syl6eq 2830 . . . . . . . . . . . . 13 (𝑛 = 1 → (log‘𝑛) = 0)
5958fsum1 14883 . . . . . . . . . . . 12 ((1 ∈ ℤ ∧ 0 ∈ ℂ) → Σ𝑛 ∈ (1...1)(log‘𝑛) = 0)
6049, 55, 59mp2an 682 . . . . . . . . . . 11 Σ𝑛 ∈ (1...1)(log‘𝑛) = 0
6154, 60syl6eq 2830 . . . . . . . . . 10 (𝑥 = 1 → Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) = 0)
62 id 22 . . . . . . . . . . . 12 (𝑥 = 1 → 𝑥 = 1)
63 fveq2 6446 . . . . . . . . . . . . . 14 (𝑥 = 1 → (log‘𝑥) = (log‘1))
6463, 57syl6eq 2830 . . . . . . . . . . . . 13 (𝑥 = 1 → (log‘𝑥) = 0)
6564oveq1d 6937 . . . . . . . . . . . 12 (𝑥 = 1 → ((log‘𝑥) − 1) = (0 − 1))
6662, 65oveq12d 6940 . . . . . . . . . . 11 (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (1 · (0 − 1)))
6755, 22subcli 10699 . . . . . . . . . . . 12 (0 − 1) ∈ ℂ
6867mulid2i 10382 . . . . . . . . . . 11 (1 · (0 − 1)) = (0 − 1)
6966, 68syl6eq 2830 . . . . . . . . . 10 (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (0 − 1))
7061, 69oveq12d 6940 . . . . . . . . 9 (𝑥 = 1 → (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (0 − (0 − 1)))
71 nncan 10652 . . . . . . . . . 10 ((0 ∈ ℂ ∧ 1 ∈ ℂ) → (0 − (0 − 1)) = 1)
7255, 22, 71mp2an 682 . . . . . . . . 9 (0 − (0 − 1)) = 1
7370, 72syl6eq 2830 . . . . . . . 8 (𝑥 = 1 → (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = 1)
7473, 39, 40fvmpt3i 6547 . . . . . . 7 (1 ∈ ℝ+ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1) = 1)
7547, 74mp1i 13 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1) = 1)
7646, 75oveq12d 6940 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1)) = (((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))
7776fveq2d 6450 . . . 4 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘(((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) = (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)))
78 ioorp 12563 . . . . . 6 (0(,)+∞) = ℝ+
7978eqcomi 2787 . . . . 5 + = (0(,)+∞)
80 nnuz 12029 . . . . 5 ℕ = (ℤ‘1)
8149a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ∈ ℤ)
82 1re 10376 . . . . . 6 1 ∈ ℝ
8382a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ∈ ℝ)
84 pnfxr 10430 . . . . . 6 +∞ ∈ ℝ*
8584a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → +∞ ∈ ℝ*)
86 1nn0 11660 . . . . . . 7 1 ∈ ℕ0
8782, 86nn0addge1i 11692 . . . . . 6 1 ≤ (1 + 1)
8887a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ≤ (1 + 1))
89 0red 10380 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 0 ∈ ℝ)
90 rpre 12145 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
9190adantl 475 . . . . . 6 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
92 relogcl 24759 . . . . . . . 8 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
9392adantl 475 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
94 peano2rem 10690 . . . . . . 7 ((log‘𝑥) ∈ ℝ → ((log‘𝑥) − 1) ∈ ℝ)
9593, 94syl 17 . . . . . 6 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) − 1) ∈ ℝ)
9691, 95remulcld 10407 . . . . 5 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ+) → (𝑥 · ((log‘𝑥) − 1)) ∈ ℝ)
97 nnrp 12150 . . . . . 6 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ+)
9897, 93sylan2 586 . . . . 5 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℕ) → (log‘𝑥) ∈ ℝ)
99 advlog 24837 . . . . . 6 (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥))
10099a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)))
101 fveq2 6446 . . . . 5 (𝑥 = 𝑛 → (log‘𝑥) = (log‘𝑛))
102 simp32 1224 . . . . . 6 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → 𝑥𝑛)
103 logleb 24786 . . . . . . 7 ((𝑥 ∈ ℝ+𝑛 ∈ ℝ+) → (𝑥𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛)))
1041033ad2ant2 1125 . . . . . 6 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → (𝑥𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛)))
105102, 104mpbid 224 . . . . 5 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+𝑛 ∈ ℝ+) ∧ (1 ≤ 𝑥𝑥𝑛𝑛 ≤ +∞)) → (log‘𝑥) ≤ (log‘𝑛))
106 simprr 763 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
107 simprl 761 . . . . . . . 8 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
108 logleb 24786 . . . . . . . 8 ((1 ∈ ℝ+𝑥 ∈ ℝ+) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
10947, 107, 108sylancr 581 . . . . . . 7 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
110106, 109mpbid 224 . . . . . 6 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥))
11157, 110syl5eqbrr 4922 . . . . 5 (((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥))
11247a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ∈ ℝ+)
113 1le1 11003 . . . . . 6 1 ≤ 1
114113a1i 11 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ≤ 1)
115 simpr 479 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 1 ≤ 𝐴)
11611rexrd 10426 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ*)
117 pnfge 12275 . . . . . 6 (𝐴 ∈ ℝ*𝐴 ≤ +∞)
118116, 117syl 17 . . . . 5 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → 𝐴 ≤ +∞)
11979, 80, 81, 83, 85, 88, 89, 96, 93, 98, 100, 101, 105, 39, 111, 112, 1, 114, 115, 118, 35dvfsum2 24234 . . . 4 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘(((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) ≤ (log‘𝐴))
12077, 119eqbrtrrd 4910 . . 3 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ≤ (log‘𝐴))
12121, 25, 13, 30, 120letrd 10533 . 2 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤ (log‘𝐴))
12219, 83, 13lesubaddd 10972 . 2 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤ (log‘𝐴) ↔ (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1)))
123121, 122mpbid 224 1 ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2107   class class class wbr 4886  cmpt 4965  cfv 6135  (class class class)co 6922  cc 10270  cr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277  +∞cpnf 10408  *cxr 10410  cle 10412  cmin 10606  cn 11374  0cn0 11642  cz 11728  +crp 12137  (,)cioo 12487  ...cfz 12643  cfl 12910  !cfa 13378  abscabs 14381  Σcsu 14824   D cdv 24064  logclog 24738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351  ax-mulf 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-ixp 8195  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fsupp 8564  df-fi 8605  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-z 11729  df-dec 11846  df-uz 11993  df-q 12096  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-ioo 12491  df-ioc 12492  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179  df-fac 13379  df-bc 13408  df-hash 13436  df-shft 14214  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-limsup 14610  df-clim 14627  df-rlim 14628  df-sum 14825  df-ef 15200  df-sin 15202  df-cos 15203  df-pi 15205  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-mulr 16352  df-starv 16353  df-sca 16354  df-vsca 16355  df-ip 16356  df-tset 16357  df-ple 16358  df-ds 16360  df-unif 16361  df-hom 16362  df-cco 16363  df-rest 16469  df-topn 16470  df-0g 16488  df-gsum 16489  df-topgen 16490  df-pt 16491  df-prds 16494  df-xrs 16548  df-qtop 16553  df-imas 16554  df-xps 16556  df-mre 16632  df-mrc 16633  df-acs 16635  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-submnd 17722  df-mulg 17928  df-cntz 18133  df-cmn 18581  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137  df-mopn 20138  df-fbas 20139  df-fg 20140  df-cnfld 20143  df-top 21106  df-topon 21123  df-topsp 21145  df-bases 21158  df-cld 21231  df-ntr 21232  df-cls 21233  df-nei 21310  df-lp 21348  df-perf 21349  df-cn 21439  df-cnp 21440  df-haus 21527  df-cmp 21599  df-tx 21774  df-hmeo 21967  df-fil 22058  df-fm 22150  df-flim 22151  df-flf 22152  df-xms 22533  df-ms 22534  df-tms 22535  df-cncf 23089  df-limc 24067  df-dv 24068  df-log 24740
This theorem is referenced by:  logfacrlim  25401
  Copyright terms: Public domain W3C validator