birthdaylem3

Description: For general N and K , upper-bound the fraction of injective functions from 1 ... K to 1 ... N . (Contributed by Mario Carneiro, 17-Apr-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	birthdaylem3	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to \frac{\|T\|}{\|S\|} \leq e^{- \frac{\frac{K^{2} - K}{2}}{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		abn0	$⊢ \{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\} \neq \emptyset \leftrightarrow \exists f f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)$
4		ovex	$⊢ (1 \dots N) \in V$
5	4	brdom	$⊢ (1 \dots K) ≼ (1 \dots N) \leftrightarrow \exists f f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)$
6	3 5	bitr4i	$⊢ \{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\} \neq \emptyset \leftrightarrow (1 \dots K) ≼ (1 \dots N)$
7		hashfz1	$⊢ K \in ℕ_{0} \to \|(1 \dots K)\| = K$
8		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
9		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
10	8 9	syl	$⊢ N \in ℕ \to \|(1 \dots N)\| = N$
11	7 10	breqan12d	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to (\|(1 \dots K)\| \leq \|(1 \dots N)\| \leftrightarrow K \leq N)$
12		fzfid	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to (1 \dots K) \in Fin$
13		fzfid	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to (1 \dots N) \in Fin$
14		hashdom	$⊢ ((1 \dots K) \in Fin \land (1 \dots N) \in Fin) \to (\|(1 \dots K)\| \leq \|(1 \dots N)\| \leftrightarrow (1 \dots K) ≼ (1 \dots N))$
15	12 13 14	syl2anc	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to (\|(1 \dots K)\| \leq \|(1 \dots N)\| \leftrightarrow (1 \dots K) ≼ (1 \dots N))$
16		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
17		nnre	$⊢ N \in ℕ \to N \in ℝ$
18		lenlt	$⊢ (K \in ℝ \land N \in ℝ) \to (K \leq N \leftrightarrow \neg N < K)$
19	16 17 18	syl2an	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to (K \leq N \leftrightarrow \neg N < K)$
20	11 15 19	3bitr3d	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to ((1 \dots K) ≼ (1 \dots N) \leftrightarrow \neg N < K)$
21	6 20	bitrid	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to (\{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\} \neq \emptyset \leftrightarrow \neg N < K)$
22	21	necon4abid	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to (\{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\} = \emptyset \leftrightarrow N < K)$
23	22	biimpar	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to \{f \| f : (1 \dots K) \underset{1-1}{⟶} (1 \dots N)\} = \emptyset$
24	2 23	eqtrid	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to T = \emptyset$
25	24	fveq2d	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to \|T\| = \|\emptyset\|$
26		hash0	$⊢ \|\emptyset\| = 0$
27	25 26	eqtrdi	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to \|T\| = 0$
28	27	oveq1d	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to \frac{\|T\|}{\|S\|} = \frac{0}{\|S\|}$
29	1 2	birthdaylem1	$⊢ (T \subseteq S \land S \in Fin \land (N \in ℕ \to S \neq \emptyset))$
30	29	simp3i	$⊢ N \in ℕ \to S \neq \emptyset$
31	30	ad2antlr	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to S \neq \emptyset$
32	29	simp2i	$⊢ S \in Fin$
33		hashnncl	$⊢ S \in Fin \to (\|S\| \in ℕ \leftrightarrow S \neq \emptyset)$
34	32 33	ax-mp	$⊢ \|S\| \in ℕ \leftrightarrow S \neq \emptyset$
35	31 34	sylibr	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to \|S\| \in ℕ$
36	35	nncnd	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to \|S\| \in ℂ$
37	35	nnne0d	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to \|S\| \neq 0$
38	36 37	div0d	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to \frac{0}{\|S\|} = 0$
39	28 38	eqtrd	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to \frac{\|T\|}{\|S\|} = 0$
40	16	adantr	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to K \in ℝ$
41	40	resqcld	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to K^{2} \in ℝ$
42	41 40	resubcld	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to K^{2} - K \in ℝ$
43	42	rehalfcld	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to \frac{K^{2} - K}{2} \in ℝ$
44		nndivre	$⊢ (\frac{K^{2} - K}{2} \in ℝ \land N \in ℕ) \to \frac{\frac{K^{2} - K}{2}}{N} \in ℝ$
45	43 44	sylancom	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to \frac{\frac{K^{2} - K}{2}}{N} \in ℝ$
46	45	renegcld	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to - \frac{\frac{K^{2} - K}{2}}{N} \in ℝ$
47	46	adantr	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to - \frac{\frac{K^{2} - K}{2}}{N} \in ℝ$
48	47	rpefcld	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to e^{- \frac{\frac{K^{2} - K}{2}}{N}} \in ℝ^{+}$
49	48	rpge0d	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to 0 \leq e^{- \frac{\frac{K^{2} - K}{2}}{N}}$
50	39 49	eqbrtrd	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land N < K) \to \frac{\|T\|}{\|S\|} \leq e^{- \frac{\frac{K^{2} - K}{2}}{N}}$
51		simplr	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to N \in ℕ$
52		simpr	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to K \leq N$
53		simpll	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to K \in ℕ_{0}$
54		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
55	53 54	eleqtrdi	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to K \in ℤ_{\geq 0}$
56		nnz	$⊢ N \in ℕ \to N \in ℤ$
57	56	ad2antlr	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to N \in ℤ$
58		elfz5	$⊢ (K \in ℤ_{\geq 0} \land N \in ℤ) \to (K \in (0 \dots N) \leftrightarrow K \leq N)$
59	55 57 58	syl2anc	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to (K \in (0 \dots N) \leftrightarrow K \leq N)$
60	52 59	mpbird	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to K \in (0 \dots N)$
61	1 2	birthdaylem2	$⊢ (N \in ℕ \land K \in (0 \dots N)) \to \frac{\|T\|}{\|S\|} = e^{\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))}$
62	51 60 61	syl2anc	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \frac{\|T\|}{\|S\|} = e^{\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))}$
63		fzfid	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to (0 \dots K - 1) \in Fin$
64		elfznn0	$⊢ k \in (0 \dots K - 1) \to k \in ℕ_{0}$
65	64	adantl	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to k \in ℕ_{0}$
66	65	nn0red	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to k \in ℝ$
67	53	nn0red	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to K \in ℝ$
68		peano2rem	$⊢ K \in ℝ \to K - 1 \in ℝ$
69	67 68	syl	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to K - 1 \in ℝ$
70	69	adantr	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to K - 1 \in ℝ$
71	51	adantr	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to N \in ℕ$
72	71	nnred	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to N \in ℝ$
73		elfzle2	$⊢ k \in (0 \dots K - 1) \to k \leq K - 1$
74	73	adantl	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to k \leq K - 1$
75	51	nnred	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to N \in ℝ$
76	67	ltm1d	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to K - 1 < K$
77	69 67 75 76 52	ltletrd	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to K - 1 < N$
78	77	adantr	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to K - 1 < N$
79	66 70 72 74 78	lelttrd	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to k < N$
80	71	nncnd	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to N \in ℂ$
81	80	mulridd	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to N \cdot 1 = N$
82	79 81	breqtrrd	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to k < N \cdot 1$
83		1red	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to 1 \in ℝ$
84	71	nngt0d	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to 0 < N$
85		ltdivmul	$⊢ (k \in ℝ \land 1 \in ℝ \land (N \in ℝ \land 0 < N)) \to (\frac{k}{N} < 1 \leftrightarrow k < N \cdot 1)$
86	66 83 72 84 85	syl112anc	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to (\frac{k}{N} < 1 \leftrightarrow k < N \cdot 1)$
87	82 86	mpbird	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to \frac{k}{N} < 1$
88	66 71	nndivred	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to \frac{k}{N} \in ℝ$
89		1re	$⊢ 1 \in ℝ$
90		difrp	$⊢ (\frac{k}{N} \in ℝ \land 1 \in ℝ) \to (\frac{k}{N} < 1 \leftrightarrow 1 - (\frac{k}{N}) \in ℝ^{+})$
91	88 89 90	sylancl	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to (\frac{k}{N} < 1 \leftrightarrow 1 - (\frac{k}{N}) \in ℝ^{+})$
92	87 91	mpbid	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to 1 - (\frac{k}{N}) \in ℝ^{+}$
93	92	relogcld	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to \log (1 - (\frac{k}{N})) \in ℝ$
94	88	renegcld	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to - \frac{k}{N} \in ℝ$
95		elfzle1	$⊢ k \in (0 \dots K - 1) \to 0 \leq k$
96	95	adantl	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to 0 \leq k$
97		divge0	$⊢ ((k \in ℝ \land 0 \leq k) \land (N \in ℝ \land 0 < N)) \to 0 \leq \frac{k}{N}$
98	66 96 72 84 97	syl22anc	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to 0 \leq \frac{k}{N}$
99	88 98 87	eflegeo	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to e^{\frac{k}{N}} \leq \frac{1}{1 - (\frac{k}{N})}$
100	88	reefcld	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to e^{\frac{k}{N}} \in ℝ$
101		efgt0	$⊢ \frac{k}{N} \in ℝ \to 0 < e^{\frac{k}{N}}$
102	88 101	syl	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to 0 < e^{\frac{k}{N}}$
103	92	rpregt0d	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to (1 - (\frac{k}{N}) \in ℝ \land 0 < 1 - (\frac{k}{N}))$
104		lerec2	$⊢ ((e^{\frac{k}{N}} \in ℝ \land 0 < e^{\frac{k}{N}}) \land (1 - (\frac{k}{N}) \in ℝ \land 0 < 1 - (\frac{k}{N}))) \to (e^{\frac{k}{N}} \leq \frac{1}{1 - (\frac{k}{N})} \leftrightarrow 1 - (\frac{k}{N}) \leq \frac{1}{e^{\frac{k}{N}}})$
105	100 102 103 104	syl21anc	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to (e^{\frac{k}{N}} \leq \frac{1}{1 - (\frac{k}{N})} \leftrightarrow 1 - (\frac{k}{N}) \leq \frac{1}{e^{\frac{k}{N}}})$
106	99 105	mpbid	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to 1 - (\frac{k}{N}) \leq \frac{1}{e^{\frac{k}{N}}}$
107	92	reeflogd	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to e^{\log (1 - (\frac{k}{N}))} = 1 - (\frac{k}{N})$
108	88	recnd	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to \frac{k}{N} \in ℂ$
109		efneg	$⊢ \frac{k}{N} \in ℂ \to e^{- \frac{k}{N}} = \frac{1}{e^{\frac{k}{N}}}$
110	108 109	syl	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to e^{- \frac{k}{N}} = \frac{1}{e^{\frac{k}{N}}}$
111	106 107 110	3brtr4d	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to e^{\log (1 - (\frac{k}{N}))} \leq e^{- \frac{k}{N}}$
112		efle	$⊢ (\log (1 - (\frac{k}{N})) \in ℝ \land - \frac{k}{N} \in ℝ) \to (\log (1 - (\frac{k}{N})) \leq - \frac{k}{N} \leftrightarrow e^{\log (1 - (\frac{k}{N}))} \leq e^{- \frac{k}{N}})$
113	93 94 112	syl2anc	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to (\log (1 - (\frac{k}{N})) \leq - \frac{k}{N} \leftrightarrow e^{\log (1 - (\frac{k}{N}))} \leq e^{- \frac{k}{N}})$
114	111 113	mpbird	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to \log (1 - (\frac{k}{N})) \leq - \frac{k}{N}$
115	63 93 94 114	fsumle	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N})) \leq \sum_{k = 0}^{K - 1} (- \frac{k}{N})$
116	63 108	fsumneg	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \sum_{k = 0}^{K - 1} (- \frac{k}{N}) = - \sum_{k = 0}^{K - 1} (\frac{k}{N})$
117	51	nncnd	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to N \in ℂ$
118	66	recnd	$⊢ (((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \land k \in (0 \dots K - 1)) \to k \in ℂ$
119		nnne0	$⊢ N \in ℕ \to N \neq 0$
120	119	ad2antlr	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to N \neq 0$
121	63 117 118 120	fsumdivc	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \frac{\sum_{k = 0}^{K - 1} k}{N} = \sum_{k = 0}^{K - 1} (\frac{k}{N})$
122		arisum2	$⊢ K \in ℕ_{0} \to \sum_{k = 0}^{K - 1} k = \frac{K^{2} - K}{2}$
123	53 122	syl	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \sum_{k = 0}^{K - 1} k = \frac{K^{2} - K}{2}$
124	123	oveq1d	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \frac{\sum_{k = 0}^{K - 1} k}{N} = \frac{\frac{K^{2} - K}{2}}{N}$
125	121 124	eqtr3d	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \sum_{k = 0}^{K - 1} (\frac{k}{N}) = \frac{\frac{K^{2} - K}{2}}{N}$
126	125	negeqd	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to - \sum_{k = 0}^{K - 1} (\frac{k}{N}) = - \frac{\frac{K^{2} - K}{2}}{N}$
127	116 126	eqtrd	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \sum_{k = 0}^{K - 1} (- \frac{k}{N}) = - \frac{\frac{K^{2} - K}{2}}{N}$
128	115 127	breqtrd	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N})) \leq - \frac{\frac{K^{2} - K}{2}}{N}$
129	63 93	fsumrecl	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N})) \in ℝ$
130	46	adantr	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to - \frac{\frac{K^{2} - K}{2}}{N} \in ℝ$
131		efle	$⊢ (\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N})) \in ℝ \land - \frac{\frac{K^{2} - K}{2}}{N} \in ℝ) \to (\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N})) \leq - \frac{\frac{K^{2} - K}{2}}{N} \leftrightarrow e^{\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))} \leq e^{- \frac{\frac{K^{2} - K}{2}}{N}})$
132	129 130 131	syl2anc	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to (\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N})) \leq - \frac{\frac{K^{2} - K}{2}}{N} \leftrightarrow e^{\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))} \leq e^{- \frac{\frac{K^{2} - K}{2}}{N}})$
133	128 132	mpbid	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to e^{\sum_{k = 0}^{K - 1} \log (1 - (\frac{k}{N}))} \leq e^{- \frac{\frac{K^{2} - K}{2}}{N}}$
134	62 133	eqbrtrd	$⊢ ((K \in ℕ_{0} \land N \in ℕ) \land K \leq N) \to \frac{\|T\|}{\|S\|} \leq e^{- \frac{\frac{K^{2} - K}{2}}{N}}$
135	17	adantl	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to N \in ℝ$
136	50 134 135 40	ltlecasei	$⊢ (K \in ℕ_{0} \land N \in ℕ) \to \frac{\|T\|}{\|S\|} \leq e^{- \frac{\frac{K^{2} - K}{2}}{N}}$

Metamath Proof Explorer

Theorem birthdaylem3

Proof