logfacbnd3 - Metamath Proof Explorer

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

Theorem logfacbnd3 26723

Description: Show the stronger statement log(𝑥!) = 𝑥log𝑥 − 𝑥 + 𝑂(log𝑥) alluded to in logfacrlim 26724. (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.

Step	Hyp	Ref	Expression
1		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ⁺)
2	1	rprege0d 13022	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
3		flge0nn0 13784	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ₀)
4	2, 3	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ₀)
5	4	faccld 14243	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (!‘(⌊‘𝐴)) ∈ ℕ)
6	5	nnrpd 13013	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (!‘(⌊‘𝐴)) ∈ ℝ⁺)
7		relogcl 26083	. . . . . . . 8 ⊢ ((!‘(⌊‘𝐴)) ∈ ℝ⁺ → (log‘(!‘(⌊‘𝐴))) ∈ ℝ)
8	6, 7	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) ∈ ℝ)
9		rpre 12981	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ)
10	9	adantr 481	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ)
11		relogcl 26083	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ⁺ → (log‘𝐴) ∈ ℝ)
12	11	adantr 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℝ)
13		peano2rem 11526	. . . . . . . . 9 ⊢ ((log‘𝐴) ∈ ℝ → ((log‘𝐴) − 1) ∈ ℝ)
14	12, 13	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((log‘𝐴) − 1) ∈ ℝ)
15	10, 14	remulcld 11243	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (𝐴 · ((log‘𝐴) − 1)) ∈ ℝ)
16	8, 15	resubcld 11641	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℝ)
17	16	recnd 11241	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ)
18	17	abscld 15382	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ∈ ℝ)
19		peano2rem 11526	. . . 4 ⊢ ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ∈ ℝ → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ∈ ℝ)
20	18, 19	syl 17	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ∈ ℝ)
21		ax-1cn 11167	. . . . 5 ⊢ 1 ∈ ℂ
22		subcl 11458	. . . . 5 ⊢ ((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈ ℂ) → (((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈ ℂ)
23	17, 21, 22	sylancl 586	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1) ∈ ℂ)
24	23	abscld 15382	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ∈ ℝ)
25		abs1 15243	. . . . 5 ⊢ (abs‘1) = 1
26	25	oveq2i 7419	. . . 4 ⊢ ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) = ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1)
27		abs2dif 15278	. . . . 5 ⊢ ((((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) ∈ ℂ ∧ 1 ∈ ℂ) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) ≤ (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)))
28	17, 21, 27	sylancl 586	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − (abs‘1)) ≤ (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)))
29	26, 28	eqbrtrrid 5184	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤ (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)))
30		fveq2 6891	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐴 → (⌊‘𝑥) = (⌊‘𝐴))
31	30	oveq2d 7424	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → (1...(⌊‘𝑥)) = (1...(⌊‘𝐴)))
32	31	sumeq1d 15646	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
33		id 22	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
34		fveq2 6891	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐴 → (log‘𝑥) = (log‘𝐴))
35	34	oveq1d 7423	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → ((log‘𝑥) − 1) = ((log‘𝐴) − 1))
36	33, 35	oveq12d 7426	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝑥 · ((log‘𝑥) − 1)) = (𝐴 · ((log‘𝐴) − 1)))
37	32, 36	oveq12d 7426	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1))))
38		eqid 2732	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))
39		ovex 7441	. . . . . . . . 9 ⊢ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) ∈ V
40	37, 38, 39	fvmpt3i 7003	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ⁺ → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1))))
41	40	adantr 481	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1))))
42		logfac 26108	. . . . . . . . 9 ⊢ ((⌊‘𝐴) ∈ ℕ₀ → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
43	4, 42	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛))
44	43	oveq1d 7423	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) − (𝐴 · ((log‘𝐴) − 1))))
45	41, 44	eqtr4d 2775	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) = ((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))))
46		1rp 12977	. . . . . . 7 ⊢ 1 ∈ ℝ⁺
47		fveq2 6891	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (⌊‘𝑥) = (⌊‘1))
48		1z 12591	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
49		flid 13772	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℤ → (⌊‘1) = 1)
50	48, 49	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (⌊‘1) = 1
51	47, 50	eqtrdi 2788	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (⌊‘𝑥) = 1)
52	51	oveq2d 7424	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (1...(⌊‘𝑥)) = (1...1))
53	52	sumeq1d 15646	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) = Σ𝑛 ∈ (1...1)(log‘𝑛))
54		0cn 11205	. . . . . . . . . . . 12 ⊢ 0 ∈ ℂ
55		fveq2 6891	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (log‘𝑛) = (log‘1))
56		log1 26093	. . . . . . . . . . . . . 14 ⊢ (log‘1) = 0
57	55, 56	eqtrdi 2788	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (log‘𝑛) = 0)
58	57	fsum1 15692	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℤ ∧ 0 ∈ ℂ) → Σ𝑛 ∈ (1...1)(log‘𝑛) = 0)
59	48, 54, 58	mp2an 690	. . . . . . . . . . 11 ⊢ Σ𝑛 ∈ (1...1)(log‘𝑛) = 0
60	53, 59	eqtrdi 2788	. . . . . . . . . 10 ⊢ (𝑥 = 1 → Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) = 0)
61		id 22	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → 𝑥 = 1)
62		fveq2 6891	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (log‘𝑥) = (log‘1))
63	62, 56	eqtrdi 2788	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (log‘𝑥) = 0)
64	63	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → ((log‘𝑥) − 1) = (0 − 1))
65	61, 64	oveq12d 7426	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (1 · (0 − 1)))
66	54, 21	subcli 11535	. . . . . . . . . . . 12 ⊢ (0 − 1) ∈ ℂ
67	66	mullidi 11218	. . . . . . . . . . 11 ⊢ (1 · (0 − 1)) = (0 − 1)
68	65, 67	eqtrdi 2788	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (𝑥 · ((log‘𝑥) − 1)) = (0 − 1))
69	60, 68	oveq12d 7426	. . . . . . . . 9 ⊢ (𝑥 = 1 → (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = (0 − (0 − 1)))
70		nncan 11488	. . . . . . . . . 10 ⊢ ((0 ∈ ℂ ∧ 1 ∈ ℂ) → (0 − (0 − 1)) = 1)
71	54, 21, 70	mp2an 690	. . . . . . . . 9 ⊢ (0 − (0 − 1)) = 1
72	69, 71	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑥 = 1 → (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))) = 1)
73	72, 38, 39	fvmpt3i 7003	. . . . . . 7 ⊢ (1 ∈ ℝ⁺ → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1) = 1)
74	46, 73	mp1i 13	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1) = 1)
75	45, 74	oveq12d 7426	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1)) = (((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1))
76	75	fveq2d 6895	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (abs‘(((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) = (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)))
77		ioorp 13401	. . . . . 6 ⊢ (0(,)+∞) = ℝ⁺
78	77	eqcomi 2741	. . . . 5 ⊢ ℝ⁺ = (0(,)+∞)
79		nnuz 12864	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
80	48	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 1 ∈ ℤ)
81		1re 11213	. . . . . 6 ⊢ 1 ∈ ℝ
82	81	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 1 ∈ ℝ)
83		pnfxr 11267	. . . . . 6 ⊢ +∞ ∈ ℝ^*
84	83	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → +∞ ∈ ℝ^*)
85		1nn0 12487	. . . . . . 7 ⊢ 1 ∈ ℕ₀
86	81, 85	nn0addge1i 12519	. . . . . 6 ⊢ 1 ≤ (1 + 1)
87	86	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 1 ≤ (1 + 1))
88		0red 11216	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 0 ∈ ℝ)
89		rpre 12981	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
90	89	adantl 482	. . . . . 6 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
91		relogcl 26083	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℝ)
92	91	adantl 482	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℝ)
93		peano2rem 11526	. . . . . . 7 ⊢ ((log‘𝑥) ∈ ℝ → ((log‘𝑥) − 1) ∈ ℝ)
94	92, 93	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ⁺) → ((log‘𝑥) − 1) ∈ ℝ)
95	90, 94	remulcld 11243	. . . . 5 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℝ⁺) → (𝑥 · ((log‘𝑥) − 1)) ∈ ℝ)
96		nnrp 12984	. . . . . 6 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℝ⁺)
97	96, 92	sylan2 593	. . . . 5 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ 𝑥 ∈ ℕ) → (log‘𝑥) ∈ ℝ)
98		advlog 26161	. . . . . 6 ⊢ (ℝ D (𝑥 ∈ ℝ⁺ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ⁺ ↦ (log‘𝑥))
99	98	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (ℝ D (𝑥 ∈ ℝ⁺ ↦ (𝑥 · ((log‘𝑥) − 1)))) = (𝑥 ∈ ℝ⁺ ↦ (log‘𝑥)))
100		fveq2 6891	. . . . 5 ⊢ (𝑥 = 𝑛 → (log‘𝑥) = (log‘𝑛))
101		simp32 1210	. . . . . 6 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → 𝑥 ≤ 𝑛)
102		logleb 26110	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 ≤ 𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛)))
103	102	3ad2ant2 1134	. . . . . 6 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → (𝑥 ≤ 𝑛 ↔ (log‘𝑥) ≤ (log‘𝑛)))
104	101, 103	mpbid 231	. . . . 5 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ∧ 𝑛 ≤ +∞)) → (log‘𝑥) ≤ (log‘𝑛))
105		simprr 771	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
106		simprl 769	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ⁺)
107		logleb 26110	. . . . . . . 8 ⊢ ((1 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
108	46, 106, 107	sylancr 587	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
109	105, 108	mpbid 231	. . . . . 6 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥))
110	56, 109	eqbrtrrid 5184	. . . . 5 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥))
111	46	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 1 ∈ ℝ⁺)
112		1le1 11841	. . . . . 6 ⊢ 1 ≤ 1
113	112	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 1 ≤ 1)
114		simpr 485	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 1 ≤ 𝐴)
115	10	rexrd 11263	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ^*)
116		pnfge 13109	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
117	115, 116	syl 17	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → 𝐴 ≤ +∞)
118	78, 79, 80, 82, 84, 87, 88, 95, 92, 97, 99, 100, 104, 38, 110, 111, 1, 113, 114, 117, 34	dvfsum2 25550	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (abs‘(((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘𝐴) − ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(log‘𝑛) − (𝑥 · ((log‘𝑥) − 1))))‘1))) ≤ (log‘𝐴))
119	76, 118	eqbrtrrd 5172	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (abs‘(((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1))) − 1)) ≤ (log‘𝐴))
120	20, 24, 12, 29, 119	letrd 11370	. 2 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → ((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤ (log‘𝐴))
121	18, 82, 12	lesubaddd 11810	. 2 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (((abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) − 1) ≤ (log‘𝐴) ↔ (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1)))
122	120, 121	mpbid 231	1 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 1 ≤ 𝐴) → (abs‘((log‘(!‘(⌊‘𝐴))) − (𝐴 · ((log‘𝐴) − 1)))) ≤ ((log‘𝐴) + 1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 class class class wbr 5148 ↦ cmpt 5231 ‘cfv 6543 (class class class)co 7408 ℂcc 11107 ℝcr 11108 0cc0 11109 1c1 11110 + caddc 11112 · cmul 11114 +∞cpnf 11244 ℝ^*cxr 11246 ≤ cle 11248 − cmin 11443 ℕcn 12211 ℕ₀cn0 12471 ℤcz 12557 ℝ⁺crp 12973 (,)cioo 13323 ...cfz 13483 ⌊cfl 13754 !cfa 14232 abscabs 15180 Σcsu 15631 D cdv 25379 logclog 26062

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7724 ax-inf2 9635 ax-cnex 11165 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186 ax-pre-sup 11187 ax-addf 11188 ax-mulf 11189

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7364 df-ov 7411 df-oprab 7412 df-mpo 7413 df-of 7669 df-om 7855 df-1st 7974 df-2nd 7975 df-supp 8146 df-frecs 8265 df-wrecs 8296 df-recs 8370 df-rdg 8409 df-1o 8465 df-2o 8466 df-er 8702 df-map 8821 df-pm 8822 df-ixp 8891 df-en 8939 df-dom 8940 df-sdom 8941 df-fin 8942 df-fsupp 9361 df-fi 9405 df-sup 9436 df-inf 9437 df-oi 9504 df-card 9933 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11445 df-neg 11446 df-div 11871 df-nn 12212 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-7 12279 df-8 12280 df-9 12281 df-n0 12472 df-z 12558 df-dec 12677 df-uz 12822 df-q 12932 df-rp 12974 df-xneg 13091 df-xadd 13092 df-xmul 13093 df-ioo 13327 df-ioc 13328 df-ico 13329 df-icc 13330 df-fz 13484 df-fzo 13627 df-fl 13756 df-mod 13834 df-seq 13966 df-exp 14027 df-fac 14233 df-bc 14262 df-hash 14290 df-shft 15013 df-cj 15045 df-re 15046 df-im 15047 df-sqrt 15181 df-abs 15182 df-limsup 15414 df-clim 15431 df-rlim 15432 df-sum 15632 df-ef 16010 df-sin 16012 df-cos 16013 df-pi 16015 df-struct 17079 df-sets 17096 df-slot 17114 df-ndx 17126 df-base 17144 df-ress 17173 df-plusg 17209 df-mulr 17210 df-starv 17211 df-sca 17212 df-vsca 17213 df-ip 17214 df-tset 17215 df-ple 17216 df-ds 17218 df-unif 17219 df-hom 17220 df-cco 17221 df-rest 17367 df-topn 17368 df-0g 17386 df-gsum 17387 df-topgen 17388 df-pt 17389 df-prds 17392 df-xrs 17447 df-qtop 17452 df-imas 17453 df-xps 17455 df-mre 17529 df-mrc 17530 df-acs 17532 df-mgm 18560 df-sgrp 18609 df-mnd 18625 df-submnd 18671 df-mulg 18950 df-cntz 19180 df-cmn 19649 df-psmet 20935 df-xmet 20936 df-met 20937 df-bl 20938 df-mopn 20939 df-fbas 20940 df-fg 20941 df-cnfld 20944 df-top 22395 df-topon 22412 df-topsp 22434 df-bases 22448 df-cld 22522 df-ntr 22523 df-cls 22524 df-nei 22601 df-lp 22639 df-perf 22640 df-cn 22730 df-cnp 22731 df-haus 22818 df-cmp 22890 df-tx 23065 df-hmeo 23258 df-fil 23349 df-fm 23441 df-flim 23442 df-flf 23443 df-xms 23825 df-ms 23826 df-tms 23827 df-cncf 24393 df-limc 25382 df-dv 25383 df-log 26064

This theorem is referenced by: logfacrlim 26724

W3C validator