Metamath Proof Explorer

Theorem 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 ... K ) --> ( 1 ... N ) }
birthday.t 
|- T = { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) }
Assertion birthdaylem3 
|- ( ( K e. NN0 /\ N e. NN ) -> ( ( # ` T ) / ( # ` S ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) )

Proof

Step Hyp Ref Expression
1 birthday.s 
 |-  S = { f | f : ( 1 ... K ) --> ( 1 ... N ) }
2 birthday.t 
 |-  T = { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) }
3 abn0 
 |-  ( { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) } =/= (/) <-> E. f f : ( 1 ... K ) -1-1-> ( 1 ... N ) )
4 ovex 
 |-  ( 1 ... N ) e. _V
5 4 brdom 
 |-  ( ( 1 ... K ) ~<_ ( 1 ... N ) <-> E. f f : ( 1 ... K ) -1-1-> ( 1 ... N ) )
6 3 5 bitr4i 
 |-  ( { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) } =/= (/) <-> ( 1 ... K ) ~<_ ( 1 ... N ) )
7 hashfz1 
 |-  ( K e. NN0 -> ( # ` ( 1 ... K ) ) = K )
8 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
9 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
10 8 9 syl 
 |-  ( N e. NN -> ( # ` ( 1 ... N ) ) = N )
11 7 10 breqan12d 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( # ` ( 1 ... K ) ) <_ ( # ` ( 1 ... N ) ) <-> K <_ N ) )
12 fzfid 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( 1 ... K ) e. Fin )
13 fzfid 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( 1 ... N ) e. Fin )
14 hashdom 
 |-  ( ( ( 1 ... K ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( # ` ( 1 ... K ) ) <_ ( # ` ( 1 ... N ) ) <-> ( 1 ... K ) ~<_ ( 1 ... N ) ) )
15 12 13 14 syl2anc 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( # ` ( 1 ... K ) ) <_ ( # ` ( 1 ... N ) ) <-> ( 1 ... K ) ~<_ ( 1 ... N ) ) )
16 nn0re 
 |-  ( K e. NN0 -> K e. RR )
17 nnre 
 |-  ( N e. NN -> N e. RR )
18 lenlt 
 |-  ( ( K e. RR /\ N e. RR ) -> ( K <_ N <-> -. N < K ) )
19 16 17 18 syl2an 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( K <_ N <-> -. N < K ) )
20 11 15 19 3bitr3d 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( 1 ... K ) ~<_ ( 1 ... N ) <-> -. N < K ) )
21 6 20 syl5bb 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) } =/= (/) <-> -. N < K ) )
22 21 necon4abid 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) } = (/) <-> N < K ) )
23 22 biimpar 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) } = (/) )
24 2 23 syl5eq 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> T = (/) )
25 24 fveq2d 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> ( # ` T ) = ( # ` (/) ) )
26 hash0 
 |-  ( # ` (/) ) = 0
27 25 26 eqtrdi 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> ( # ` T ) = 0 )
28 27 oveq1d 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> ( ( # ` T ) / ( # ` S ) ) = ( 0 / ( # ` S ) ) )
29 1 2 birthdaylem1 
 |-  ( T C_ S /\ S e. Fin /\ ( N e. NN -> S =/= (/) ) )
30 29 simp3i 
 |-  ( N e. NN -> S =/= (/) )
31 30 ad2antlr 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> S =/= (/) )
32 29 simp2i 
 |-  S e. Fin
33 hashnncl 
 |-  ( S e. Fin -> ( ( # ` S ) e. NN <-> S =/= (/) ) )
34 32 33 ax-mp 
 |-  ( ( # ` S ) e. NN <-> S =/= (/) )
35 31 34 sylibr 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> ( # ` S ) e. NN )
36 35 nncnd 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> ( # ` S ) e. CC )
37 35 nnne0d 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> ( # ` S ) =/= 0 )
38 36 37 div0d 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> ( 0 / ( # ` S ) ) = 0 )
39 28 38 eqtrd 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> ( ( # ` T ) / ( # ` S ) ) = 0 )
40 16 adantr 
 |-  ( ( K e. NN0 /\ N e. NN ) -> K e. RR )
41 40 resqcld 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( K ^ 2 ) e. RR )
42 41 40 resubcld 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( K ^ 2 ) - K ) e. RR )
43 42 rehalfcld 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( ( K ^ 2 ) - K ) / 2 ) e. RR )
44 nndivre 
 |-  ( ( ( ( ( K ^ 2 ) - K ) / 2 ) e. RR /\ N e. NN ) -> ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR )
45 43 44 sylancom 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR )
46 45 renegcld 
 |-  ( ( K e. NN0 /\ N e. NN ) -> -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR )
47 46 adantr 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR )
48 47 rpefcld 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) e. RR+ )
49 48 rpge0d 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> 0 <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) )
50 39 49 eqbrtrd 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ N < K ) -> ( ( # ` T ) / ( # ` S ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) )
51 simplr 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> N e. NN )
52 simpr 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> K <_ N )
53 simpll 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> K e. NN0 )
54 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
55 53 54 eleqtrdi 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> K e. ( ZZ>= ` 0 ) )
56 nnz 
 |-  ( N e. NN -> N e. ZZ )
57 56 ad2antlr 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> N e. ZZ )
58 elfz5 
 |-  ( ( K e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( K e. ( 0 ... N ) <-> K <_ N ) )
59 55 57 58 syl2anc 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( K e. ( 0 ... N ) <-> K <_ N ) )
60 52 59 mpbird 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> K e. ( 0 ... N ) )
61 1 2 birthdaylem2 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) ) -> ( ( # ` T ) / ( # ` S ) ) = ( exp ` sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) ) )
62 51 60 61 syl2anc 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( ( # ` T ) / ( # ` S ) ) = ( exp ` sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) ) )
63 fzfid 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( 0 ... ( K - 1 ) ) e. Fin )
64 elfznn0 
 |-  ( k e. ( 0 ... ( K - 1 ) ) -> k e. NN0 )
65 64 adantl 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> k e. NN0 )
66 65 nn0red 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> k e. RR )
67 53 nn0red 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> K e. RR )
68 peano2rem 
 |-  ( K e. RR -> ( K - 1 ) e. RR )
69 67 68 syl 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( K - 1 ) e. RR )
70 69 adantr 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( K - 1 ) e. RR )
71 51 adantr 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> N e. NN )
72 71 nnred 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> N e. RR )
73 elfzle2 
 |-  ( k e. ( 0 ... ( K - 1 ) ) -> k <_ ( K - 1 ) )
