True ↔ Erdos1146.IsEssentialComponent {k | ∃ m n, k = 2 ^ m * 3 ^ n}