logfaclbnd

Description: A lower bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016)

		Ref	Expression
	Assertion	logfaclbnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · ( ( log ‘ 𝐴 ) − 2 ) ) ≤ ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℂ )
2	1	times2d	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · 2 ) = ( 𝐴 + 𝐴 ) )
3	2	oveq2d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 · ( log ‘ 𝐴 ) ) − ( 𝐴 · 2 ) ) = ( ( 𝐴 · ( log ‘ 𝐴 ) ) − ( 𝐴 + 𝐴 ) ) )
4		relogcl	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ 𝐴 ) ∈ ℝ )
5	4	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ 𝐴 ) ∈ ℂ )
6		2cnd	⊢ ( 𝐴 ∈ ℝ⁺ → 2 ∈ ℂ )
7	1 5 6	subdid	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · ( ( log ‘ 𝐴 ) − 2 ) ) = ( ( 𝐴 · ( log ‘ 𝐴 ) ) − ( 𝐴 · 2 ) ) )
8		rpre	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ )
9	8 4	remulcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · ( log ‘ 𝐴 ) ) ∈ ℝ )
10	9	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · ( log ‘ 𝐴 ) ) ∈ ℂ )
11	10 1 1	subsub4d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( 𝐴 · ( log ‘ 𝐴 ) ) − 𝐴 ) − 𝐴 ) = ( ( 𝐴 · ( log ‘ 𝐴 ) ) − ( 𝐴 + 𝐴 ) ) )
12	3 7 11	3eqtr4d	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · ( ( log ‘ 𝐴 ) − 2 ) ) = ( ( ( 𝐴 · ( log ‘ 𝐴 ) ) − 𝐴 ) − 𝐴 ) )
13	9 8	resubcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 · ( log ‘ 𝐴 ) ) − 𝐴 ) ∈ ℝ )
14		fzfid	⊢ ( 𝐴 ∈ ℝ⁺ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
15		fzfid	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... 𝑛 ) ∈ Fin )
16		elfznn	⊢ ( 𝑑 ∈ ( 1 ... 𝑛 ) → 𝑑 ∈ ℕ )
17	16	adantl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ ( 1 ... 𝑛 ) ) → 𝑑 ∈ ℕ )
18	17	nnrecred	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ ( 1 ... 𝑛 ) ) → ( 1 / 𝑑 ) ∈ ℝ )
19	15 18	fsumrecl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) ∈ ℝ )
20	14 19	fsumrecl	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) ∈ ℝ )
21		rprege0	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
22		flge0nn0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ₀ )
23	21 22	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) ∈ ℕ₀ )
24	23	faccld	⊢ ( 𝐴 ∈ ℝ⁺ → ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℕ )
25	24	nnrpd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℝ⁺ )
26	25	relogcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ℝ )
27	26 8	readdcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) + 𝐴 ) ∈ ℝ )
28		elfznn	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℕ )
29	28	adantl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℕ )
30	29	nnrecred	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑑 ) ∈ ℝ )
31	14 30	fsumrecl	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ∈ ℝ )
32	8 31	remulcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ) ∈ ℝ )
33		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
34	8 33	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
35	32 34	resubcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ) − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
36		harmoniclbnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ 𝐴 ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) )
37		rpregt0	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
38		lemul2	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( log ‘ 𝐴 ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ↔ ( 𝐴 · ( log ‘ 𝐴 ) ) ≤ ( 𝐴 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ) ) )
39	4 31 37 38	syl3anc	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( log ‘ 𝐴 ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ↔ ( 𝐴 · ( log ‘ 𝐴 ) ) ≤ ( 𝐴 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ) ) )
40	36 39	mpbid	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · ( log ‘ 𝐴 ) ) ≤ ( 𝐴 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ) )
41		flle	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
42	8 41	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
43	9 34 32 8 40 42	le2subd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 · ( log ‘ 𝐴 ) ) − 𝐴 ) ≤ ( ( 𝐴 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ) − ( ⌊ ‘ 𝐴 ) ) )
44	28	nnrecred	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → ( 1 / 𝑑 ) ∈ ℝ )
45		remulcl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 1 / 𝑑 ) ∈ ℝ ) → ( 𝐴 · ( 1 / 𝑑 ) ) ∈ ℝ )
46	8 44 45	syl2an	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 · ( 1 / 𝑑 ) ) ∈ ℝ )
47		peano2rem	⊢ ( ( 𝐴 · ( 1 / 𝑑 ) ) ∈ ℝ → ( ( 𝐴 · ( 1 / 𝑑 ) ) − 1 ) ∈ ℝ )
48	46 47	syl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝐴 · ( 1 / 𝑑 ) ) − 1 ) ∈ ℝ )
49		fzfid	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
50	30	adantr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑑 ) ∈ ℝ )
51	49 50	fsumrecl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ∈ ℝ )
52	8	adantr	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℝ )
53	52 33	syl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
54		peano2re	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ )
55	53 54	syl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ )
56	29	nnred	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℝ )
57		fllep1	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) )
58	8 57	syl	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) )
59	58	adantr	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) )
60	52 55 56 59	lesub1dd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 − 𝑑 ) ≤ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 𝑑 ) )
61	52 56	resubcld	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 − 𝑑 ) ∈ ℝ )
62	55 56	resubcld	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 𝑑 ) ∈ ℝ )
63	29	nnrpd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℝ⁺ )
64	63	rpreccld	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑑 ) ∈ ℝ⁺ )
65	61 62 64	lemul1d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝐴 − 𝑑 ) ≤ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 𝑑 ) ↔ ( ( 𝐴 − 𝑑 ) · ( 1 / 𝑑 ) ) ≤ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 𝑑 ) · ( 1 / 𝑑 ) ) ) )
66	60 65	mpbid	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝐴 − 𝑑 ) · ( 1 / 𝑑 ) ) ≤ ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 𝑑 ) · ( 1 / 𝑑 ) ) )
67	1	adantr	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℂ )
68	29	nncnd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℂ )
69	30	recnd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑑 ) ∈ ℂ )
70	67 68 69	subdird	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝐴 − 𝑑 ) · ( 1 / 𝑑 ) ) = ( ( 𝐴 · ( 1 / 𝑑 ) ) − ( 𝑑 · ( 1 / 𝑑 ) ) ) )
71	29	nnne0d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ≠ 0 )
72	68 71	recidd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑑 · ( 1 / 𝑑 ) ) = 1 )
73	72	oveq2d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝐴 · ( 1 / 𝑑 ) ) − ( 𝑑 · ( 1 / 𝑑 ) ) ) = ( ( 𝐴 · ( 1 / 𝑑 ) ) − 1 ) )
74	70 73	eqtr2d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝐴 · ( 1 / 𝑑 ) ) − 1 ) = ( ( 𝐴 − 𝑑 ) · ( 1 / 𝑑 ) ) )
75		fsumconst	⊢ ( ( ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ∧ ( 1 / 𝑑 ) ∈ ℂ ) → Σ 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) = ( ( ♯ ‘ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ) · ( 1 / 𝑑 ) ) )
76	49 69 75	syl2anc	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) = ( ( ♯ ‘ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ) · ( 1 / 𝑑 ) ) )
77		elfzuz3	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) )
78	77	adantl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) )
79		hashfz	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) → ( ♯ ‘ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ( ( ⌊ ‘ 𝐴 ) − 𝑑 ) + 1 ) )
80	78 79	syl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ( ( ⌊ ‘ 𝐴 ) − 𝑑 ) + 1 ) )
81	34	recnd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) ∈ ℂ )
82	81	adantr	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ⌊ ‘ 𝐴 ) ∈ ℂ )
83		1cnd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 1 ∈ ℂ )
84	82 83 68	addsubd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 𝑑 ) = ( ( ( ⌊ ‘ 𝐴 ) − 𝑑 ) + 1 ) )
85	80 84	eqtr4d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 𝑑 ) )
86	85	oveq1d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ♯ ‘ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ) · ( 1 / 𝑑 ) ) = ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 𝑑 ) · ( 1 / 𝑑 ) ) )
87	76 86	eqtrd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) = ( ( ( ( ⌊ ‘ 𝐴 ) + 1 ) − 𝑑 ) · ( 1 / 𝑑 ) ) )
88	66 74 87	3brtr4d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝐴 · ( 1 / 𝑑 ) ) − 1 ) ≤ Σ 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) )
89	14 48 51 88	fsumle	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝐴 · ( 1 / 𝑑 ) ) − 1 ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) )
90	14 1 69	fsummulc2	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 𝐴 · ( 1 / 𝑑 ) ) )
91		ax-1cn	⊢ 1 ∈ ℂ
92		fsumconst	⊢ ( ( ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 1 = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) · 1 ) )
93	14 91 92	sylancl	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 1 = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) · 1 ) )
94		hashfz1	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ₀ → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ⌊ ‘ 𝐴 ) )
95	23 94	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ⌊ ‘ 𝐴 ) )
96	95	oveq1d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) · 1 ) = ( ( ⌊ ‘ 𝐴 ) · 1 ) )
97	81	mulid1d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ⌊ ‘ 𝐴 ) · 1 ) = ( ⌊ ‘ 𝐴 ) )
98	93 96 97	3eqtrrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 1 )
99	90 98	oveq12d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ) − ( ⌊ ‘ 𝐴 ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 𝐴 · ( 1 / 𝑑 ) ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 1 ) )
100	46	recnd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 · ( 1 / 𝑑 ) ) ∈ ℂ )
101	14 100 83	fsumsub	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝐴 · ( 1 / 𝑑 ) ) − 1 ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 𝐴 · ( 1 / 𝑑 ) ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 1 ) )
102	99 101	eqtr4d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ) − ( ⌊ ‘ 𝐴 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝐴 · ( 1 / 𝑑 ) ) − 1 ) )
103		eqid	⊢ ( ℤ_≥ ‘ 1 ) = ( ℤ_≥ ‘ 1 )
104	103	uztrn2	⊢ ( ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) → 𝑛 ∈ ( ℤ_≥ ‘ 1 ) )
105	104	adantl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ) → 𝑛 ∈ ( ℤ_≥ ‘ 1 ) )
106	105	biantrurd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ) → ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ↔ ( 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) )
107		uzss	⊢ ( 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) → ( ℤ_≥ ‘ 𝑛 ) ⊆ ( ℤ_≥ ‘ 𝑑 ) )
108	107	ad2antll	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ) → ( ℤ_≥ ‘ 𝑛 ) ⊆ ( ℤ_≥ ‘ 𝑑 ) )
109	108	sseld	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ) → ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) ) )
110	109	pm4.71rd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ) → ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ↔ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) )
111	106 110	bitr3d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ) → ( ( 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ↔ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) )
112	111	pm5.32da	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ∧ ( 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ∧ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) ) )
113		ancom	⊢ ( ( ( 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ∧ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ∧ ( 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) )
114		an4	⊢ ( ( ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) ) ∧ ( 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ∧ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) )
115	112 113 114	3bitr4g	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ∧ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) ) ∧ ( 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) ) )
116		elfzuzb	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) )
117		elfzuzb	⊢ ( 𝑑 ∈ ( 1 ... 𝑛 ) ↔ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) )
118	116 117	anbi12i	⊢ ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ ( 1 ... 𝑛 ) ) ↔ ( ( 𝑛 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ∧ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ) ) )
119		elfzuzb	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) ) )
120		elfzuzb	⊢ ( 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) )
121	119 120	anbi12i	⊢ ( ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ) ↔ ( ( 𝑑 ∈ ( ℤ_≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑑 ) ) ∧ ( 𝑛 ∈ ( ℤ_≥ ‘ 𝑑 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) )
122	115 118 121	3bitr4g	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ ( 1 ... 𝑛 ) ) ↔ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ) ) )
123	18	recnd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ ( 1 ... 𝑛 ) ) → ( 1 / 𝑑 ) ∈ ℂ )
124	123	anasss	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ ( 1 ... 𝑛 ) ) ) → ( 1 / 𝑑 ) ∈ ℂ )
125	14 14 15 122 124	fsumcom2	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑛 ∈ ( 𝑑 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) )
126	89 102 125	3brtr4d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑑 ) ) − ( ⌊ ‘ 𝐴 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) )
127	13 35 20 43 126	letrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 · ( log ‘ 𝐴 ) ) − 𝐴 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) )
128	26 34	readdcld	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) + ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
129		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
130	129	adantl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
131	130	nnrpd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℝ⁺ )
132	131	relogcld	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
133		peano2re	⊢ ( ( log ‘ 𝑛 ) ∈ ℝ → ( ( log ‘ 𝑛 ) + 1 ) ∈ ℝ )
134	132 133	syl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( log ‘ 𝑛 ) + 1 ) ∈ ℝ )
135		nnz	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
136		flid	⊢ ( 𝑛 ∈ ℤ → ( ⌊ ‘ 𝑛 ) = 𝑛 )
137	135 136	syl	⊢ ( 𝑛 ∈ ℕ → ( ⌊ ‘ 𝑛 ) = 𝑛 )
138	137	oveq2d	⊢ ( 𝑛 ∈ ℕ → ( 1 ... ( ⌊ ‘ 𝑛 ) ) = ( 1 ... 𝑛 ) )
139	138	sumeq1d	⊢ ( 𝑛 ∈ ℕ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑛 ) ) ( 1 / 𝑑 ) = Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) )
140		nnre	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
141		nnge1	⊢ ( 𝑛 ∈ ℕ → 1 ≤ 𝑛 )
142		harmonicubnd	⊢ ( ( 𝑛 ∈ ℝ ∧ 1 ≤ 𝑛 ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑛 ) ) ( 1 / 𝑑 ) ≤ ( ( log ‘ 𝑛 ) + 1 ) )
143	140 141 142	syl2anc	⊢ ( 𝑛 ∈ ℕ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑛 ) ) ( 1 / 𝑑 ) ≤ ( ( log ‘ 𝑛 ) + 1 ) )
144	139 143	eqbrtrrd	⊢ ( 𝑛 ∈ ℕ → Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) ≤ ( ( log ‘ 𝑛 ) + 1 ) )
145	130 144	syl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) ≤ ( ( log ‘ 𝑛 ) + 1 ) )
146	14 19 134 145	fsumle	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑛 ) + 1 ) )
147	132	recnd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
148		1cnd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 1 ∈ ℂ )
149	14 147 148	fsumadd	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑛 ) + 1 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 1 ) )
150		logfac	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ₀ → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) )
151	23 150	syl	⊢ ( 𝐴 ∈ ℝ⁺ → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) )
152		fsumconst	⊢ ( ( ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 1 = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) · 1 ) )
153	14 91 152	sylancl	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 1 = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) · 1 ) )
154	153 96 97	3eqtrrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ⌊ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 1 )
155	151 154	oveq12d	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) + ( ⌊ ‘ 𝐴 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 1 ) )
156	149 155	eqtr4d	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑛 ) + 1 ) = ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) + ( ⌊ ‘ 𝐴 ) ) )
157	146 156	breqtrd	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) ≤ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) + ( ⌊ ‘ 𝐴 ) ) )
158	34 8 26 42	leadd2dd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) + ( ⌊ ‘ 𝐴 ) ) ≤ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) + 𝐴 ) )
159	20 128 27 157 158	letrd	⊢ ( 𝐴 ∈ ℝ⁺ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑑 ) ≤ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) + 𝐴 ) )
160	13 20 27 127 159	letrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( 𝐴 · ( log ‘ 𝐴 ) ) − 𝐴 ) ≤ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) + 𝐴 ) )
161	13 8 26	lesubaddd	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( ( 𝐴 · ( log ‘ 𝐴 ) ) − 𝐴 ) − 𝐴 ) ≤ ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) ↔ ( ( 𝐴 · ( log ‘ 𝐴 ) ) − 𝐴 ) ≤ ( ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) + 𝐴 ) ) )
162	160 161	mpbird	⊢ ( 𝐴 ∈ ℝ⁺ → ( ( ( 𝐴 · ( log ‘ 𝐴 ) ) − 𝐴 ) − 𝐴 ) ≤ ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) )
163	12 162	eqbrtrd	⊢ ( 𝐴 ∈ ℝ⁺ → ( 𝐴 · ( ( log ‘ 𝐴 ) − 2 ) ) ≤ ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) )

Metamath Proof Explorer

Theorem logfaclbnd

Proof