harmonicbnd4

Description: The asymptotic behavior of sum_ m <_ A , 1 / m = log A + gamma + O ( 1 / A ) . (Contributed by Mario Carneiro, 14-May-2016)

		Ref	Expression
	Assertion	harmonicbnd4	⊢ ( 𝐴 ∈ ℝ⁺ → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ≤ ( 1 / 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fzfid	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
2		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑚 ∈ ℕ )
3	2	adantl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℕ )
4	3	nnrecred	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑚 ) ∈ ℝ )
5	1 4	fsumrecl	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ∈ ℝ )
6	5	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ∈ ℂ )
7		relogcl	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ 𝐴 ) ∈ ℝ )
8	7	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ 𝐴 ) ∈ ℂ )
9		emre	⊢ γ ∈ ℝ
10	9	a1i	⊢ ( 𝐴 ∈ ℝ⁺ → γ ∈ ℝ )
11	10	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → γ ∈ ℂ )
12	6 8 11	subsub4d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) − γ ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) )
13	12	fveq2d	⊢ ( 𝐴 ∈ ℝ⁺ → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) − γ ) ) = ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) )
14		rpreccl	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / 𝐴 ) ∈ ℝ⁺ )
15	14	rpred	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / 𝐴 ) ∈ ℝ )
16		resubcl	⊢ ( ( γ ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ) → ( γ − ( 1 / 𝐴 ) ) ∈ ℝ )
17	9 15 16	sylancr	⊢ ( 𝐴 ∈ ℝ⁺ → ( γ − ( 1 / 𝐴 ) ) ∈ ℝ )
18		rprege0	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
19		flge0nn0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ₀ )
20	18 19	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) ∈ ℕ₀ )
21		nn0p1nn	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ₀ → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℕ )
22	20 21	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℕ )
23	22	nnrpd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ⁺ )
24		relogcl	⊢ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ⁺ → ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ∈ ℝ )
25	23 24	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ∈ ℝ )
26	5 25	resubcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ℝ )
27	5 7	resubcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) ∈ ℝ )
28	22	nnrecred	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ∈ ℝ )
29		fzfid	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ∈ Fin )
30		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) → 𝑚 ∈ ℕ )
31	30	adantl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) → 𝑚 ∈ ℕ )
32	31	nnrecred	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) → ( 1 / 𝑚 ) ∈ ℝ )
33	29 32	fsumrecl	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) ∈ ℝ )
34	33 25	resubcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ℝ )
35		harmonicbnd	⊢ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( γ [,] 1 ) )
36	22 35	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( γ [,] 1 ) )
37		1re	⊢ 1 ∈ ℝ
38	9 37	elicc2i	⊢ ( ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( γ [,] 1 ) ↔ ( ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ℝ ∧ γ ≤ ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∧ ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ≤ 1 ) )
39	38	simp2bi	⊢ ( ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( γ [,] 1 ) → γ ≤ ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
40	36 39	syl	⊢ ( 𝐴 ∈ ℝ⁺ → γ ≤ ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
41		rpre	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ )
42		fllep1	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) )
43	41 42	syl	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) )
44		rpregt0	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
45	22	nnred	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ )
46	22	nngt0d	⊢ ( 𝐴 ∈ ℝ⁺ → 0 < ( ( ⌊ ‘ 𝐴 ) + 1 ) )
47		lerec	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ ∧ 0 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) → ( 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) ↔ ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ≤ ( 1 / 𝐴 ) ) )
48	44 45 46 47	syl12anc	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) ↔ ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ≤ ( 1 / 𝐴 ) ) )
49	43 48	mpbid	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ≤ ( 1 / 𝐴 ) )
50	10 28 34 15 40 49	le2subd	⊢ ( 𝐴 ∈ ℝ⁺ → ( γ − ( 1 / 𝐴 ) ) ≤ ( ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) − ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
51	33	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) ∈ ℂ )
52	25	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ∈ ℂ )
53	28	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ∈ ℂ )
54	51 52 53	sub32d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) − ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
55		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
56	22 55	eleqtrdi	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
57	32	recnd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) → ( 1 / 𝑚 ) ∈ ℂ )
58		oveq2	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝐴 ) + 1 ) → ( 1 / 𝑚 ) = ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
59	56 57 58	fsumm1	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) = ( Σ 𝑚 ∈ ( 1 ... ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 1 ) ) ( 1 / 𝑚 ) + ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
60	20	nn0cnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) ∈ ℂ )
61		ax-1cn	⊢ 1 ∈ ℂ
62		pncan	⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝐴 ) )
63	60 61 62	sylancl	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝐴 ) )
64	63	oveq2d	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 ... ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 1 ) ) = ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
65	64	sumeq1d	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑚 ∈ ( 1 ... ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 1 ) ) ( 1 / 𝑚 ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) )
66	65	oveq1d	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 1 ) ) ( 1 / 𝑚 ) + ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) + ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
67	59 66	eqtrd	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) + ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
68	6 53 67	mvrraddd	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) )
69	68	oveq1d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
70	54 69	eqtrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( Σ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) − ( 1 / ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
71	50 70	breqtrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( γ − ( 1 / 𝐴 ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
72		logleb	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ⁺ ) → ( 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
73	23 72	mpdan	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
74	43 73	mpbid	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ 𝐴 ) ≤ ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
75	7 25 5 74	lesub2dd	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) )
76	17 26 27 71 75	letrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( γ − ( 1 / 𝐴 ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) )
77	27 15	resubcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) − ( 1 / 𝐴 ) ) ∈ ℝ )
78	15	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 / 𝐴 ) ∈ ℂ )
79	6 8 78	subsub4d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) − ( 1 / 𝐴 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + ( 1 / 𝐴 ) ) ) )
80	7 15	readdcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( log ‘ 𝐴 ) + ( 1 / 𝐴 ) ) ∈ ℝ )
81		id	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ⁺ )
82	23 81	relogdivd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ) = ( ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) − ( log ‘ 𝐴 ) ) )
83		rerpdivcl	⊢ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ ∧ 𝐴 ∈ ℝ⁺ ) → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ∈ ℝ )
84	45 83	mpancom	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ∈ ℝ )
85	37	a1i	⊢ ( 𝐴 ∈ ℝ⁺ → 1 ∈ ℝ )
86	85 15	readdcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 + ( 1 / 𝐴 ) ) ∈ ℝ )
87	15	reefcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( exp ‘ ( 1 / 𝐴 ) ) ∈ ℝ )
88	61	a1i	⊢ ( 𝐴 ∈ ℝ⁺ → 1 ∈ ℂ )
89		rpcnne0	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
90		divdir	⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) = ( ( ( ⌊ ‘ 𝐴 ) / 𝐴 ) + ( 1 / 𝐴 ) ) )
91	60 88 89 90	syl3anc	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) = ( ( ( ⌊ ‘ 𝐴 ) / 𝐴 ) + ( 1 / 𝐴 ) ) )
92		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
93	41 92	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
94		rerpdivcl	⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℝ ∧ 𝐴 ∈ ℝ⁺ ) → ( ( ⌊ ‘ 𝐴 ) / 𝐴 ) ∈ ℝ )
95	93 94	mpancom	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ⌊ ‘ 𝐴 ) / 𝐴 ) ∈ ℝ )
96		flle	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
97	41 96	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
98		rpcn	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℂ )
99	98	mulid1d	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · 1 ) = 𝐴 )
100	97 99	breqtrrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) ≤ ( 𝐴 · 1 ) )
101		ledivmul	⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( ( ⌊ ‘ 𝐴 ) / 𝐴 ) ≤ 1 ↔ ( ⌊ ‘ 𝐴 ) ≤ ( 𝐴 · 1 ) ) )
102	93 85 44 101	syl3anc	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( ⌊ ‘ 𝐴 ) / 𝐴 ) ≤ 1 ↔ ( ⌊ ‘ 𝐴 ) ≤ ( 𝐴 · 1 ) ) )
103	100 102	mpbird	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ⌊ ‘ 𝐴 ) / 𝐴 ) ≤ 1 )
104	95 85 15 103	leadd1dd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( ⌊ ‘ 𝐴 ) / 𝐴 ) + ( 1 / 𝐴 ) ) ≤ ( 1 + ( 1 / 𝐴 ) ) )
105	91 104	eqbrtrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ≤ ( 1 + ( 1 / 𝐴 ) ) )
106		efgt1p	⊢ ( ( 1 / 𝐴 ) ∈ ℝ⁺ → ( 1 + ( 1 / 𝐴 ) ) < ( exp ‘ ( 1 / 𝐴 ) ) )
107	14 106	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 + ( 1 / 𝐴 ) ) < ( exp ‘ ( 1 / 𝐴 ) ) )
108	86 87 107	ltled	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 + ( 1 / 𝐴 ) ) ≤ ( exp ‘ ( 1 / 𝐴 ) ) )
109	84 86 87 105 108	letrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ≤ ( exp ‘ ( 1 / 𝐴 ) ) )
110		rpdivcl	⊢ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ⁺ ∧ 𝐴 ∈ ℝ⁺ ) → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ∈ ℝ⁺ )
111	23 110	mpancom	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ∈ ℝ⁺ )
112	15	rpefcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( exp ‘ ( 1 / 𝐴 ) ) ∈ ℝ⁺ )
113	111 112	logled	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ≤ ( exp ‘ ( 1 / 𝐴 ) ) ↔ ( log ‘ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ) ≤ ( log ‘ ( exp ‘ ( 1 / 𝐴 ) ) ) ) )
114	109 113	mpbid	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ) ≤ ( log ‘ ( exp ‘ ( 1 / 𝐴 ) ) ) )
115	15	relogefd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( exp ‘ ( 1 / 𝐴 ) ) ) = ( 1 / 𝐴 ) )
116	114 115	breqtrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) / 𝐴 ) ) ≤ ( 1 / 𝐴 ) )
117	82 116	eqbrtrrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) − ( log ‘ 𝐴 ) ) ≤ ( 1 / 𝐴 ) )
118	25 7 15	lesubadd2d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) − ( log ‘ 𝐴 ) ) ≤ ( 1 / 𝐴 ) ↔ ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ≤ ( ( log ‘ 𝐴 ) + ( 1 / 𝐴 ) ) ) )
119	117 118	mpbid	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ≤ ( ( log ‘ 𝐴 ) + ( 1 / 𝐴 ) ) )
120	25 80 5 119	lesub2dd	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + ( 1 / 𝐴 ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
121	79 120	eqbrtrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) − ( 1 / 𝐴 ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
122		harmonicbnd3	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ₀ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( 0 [,] γ ) )
123	20 122	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( 0 [,] γ ) )
124		0re	⊢ 0 ∈ ℝ
125	124 9	elicc2i	⊢ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( 0 [,] γ ) ↔ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ℝ ∧ 0 ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∧ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ≤ γ ) )
126	125	simp3bi	⊢ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( 0 [,] γ ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ≤ γ )
127	123 126	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ≤ γ )
128	77 26 10 121 127	letrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) − ( 1 / 𝐴 ) ) ≤ γ )
129	27 15 10	lesubaddd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) − ( 1 / 𝐴 ) ) ≤ γ ↔ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) ≤ ( γ + ( 1 / 𝐴 ) ) ) )
130	128 129	mpbid	⊢ ( 𝐴 ∈ ℝ⁺ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) ≤ ( γ + ( 1 / 𝐴 ) ) )
131	27 10 15	absdifled	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) − γ ) ) ≤ ( 1 / 𝐴 ) ↔ ( ( γ − ( 1 / 𝐴 ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) ∧ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) ≤ ( γ + ( 1 / 𝐴 ) ) ) ) )
132	76 130 131	mpbir2and	⊢ ( 𝐴 ∈ ℝ⁺ → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ 𝐴 ) ) − γ ) ) ≤ ( 1 / 𝐴 ) )
133	13 132	eqbrtrrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ≤ ( 1 / 𝐴 ) )

Metamath Proof Explorer

Theorem harmonicbnd4

Proof