It is known that Fermat's last theorem can be proven in finite-order arithmetic (e.g. accoridng to this site). This is still an extremely high upper bound on proof complexity (for example, compared to Friedman's conjecture that it's provable in EFA).
I've been wondering, are there any (nontrivial) lower bounds for such possible proof? For example, is it possibly known if FLT is independent of $I\Delta_0$ theory?
Thanks in advance.