birthdaylem2

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

	Ref	Expression
Hypotheses	birthday.s	$⊢ S = \{f \| f : (1 \dots K) ⟶ (1 \dots N)\}$
	birthday.t	$⊢ T = \{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\}$
Assertion	birthdaylem2	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \frac{\|T\|}{\|S\|} = e^{\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))}$

Proof

Step	Hyp	Ref	Expression
1		birthday.s	$⊢ S = \{f \| f : (1 \dots K) ⟶ (1 \dots N)\}$
2		birthday.t	$⊢ T = \{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\}$
3	2	fveq2i	$⊢ \|T\| = \|\{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\}\|$
4		fzfi	$⊢ (1 \dots K) \in Fin$
5		fzfi	$⊢ (1 \dots N) \in Fin$
6		hashf1	$⊢ ((1 \dots K) \in Fin \land (1 \dots N) \in Fin) \to \|\{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\}\| = \|(1 \dots K)\|! (\binom{\|(1 \dots N)\|}{\|(1 \dots K)\|})$
7	4 5 6	mp2an	$⊢ \|\{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\}\| = \|(1 \dots K)\|! (\binom{\|(1 \dots N)\|}{\|(1 \dots K)\|})$
8	3 7	eqtri	$⊢ \|T\| = \|(1 \dots K)\|! (\binom{\|(1 \dots N)\|}{\|(1 \dots K)\|})$
9		elfznn0	$⊢ K \in (0 \dots N) \to K \in ℕ_{0}$
10	9	adantl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K \in ℕ_{0}$
11		hashfz1	$⊢ K \in ℕ_{0} \to \|(1 \dots K)\| = K$
12	10 11	syl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|(1 \dots K)\| = K$
13	12	fveq2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|(1 \dots K)\|! = K!$
14		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
15		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
16	14 15	syl	$⊢ N \in ℕ \to \|(1 \dots N)\| = N$
17	16	adantr	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|(1 \dots N)\| = N$
18	17 12	oveq12d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (\binom{\|(1 \dots N)\|}{\|(1 \dots K)\|}) = (\binom{N}{K})$
19	13 18	oveq12d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|(1 \dots K)\|! (\binom{\|(1 \dots N)\|}{\|(1 \dots K)\|}) = K! (\binom{N}{K})$
20	8 19	syl5eq	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|T\| = K! (\binom{N}{K})$
21	14	adantr	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N \in ℕ_{0}$
22	21	faccld	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N! \in ℕ$
23	22	nncnd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N! \in ℂ$
24		fznn0sub	$⊢ K \in (0 \dots N) \to N - K \in ℕ_{0}$
25	24	adantl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - K \in ℕ_{0}$
26	25	faccld	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (N - K)! \in ℕ$
27	26	nncnd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (N - K)! \in ℂ$
28	26	nnne0d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (N - K)! \neq 0$
29	23 27 28	divcld	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \frac{N!}{(N - K)!} \in ℂ$
30	10	faccld	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K! \in ℕ$
31	30	nncnd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K! \in ℂ$
32	30	nnne0d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K! \neq 0$
33	29 31 32	divcan2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K! (\frac{\frac{N!}{(N - K)!}}{K!}) = \frac{N!}{(N - K)!}$
34		bcval2	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
35	34	adantl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
36	23 27 31 28 32	divdiv1d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \frac{\frac{N!}{(N - K)!}}{K!} = \frac{N!}{(N - K)! K!}$
37	35 36	eqtr4d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (\binom{N}{K}) = \frac{\frac{N!}{(N - K)!}}{K!}$
38	37	oveq2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K! (\binom{N}{K}) = K! (\frac{\frac{N!}{(N - K)!}}{K!})$
39		fzfid	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (1 \dots N) \in Fin$
40		elfznn	$⊢ n \in (1 \dots N) \to n \in ℕ$
41	40	adantl	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (1 \dots N)) \to n \in ℕ$
42		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
43	42	relogcld	$⊢ n \in ℕ \to \log n \in ℝ$
44	43	recnd	$⊢ n \in ℕ \to \log n \in ℂ$
45	41 44	syl	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (1 \dots N)) \to \log n \in ℂ$
46	39 45	fsumcl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = 1}^{N} \log n \in ℂ$
47		fzfid	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (1 \dots N - K) \in Fin$
48		elfznn	$⊢ n \in (1 \dots N - K) \to n \in ℕ$
49	48	adantl	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (1 \dots N - K)) \to n \in ℕ$
50	49 44	syl	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (1 \dots N - K)) \to \log n \in ℂ$
51	47 50	fsumcl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = 1}^{N - K} \log n \in ℂ$
52		efsub	$⊢ (\sum_{n = 1}^{N} \log n \in ℂ \land \sum_{n = 1}^{N - K} \log n \in ℂ) \to e^{\sum_{n = 1}^{N} \log n - \sum_{n = 1}^{N - K} \log n} = \frac{e^{\sum_{n = 1}^{N} \log n}}{e^{\sum_{n = 1}^{N - K} \log n}}$
53	46 51 52	syl2anc	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to e^{\sum_{n = 1}^{N} \log n - \sum_{n = 1}^{N - K} \log n} = \frac{e^{\sum_{n = 1}^{N} \log n}}{e^{\sum_{n = 1}^{N - K} \log n}}$
54	25	nn0red	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - K \in ℝ$
55	54	ltp1d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - K < N - K + 1$
56		fzdisj	$⊢ N - K < N - K + 1 \to (1 \dots N - K) \cap (N - K + 1 \dots N) = \emptyset$
57	55 56	syl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (1 \dots N - K) \cap (N - K + 1 \dots N) = \emptyset$
58		fznn0sub2	$⊢ K \in (0 \dots N) \to N - K \in (0 \dots N)$
59	58	adantl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - K \in (0 \dots N)$
60		elfzle2	$⊢ N - K \in (0 \dots N) \to N - K \leq N$
61	59 60	syl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - K \leq N$
62	61	adantr	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K \in ℕ) \to N - K \leq N$
63		simpr	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K \in ℕ) \to N - K \in ℕ$
64		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
65	63 64	eleqtrdi	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K \in ℕ) \to N - K \in ℤ_{\geq 1}$
66		nnz	$⊢ N \in ℕ \to N \in ℤ$
67	66	ad2antrr	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K \in ℕ) \to N \in ℤ$
68		elfz5	$⊢ (N - K \in ℤ_{\geq 1} \land N \in ℤ) \to (N - K \in (1 \dots N) \leftrightarrow N - K \leq N)$
69	65 67 68	syl2anc	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K \in ℕ) \to (N - K \in (1 \dots N) \leftrightarrow N - K \leq N)$
70	62 69	mpbird	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K \in ℕ) \to N - K \in (1 \dots N)$
71		fzsplit	$⊢ N - K \in (1 \dots N) \to (1 \dots N) = (1 \dots N - K) \cup (N - K + 1 \dots N)$
72	70 71	syl	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K \in ℕ) \to (1 \dots N) = (1 \dots N - K) \cup (N - K + 1 \dots N)$
73		simpr	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K = 0) \to N - K = 0$
74	73	oveq2d	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K = 0) \to (1 \dots N - K) = (1 \dots 0)$
75		fz10	$⊢ (1 \dots 0) = \emptyset$
76	74 75	syl6eq	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K = 0) \to (1 \dots N - K) = \emptyset$
77	76	uneq1d	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K = 0) \to (1 \dots N - K) \cup (N - K + 1 \dots N) = \emptyset \cup (N - K + 1 \dots N)$
78		uncom	$⊢ \emptyset \cup (N - K + 1 \dots N) = (N - K + 1 \dots N) \cup \emptyset$
79		un0	$⊢ (N - K + 1 \dots N) \cup \emptyset = (N - K + 1 \dots N)$
80	78 79	eqtri	$⊢ \emptyset \cup (N - K + 1 \dots N) = (N - K + 1 \dots N)$
81	73	oveq1d	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K = 0) \to N - K + 1 = 0 + 1$
82		1e0p1	$⊢ 1 = 0 + 1$
83	81 82	syl6eqr	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K = 0) \to N - K + 1 = 1$
84	83	oveq1d	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K = 0) \to (N - K + 1 \dots N) = (1 \dots N)$
85	80 84	syl5eq	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K = 0) \to \emptyset \cup (N - K + 1 \dots N) = (1 \dots N)$
86	77 85	eqtr2d	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land N - K = 0) \to (1 \dots N) = (1 \dots N - K) \cup (N - K + 1 \dots N)$
87		elnn0	$⊢ N - K \in ℕ_{0} \leftrightarrow (N - K \in ℕ \lor N - K = 0)$
88	25 87	sylib	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (N - K \in ℕ \lor N - K = 0)$
89	72 86 88	mpjaodan	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (1 \dots N) = (1 \dots N - K) \cup (N - K + 1 \dots N)$
90	57 89 39 45	fsumsplit	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = 1}^{N} \log n = \sum_{n = 1}^{N - K} \log n + \sum_{n = N - K + 1}^{N} \log n$
91	90	oveq1d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = 1}^{N} \log n - \sum_{n = 1}^{N - K} \log n = \sum_{n = 1}^{N - K} \log n + \sum_{n = N - K + 1}^{N} \log n - \sum_{n = 1}^{N - K} \log n$
92		fzfid	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (N - K + 1 \dots N) \in Fin$
93		nn0p1nn	$⊢ N - K \in ℕ_{0} \to N - K + 1 \in ℕ$
94	25 93	syl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - K + 1 \in ℕ$
95		elfzuz	$⊢ n \in (N - K + 1 \dots N) \to n \in ℤ_{\geq (N - K + 1)}$
96		eluznn	$⊢ (N - K + 1 \in ℕ \land n \in ℤ_{\geq (N - K + 1)}) \to n \in ℕ$
97	94 95 96	syl2an	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (N - K + 1 \dots N)) \to n \in ℕ$
98	97 44	syl	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (N - K + 1 \dots N)) \to \log n \in ℂ$
99	92 98	fsumcl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} \log n \in ℂ$
100	51 99	pncan2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = 1}^{N - K} \log n + \sum_{n = N - K + 1}^{N} \log n - \sum_{n = 1}^{N - K} \log n = \sum_{n = N - K + 1}^{N} \log n$
101	91 100	eqtr2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} \log n = \sum_{n = 1}^{N} \log n - \sum_{n = 1}^{N - K} \log n$
102	101	fveq2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to e^{\sum_{n = N - K + 1}^{N} \log n} = e^{\sum_{n = 1}^{N} \log n - \sum_{n = 1}^{N - K} \log n}$
103	22	nnne0d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N! \neq 0$
104		eflog	$⊢ (N! \in ℂ \land N! \neq 0) \to e^{\log N!} = N!$
105	23 103 104	syl2anc	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to e^{\log N!} = N!$
106		logfac	$⊢ N \in ℕ_{0} \to \log N! = \sum_{n = 1}^{N} \log n$
107	21 106	syl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \log N! = \sum_{n = 1}^{N} \log n$
108	107	fveq2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to e^{\log N!} = e^{\sum_{n = 1}^{N} \log n}$
109	105 108	eqtr3d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N! = e^{\sum_{n = 1}^{N} \log n}$
110		eflog	$⊢ ((N - K)! \in ℂ \land (N - K)! \neq 0) \to e^{\log (N - K)!} = (N - K)!$
111	27 28 110	syl2anc	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to e^{\log (N - K)!} = (N - K)!$
112		logfac	$⊢ N - K \in ℕ_{0} \to \log (N - K)! = \sum_{n = 1}^{N - K} \log n$
113	25 112	syl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \log (N - K)! = \sum_{n = 1}^{N - K} \log n$
114	113	fveq2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to e^{\log (N - K)!} = e^{\sum_{n = 1}^{N - K} \log n}$
115	111 114	eqtr3d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (N - K)! = e^{\sum_{n = 1}^{N - K} \log n}$
116	109 115	oveq12d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \frac{N!}{(N - K)!} = \frac{e^{\sum_{n = 1}^{N} \log n}}{e^{\sum_{n = 1}^{N - K} \log n}}$
117	53 102 116	3eqtr4d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to e^{\sum_{n = N - K + 1}^{N} \log n} = \frac{N!}{(N - K)!}$
118	33 38 117	3eqtr4d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K! (\binom{N}{K}) = e^{\sum_{n = N - K + 1}^{N} \log n}$
119	20 118	eqtrd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|T\| = e^{\sum_{n = N - K + 1}^{N} \log n}$
120		mapvalg	$⊢ ((1 \dots N) \in Fin \land (1 \dots K) \in Fin) \to {(1 \dots N)}^{(1 \dots K)} = \{f \| f : (1 \dots K) ⟶ (1 \dots N)\}$
121	5 4 120	mp2an	$⊢ {(1 \dots N)}^{(1 \dots K)} = \{f \| f : (1 \dots K) ⟶ (1 \dots N)\}$
122	1 121	eqtr4i	$⊢ S = {(1 \dots N)}^{(1 \dots K)}$
123	122	fveq2i	$⊢ \|S\| = \|{(1 \dots N)}^{(1 \dots K)}\|$
124		hashmap	$⊢ ((1 \dots N) \in Fin \land (1 \dots K) \in Fin) \to \|{(1 \dots N)}^{(1 \dots K)}\| = {\|(1 \dots N)\|}^{\|(1 \dots K)\|}$
125	5 4 124	mp2an	$⊢ \|{(1 \dots N)}^{(1 \dots K)}\| = {\|(1 \dots N)\|}^{\|(1 \dots K)\|}$
126	123 125	eqtri	$⊢ \|S\| = {\|(1 \dots N)\|}^{\|(1 \dots K)\|}$
127	17 12	oveq12d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to {\|(1 \dots N)\|}^{\|(1 \dots K)\|} = N^{K}$
128	126 127	syl5eq	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|S\| = N^{K}$
129		nncn	$⊢ N \in ℕ \to N \in ℂ$
130	129	adantr	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N \in ℂ$
131		nnne0	$⊢ N \in ℕ \to N \neq 0$
132	131	adantr	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N \neq 0$
133		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
134	133	adantl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K \in ℤ$
135		explog	$⊢ (N \in ℂ \land N \neq 0 \land K \in ℤ) \to N^{K} = e^{K \log N}$
136	130 132 134 135	syl3anc	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N^{K} = e^{K \log N}$
137	128 136	eqtrd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|S\| = e^{K \log N}$
138	119 137	oveq12d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \frac{\|T\|}{\|S\|} = \frac{e^{\sum_{n = N - K + 1}^{N} \log n}}{e^{K \log N}}$
139	10	nn0cnd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K \in ℂ$
140		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
141	140	adantr	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N \in ℝ^{+}$
142	141	relogcld	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \log N \in ℝ$
143	142	recnd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \log N \in ℂ$
144	139 143	mulcld	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K \log N \in ℂ$
145		efsub	$⊢ (\sum_{n = N - K + 1}^{N} \log n \in ℂ \land K \log N \in ℂ) \to e^{\sum_{n = N - K + 1}^{N} \log n - K \log N} = \frac{e^{\sum_{n = N - K + 1}^{N} \log n}}{e^{K \log N}}$
146	99 144 145	syl2anc	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to e^{\sum_{n = N - K + 1}^{N} \log n - K \log N} = \frac{e^{\sum_{n = N - K + 1}^{N} \log n}}{e^{K \log N}}$
147		relogdiv	$⊢ (n \in ℝ^{+} \land N \in ℝ^{+}) \to \log (\frac{n}{N}) = \log n - \log N$
148	42 141 147	syl2anr	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in ℕ) \to \log (\frac{n}{N}) = \log n - \log N$
149	97 148	syldan	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (N - K + 1 \dots N)) \to \log (\frac{n}{N}) = \log n - \log N$
150	149	sumeq2dv	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} \log (\frac{n}{N}) = \sum_{n = N - K + 1}^{N} (\log n - \log N)$
151	66	adantr	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N \in ℤ$
152	25	nn0zd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - K \in ℤ$
153	152	peano2zd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - K + 1 \in ℤ$
154	97	nnrpd	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (N - K + 1 \dots N)) \to n \in ℝ^{+}$
155	141	adantr	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (N - K + 1 \dots N)) \to N \in ℝ^{+}$
156	154 155	rpdivcld	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (N - K + 1 \dots N)) \to \frac{n}{N} \in ℝ^{+}$
157	156	relogcld	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (N - K + 1 \dots N)) \to \log (\frac{n}{N}) \in ℝ$
158	157	recnd	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (N - K + 1 \dots N)) \to \log (\frac{n}{N}) \in ℂ$
159		fvoveq1	$⊢ n = N - k \to \log (\frac{n}{N}) = \log (\frac{N - k}{N})$
160	151 153 151 158 159	fsumrev	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} \log (\frac{n}{N}) = \sum_{k = N - N}^{N - (N - K + 1)} \log (\frac{N - k}{N})$
161	130	subidd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - N = 0$
162		1cnd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to 1 \in ℂ$
163	130 139 162	subsubd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - (K - 1) = N - K + 1$
164	163	oveq2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - (N - (K - 1)) = N - (N - K + 1)$
165		ax-1cn	$⊢ 1 \in ℂ$
166		subcl	$⊢ (K \in ℂ \land 1 \in ℂ) \to K - 1 \in ℂ$
167	139 165 166	sylancl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K - 1 \in ℂ$
168	130 167	nncand	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - (N - (K - 1)) = K - 1$
169	164 168	eqtr3d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - (N - K + 1) = K - 1$
170	161 169	oveq12d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (N - N \dots N - (N - K + 1)) = (0 \dots K - 1)$
171	130	adantr	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land k \in (0 \dots K - 1)) \to N \in ℂ$
172		elfznn0	$⊢ k \in (0 \dots K - 1) \to k \in ℕ_{0}$
173	172	adantl	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land k \in (0 \dots K - 1)) \to k \in ℕ_{0}$
174	173	nn0cnd	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land k \in (0 \dots K - 1)) \to k \in ℂ$
175	132	adantr	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land k \in (0 \dots K - 1)) \to N \neq 0$
176	171 174 171 175	divsubdird	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land k \in (0 \dots K - 1)) \to \frac{N - k}{N} = (\frac{N}{N}) - (\frac{k}{N})$
177	171 175	dividd	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land k \in (0 \dots K - 1)) \to \frac{N}{N} = 1$
178	177	oveq1d	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land k \in (0 \dots K - 1)) \to (\frac{N}{N}) - (\frac{k}{N}) = 1 - (\frac{k}{N})$
179	176 178	eqtrd	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land k \in (0 \dots K - 1)) \to \frac{N - k}{N} = 1 - (\frac{k}{N})$
180	179	fveq2d	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land k \in (0 \dots K - 1)) \to \log (\frac{N - k}{N}) = \log (1 - (\frac{k}{N}))$
181	170 180	sumeq12rdv	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{k = N - N}^{N - (N - K + 1)} \log (\frac{N - k}{N}) = \sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))$
182	160 181	eqtrd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} \log (\frac{n}{N}) = \sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))$
183	143	adantr	$⊢ ((N \in ℕ \land K \in (0 \dots N)) \land n \in (N - K + 1 \dots N)) \to \log N \in ℂ$
184	92 98 183	fsumsub	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} (\log n - \log N) = \sum_{n = N - K + 1}^{N} \log n - \sum_{n = N - K + 1}^{N} \log N$
185		fsumconst	$⊢ ((N - K + 1 \dots N) \in Fin \land \log N \in ℂ) \to \sum_{n = N - K + 1}^{N} \log N = \|(N - K + 1 \dots N)\| \log N$
186	92 143 185	syl2anc	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} \log N = \|(N - K + 1 \dots N)\| \log N$
187		1zzd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to 1 \in ℤ$
188		fzen	$⊢ (1 \in ℤ \land K \in ℤ \land N - K \in ℤ) \to (1 \dots K) \approx (1 + N - K \dots K + N - K)$
189	187 134 152 188	syl3anc	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (1 \dots K) \approx (1 + N - K \dots K + N - K)$
190	25	nn0cnd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to N - K \in ℂ$
191		addcom	$⊢ (1 \in ℂ \land N - K \in ℂ) \to 1 + N - K = N - K + 1$
192	165 190 191	sylancr	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to 1 + N - K = N - K + 1$
193	139 130	pncan3d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to K + N - K = N$
194	192 193	oveq12d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (1 + N - K \dots K + N - K) = (N - K + 1 \dots N)$
195	189 194	breqtrd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to (1 \dots K) \approx (N - K + 1 \dots N)$
196		hasheni	$⊢ (1 \dots K) \approx (N - K + 1 \dots N) \to \|(1 \dots K)\| = \|(N - K + 1 \dots N)\|$
197	195 196	syl	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|(1 \dots K)\| = \|(N - K + 1 \dots N)\|$
198	197 12	eqtr3d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|(N - K + 1 \dots N)\| = K$
199	198	oveq1d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \|(N - K + 1 \dots N)\| \log N = K \log N$
200	186 199	eqtrd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} \log N = K \log N$
201	200	oveq2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} \log n - \sum_{n = N - K + 1}^{N} \log N = \sum_{n = N - K + 1}^{N} \log n - K \log N$
202	184 201	eqtrd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} (\log n - \log N) = \sum_{n = N - K + 1}^{N} \log n - K \log N$
203	150 182 202	3eqtr3rd	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \sum_{n = N - K + 1}^{N} \log n - K \log N = \sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))$
204	203	fveq2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to e^{\sum_{n = N - K + 1}^{N} \log n - K \log N} = e^{\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))}$
205	138 146 204	3eqtr2d	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \frac{\|T\|}{\|S\|} = e^{\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))}$

Metamath Proof Explorer

Theorem birthdaylem2

Proof