logfac - Intuitionistic Logic Explorer

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

Theorem logfac 16090

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 9570	. 2 ⊢ (𝑁 ∈ ℕ₀ ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
2		elnn1uz2 10017	. . . . 5 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ_≥‘2)))
3		1zzd 9676	. . . . . . . . . . 11 ⊢ (𝑁 = 1 → 1 ∈ ℤ)
4		fvi 5760	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → ( I ‘𝑘) = 𝑘)
5		elnnuz 9969	. . . . . . . . . . . . . 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 9328	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑘 · 𝑛) ∈ ℕ)
10	9	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 = 1 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (𝑘 · 𝑛) ∈ ℕ)
11	3, 8, 10	seq3-1 10914	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (seq1( · , I )‘1) = ( I ‘1))
12		1nn 9318	. . . . . . . . . . 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 10075	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ⁺)
18		relogcl 16055	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℝ⁺ → (log‘𝑘) ∈ ℝ)
19	6, 17, 18	3syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (log‘𝑘) ∈ ℝ)
20	19	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 = 1 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℝ)
21		readdcl 8306	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑘 + 𝑛) ∈ ℝ)
22	21	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 = 1 ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝑘 + 𝑛) ∈ ℝ)
23	3, 20, 22	seq3-1 10914	. . . . . . . 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 10090	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑘 · 𝑛) ∈ ℝ⁺)
29	28	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺)) → (𝑘 · 𝑛) ∈ ℝ⁺)
30		fvi 5760	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘2) → ( I ‘𝑘) = 𝑘)
31		eluz2nn 9976	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℕ)
32	31	nnrpd 10106	. . . . . . . . . 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 16063	. . . . . . . . 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 9320	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℝ)
43	42	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑘 ∈ ℝ)
44		eluz2gt1 10012	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 1 < 𝑘)
45	44	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → 1 < 𝑘)
46	43, 45	rplogcld 16082	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → (log‘𝑘) ∈ ℝ⁺)
47		rpaddcl 10089	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑘 + 𝑛) ∈ ℝ⁺)
48	47	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺)) → (𝑘 + 𝑛) ∈ ℝ⁺)
49	29, 34, 35, 37, 41, 46, 48	seq3homo 10979	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (log‘(seq2( · , I )‘𝑁)) = (seq2( + , log)‘𝑁))
50		remulcl 8308	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑘 · 𝑛) ∈ ℝ)
51	50	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝑘 · 𝑛) ∈ ℝ)
52		simp1 1028	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑘 ∈ ℝ)
53	52	recnd 8355	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑘 ∈ ℂ)
54		simp2 1029	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑛 ∈ ℝ)
55	54	recnd 8355	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑛 ∈ ℂ)
56		simp3 1030	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ∈ ℝ)
57	56	recnd 8355	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ∈ ℂ)
58	53, 55, 57	mulassd 8350	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑘 · 𝑛) · 𝑚) = (𝑘 · (𝑛 · 𝑚)))
59	58	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((𝑘 · 𝑛) · 𝑚) = (𝑘 · (𝑛 · 𝑚)))
60		1p1e2 9424	. . . . . . . . . . . . . . 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 9676	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 1 ∈ ℤ)
65	7	nnred 9320	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → ( I ‘𝑘) ∈ ℝ)
66	65	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘1)) → ( I ‘𝑘) ∈ ℝ)
67	51, 59, 63, 64, 66	seq3-1p 10942	. . . . . . . . . . 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 10902	. . . . . . . . . . . . . 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 9936	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘2) → 2 ∈ ℤ)
75		eluzelz 9941	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℤ)
76	30, 75	eqeltrd 2315	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘2) → ( I ‘𝑘) ∈ ℤ)
77	76	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘2)) → ( I ‘𝑘) ∈ ℤ)
78		zmulcl 9703	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑘 · 𝑛) ∈ ℤ)
79	78	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ)) → (𝑘 · 𝑛) ∈ ℤ)
80	73, 74, 77, 79	seqf 10916	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘2) → seq2( · , I ):(ℤ_≥‘2)⟶ℤ)
81	80, 35	ffvelcdmd 5844	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( · , I )‘𝑁) ∈ ℤ)
82	81	zcnd 9774	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( · , I )‘𝑁) ∈ ℂ)
83	72, 82	eqeltrid 2325	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq(1 + 1)( · , I )‘𝑁) ∈ ℂ)
84	83	mullidd 8345	. . . . . . . . . 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 8349	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑘 + 𝑛) + 𝑚) = (𝑘 + (𝑛 + 𝑚)))
90	89	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ (𝑘 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((𝑘 + 𝑛) + 𝑚) = (𝑘 + (𝑛 + 𝑚)))
91	6	nnrpd 10106	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘1) → 𝑘 ∈ ℝ⁺)
92	91	relogcld 16076	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘1) → (log‘𝑘) ∈ ℝ)
93	92	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℝ)
94	88, 90, 63, 64, 93	seq3-1p 10942	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq1( + , log)‘𝑁) = ((log‘1) + (seq(1 + 1)( + , log)‘𝑁)))
95		seqeq1 10902	. . . . . . . . . . . . 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 16059	. . . . . . . . . 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 10916	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘2) → seq2( + , log):(ℤ_≥‘2)⟶ℝ⁺)
104	103, 35	ffvelcdmd 5844	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( + , log)‘𝑁) ∈ ℝ⁺)
105	104	rpcnd 10110	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘2) → (seq2( + , log)‘𝑁) ∈ ℂ)
106	105	addlidd 8478	. . . . . . . 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 11181	. . . . 5 ⊢ (𝑁 ∈ ℕ → (!‘𝑁) = (seq1( · , I )‘𝑁))
112	111	fveq2d 5699	. . . 4 ⊢ (𝑁 ∈ ℕ → (log‘(!‘𝑁)) = (log‘(seq1( · , I )‘𝑁)))
113		eqidd 2239	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) = (log‘𝑘))
114		elnnuz 9969	. . . . . 6 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
115	114	biimpi 120	. . . . 5 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘1))
116	19	adantl 277	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℝ)
117	116	recnd 8355	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘1)) → (log‘𝑘) ∈ ℂ)
118	113, 115, 117	fsum3ser 12183	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...𝑁)(log‘𝑘) = (seq1( + , log)‘𝑁))
119	110, 112, 118	3eqtr4d 2281	. . 3 ⊢ (𝑁 ∈ ℕ → (log‘(!‘𝑁)) = Σ𝑘 ∈ (1...𝑁)(log‘𝑘))
120		sum0 12174	. . . . 5 ⊢ Σ𝑘 ∈ ∅ (log‘𝑘) = 0
121	100, 120	eqtr4i 2262	. . . 4 ⊢ (log‘1) = Σ𝑘 ∈ ∅ (log‘𝑘)
122		fveq2 5695	. . . . . 6 ⊢ (𝑁 = 0 → (!‘𝑁) = (!‘0))
123		fac0 11182	. . . . . 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 10461	. . . . . 6 ⊢ (1...0) = ∅
128	126, 127	eqtrdi 2287	. . . . 5 ⊢ (𝑁 = 0 → (1...𝑁) = ∅)
129	128	sumeq1d 12151	. . . 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 8178 ℝcr 8179 0cc0 8180 1c1 8181 + caddc 8183 · cmul 8185 < clt 8361 ℕcn 9307 2c2 9358 ℕ₀cn0 9568 ℤcz 9649 ℤ_≥cuz 9931 ℝ⁺crp 10065 ...cfz 10422 seqcseq 10899 !cfa 11179 Σcsu 12138 logclog 16049

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

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 7325 df-inf 7326 df-pnf 8363 df-mnf 8364 df-xr 8365 df-ltxr 8366 df-le 8367 df-sub 8501 df-neg 8502 df-reap 8906 df-ap 8913 df-div 9006 df-inn 9308 df-2 9366 df-3 9367 df-4 9368 df-n0 9569 df-z 9650 df-uz 9932 df-q 10030 df-rp 10066 df-xneg 10185 df-xadd 10186 df-ioo 10305 df-ico 10307 df-icc 10308 df-fz 10423 df-fzo 10561 df-seqfrec 10900 df-exp 10991 df-fac 11180 df-bc 11202 df-ihash 11231 df-shft 11596 df-cj 11623 df-re 11624 df-im 11625 df-rsqrt 11780 df-abs 11781 df-clim 12064 df-sumdc 12139 df-ef 12434 df-e 12435 df-rest 13648 df-topgen 13667 df-psmet 14964 df-xmet 14965 df-met 14966 df-bl 14967 df-mopn 14968 df-top 15190 df-topon 15203 df-bases 15235 df-ntr 15288 df-cn 15380 df-cnp 15381 df-tx 15445 df-cncf 15763 df-limced 15848 df-dvap 15849 df-relog 16051

This theorem is used by: birthdaylem2 16187

W3C validator