F(n) = { a/b | aとbは互いに素、0 < a < b、n/bの小数部分が1/2以上 }
= { a/b | aとbは互いに素、0 < a < b、(n%b)/b ≥ 1/2 }
とおくわ。|F(n)|を知りたいの。
注意なんだけど、F(n)の要素として既約分数とそうでないものの区別はないわ。
たとえば 1/2 ∈ F(1) だから 3/6 ∈ F(1) でもあるの。
X∖Yで {x ∈ X | x ∉ Y} を表すわ。そしてbがnを割り切ることを b|n で表すわね。
補題１
F(n)∖F(n+1) = { i/(n+1) | 1≤ i ≤ n }. したがって |F(n)∖F(n+1)| = n.
証明
既約分数 a/b がF(n)∖F(n+1)の要素とするわ。
これは (n%b)/b ≥ 1/2 でありかつ ((n+1)%b)/b ≱ 1/2ということね。
(n+1)%b は (n%b)+1 か 0 のどちらかに等しいから、これは (n+1)%b = 0 を意味するわ。
つまり b|(n+1) だから、1≤ i ≤ nを満たすあるiに対して a/b = i/(n+1) となるわ。
逆に 1≤ i ≤ n ならば、ある既約分数 a/b があって i/(n+1) = a/b になるけど
すると b|(n+1) だから ((n+1)%b)/b = 0/b = 0 ≱ 1/2 なので a/b ∉ F(n+1) ね。
b|(n+1) だから n%b = b-1 となるわ。b > a > 0 だから b ≥ 2 なので
(n%b)/b = (b-1)/b = 1 - 1/b ≥ 1/2 だから a/b ∈ F(n) ね。
以上から i/(n+1) = a/b ∈ F(n)∖F(n+1) となるわ。QED