logfac - Intuitionistic Logic Explorer

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

Theorem logfac 15995

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 9565	. 2 ⊢ (𝑁 ∈ ℕ₀ ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnn1uz2 10007	. . . . 5 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ_≥‘2)))
3		1zzd 9671	. . . . . . . . . . 11 ⊢ (𝑁 = 1 → 1 ∈ ℤ)
4		fvi 5760	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → ( I ‘𝑘) = 𝑘)
5		elnnuz 9959	. . . . . . . . . . . . . 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 9325	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑘 · 𝑛) ∈ ℕ)
10	9	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 = 1 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝑘 · 𝑛) ∈ ℕ)
11	3, 8, 10	seq3-1 10899	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (seq1( · , I )‘1) = ( I ‘1))
12		1nn 9315	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ
13		fvi 5760	. . . . . . . . . . 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 5699	. . . . . . . 8 ⊢ (𝑁 = 1 → (log‘(seq1( · , I )‘1)) = (log‘1))
17		nnrp 10064	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ⁺)
18		relogcl 15963	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℝ⁺ → (log‘𝑘) ∈ ℝ)
19	6, 17, 18	3syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (log‘𝑘) ∈ ℝ)
20	19	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 = 1 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℝ)
21		readdcl 8305	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑘 + 𝑛) ∈ ℝ)
22	21	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 = 1 ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝑘 + 𝑛) ∈ ℝ)
23	3, 20, 22	seq3-1 10899	. . . . . . . 8 ⊢ (𝑁 = 1 → (seq1( + , log)‘1) = (log‘1))
24	16, 23	eqtr4d 2274	. . . . . . 7 ⊢ (𝑁 = 1 → (log‘(seq1( · , I )‘1)) = (seq1( + , log)‘1))
25		2fveq3 5700	. . . . . . 7 ⊢ (𝑁 = 1 → (log‘(seq1( · , I )‘𝑁)) = (log‘(seq1( · , I )‘1)))
26		fveq2 5695	. . . . . . 7 ⊢ (𝑁 = 1 → (seq1( + , log)‘𝑁) = (seq1( + , log)‘1))
27	24, 25, 26	3eqtr4d 2281	. . . . . 6 ⊢ (𝑁 = 1 → (log‘(seq1( · , I )‘𝑁)) = (seq1( + , log)‘𝑁))
28		rpmulcl 10079	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑘 · 𝑛) ∈ ℝ⁺)
29	28	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺)) → (𝑘 · 𝑛) ∈ ℝ⁺)
30		fvi 5760	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘2) → ( I ‘𝑘) = 𝑘)
31		eluz2nn 9966	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℕ)
32	31	nnrpd 10095	. . . . . . . . . 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 15970	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (log‘(𝑘 · 𝑛)) = ((log‘𝑘) + (log‘𝑛)))
37	36	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺)) → (log‘(𝑘 · 𝑛)) = ((log‘𝑘) + (log‘𝑛)))
38		fvi 5760	. . . . . . . . . . 11 ⊢ (𝑘 ∈ V → ( I ‘𝑘) = 𝑘)
39	38	elv 2825	. . . . . . . . . 10 ⊢ ( I ‘𝑘) = 𝑘
40	39	fveq2i 5698	. . . . . . . . 9 ⊢ (log‘( I ‘𝑘)) = (log‘𝑘)
41	40	a1i 9	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → (log‘( I ‘𝑘)) = (log‘𝑘))
42	31	nnred 9317	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℝ)
43	42	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑘 ∈ ℝ)
44		eluz2gt1 10002	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 1 < 𝑘)
45	44	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → 1 < 𝑘)
46	43, 45	rplogcld 15989	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → (log‘𝑘) ∈ ℝ⁺)
47		rpaddcl 10078	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑘 + 𝑛) ∈ ℝ⁺)
48	47	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺)) → (𝑘 + 𝑛) ∈ ℝ⁺)
49	29, 34, 35, 37, 41, 46, 48	seq3homo 10964	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (log‘(seq2( · , I )‘𝑁)) = (seq2( + , log)‘𝑁))
50		remulcl 8307	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑘 · 𝑛) ∈ ℝ)
51	50	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝑘 · 𝑛) ∈ ℝ)
52		simp1 1028	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑘 ∈ ℝ)
53	52	recnd 8354	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑘 ∈ ℂ)
54		simp2 1029	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑛 ∈ ℝ)
55	54	recnd 8354	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑛 ∈ ℂ)
56		simp3 1030	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ∈ ℝ)
57	56	recnd 8354	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ∈ ℂ)
58	53, 55, 57	mulassd 8349	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑘 · 𝑛) · 𝑚) = (𝑘 · (𝑛 · 𝑚)))
59	58	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((𝑘 · 𝑛) · 𝑚) = (𝑘 · (𝑛 · 𝑚)))
60		1p1e2 9421	. . . . . . . . . . . . . . 15 ⊢ (1 + 1) = 2
61	60	fveq2i 5698	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘(1 + 1)) = (ℤ_≥‘2)
62	61	eleq2i 2305	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘(1 + 1)) ↔ 𝑁 ∈ (ℤ_≥‘2))
63	62	biimpri 133	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 𝑁 ∈ (ℤ_≥‘(1 + 1)))
64		1zzd 9671	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 1 ∈ ℤ)
65	7	nnred 9317	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → ( I ‘𝑘) ∈ ℝ)
66	65	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ( I ‘𝑘) ∈ ℝ)
67	51, 59, 63, 64, 66	seq3-1p 10927	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( · , I )‘𝑁) = (( I ‘1) · (seq(1 + 1)( · , I )‘𝑁)))
68	14	oveq1i 6095	. . . . . . . . . . 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 10887	. . . . . . . . . . . . . 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 5696	. . . . . . . . . . . 12 ⊢ (seq(1 + 1)( · , I )‘𝑁) = (seq2( · , I )‘𝑁)
73		eqid 2238	. . . . . . . . . . . . . . 15 ⊢ (ℤ_≥‘2) = (ℤ_≥‘2)
74		eluzel2 9926	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 2 ∈ ℤ)
75		eluzelz 9931	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℤ)
76	30, 75	eqeltrd 2315	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘2) → ( I ‘𝑘) ∈ ℤ)
77	76	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → ( I ‘𝑘) ∈ ℤ)
78		zmulcl 9698	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑘 · 𝑛) ∈ ℤ)
79	78	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝑘 · 𝑛) ∈ ℤ)
80	73, 74, 77, 79	seqf 10901	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘2) → seq2( · , I ):(ℤ_≥‘2)⟶ℤ)
81	80, 35	ffvelcdmd 5844	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( · , I )‘𝑁) ∈ ℤ)
82	81	zcnd 9769	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( · , I )‘𝑁) ∈ ℂ)
83	72, 82	eqeltrid 2325	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq(1 + 1)( · , I )‘𝑁) ∈ ℂ)
84	83	mullidd 8344	. . . . . . . . . 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 5699	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (log‘(seq1( · , I )‘𝑁)) = (log‘(seq2( · , I )‘𝑁)))
88	21	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝑘 + 𝑛) ∈ ℝ)
89	53, 55, 57	addassd 8348	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑘 + 𝑛) + 𝑚) = (𝑘 + (𝑛 + 𝑚)))
90	89	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((𝑘 + 𝑛) + 𝑚) = (𝑘 + (𝑛 + 𝑚)))
91	6	nnrpd 10095	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → 𝑘 ∈ ℝ⁺)
92	91	relogcld 15983	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (log‘𝑘) ∈ ℝ)
93	92	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℝ)
94	88, 90, 63, 64, 93	seq3-1p 10927	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( + , log)‘𝑁) = ((log‘1) + (seq(1 + 1)( + , log)‘𝑁)))
95		seqeq1 10887	. . . . . . . . . . . . 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 5696	. . . . . . . . . . 11 ⊢ (seq(1 + 1)( + , log)‘𝑁) = (seq2( + , log)‘𝑁)
98	97	oveq2i 6096	. . . . . . . . . 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 15967	. . . . . . . . . 10 ⊢ (log‘1) = 0
101	100	oveq1i 6095	. . . . . . . . 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 10901	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘2) → seq2( + , log):(ℤ_≥‘2)⟶ℝ⁺)
104	103, 35	ffvelcdmd 5844	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( + , log)‘𝑁) ∈ ℝ⁺)
105	104	rpcnd 10099	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( + , log)‘𝑁) ∈ ℂ)
106	105	addlidd 8476	. . . . . . . 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 11165	. . . . 5 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) = (seq1( · , I )‘𝑁))
112	111	fveq2d 5699	. . . 4 ⊢ (𝑁 ∈ ℕ → (log‘(!‘𝑁)) = (log‘(seq1( · , I )‘𝑁)))
113		eqidd 2239	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) = (log‘𝑘))
114		elnnuz 9959	. . . . . 6 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
115	114	biimpi 120	. . . . 5 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘1))
116	19	adantl 277	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℝ)
117	116	recnd 8354	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℂ)
118	113, 115, 117	fsum3ser 12164	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...𝑁)(log‘𝑘) = (seq1( + , log)‘𝑁))
119	110, 112, 118	3eqtr4d 2281	. . 3 ⊢ (𝑁 ∈ ℕ → (log‘(!‘𝑁)) = Σ𝑘 ∈ (1...𝑁)(log‘𝑘))
120		sum0 12155	. . . . 5 ⊢ Σ𝑘 ∈ ∅ (log‘𝑘) = 0
121	100, 120	eqtr4i 2262	. . . 4 ⊢ (log‘1) = Σ𝑘 ∈ ∅ (log‘𝑘)
122		fveq2 5695	. . . . . 6 ⊢ (𝑁 = 0 → (!‘𝑁) = (!‘0))
123		fac0 11166	. . . . . 6 ⊢ (!‘0) = 1
124	122, 123	eqtrdi 2287	. . . . 5 ⊢ (𝑁 = 0 → (!‘𝑁) = 1)
125	124	fveq2d 5699	. . . 4 ⊢ (𝑁 = 0 → (log‘(!‘𝑁)) = (log‘1))
126		oveq2 6093	. . . . . 6 ⊢ (𝑁 = 0 → (1...𝑁) = (1...0))
127		fz10 10450	. . . . . 6 ⊢ (1...0) = ∅
128	126, 127	eqtrdi 2287	. . . . 5 ⊢ (𝑁 = 0 → (1...𝑁) = ∅)
129	128	sumeq1d 12132	. . . 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 4130 I cid 4433 ‘cfv 5377 (class class class)co 6085 ℂcc 8177 ℝcr 8178 0cc0 8179 1c1 8180 + caddc 8182 · cmul 8184 < clt 8360 ℕcn 9304 2c2 9355 ℕ₀cn0 9563 ℤcz 9644 ℤ_≥cuz 9921 ℝ⁺crp 10054 ...cfz 10411 seqcseq 10884 !cfa 11163 Σcsu 12119 logclog 15957

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 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299 ax-pre-suploc 8300 ax-addf 8301 ax-mulf 8302

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 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-disj 4107 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-of 6302 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-oadd 6691 df-er 6807 df-map 6924 df-pm 6925 df-en 7023 df-dom 7024 df-fin 7025 df-sup 7324 df-inf 7325 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8903 df-ap 8910 df-div 9003 df-inn 9305 df-2 9363 df-3 9364 df-4 9365 df-n0 9564 df-z 9645 df-uz 9922 df-q 10020 df-rp 10055 df-xneg 10174 df-xadd 10175 df-ioo 10294 df-ico 10296 df-icc 10297 df-fz 10412 df-fzo 10550 df-seqfrec 10885 df-exp 10976 df-fac 11164 df-bc 11186 df-ihash 11215 df-shft 11580 df-cj 11607 df-re 11608 df-im 11609 df-rsqrt 11764 df-abs 11765 df-clim 12045 df-sumdc 12120 df-ef 12415 df-e 12416 df-rest 13595 df-topgen 13614 df-psmet 14880 df-xmet 14881 df-met 14882 df-bl 14883 df-mopn 14884 df-top 15099 df-topon 15112 df-bases 15144 df-ntr 15197 df-cn 15289 df-cnp 15290 df-tx 15354 df-cncf 15672 df-limced 15757 df-dvap 15758 df-relog 15959

This theorem is used by: birthdaylem2 16088

W3C validator