logdifbnd

Description: Bound on the difference of logs. (Contributed by Mario Carneiro, 23-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℂ )
2		1cnd	⊢ ( 𝐴 ∈ ℝ⁺ → 1 ∈ ℂ )
3		rpne0	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ≠ 0 )
4	1 2 1 3	divdird	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 + 1 ) / 𝐴 ) = ( ( 𝐴 / 𝐴 ) + ( 1 / 𝐴 ) ) )
5	1 3	dividd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 / 𝐴 ) = 1 )
6	5	oveq1d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 / 𝐴 ) + ( 1 / 𝐴 ) ) = ( 1 + ( 1 / 𝐴 ) ) )
7	4 6	eqtr2d	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 + ( 1 / 𝐴 ) ) = ( ( 𝐴 + 1 ) / 𝐴 ) )
8	7	fveq2d	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) = ( log ‘ ( ( 𝐴 + 1 ) / 𝐴 ) ) )
9		1rp	⊢ 1 ∈ ℝ⁺
10		rpaddcl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 1 ∈ ℝ⁺ ) → ( 𝐴 + 1 ) ∈ ℝ⁺ )
11	9 10	mpan2	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 + 1 ) ∈ ℝ⁺ )
12		relogdiv	⊢ ( ( ( 𝐴 + 1 ) ∈ ℝ⁺ ∧ 𝐴 ∈ ℝ⁺ ) → ( log ‘ ( ( 𝐴 + 1 ) / 𝐴 ) ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ 𝐴 ) ) )
13	11 12	mpancom	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( ( 𝐴 + 1 ) / 𝐴 ) ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ 𝐴 ) ) )
14	8 13	eqtrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) = ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ 𝐴 ) ) )
15		rpreccl	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / 𝐴 ) ∈ ℝ⁺ )
16		rpaddcl	⊢ ( ( 1 ∈ ℝ⁺ ∧ ( 1 / 𝐴 ) ∈ ℝ⁺ ) → ( 1 + ( 1 / 𝐴 ) ) ∈ ℝ⁺ )
17	9 15 16	sylancr	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 + ( 1 / 𝐴 ) ) ∈ ℝ⁺ )
18	17	reeflogd	⊢ ( 𝐴 ∈ ℝ⁺ → ( exp ‘ ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) ) = ( 1 + ( 1 / 𝐴 ) ) )
19	17	rpred	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 + ( 1 / 𝐴 ) ) ∈ ℝ )
20	15	rpred	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / 𝐴 ) ∈ ℝ )
21	20	reefcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( exp ‘ ( 1 / 𝐴 ) ) ∈ ℝ )
22		efgt1p	⊢ ( ( 1 / 𝐴 ) ∈ ℝ⁺ → ( 1 + ( 1 / 𝐴 ) ) < ( exp ‘ ( 1 / 𝐴 ) ) )
23	15 22	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 + ( 1 / 𝐴 ) ) < ( exp ‘ ( 1 / 𝐴 ) ) )
24	19 21 23	ltled	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 + ( 1 / 𝐴 ) ) ≤ ( exp ‘ ( 1 / 𝐴 ) ) )
25	18 24	eqbrtrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( exp ‘ ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) ) ≤ ( exp ‘ ( 1 / 𝐴 ) ) )
26		relogcl	⊢ ( ( 𝐴 + 1 ) ∈ ℝ⁺ → ( log ‘ ( 𝐴 + 1 ) ) ∈ ℝ )
27	11 26	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( 𝐴 + 1 ) ) ∈ ℝ )
28		relogcl	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ 𝐴 ) ∈ ℝ )
29	27 28	resubcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ 𝐴 ) ) ∈ ℝ )
30	14 29	eqeltrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) ∈ ℝ )
31		efle	⊢ ( ( ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ) → ( ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) ≤ ( 1 / 𝐴 ) ↔ ( exp ‘ ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) ) ≤ ( exp ‘ ( 1 / 𝐴 ) ) ) )
32	30 20 31	syl2anc	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) ≤ ( 1 / 𝐴 ) ↔ ( exp ‘ ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) ) ≤ ( exp ‘ ( 1 / 𝐴 ) ) ) )
33	25 32	mpbird	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( 1 + ( 1 / 𝐴 ) ) ) ≤ ( 1 / 𝐴 ) )
34	14 33	eqbrtrrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( log ‘ ( 𝐴 + 1 ) ) − ( log ‘ 𝐴 ) ) ≤ ( 1 / 𝐴 ) )

Metamath Proof Explorer

Theorem logdifbnd

Proof