Mice with Finitely Many Woodin Cardinals from Optimal Determinacy Hypotheses

We prove the following result which is due to the third author. Let n ≥ 1. If Πn1 determinacy and Πn+11 determinacy both hold true and there is no Σn+21-definable ω1-sequence of pairwise distinct r...