This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem logfac

Description: The logarithm of a factorial can be expressed as a finite sum of logs. (Contributed by Mario Carneiro, 17-Apr-2015)

Ref Expression
Assertion logfac ( 𝑁 ∈ ℕ0 → ( log ‘ ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 rpmulcl ⊢ ( ( 𝑘 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑘 · 𝑛 ) ∈ ℝ+ )
3 2 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑘 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ) → ( 𝑘 · 𝑛 ) ∈ ℝ+ )
4 fvi ⊢ ( 𝑘 ∈ V → ( I ‘ 𝑘 ) = 𝑘 )
5 4 elv ⊢ ( I ‘ 𝑘 ) = 𝑘
6 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
7 6 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
8 7 nnrpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℝ+ )
9 5 8 eqeltrid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( I ‘ 𝑘 ) ∈ ℝ+ )
10 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
11 10 biimpi ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
12 relogmul ⊢ ( ( 𝑘 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( log ‘ ( 𝑘 · 𝑛 ) ) = ( ( log ‘ 𝑘 ) + ( log ‘ 𝑛 ) ) )
13 12 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑘 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ) → ( log ‘ ( 𝑘 · 𝑛 ) ) = ( ( log ‘ 𝑘 ) + ( log ‘ 𝑛 ) ) )
14 5 fveq2i ⊢ ( log ‘ ( I ‘ 𝑘 ) ) = ( log ‘ 𝑘 )
15 14 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ ( I ‘ 𝑘 ) ) = ( log ‘ 𝑘 ) )
16 3 9 11 13 15 seqhomo ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( seq 1 ( · , I ) ‘ 𝑁 ) ) = ( seq 1 ( + , log ) ‘ 𝑁 ) )
17 facnn ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
18 17 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ! ‘ 𝑁 ) ) = ( log ‘ ( seq 1 ( · , I ) ‘ 𝑁 ) ) )
19 eqidd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ 𝑘 ) = ( log ‘ 𝑘 ) )
20 relogcl ⊢ ( 𝑘 ∈ ℝ+ → ( log ‘ 𝑘 ) ∈ ℝ )
21 8 20 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ 𝑘 ) ∈ ℝ )
22 21 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ 𝑘 ) ∈ ℂ )
23 19 11 22 fsumser ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) = ( seq 1 ( + , log ) ‘ 𝑁 ) )
24 16 18 23 3eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) )
25 log1 ⊢ ( log ‘ 1 ) = 0
26 sum0 ⊢ Σ 𝑘 ∈ ∅ ( log ‘ 𝑘 ) = 0
27 25 26 eqtr4i ⊢ ( log ‘ 1 ) = Σ 𝑘 ∈ ∅ ( log ‘ 𝑘 )
28 fveq2 ⊢ ( 𝑁 = 0 → ( ! ‘ 𝑁 ) = ( ! ‘ 0 ) )
29 fac0 ⊢ ( ! ‘ 0 ) = 1
30 28 29 eqtrdi ⊢ ( 𝑁 = 0 → ( ! ‘ 𝑁 ) = 1 )
31 30 fveq2d ⊢ ( 𝑁 = 0 → ( log ‘ ( ! ‘ 𝑁 ) ) = ( log ‘ 1 ) )
32 oveq2 ⊢ ( 𝑁 = 0 → ( 1 ... 𝑁 ) = ( 1 ... 0 ) )
33 fz10 ⊢ ( 1 ... 0 ) = ∅
34 32 33 eqtrdi ⊢ ( 𝑁 = 0 → ( 1 ... 𝑁 ) = ∅ )
35 34 sumeq1d ⊢ ( 𝑁 = 0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) = Σ 𝑘 ∈ ∅ ( log ‘ 𝑘 ) )
36 27 31 35 3eqtr4a ⊢ ( 𝑁 = 0 → ( log ‘ ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) )
37 24 36 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( log ‘ ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) )
38 1 37 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( log ‘ ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) )