logfac - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > logfac		GIF version

Theorem logfac 15978

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

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

Distinct variable group: 𝑘,𝑁

Proof of Theorem logfac Dummy variables 𝑛 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elnn0 9548	. 2 ⊢ (𝑁 ∈ ℕ₀ ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnn1uz2 9990	. . . . 5 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ_≥‘2)))
3		1zzd 9654	. . . . . . . . . . 11 ⊢ (𝑁 = 1 → 1 ∈ ℤ)
4		fvi 5757	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → ( I ‘𝑘) = 𝑘)
5		elnnuz 9942	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ_≥‘1))
6	5	biimpri 133	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → 𝑘 ∈ ℕ)
7	4, 6	eqeltrd 2315	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘1) → ( I ‘𝑘) ∈ ℕ)
8	7	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 = 1 ∧ 𝑘 ∈ (ℤ_≥‘1)) → ( I ‘𝑘) ∈ ℕ)
9		nnmulcl 9308	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑘 · 𝑛) ∈ ℕ)
10	9	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 = 1 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝑘 · 𝑛) ∈ ℕ)
11	3, 8, 10	seq3-1 10882	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (seq1( · , I )‘1) = ( I ‘1))
12		1nn 9298	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
13		fvi 5757	. . . . . . . . . . 11 ⊢ (1 ∈ ℕ → ( I ‘1) = 1)
14	12, 13	ax-mp 5	. . . . . . . . . 10 ⊢ ( I ‘1) = 1
15	11, 14	eqtrdi 2287	. . . . . . . . 9 ⊢ (𝑁 = 1 → (seq1( · , I )‘1) = 1)
16	15	fveq2d 5697	. . . . . . . 8 ⊢ (𝑁 = 1 → (log‘(seq1( · , I )‘1)) = (log‘1))
17		nnrp 10047	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ⁺)
18		relogcl 15946	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℝ⁺ → (log‘𝑘) ∈ ℝ)
19	6, 17, 18	3syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (log‘𝑘) ∈ ℝ)
20	19	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 = 1 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℝ)
21		readdcl 8299	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑘 + 𝑛) ∈ ℝ)
22	21	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 = 1 ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝑘 + 𝑛) ∈ ℝ)
23	3, 20, 22	seq3-1 10882	. . . . . . . 8 ⊢ (𝑁 = 1 → (seq1( + , log)‘1) = (log‘1))
24	16, 23	eqtr4d 2274	. . . . . . 7 ⊢ (𝑁 = 1 → (log‘(seq1( · , I )‘1)) = (seq1( + , log)‘1))
25		2fveq3 5698	. . . . . . 7 ⊢ (𝑁 = 1 → (log‘(seq1( · , I )‘𝑁)) = (log‘(seq1( · , I )‘1)))
26		fveq2 5693	. . . . . . 7 ⊢ (𝑁 = 1 → (seq1( + , log)‘𝑁) = (seq1( + , log)‘1))
27	24, 25, 26	3eqtr4d 2281	. . . . . 6 ⊢ (𝑁 = 1 → (log‘(seq1( · , I )‘𝑁)) = (seq1( + , log)‘𝑁))
28		rpmulcl 10062	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑘 · 𝑛) ∈ ℝ⁺)
29	28	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺)) → (𝑘 · 𝑛) ∈ ℝ⁺)
30		fvi 5757	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘2) → ( I ‘𝑘) = 𝑘)
31		eluz2nn 9949	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℕ)
32	31	nnrpd 10078	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℝ⁺)
33	30, 32	eqeltrd 2315	. . . . . . . . 9 ⊢ (𝑘 ∈ (ℤ_≥‘2) → ( I ‘𝑘) ∈ ℝ⁺)
34	33	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → ( I ‘𝑘) ∈ ℝ⁺)
35		id 19	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 𝑁 ∈ (ℤ_≥‘2))
36		relogmul 15953	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (log‘(𝑘 · 𝑛)) = ((log‘𝑘) + (log‘𝑛)))
37	36	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺)) → (log‘(𝑘 · 𝑛)) = ((log‘𝑘) + (log‘𝑛)))
38		fvi 5757	. . . . . . . . . . 11 ⊢ (𝑘 ∈ V → ( I ‘𝑘) = 𝑘)
39	38	elv 2825	. . . . . . . . . 10 ⊢ ( I ‘𝑘) = 𝑘
40	39	fveq2i 5696	. . . . . . . . 9 ⊢ (log‘( I ‘𝑘)) = (log‘𝑘)
41	40	a1i 9	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → (log‘( I ‘𝑘)) = (log‘𝑘))
42	31	nnred 9300	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℝ)
43	42	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑘 ∈ ℝ)
44		eluz2gt1 9985	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 1 < 𝑘)
45	44	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → 1 < 𝑘)
46	43, 45	rplogcld 15972	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → (log‘𝑘) ∈ ℝ⁺)
47		rpaddcl 10061	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑘 + 𝑛) ∈ ℝ⁺)
48	47	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺)) → (𝑘 + 𝑛) ∈ ℝ⁺)
49	29, 34, 35, 37, 41, 46, 48	seq3homo 10947	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (log‘(seq2( · , I )‘𝑁)) = (seq2( + , log)‘𝑁))
50		remulcl 8301	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑘 · 𝑛) ∈ ℝ)
51	50	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝑘 · 𝑛) ∈ ℝ)
52		simp1 1028	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑘 ∈ ℝ)
53	52	recnd 8348	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑘 ∈ ℂ)
54		simp2 1029	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑛 ∈ ℝ)
55	54	recnd 8348	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑛 ∈ ℂ)
56		simp3 1030	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ∈ ℝ)
57	56	recnd 8348	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ∈ ℂ)
58	53, 55, 57	mulassd 8343	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑘 · 𝑛) · 𝑚) = (𝑘 · (𝑛 · 𝑚)))
59	58	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((𝑘 · 𝑛) · 𝑚) = (𝑘 · (𝑛 · 𝑚)))
60		1p1e2 9404	. . . . . . . . . . . . . . 15 ⊢ (1 + 1) = 2
61	60	fveq2i 5696	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘(1 + 1)) = (ℤ_≥‘2)
62	61	eleq2i 2305	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘(1 + 1)) ↔ 𝑁 ∈ (ℤ_≥‘2))
63	62	biimpri 133	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 𝑁 ∈ (ℤ_≥‘(1 + 1)))
64		1zzd 9654	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 1 ∈ ℤ)
65	7	nnred 9300	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → ( I ‘𝑘) ∈ ℝ)
66	65	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ( I ‘𝑘) ∈ ℝ)
67	51, 59, 63, 64, 66	seq3-1p 10910	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( · , I )‘𝑁) = (( I ‘1) · (seq(1 + 1)( · , I )‘𝑁)))
68	14	oveq1i 6089	. . . . . . . . . . 11 ⊢ (( I ‘1) · (seq(1 + 1)( · , I )‘𝑁)) = (1 · (seq(1 + 1)( · , I )‘𝑁))
69	67, 68	eqtrdi 2287	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( · , I )‘𝑁) = (1 · (seq(1 + 1)( · , I )‘𝑁)))
70		seqeq1 10870	. . . . . . . . . . . . . 14 ⊢ ((1 + 1) = 2 → seq(1 + 1)( · , I ) = seq2( · , I ))
71	60, 70	ax-mp 5	. . . . . . . . . . . . 13 ⊢ seq(1 + 1)( · , I ) = seq2( · , I )
72	71	fveq1i 5694	. . . . . . . . . . . 12 ⊢ (seq(1 + 1)( · , I )‘𝑁) = (seq2( · , I )‘𝑁)
73		eqid 2238	. . . . . . . . . . . . . . 15 ⊢ (ℤ_≥‘2) = (ℤ_≥‘2)
74		eluzel2 9909	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 2 ∈ ℤ)
75		eluzelz 9914	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℤ)
76	30, 75	eqeltrd 2315	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘2) → ( I ‘𝑘) ∈ ℤ)
77	76	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → ( I ‘𝑘) ∈ ℤ)
78		zmulcl 9681	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑘 · 𝑛) ∈ ℤ)
79	78	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝑘 · 𝑛) ∈ ℤ)
80	73, 74, 77, 79	seqf 10884	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘2) → seq2( · , I ):(ℤ_≥‘2)⟶ℤ)
81	80, 35	ffvelcdmd 5838	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( · , I )‘𝑁) ∈ ℤ)
82	81	zcnd 9752	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( · , I )‘𝑁) ∈ ℂ)
83	72, 82	eqeltrid 2325	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq(1 + 1)( · , I )‘𝑁) ∈ ℂ)
84	83	mullidd 8338	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (1 · (seq(1 + 1)( · , I )‘𝑁)) = (seq(1 + 1)( · , I )‘𝑁))
85	69, 84	eqtrd 2271	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( · , I )‘𝑁) = (seq(1 + 1)( · , I )‘𝑁))
86	85, 72	eqtrdi 2287	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( · , I )‘𝑁) = (seq2( · , I )‘𝑁))
87	86	fveq2d 5697	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (log‘(seq1( · , I )‘𝑁)) = (log‘(seq2( · , I )‘𝑁)))
88	21	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝑘 + 𝑛) ∈ ℝ)
89	53, 55, 57	addassd 8342	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑘 + 𝑛) + 𝑚) = (𝑘 + (𝑛 + 𝑚)))
90	89	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((𝑘 + 𝑛) + 𝑚) = (𝑘 + (𝑛 + 𝑚)))
91	6	nnrpd 10078	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → 𝑘 ∈ ℝ⁺)
92	91	relogcld 15966	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (log‘𝑘) ∈ ℝ)
93	92	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℝ)
94	88, 90, 63, 64, 93	seq3-1p 10910	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( + , log)‘𝑁) = ((log‘1) + (seq(1 + 1)( + , log)‘𝑁)))
95		seqeq1 10870	. . . . . . . . . . . . 13 ⊢ ((1 + 1) = 2 → seq(1 + 1)( + , log) = seq2( + , log))
96	60, 95	ax-mp 5	. . . . . . . . . . . 12 ⊢ seq(1 + 1)( + , log) = seq2( + , log)
97	96	fveq1i 5694	. . . . . . . . . . 11 ⊢ (seq(1 + 1)( + , log)‘𝑁) = (seq2( + , log)‘𝑁)
98	97	oveq2i 6090	. . . . . . . . . 10 ⊢ ((log‘1) + (seq(1 + 1)( + , log)‘𝑁)) = ((log‘1) + (seq2( + , log)‘𝑁))
99	94, 98	eqtrdi 2287	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( + , log)‘𝑁) = ((log‘1) + (seq2( + , log)‘𝑁)))
100		log1 15950	. . . . . . . . . 10 ⊢ (log‘1) = 0
101	100	oveq1i 6089	. . . . . . . . 9 ⊢ ((log‘1) + (seq2( + , log)‘𝑁)) = (0 + (seq2( + , log)‘𝑁))
102	99, 101	eqtrdi 2287	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( + , log)‘𝑁) = (0 + (seq2( + , log)‘𝑁)))
103	73, 74, 46, 48	seqf 10884	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘2) → seq2( + , log):(ℤ_≥‘2)⟶ℝ⁺)
104	103, 35	ffvelcdmd 5838	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( + , log)‘𝑁) ∈ ℝ⁺)
105	104	rpcnd 10082	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( + , log)‘𝑁) ∈ ℂ)
106	105	addlidd 8470	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (0 + (seq2( + , log)‘𝑁)) = (seq2( + , log)‘𝑁))
107	102, 106	eqtrd 2271	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( + , log)‘𝑁) = (seq2( + , log)‘𝑁))
108	49, 87, 107	3eqtr4d 2281	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (log‘(seq1( · , I )‘𝑁)) = (seq1( + , log)‘𝑁))
109	27, 108	jaoi 728	. . . . 5 ⊢ ((𝑁 = 1 ∨ 𝑁 ∈ (ℤ_≥‘2)) → (log‘(seq1( · , I )‘𝑁)) = (seq1( + , log)‘𝑁))
110	2, 109	sylbi 121	. . . 4 ⊢ (𝑁 ∈ ℕ → (log‘(seq1( · , I )‘𝑁)) = (seq1( + , log)‘𝑁))
111		facnn 11148	. . . . 5 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) = (seq1( · , I )‘𝑁))
112	111	fveq2d 5697	. . . 4 ⊢ (𝑁 ∈ ℕ → (log‘(!‘𝑁)) = (log‘(seq1( · , I )‘𝑁)))
113		eqidd 2239	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) = (log‘𝑘))
114		elnnuz 9942	. . . . . 6 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
115	114	biimpi 120	. . . . 5 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘1))
116	19	adantl 277	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℝ)
117	116	recnd 8348	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℂ)
118	113, 115, 117	fsum3ser 12147	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...𝑁)(log‘𝑘) = (seq1( + , log)‘𝑁))
119	110, 112, 118	3eqtr4d 2281	. . 3 ⊢ (𝑁 ∈ ℕ → (log‘(!‘𝑁)) = Σ𝑘 ∈ (1...𝑁)(log‘𝑘))
120		sum0 12138	. . . . 5 ⊢ Σ𝑘 ∈ ∅ (log‘𝑘) = 0
121	100, 120	eqtr4i 2262	. . . 4 ⊢ (log‘1) = Σ𝑘 ∈ ∅ (log‘𝑘)
122		fveq2 5693	. . . . . 6 ⊢ (𝑁 = 0 → (!‘𝑁) = (!‘0))
123		fac0 11149	. . . . . 6 ⊢ (!‘0) = 1
124	122, 123	eqtrdi 2287	. . . . 5 ⊢ (𝑁 = 0 → (!‘𝑁) = 1)
125	124	fveq2d 5697	. . . 4 ⊢ (𝑁 = 0 → (log‘(!‘𝑁)) = (log‘1))
126		oveq2 6087	. . . . . 6 ⊢ (𝑁 = 0 → (1...𝑁) = (1...0))
127		fz10 10433	. . . . . 6 ⊢ (1...0) = ∅
128	126, 127	eqtrdi 2287	. . . . 5 ⊢ (𝑁 = 0 → (1...𝑁) = ∅)
129	128	sumeq1d 12115	. . . 4 ⊢ (𝑁 = 0 → Σ𝑘 ∈ (1...𝑁)(log‘𝑘) = Σ𝑘 ∈ ∅ (log‘𝑘))
130	121, 125, 129	3eqtr4a 2297	. . 3 ⊢ (𝑁 = 0 → (log‘(!‘𝑁)) = Σ𝑘 ∈ (1...𝑁)(log‘𝑘))
131	119, 130	jaoi 728	. 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (log‘(!‘𝑁)) = Σ𝑘 ∈ (1...𝑁)(log‘𝑘))
132	1, 131	sylbi 121	1 ⊢ (𝑁 ∈ ℕ₀ → (log‘(!‘𝑁)) = Σ𝑘 ∈ (1...𝑁)(log‘𝑘))

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ∧ wa 104 ∨ wo 720 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 Vcvv 2821 ∅c0 3520 class class class wbr 4128 I cid 4431 ‘cfv 5375 (class class class)co 6079 ℂcc 8171 ℝcr 8172 0cc0 8173 1c1 8174 + caddc 8176 · cmul 8178 < clt 8354 ℕcn 9287 2c2 9338 ℕ₀cn0 9546 ℤcz 9627 ℤ_≥cuz 9904 ℝ⁺crp 10037 ...cfz 10394 seqcseq 10867 !cfa 11146 Σcsu 12102 logclog 15940

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4244 ax-sep 4247 ax-nul 4257 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-setind 4682 ax-iinf 4733 ax-cnex 8264 ax-resscn 8265 ax-1cn 8266 ax-1re 8267 ax-icn 8268 ax-addcl 8269 ax-addrcl 8270 ax-mulcl 8271 ax-mulrcl 8272 ax-addcom 8273 ax-mulcom 8274 ax-addass 8275 ax-mulass 8276 ax-distr 8277 ax-i2m1 8278 ax-0lt1 8279 ax-1rid 8280 ax-0id 8281 ax-rnegex 8282 ax-precex 8283 ax-cnre 8284 ax-pre-ltirr 8285 ax-pre-ltwlin 8286 ax-pre-lttrn 8287 ax-pre-apti 8288 ax-pre-ltadd 8289 ax-pre-mulgt0 8290 ax-pre-mulext 8291 ax-arch 8292 ax-caucvg 8293 ax-pre-suploc 8294 ax-addf 8295 ax-mulf 8296

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3714 df-pr 3715 df-op 3717 df-uni 3934 df-int 3969 df-iun 4012 df-disj 4105 df-br 4129 df-opab 4191 df-mpt 4192 df-tr 4228 df-id 4436 df-po 4439 df-iso 4440 df-iord 4509 df-on 4511 df-ilim 4512 df-suc 4514 df-iom 4736 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-ima 4785 df-iota 5335 df-fun 5377 df-fn 5378 df-f 5379 df-f1 5380 df-fo 5381 df-f1o 5382 df-fv 5383 df-isom 5384 df-riota 6032 df-ov 6082 df-oprab 6083 df-mpo 6084 df-of 6296 df-1st 6368 df-2nd 6369 df-recs 6570 df-irdg 6635 df-frec 6656 df-1o 6681 df-oadd 6685 df-er 6801 df-map 6918 df-pm 6919 df-en 7017 df-dom 7018 df-fin 7019 df-sup 7318 df-inf 7319 df-pnf 8356 df-mnf 8357 df-xr 8358 df-ltxr 8359 df-le 8360 df-sub 8493 df-neg 8494 df-reap 8897 df-ap 8904 df-div 8997 df-inn 9288 df-2 9346 df-3 9347 df-4 9348 df-n0 9547 df-z 9628 df-uz 9905 df-q 10003 df-rp 10038 df-xneg 10157 df-xadd 10158 df-ioo 10277 df-ico 10279 df-icc 10280 df-fz 10395 df-fzo 10533 df-seqfrec 10868 df-exp 10959 df-fac 11147 df-bc 11169 df-ihash 11198 df-shft 11563 df-cj 11590 df-re 11591 df-im 11592 df-rsqrt 11747 df-abs 11748 df-clim 12028 df-sumdc 12103 df-ef 12398 df-e 12399 df-rest 13578 df-topgen 13597 df-psmet 14863 df-xmet 14864 df-met 14865 df-bl 14866 df-mopn 14867 df-top 15082 df-topon 15095 df-bases 15127 df-ntr 15180 df-cn 15272 df-cnp 15273 df-tx 15337 df-cncf 15655 df-limced 15740 df-dvap 15741 df-relog 15942

This theorem is used by: birthdaylem2 16071

W3C validator