74 73 adantl 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> k <_ ( K - 1 ) )
75 51 nnred 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> N e. RR )
76 67 ltm1d 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( K - 1 ) < K )
77 69 67 75 76 52 ltletrd 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( K - 1 ) < N )
78 77 adantr 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( K - 1 ) < N )
79 66 70 72 74 78 lelttrd 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> k < N )
80 71 nncnd 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> N e. CC )
81 80 mulid1d 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( N x. 1 ) = N )
82 79 81 breqtrrd 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> k < ( N x. 1 ) )
83 1red 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> 1 e. RR )
84 71 nngt0d 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> 0 < N )
85 ltdivmul 
 |-  ( ( k e. RR /\ 1 e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( k / N ) < 1 <-> k < ( N x. 1 ) ) )
86 66 83 72 84 85 syl112anc 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( ( k / N ) < 1 <-> k < ( N x. 1 ) ) )
87 82 86 mpbird 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( k / N ) < 1 )
88 66 71 nndivred 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( k / N ) e. RR )
89 1re 
 |-  1 e. RR
90 difrp 
 |-  ( ( ( k / N ) e. RR /\ 1 e. RR ) -> ( ( k / N ) < 1 <-> ( 1 - ( k / N ) ) e. RR+ ) )
91 88 89 90 sylancl 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( ( k / N ) < 1 <-> ( 1 - ( k / N ) ) e. RR+ ) )
92 87 91 mpbid 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( 1 - ( k / N ) ) e. RR+ )
93 92 relogcld 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( log ` ( 1 - ( k / N ) ) ) e. RR )
94 88 renegcld 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> -u ( k / N ) e. RR )
95 elfzle1 
 |-  ( k e. ( 0 ... ( K - 1 ) ) -> 0 <_ k )
96 95 adantl 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> 0 <_ k )
97 divge0 
 |-  ( ( ( k e. RR /\ 0 <_ k ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( k / N ) )
98 66 96 72 84 97 syl22anc 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> 0 <_ ( k / N ) )
99 88 98 87 eflegeo 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( exp ` ( k / N ) ) <_ ( 1 / ( 1 - ( k / N ) ) ) )
100 88 reefcld 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( exp ` ( k / N ) ) e. RR )
101 efgt0 
 |-  ( ( k / N ) e. RR -> 0 < ( exp ` ( k / N ) ) )
