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 ⊢ 𝑆 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) }
birthday.t ⊢ 𝑇 = { 𝑓 ∣ 𝑓 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) }
Assertion birthdaylem3 ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( ( ♯ ‘ 𝑇 ) / ( ♯ ‘ 𝑆 ) ) ≤ ( exp ‘ - ( ( ( ( 𝐾 ↑ 2 ) − 𝐾 ) / 2 ) / 𝑁 ) ) )

Proof

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