Theorem flt4ALT

Description: Fermat's last theorem for the exponent four, derived from Fermat's right triangle theorem (which is not proved yet, see fermrtt: after a proof is available, the hypothesis flt4ALT.r can be removed - TODO-AV). (Contributed by AV, 15-Sep-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	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}$$
	flt4ALT.r	$$⊢\phi \to \forall a\in \mathbb{N}\forall b\in \mathbb{N}\forall c\in \mathbb{N}{a}^4-b^4\ne c^2$$
Assertion	flt4ALT	$$⊢\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		flt4ALT.r	$$⊢\phi \to \forall a\in \mathbb{N}\forall b\in \mathbb{N}\forall c\in \mathbb{N}{a}^4-b^4\ne c^2$$
5	1	nnsqcld	$$⊢\phi \to A^2\in \mathbb{N}$$
6	3 2 5	3jca	$$⊢\phi \to \left(C\in \mathbb{N}\wedge B\in \mathbb{N}\wedge A^2\in \mathbb{N}\right)$$
7		oveq1	$$⊢a=C\to a^4=C^4$$
8	7	oveq1d	$$⊢a=C\to a^4-b^4=C^4-b^4$$
9	8	neeq1d	$$⊢a=C\to \left(a^4-b^4\ne c^2\leftrightarrow C^4-b^4\ne c^2\right)$$
10		oveq1	$$⊢b=B\to b^4=B^4$$
11	10	oveq2d	$$⊢b=B\to C^4-b^4=C^4-B^4$$
12	11	neeq1d	$$⊢b=B\to \left(C^4-b^4\ne c^2\leftrightarrow C^4-B^4\ne c^2\right)$$
13		oveq1	$$⊢c=A^2\to c^2={\left(A^2\right)}^2$$
14	13	neeq2d	$$⊢c=A^2\to \left(C^4-B^4\ne c^2\leftrightarrow C^4-B^4\ne {\left(A^2\right)}^2\right)$$
15	9 12 14	rspc3v	$$⊢\left(C\in \mathbb{N}\wedge B\in \mathbb{N}\wedge A^2\in \mathbb{N}\right)\to \left(\forall a\in \mathbb{N}\forall b\in \mathbb{N}\forall c\in \mathbb{N}{a}^4-b^4\ne c^2\to C^4-B^4\ne {\left(A^2\right)}^2\right)$$
16	6 4 15	sylc	$$⊢\phi \to C^4-B^4\ne {\left(A^2\right)}^2$$
17	16	neneqd	$$⊢\phi \to \neg C^4-B^4={\left(A^2\right)}^2$$
18		4nn0	$$⊢4\in {\mathbb{N}}_0$$
19	18	a1i	$$⊢\phi \to 4\in {\mathbb{N}}_0$$
20	3 19	nnexpcld	$$⊢\phi \to C^4\in \mathbb{N}$$
21	20	nncnd	$$⊢\phi \to C^4\in ℂ$$
22	2 19	nnexpcld	$$⊢\phi \to B^4\in \mathbb{N}$$
23	22	nncnd	$$⊢\phi \to B^4\in ℂ$$
24	1 19	nnexpcld	$$⊢\phi \to A^4\in \mathbb{N}$$
25	24	nncnd	$$⊢\phi \to A^4\in ℂ$$
26	21 23 25	subadd2d	$$⊢\phi \to \left(C^4-B^4=A^4\leftrightarrow A^4+B^4=C^4\right)$$
27	1	nncnd	$$⊢\phi \to A\in ℂ$$
28	27	exp4sqsq	$$⊢\phi \to A^4={\left(A^2\right)}^2$$
29	28	eqeq2d	$$⊢\phi \to \left(C^4-B^4=A^4\leftrightarrow C^4-B^4={\left(A^2\right)}^2\right)$$
30	26 29	bitr3d	$$⊢\phi \to \left(A^4+B^4=C^4\leftrightarrow C^4-B^4={\left(A^2\right)}^2\right)$$
31	17 30	mtbird	$$⊢\phi \to \neg A^4+B^4=C^4$$
32	31	neqned	$$⊢\phi \to A^4+B^4\ne C^4$$