Theorem logfacubnd

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

	Ref	Expression
Assertion	logfacubnd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ ( 𝐴 · ( log ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
2		flge1nn	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ )
3	1 2	sylan	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ )
4	3	nnnn0d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 )
5	4	faccld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℕ )
6	5	nnrpd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℝ+ )
7	6	relogcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ℝ )
8	1	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
9		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
10	8 9	syl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
11	3	nnrpd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ+ )
12	11	relogcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
13	10 12	remulcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) · ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ℝ )
14		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
15	14	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ )
16	8 15	remulcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( 𝐴 · ( log ‘ 𝐴 ) ) ∈ ℝ )
17		facubnd	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ0 → ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( ( ⌊ ‘ 𝐴 ) ↑ ( ⌊ ‘ 𝐴 ) ) )
18	4 17	syl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( ( ⌊ ‘ 𝐴 ) ↑ ( ⌊ ‘ 𝐴 ) ) )
19	3 4	nnexpcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) ↑ ( ⌊ ‘ 𝐴 ) ) ∈ ℕ )
20	19	nnrpd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) ↑ ( ⌊ ‘ 𝐴 ) ) ∈ ℝ+ )
21	6 20	logled	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( ( ⌊ ‘ 𝐴 ) ↑ ( ⌊ ‘ 𝐴 ) ) ↔ ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ ( log ‘ ( ( ⌊ ‘ 𝐴 ) ↑ ( ⌊ ‘ 𝐴 ) ) ) ) )
22	18 21	mpbid	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ ( log ‘ ( ( ⌊ ‘ 𝐴 ) ↑ ( ⌊ ‘ 𝐴 ) ) ) )
23	3	nnzd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
24		relogexp	⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℤ ) → ( log ‘ ( ( ⌊ ‘ 𝐴 ) ↑ ( ⌊ ‘ 𝐴 ) ) ) = ( ( ⌊ ‘ 𝐴 ) · ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) )
25	11 23 24	syl2anc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ( ⌊ ‘ 𝐴 ) ↑ ( ⌊ ‘ 𝐴 ) ) ) = ( ( ⌊ ‘ 𝐴 ) · ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) )
26	22 25	breqtrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ ( ( ⌊ ‘ 𝐴 ) · ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) )
27		flle	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
28	8 27	syl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
29		simpl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ+ )
30	11 29	logled	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ↔ ( log ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( log ‘ 𝐴 ) ) )
31	28 30	mpbid	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( log ‘ 𝐴 ) )
32	11	rprege0d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( ⌊ ‘ 𝐴 ) ) )
33		log1	⊢ ( log ‘ 1 ) = 0
34	3	nnge1d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → 1 ≤ ( ⌊ ‘ 𝐴 ) )
35		1rp	⊢ 1 ∈ ℝ+
36		logleb	⊢ ( ( 1 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ+ ) → ( 1 ≤ ( ⌊ ‘ 𝐴 ) ↔ ( log ‘ 1 ) ≤ ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) )
37	35 11 36	sylancr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( 1 ≤ ( ⌊ ‘ 𝐴 ) ↔ ( log ‘ 1 ) ≤ ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) )
38	34 37	mpbid	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( log ‘ 1 ) ≤ ( log ‘ ( ⌊ ‘ 𝐴 ) ) )
39	33 38	eqbrtrrid	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → 0 ≤ ( log ‘ ( ⌊ ‘ 𝐴 ) ) )
40	12 39	jca	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) )
41		lemul12a	⊢ ( ( ( ( ( ⌊ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( ⌊ ‘ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) ∧ ( ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∧ ( log ‘ 𝐴 ) ∈ ℝ ) ) → ( ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ ( log ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( log ‘ 𝐴 ) ) → ( ( ⌊ ‘ 𝐴 ) · ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ ( 𝐴 · ( log ‘ 𝐴 ) ) ) )
42	32 8 40 15 41	syl22anc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ ( log ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( log ‘ 𝐴 ) ) → ( ( ⌊ ‘ 𝐴 ) · ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ ( 𝐴 · ( log ‘ 𝐴 ) ) ) )
43	28 31 42	mp2and	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) · ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ ( 𝐴 · ( log ‘ 𝐴 ) ) )
44	7 13 16 26 43	letrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ ( 𝐴 · ( log ‘ 𝐴 ) ) )