logdiflbnd

Description: Lower bound on the difference of logs. (Contributed by Mario Carneiro, 3-Jul-2017)

		Ref	Expression
	Assertion	logdiflbnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / ( 𝐴 + 1 ) ) ≤ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ )
2		rpge0	⊢ ( 𝐴 ∈ ℝ⁺ → 0 ≤ 𝐴 )
3	1 2	ge0p1rpd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 + 1 ) ∈ ℝ⁺ )
4	3	rprecred	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / ( 𝐴 + 1 ) ) ∈ ℝ )
5		1red	⊢ ( 𝐴 ∈ ℝ⁺ → 1 ∈ ℝ )
6		0le1	⊢ 0 ≤ 1
7	6	a1i	⊢ ( 𝐴 ∈ ℝ⁺ → 0 ≤ 1 )
8	5 3 7	divge0d	⊢ ( 𝐴 ∈ ℝ⁺ → 0 ≤ ( 1 / ( 𝐴 + 1 ) ) )
9		id	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ⁺ )
10	5 9	ltaddrp2d	⊢ ( 𝐴 ∈ ℝ⁺ → 1 < ( 𝐴 + 1 ) )
11	1 5	readdcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 + 1 ) ∈ ℝ )
12	11	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 + 1 ) ∈ ℂ )
13	12	mulridd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 + 1 ) · 1 ) = ( 𝐴 + 1 ) )
14	10 13	breqtrrd	⊢ ( 𝐴 ∈ ℝ⁺ → 1 < ( ( 𝐴 + 1 ) · 1 ) )
15	5 5 3	ltdivmuld	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 1 / ( 𝐴 + 1 ) ) < 1 ↔ 1 < ( ( 𝐴 + 1 ) · 1 ) ) )
16	14 15	mpbird	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / ( 𝐴 + 1 ) ) < 1 )
17	4 8 16	eflegeo	⊢ ( 𝐴 ∈ ℝ⁺ → ( exp ‘ ( 1 / ( 𝐴 + 1 ) ) ) ≤ ( 1 / ( 1 − ( 1 / ( 𝐴 + 1 ) ) ) ) )
18	5	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → 1 ∈ ℂ )
19	3	rpne0d	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 + 1 ) ≠ 0 )
20	12 18 12 19	divsubdird	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( 𝐴 + 1 ) − 1 ) / ( 𝐴 + 1 ) ) = ( ( ( 𝐴 + 1 ) / ( 𝐴 + 1 ) ) − ( 1 / ( 𝐴 + 1 ) ) ) )
21	1	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℂ )
22	21 18	pncand	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
23	22	oveq1d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( 𝐴 + 1 ) − 1 ) / ( 𝐴 + 1 ) ) = ( 𝐴 / ( 𝐴 + 1 ) ) )
24	12 19	dividd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 + 1 ) / ( 𝐴 + 1 ) ) = 1 )
25	24	oveq1d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( 𝐴 + 1 ) / ( 𝐴 + 1 ) ) − ( 1 / ( 𝐴 + 1 ) ) ) = ( 1 − ( 1 / ( 𝐴 + 1 ) ) ) )
26	20 23 25	3eqtr3rd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 − ( 1 / ( 𝐴 + 1 ) ) ) = ( 𝐴 / ( 𝐴 + 1 ) ) )
27	26	oveq2d	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / ( 1 − ( 1 / ( 𝐴 + 1 ) ) ) ) = ( 1 / ( 𝐴 / ( 𝐴 + 1 ) ) ) )
28		rpne0	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ≠ 0 )
29	21 12 28 19	recdivd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / ( 𝐴 / ( 𝐴 + 1 ) ) ) = ( ( 𝐴 + 1 ) / 𝐴 ) )
30	27 29	eqtrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / ( 1 − ( 1 / ( 𝐴 + 1 ) ) ) ) = ( ( 𝐴 + 1 ) / 𝐴 ) )
31	17 30	breqtrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( exp ‘ ( 1 / ( 𝐴 + 1 ) ) ) ≤ ( ( 𝐴 + 1 ) / 𝐴 ) )
32	4	rpefcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( exp ‘ ( 1 / ( 𝐴 + 1 ) ) ) ∈ ℝ⁺ )
33	3 9	rpdivcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 + 1 ) / 𝐴 ) ∈ ℝ⁺ )
34	32 33	logled	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( exp ‘ ( 1 / ( 𝐴 + 1 ) ) ) ≤ ( ( 𝐴 + 1 ) / 𝐴 ) ↔ ( log ‘ ( exp ‘ ( 1 / ( 𝐴 + 1 ) ) ) ) ≤ ( log ‘ ( ( 𝐴 + 1 ) / 𝐴 ) ) ) )
35	31 34	mpbid	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( exp ‘ ( 1 / ( 𝐴 + 1 ) ) ) ) ≤ ( log ‘ ( ( 𝐴 + 1 ) / 𝐴 ) ) )
36	4	relogefd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( exp ‘ ( 1 / ( 𝐴 + 1 ) ) ) ) = ( 1 / ( 𝐴 + 1 ) ) )
37	3 9	relogdivd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( ( 𝐴 + 1 ) / 𝐴 ) ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ 𝐴 ) ) )
38	35 36 37	3brtr3d	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / ( 𝐴 + 1 ) ) ≤ ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ 𝐴 ) ) )

Metamath Proof Explorer

Theorem logdiflbnd

Proof