"Efficient" is a pretty vague expression. If you are trying to prove $\exists$ or disprove $\forall$ (which are essentially the same thing, as $\exists x\,\phi\equiv\neg\forall x\neg\phi$), then all you need to do is to find a (counter-)example and you are done, assuming that you have reason to believe that one exists. If you are trying to prove $\forall$ or disprove $\exists$ and you believe that they are true, then you are in trouble. Evidently, going through the domain element by element would not go too well, if your domain contains infinitely many elements like the natural numbers.
One can formalize this idea about the proof process in terms of recursion theory. The search for a (counter-)example is a process which will definitely yield an answer eventually if the answer is "yes, one exists", and which will keep on running forever if the answer is "no." This differs from what is probably your notion of "efficiency", which would be a process that stops no matter what and give us a "yes/no" result. This makes the problem computable. Therefore, in your problem, to determine whether a number divides another is computable. (We might have to search for some $z$ such that $zx=y$, but this search is bounded above by $y$, so our computation will still reliably end.)
To determine whether all natural numbers satisfy some (computable) requirement, such as being divisible by $1$, is a more difficult problem, assuming that we don't just appeal to the metatheory and prove up there that $1$ divides everything (which would have been easy, as the other answer demonstrates). If we are really determined to go through all natural numbers to test this hypothesis, then this gives us a process that does not end if and only if the hypothesis is correct. (If we are right and everything is divisible by $1$, then the process will dutifully test every natural number and never stop; if we are wrong, then something is not divisible by $1$ and the process will end as soon as it gets there.) This type of process is called co-recursively enumerable (co-RE), or $\Pi^0_1$. The natural dual is when we try to determine whether there exists a natural number satisfying some computable requirement. Then the process stops if we are correct and runs forever if we are wrong. That would give us a recursively enumerable (RE), or $\Sigma^0_1$ process.
As you may guess, we can take this definition further and build a whole hierarchy of classification; if we want to show $\forall x\,\exists y\,\phi$ where $\phi$ is computable, then without appealing to the metatheory we must do this: take a $x$, go through all $y$'s and see if one of them works, then move on to the next $x$ and go through all $y$'s... As you can see, this would have been a $\Pi^0_1$ process if you had some magic machine that will take care of the $\Sigma^0_1$ process for you. In this case, you have a $\Pi^0_2$ process. Similarly, one can define the kind of demonstration required for $\exists x\,\forall y\,\phi$ to be $\Sigma^0_2$, et cetera. This gives you what is called the "Arithmetic Hierarchy". The arithmetic hierarchy, in a precise sence, "quantifies" what you call here "difficulty"; the higher up you are in the hierarchy, the more difficult you are to run in the sense of more magic machines being needed to take care of the lower level processes. So, in this notion, your intuition that "proving universal quantification seems difficult (than proving a bounded quantification or unquantified formula)" is made precise in the sense that the former is co-RE while the latter is computable.