It is not directly proved, but simply stated in Grover's 1996 paper that his result was optimal.
It was established in [BBBV96] that any quantum algorithm can not identify a single marked element in fewer than (). Grover's algorithm takes O() iterations, and is thus asymptotically optimal.
It has been shown since that any quantum algorithm would require at least /4 queries, which is precisely the number queries required by Grover's algorithm. [Grover99]