102 88 101 syl 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> 0 < ( exp ` ( k / N ) ) )
103 92 rpregt0d 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( ( 1 - ( k / N ) ) e. RR /\ 0 < ( 1 - ( k / N ) ) ) )
104 lerec2 
 |-  ( ( ( ( exp ` ( k / N ) ) e. RR /\ 0 < ( exp ` ( k / N ) ) ) /\ ( ( 1 - ( k / N ) ) e. RR /\ 0 < ( 1 - ( k / N ) ) ) ) -> ( ( exp ` ( k / N ) ) <_ ( 1 / ( 1 - ( k / N ) ) ) <-> ( 1 - ( k / N ) ) <_ ( 1 / ( exp ` ( k / N ) ) ) ) )
105 100 102 103 104 syl21anc 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( ( exp ` ( k / N ) ) <_ ( 1 / ( 1 - ( k / N ) ) ) <-> ( 1 - ( k / N ) ) <_ ( 1 / ( exp ` ( k / N ) ) ) ) )
106 99 105 mpbid 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( 1 - ( k / N ) ) <_ ( 1 / ( exp ` ( k / N ) ) ) )
107 92 reeflogd 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( exp ` ( log ` ( 1 - ( k / N ) ) ) ) = ( 1 - ( k / N ) ) )
108 88 recnd 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( k / N ) e. CC )
109 efneg 
 |-  ( ( k / N ) e. CC -> ( exp ` -u ( k / N ) ) = ( 1 / ( exp ` ( k / N ) ) ) )
110 108 109 syl 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( exp ` -u ( k / N ) ) = ( 1 / ( exp ` ( k / N ) ) ) )
111 106 107 110 3brtr4d 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( exp ` ( log ` ( 1 - ( k / N ) ) ) ) <_ ( exp ` -u ( k / N ) ) )
112 efle 
 |-  ( ( ( log ` ( 1 - ( k / N ) ) ) e. RR /\ -u ( k / N ) e. RR ) -> ( ( log ` ( 1 - ( k / N ) ) ) <_ -u ( k / N ) <-> ( exp ` ( log ` ( 1 - ( k / N ) ) ) ) <_ ( exp ` -u ( k / N ) ) ) )
113 93 94 112 syl2anc 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( ( log ` ( 1 - ( k / N ) ) ) <_ -u ( k / N ) <-> ( exp ` ( log ` ( 1 - ( k / N ) ) ) ) <_ ( exp ` -u ( k / N ) ) ) )
114 111 113 mpbird 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( log ` ( 1 - ( k / N ) ) ) <_ -u ( k / N ) )
115 63 93 94 114 fsumle 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) <_ sum_ k e. ( 0 ... ( K - 1 ) ) -u ( k / N ) )
116 63 108 fsumneg 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> sum_ k e. ( 0 ... ( K - 1 ) ) -u ( k / N ) = -u sum_ k e. ( 0 ... ( K - 1 ) ) ( k / N ) )
117 51 nncnd 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> N e. CC )
118 66 recnd 
 |-  ( ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> k e. CC )
119 nnne0 
 |-  ( N e. NN -> N =/= 0 )
120 119 ad2antlr 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> N =/= 0 )
121 63 117 118 120 fsumdivc 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( sum_ k e. ( 0 ... ( K - 1 ) ) k / N ) = sum_ k e. ( 0 ... ( K - 1 ) ) ( k / N ) )
122 arisum2 
 |-  ( K e. NN0 -> sum_ k e. ( 0 ... ( K - 1 ) ) k = ( ( ( K ^ 2 ) - K ) / 2 ) )
123 53 122 syl 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> sum_ k e. ( 0 ... ( K - 1 ) ) k = ( ( ( K ^ 2 ) - K ) / 2 ) )
124 123 oveq1d 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( sum_ k e. ( 0 ... ( K - 1 ) ) k / N ) = ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) )
125 121 124 eqtr3d 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> sum_ k e. ( 0 ... ( K - 1 ) ) ( k / N ) = ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) )
126 125 negeqd 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> -u sum_ k e. ( 0 ... ( K - 1 ) ) ( k / N ) = -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) )
127 116 126 eqtrd 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> sum_ k e. ( 0 ... ( K - 1 ) ) -u ( k / N ) = -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) )
128 115 127 breqtrd 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) <_ -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) )
129 63 93 fsumrecl 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) e. RR )
130 46 adantr 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR )
131 efle 
 |-  ( ( sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) e. RR /\ -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) e. RR ) -> ( sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) <_ -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) <-> ( exp ` sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) ) )
132 129 130 131 syl2anc 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) <_ -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) <-> ( exp ` sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) ) )
133 128 132 mpbid 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( exp ` sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) )
134 62 133 eqbrtrd 
 |-  ( ( ( K e. NN0 /\ N e. NN ) /\ K <_ N ) -> ( ( # ` T ) / ( # ` S ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) )
135 17 adantl 
 |-  ( ( K e. NN0 /\ N e. NN ) -> N e. RR )
136 50 134 135 40 ltlecasei 
 |-  ( ( K e. NN0 /\ N e. NN ) -> ( ( # ` T ) / ( # ` S ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) )