Metamath Proof Explorer

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 ‘ 𝐴 ) ) )