Theorem flt4

Description: Fermat's last theorem for the exponent four. (Contributed by AV, 15-Sep-2026)

	Ref	Expression
Hypotheses	flt4.a	$$⊢\phi \to A\in \mathbb{N}$$
	flt4.b	$$⊢\phi \to B\in \mathbb{N}$$
	flt4.c	$$⊢\phi \to C\in \mathbb{N}$$
Assertion	flt4	$$⊢\phi \to A^4+B^4\ne C^4$$

Proof

Step	Hyp	Ref	Expression
1		flt4.a	$$⊢\phi \to A\in \mathbb{N}$$
2		flt4.b	$$⊢\phi \to B\in \mathbb{N}$$
3		flt4.c	$$⊢\phi \to C\in \mathbb{N}$$
4	3	nnsqcld	$$⊢\phi \to C^2\in \mathbb{N}$$
5	1 2 4	nna4b4nsq	$$⊢\phi \to A^4+B^4\ne {\left(C^2\right)}^2$$
6	3	nncnd	$$⊢\phi \to C\in ℂ$$
7	6	exp4sqsq	$$⊢\phi \to C^4={\left(C^2\right)}^2$$
8	5 7	neeqtrrd	$$⊢\phi \to A^4+B^4\ne C^4$$