birthdaylem2 - Intuitionistic Logic Explorer

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

Theorem birthdaylem2 16088

Description: For general 𝑁 and 𝐾, count the fraction of injective functions from 1...𝐾 to 1...𝑁. (Contributed by Mario Carneiro, 7-May-2015.)

**Hypotheses**
Ref	Expression
birthday.s	⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}
birthday.t	⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}

**Assertion**
Ref	Expression
birthdaylem2	⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘𝑇) / (♯‘𝑆)) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁)))))

Distinct variable groups: 𝑓,𝑘,𝐾 𝑓,𝑁,𝑘 Allowed substitution hints: 𝑆(𝑓, 𝑘) 𝑇(𝑓, 𝑘)

Proof of Theorem birthdaylem2 Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		birthday.t	. . . . . 6 ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}
2	1	fveq2i 5698	. . . . 5 ⊢ (♯‘𝑇) = (♯‘{𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)})
3		1zzd 9671	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 1 ∈ ℤ)
4		elfzelz 10428	. . . . . . . 8 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ)
5	4	adantl 277	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℤ)
6	3, 5	fzfigd 10868	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝐾) ∈ Fin)
7		nnz 9663	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
8	7	adantr 276	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℤ)
9	3, 8	fzfigd 10868	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
10		hashf1 11287	. . . . . 6 ⊢ (((1...𝐾) ∈ Fin ∧ (1...𝑁) ∈ Fin) → (♯‘{𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}) = ((!‘(♯‘(1...𝐾))) · ((♯‘(1...𝑁))C(♯‘(1...𝐾)))))
11	6, 9, 10	syl2anc 415	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘{𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}) = ((!‘(♯‘(1...𝐾))) · ((♯‘(1...𝑁))C(♯‘(1...𝐾)))))
12	2, 11	eqtrid 2283	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘𝑇) = ((!‘(♯‘(1...𝐾))) · ((♯‘(1...𝑁))C(♯‘(1...𝐾)))))
13		elfznn0 10521	. . . . . . . 8 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℕ₀)
14	13	adantl 277	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℕ₀)
15		hashfz1 11222	. . . . . . 7 ⊢ (𝐾 ∈ ℕ₀ → (♯‘(1...𝐾)) = 𝐾)
16	14, 15	syl 14	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘(1...𝐾)) = 𝐾)
17	16	fveq2d 5699	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(♯‘(1...𝐾))) = (!‘𝐾))
18		nnnn0 9570	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
19		hashfz1 11222	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
20	18, 19	syl 14	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (♯‘(1...𝑁)) = 𝑁)
21	20	adantr 276	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘(1...𝑁)) = 𝑁)
22	21, 16	oveq12d 6103	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘(1...𝑁))C(♯‘(1...𝐾))) = (𝑁C𝐾))
23	17, 22	oveq12d 6103	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘(♯‘(1...𝐾))) · ((♯‘(1...𝑁))C(♯‘(1...𝐾)))) = ((!‘𝐾) · (𝑁C𝐾)))
24	18	adantr 276	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℕ₀)
25	24	faccld 11174	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈ ℕ)
26	25	nncnd 9318	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈ ℂ)
27		fznn0sub 10463	. . . . . . . . . 10 ⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈ ℕ₀)
28	27	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℕ₀)
29	28	faccld 11174	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℕ)
30	29	nncnd 9318	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℂ)
31	29	nnap0d 9350	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) # 0)
32	26, 30, 31	divclapd 9120	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝑁) / (!‘(𝑁 − 𝐾))) ∈ ℂ)
33	14	faccld 11174	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈ ℕ)
34	33	nncnd 9318	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) ∈ ℂ)
35	33	nnap0d 9350	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝐾) # 0)
36	32, 34, 35	divcanap2d 9122	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝐾) · (((!‘𝑁) / (!‘(𝑁 − 𝐾))) / (!‘𝐾))) = ((!‘𝑁) / (!‘(𝑁 − 𝐾))))
37		bcval2 11188	. . . . . . . 8 ⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))))
38	37	adantl 277	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))))
39	26, 30, 34, 31, 35	divdivap1d 9152	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (((!‘𝑁) / (!‘(𝑁 − 𝐾))) / (!‘𝐾)) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))))
40	38, 39	eqtr4d 2274	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = (((!‘𝑁) / (!‘(𝑁 − 𝐾))) / (!‘𝐾)))
41	40	oveq2d 6101	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝐾) · (𝑁C𝐾)) = ((!‘𝐾) · (((!‘𝑁) / (!‘(𝑁 − 𝐾))) / (!‘𝐾))))
42	24	nn0zd 9766	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℤ)
43	3, 42	fzfigd 10868	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
44		elfznn 10460	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
45	44	adantl 277	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
46		nnrp 10064	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ⁺)
47	46	relogcld 15983	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (log‘𝑛) ∈ ℝ)
48	47	recnd 8354	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (log‘𝑛) ∈ ℂ)
49	45, 48	syl 14	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (log‘𝑛) ∈ ℂ)
50	43, 49	fsumcl 12167	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(log‘𝑛) ∈ ℂ)
51	28	nn0zd 9766	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ)
52	3, 51	fzfigd 10868	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...(𝑁 − 𝐾)) ∈ Fin)
53		elfznn 10460	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(𝑁 − 𝐾)) → 𝑛 ∈ ℕ)
54	53	adantl 277	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...(𝑁 − 𝐾))) → 𝑛 ∈ ℕ)
55	54, 48	syl 14	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...(𝑁 − 𝐾))) → (log‘𝑛) ∈ ℂ)
56	52, 55	fsumcl 12167	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛) ∈ ℂ)
57		efsub 12448	. . . . . . 7 ⊢ ((Σ𝑛 ∈ (1...𝑁)(log‘𝑛) ∈ ℂ ∧ Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛) ∈ ℂ) → (exp‘(Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))) = ((exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) / (exp‘Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))))
58	50, 56, 57	syl2anc 415	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))) = ((exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) / (exp‘Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))))
59	28	nn0red 9621	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℝ)
60	59	ltp1d 9260	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) < ((𝑁 − 𝐾) + 1))
61		fzdisj 10457	. . . . . . . . . . 11 ⊢ ((𝑁 − 𝐾) < ((𝑁 − 𝐾) + 1) → ((1...(𝑁 − 𝐾)) ∩ (((𝑁 − 𝐾) + 1)...𝑁)) = ∅)
62	60, 61	syl 14	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((1...(𝑁 − 𝐾)) ∩ (((𝑁 − 𝐾) + 1)...𝑁)) = ∅)
63		fznn0sub2 10535	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈ (0...𝑁))
64	63	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ (0...𝑁))
65		elfzle2 10432	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (𝑁 − 𝐾) ≤ 𝑁)
66	64, 65	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ≤ 𝑁)
67	66	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → (𝑁 − 𝐾) ≤ 𝑁)
68		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → (𝑁 − 𝐾) ∈ ℕ)
69		nnuz 9958	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
70	68, 69	eleqtrdi 2331	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → (𝑁 − 𝐾) ∈ (ℤ_≥‘1))
71	7	ad2antrr 492	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → 𝑁 ∈ ℤ)
72		elfz5 10420	. . . . . . . . . . . . . 14 ⊢ (((𝑁 − 𝐾) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑁 − 𝐾) ∈ (1...𝑁) ↔ (𝑁 − 𝐾) ≤ 𝑁))
73	70, 71, 72	syl2anc 415	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → ((𝑁 − 𝐾) ∈ (1...𝑁) ↔ (𝑁 − 𝐾) ≤ 𝑁))
74	67, 73	mpbird 167	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → (𝑁 − 𝐾) ∈ (1...𝑁))
75		fzsplit 10456	. . . . . . . . . . . 12 ⊢ ((𝑁 − 𝐾) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑁 − 𝐾)) ∪ (((𝑁 − 𝐾) + 1)...𝑁)))
76	74, 75	syl 14	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) ∈ ℕ) → (1...𝑁) = ((1...(𝑁 − 𝐾)) ∪ (((𝑁 − 𝐾) + 1)...𝑁)))
77		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (𝑁 − 𝐾) = 0)
78	77	oveq2d 6101	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (1...(𝑁 − 𝐾)) = (1...0))
79		fz10 10450	. . . . . . . . . . . . . 14 ⊢ (1...0) = ∅
80	78, 79	eqtrdi 2287	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (1...(𝑁 − 𝐾)) = ∅)
81	80	uneq1d 3382	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → ((1...(𝑁 − 𝐾)) ∪ (((𝑁 − 𝐾) + 1)...𝑁)) = (∅ ∪ (((𝑁 − 𝐾) + 1)...𝑁)))
82		uncom 3373	. . . . . . . . . . . . . 14 ⊢ (∅ ∪ (((𝑁 − 𝐾) + 1)...𝑁)) = ((((𝑁 − 𝐾) + 1)...𝑁) ∪ ∅)
83		un0 3556	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 − 𝐾) + 1)...𝑁) ∪ ∅) = (((𝑁 − 𝐾) + 1)...𝑁)
84	82, 83	eqtri 2259	. . . . . . . . . . . . 13 ⊢ (∅ ∪ (((𝑁 − 𝐾) + 1)...𝑁)) = (((𝑁 − 𝐾) + 1)...𝑁)
85	77	oveq1d 6100	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → ((𝑁 − 𝐾) + 1) = (0 + 1))
86		1e0p1 9818	. . . . . . . . . . . . . . 15 ⊢ 1 = (0 + 1)
87	85, 86	eqtr4di 2289	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → ((𝑁 − 𝐾) + 1) = 1)
88	87	oveq1d 6100	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (((𝑁 − 𝐾) + 1)...𝑁) = (1...𝑁))
89	84, 88	eqtrid 2283	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (∅ ∪ (((𝑁 − 𝐾) + 1)...𝑁)) = (1...𝑁))
90	81, 89	eqtr2d 2272	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ (𝑁 − 𝐾) = 0) → (1...𝑁) = ((1...(𝑁 − 𝐾)) ∪ (((𝑁 − 𝐾) + 1)...𝑁)))
91		elnn0 9565	. . . . . . . . . . . 12 ⊢ ((𝑁 − 𝐾) ∈ ℕ₀ ↔ ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0))
92	28, 91	sylib 122	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) ∈ ℕ ∨ (𝑁 − 𝐾) = 0))
93	76, 90, 92	mpjaodan 810	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝑁) = ((1...(𝑁 − 𝐾)) ∪ (((𝑁 − 𝐾) + 1)...𝑁)))
94	62, 93, 43, 49	fsumsplit 12174	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(log‘𝑛) = (Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛) + Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)))
95	94	oveq1d 6100	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)) = ((Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛) + Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)))
96	51	peano2zd 9771	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℤ)
97	96, 42	fzfigd 10868	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (((𝑁 − 𝐾) + 1)...𝑁) ∈ Fin)
98		nn0p1nn 9602	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 𝐾) ∈ ℕ₀ → ((𝑁 − 𝐾) + 1) ∈ ℕ)
99	28, 98	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝐾) + 1) ∈ ℕ)
100		elfzuz 10424	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁) → 𝑛 ∈ (ℤ_≥‘((𝑁 − 𝐾) + 1)))
101		eluznn 10000	. . . . . . . . . . . 12 ⊢ ((((𝑁 − 𝐾) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ_≥‘((𝑁 − 𝐾) + 1))) → 𝑛 ∈ ℕ)
102	99, 100, 101	syl2an 289	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → 𝑛 ∈ ℕ)
103	102, 48	syl 14	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (log‘𝑛) ∈ ℂ)
104	97, 103	fsumcl 12167	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) ∈ ℂ)
105	56, 104	pncan2d 8639	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛) + Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)) = Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛))
106	95, 105	eqtr2d 2272	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) = (Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)))
107	106	fveq2d 5699	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) = (exp‘(Σ𝑛 ∈ (1...𝑁)(log‘𝑛) − Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))))
108	25	nnrpd 10095	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) ∈ ℝ⁺)
109	108	reeflogd 15984	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(log‘(!‘𝑁))) = (!‘𝑁))
110		logfac 15995	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (log‘(!‘𝑁)) = Σ𝑛 ∈ (1...𝑁)(log‘𝑛))
111	24, 110	syl 14	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘(!‘𝑁)) = Σ𝑛 ∈ (1...𝑁)(log‘𝑛))
112	111	fveq2d 5699	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(log‘(!‘𝑁))) = (exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)))
113	109, 112	eqtr3d 2273	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘𝑁) = (exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)))
114	29	nnrpd 10095	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) ∈ ℝ⁺)
115	114	reeflogd 15984	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(log‘(!‘(𝑁 − 𝐾)))) = (!‘(𝑁 − 𝐾)))
116		logfac 15995	. . . . . . . . . 10 ⊢ ((𝑁 − 𝐾) ∈ ℕ₀ → (log‘(!‘(𝑁 − 𝐾))) = Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))
117	28, 116	syl 14	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘(!‘(𝑁 − 𝐾))) = Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))
118	117	fveq2d 5699	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(log‘(!‘(𝑁 − 𝐾)))) = (exp‘Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)))
119	115, 118	eqtr3d 2273	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (!‘(𝑁 − 𝐾)) = (exp‘Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛)))
120	113, 119	oveq12d 6103	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝑁) / (!‘(𝑁 − 𝐾))) = ((exp‘Σ𝑛 ∈ (1...𝑁)(log‘𝑛)) / (exp‘Σ𝑛 ∈ (1...(𝑁 − 𝐾))(log‘𝑛))))
121	58, 107, 120	3eqtr4d 2281	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) = ((!‘𝑁) / (!‘(𝑁 − 𝐾))))
122	36, 41, 121	3eqtr4d 2281	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((!‘𝐾) · (𝑁C𝐾)) = (exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)))
123	12, 23, 122	3eqtrd 2275	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘𝑇) = (exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)))
124		birthday.s	. . . . . . 7 ⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}
125		mapvalg 6932	. . . . . . . 8 ⊢ (((1...𝑁) ∈ Fin ∧ (1...𝐾) ∈ Fin) → ((1...𝑁) ↑_𝑚 (1...𝐾)) = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)})
126	9, 6, 125	syl2anc 415	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((1...𝑁) ↑_𝑚 (1...𝐾)) = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)})
127	124, 126	eqtr4id 2290	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑆 = ((1...𝑁) ↑_𝑚 (1...𝐾)))
128	127	fveq2d 5699	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘𝑆) = (♯‘((1...𝑁) ↑_𝑚 (1...𝐾))))
129		hashmap 11268	. . . . . 6 ⊢ (((1...𝑁) ∈ Fin ∧ (1...𝐾) ∈ Fin) → (♯‘((1...𝑁) ↑_𝑚 (1...𝐾))) = ((♯‘(1...𝑁))↑(♯‘(1...𝐾))))
130	9, 6, 129	syl2anc 415	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘((1...𝑁) ↑_𝑚 (1...𝐾))) = ((♯‘(1...𝑁))↑(♯‘(1...𝐾))))
131	128, 130	eqtrd 2271	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘𝑆) = ((♯‘(1...𝑁))↑(♯‘(1...𝐾))))
132	21, 16	oveq12d 6103	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘(1...𝑁))↑(♯‘(1...𝐾))) = (𝑁↑𝐾))
133		nnrp 10064	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺)
134	133	adantr 276	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℝ⁺)
135		reexplog 15972	. . . . 5 ⊢ ((𝑁 ∈ ℝ⁺ ∧ 𝐾 ∈ ℤ) → (𝑁↑𝐾) = (exp‘(𝐾 · (log‘𝑁))))
136	134, 5, 135	syl2anc 415	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁↑𝐾) = (exp‘(𝐾 · (log‘𝑁))))
137	131, 132, 136	3eqtrd 2275	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘𝑆) = (exp‘(𝐾 · (log‘𝑁))))
138	123, 137	oveq12d 6103	. 2 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘𝑇) / (♯‘𝑆)) = ((exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) / (exp‘(𝐾 · (log‘𝑁)))))
139	14	nn0cnd 9622	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℂ)
140	134	relogcld 15983	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘𝑁) ∈ ℝ)
141	140	recnd 8354	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (log‘𝑁) ∈ ℂ)
142	139, 141	mulcld 8346	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝐾 · (log‘𝑁)) ∈ ℂ)
143		efsub 12448	. . 3 ⊢ ((Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) ∈ ℂ ∧ (𝐾 · (log‘𝑁)) ∈ ℂ) → (exp‘(Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) = ((exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) / (exp‘(𝐾 · (log‘𝑁)))))
144	104, 142, 143	syl2anc 415	. 2 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) = ((exp‘Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛)) / (exp‘(𝐾 · (log‘𝑁)))))
145		relogdiv 15971	. . . . . . 7 ⊢ ((𝑛 ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → (log‘(𝑛 / 𝑁)) = ((log‘𝑛) − (log‘𝑁)))
146	46, 134, 145	syl2anr 290	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ ℕ) → (log‘(𝑛 / 𝑁)) = ((log‘𝑛) − (log‘𝑁)))
147	102, 146	syldan 282	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (log‘(𝑛 / 𝑁)) = ((log‘𝑛) − (log‘𝑁)))
148	147	sumeq2dv 12134	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘(𝑛 / 𝑁)) = Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)((log‘𝑛) − (log‘𝑁)))
149	102	nnrpd 10095	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → 𝑛 ∈ ℝ⁺)
150	134	adantr 276	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → 𝑁 ∈ ℝ⁺)
151	149, 150	rpdivcld 10115	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (𝑛 / 𝑁) ∈ ℝ⁺)
152	151	relogcld 15983	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (log‘(𝑛 / 𝑁)) ∈ ℝ)
153	152	recnd 8354	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (log‘(𝑛 / 𝑁)) ∈ ℂ)
154		fvoveq1 6108	. . . . . 6 ⊢ (𝑛 = (𝑁 − 𝑘) → (log‘(𝑛 / 𝑁)) = (log‘((𝑁 − 𝑘) / 𝑁)))
155	8, 96, 8, 153, 154	fsumrev 12210	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘(𝑛 / 𝑁)) = Σ𝑘 ∈ ((𝑁 − 𝑁)...(𝑁 − ((𝑁 − 𝐾) + 1)))(log‘((𝑁 − 𝑘) / 𝑁)))
156		nncn 9312	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
157	156	adantr 276	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℂ)
158	157	subidd 8625	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝑁) = 0)
159		1cnd 8342	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → 1 ∈ ℂ)
160	157, 139, 159	subsubd 8665	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − (𝐾 − 1)) = ((𝑁 − 𝐾) + 1))
161	160	oveq2d 6101	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − (𝑁 − (𝐾 − 1))) = (𝑁 − ((𝑁 − 𝐾) + 1)))
162		ax-1cn 8272	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
163		subcl 8525	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐾 − 1) ∈ ℂ)
164	139, 162, 163	sylancl 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝐾 − 1) ∈ ℂ)
165	157, 164	nncand 8642	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − (𝑁 − (𝐾 − 1))) = (𝐾 − 1))
166	161, 165	eqtr3d 2273	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − ((𝑁 − 𝐾) + 1)) = (𝐾 − 1))
167	158, 166	oveq12d 6103	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝑁)...(𝑁 − ((𝑁 − 𝐾) + 1))) = (0...(𝐾 − 1)))
168	157	adantr 276	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑁 ∈ ℂ)
169		elfznn0 10521	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...(𝐾 − 1)) → 𝑘 ∈ ℕ₀)
170	169	adantl 277	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑘 ∈ ℕ₀)
171	170	nn0cnd 9622	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑘 ∈ ℂ)
172		nnap0 9333	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 # 0)
173	172	ad2antrr 492	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → 𝑁 # 0)
174	168, 171, 168, 173	divsubdirapd 9160	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → ((𝑁 − 𝑘) / 𝑁) = ((𝑁 / 𝑁) − (𝑘 / 𝑁)))
175	168, 173	dividapd 9116	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → (𝑁 / 𝑁) = 1)
176	175	oveq1d 6100	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → ((𝑁 / 𝑁) − (𝑘 / 𝑁)) = (1 − (𝑘 / 𝑁)))
177	174, 176	eqtrd 2271	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → ((𝑁 − 𝑘) / 𝑁) = (1 − (𝑘 / 𝑁)))
178	177	fveq2d 5699	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑘 ∈ (0...(𝐾 − 1))) → (log‘((𝑁 − 𝑘) / 𝑁)) = (log‘(1 − (𝑘 / 𝑁))))
179	167, 178	sumeq12rdv 12139	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑘 ∈ ((𝑁 − 𝑁)...(𝑁 − ((𝑁 − 𝐾) + 1)))(log‘((𝑁 − 𝑘) / 𝑁)) = Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁))))
180	155, 179	eqtrd 2271	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘(𝑛 / 𝑁)) = Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁))))
181	141	adantr 276	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)) → (log‘𝑁) ∈ ℂ)
182	97, 103, 181	fsumsub 12219	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)((log‘𝑛) − (log‘𝑁)) = (Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑁)))
183		fsumconst 12221	. . . . . . . 8 ⊢ (((((𝑁 − 𝐾) + 1)...𝑁) ∈ Fin ∧ (log‘𝑁) ∈ ℂ) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑁) = ((♯‘(((𝑁 − 𝐾) + 1)...𝑁)) · (log‘𝑁)))
184	97, 141, 183	syl2anc 415	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑁) = ((♯‘(((𝑁 − 𝐾) + 1)...𝑁)) · (log‘𝑁)))
185		fzen 10447	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑁 − 𝐾) ∈ ℤ) → (1...𝐾) ≈ ((1 + (𝑁 − 𝐾))...(𝐾 + (𝑁 − 𝐾))))
186	3, 5, 51, 185	syl3anc 1278	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝐾) ≈ ((1 + (𝑁 − 𝐾))...(𝐾 + (𝑁 − 𝐾))))
187	28	nn0cnd 9622	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ ℂ)
188		addcom 8463	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ (𝑁 − 𝐾) ∈ ℂ) → (1 + (𝑁 − 𝐾)) = ((𝑁 − 𝐾) + 1))
189	162, 187, 188	sylancr 418	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1 + (𝑁 − 𝐾)) = ((𝑁 − 𝐾) + 1))
190	139, 157	pncan3d 8640	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (𝐾 + (𝑁 − 𝐾)) = 𝑁)
191	189, 190	oveq12d 6103	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((1 + (𝑁 − 𝐾))...(𝐾 + (𝑁 − 𝐾))) = (((𝑁 − 𝐾) + 1)...𝑁))
192	186, 191	breqtrd 4156	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (1...𝐾) ≈ (((𝑁 − 𝐾) + 1)...𝑁))
193		hashen 11223	. . . . . . . . . . 11 ⊢ (((1...𝐾) ∈ Fin ∧ (((𝑁 − 𝐾) + 1)...𝑁) ∈ Fin) → ((♯‘(1...𝐾)) = (♯‘(((𝑁 − 𝐾) + 1)...𝑁)) ↔ (1...𝐾) ≈ (((𝑁 − 𝐾) + 1)...𝑁)))
194	6, 97, 193	syl2anc 415	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘(1...𝐾)) = (♯‘(((𝑁 − 𝐾) + 1)...𝑁)) ↔ (1...𝐾) ≈ (((𝑁 − 𝐾) + 1)...𝑁)))
195	192, 194	mpbird 167	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘(1...𝐾)) = (♯‘(((𝑁 − 𝐾) + 1)...𝑁)))
196	195, 16	eqtr3d 2273	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (♯‘(((𝑁 − 𝐾) + 1)...𝑁)) = 𝐾)
197	196	oveq1d 6100	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘(((𝑁 − 𝐾) + 1)...𝑁)) · (log‘𝑁)) = (𝐾 · (log‘𝑁)))
198	184, 197	eqtrd 2271	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑁) = (𝐾 · (log‘𝑁)))
199	198	oveq2d 6101	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑁)) = (Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁))))
200	182, 199	eqtrd 2271	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)((log‘𝑛) − (log‘𝑁)) = (Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁))))
201	148, 180, 200	3eqtr3rd 2280	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁))) = Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁))))
202	201	fveq2d 5699	. 2 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → (exp‘(Σ𝑛 ∈ (((𝑁 − 𝐾) + 1)...𝑁)(log‘𝑛) − (𝐾 · (log‘𝑁)))) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁)))))
203	138, 144, 202	3eqtr2d 2277	1 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘𝑇) / (♯‘𝑆)) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁)))))

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 = wceq 1402 ∈ wcel 2209 {cab 2224 ∪ cun 3218 ∩ cin 3219 ∅c0 3520 class class class wbr 4130 ⟶wf 5373 –1-1→wf1 5374 ‘cfv 5377 (class class class)co 6085 ↑_𝑚 cmap 6922 ≈ cen 7020 Fincfn 7022 ℂcc 8177 0cc0 8179 1c1 8180 + caddc 8182 · cmul 8184 < clt 8360 ≤ cle 8361 − cmin 8497 # cap 8909 / cdiv 9002 ℕcn 9304 ℕ₀cn0 9563 ℤcz 9644 ℤ_≥cuz 9921 ℝ⁺crp 10054 ...cfz 10411 ↑cexp 10975 !cfa 11163 Ccbc 11185 ♯chash 11214 Σcsu 12119 expce 12409 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: birthdaylem3 16089

W3C validator