Theorem flt4

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

	Ref	Expression
Hypotheses	flt4.a	|- ( ph -> A e. NN )
	flt4.b	|- ( ph -> B e. NN )
	flt4.c	|- ( ph -> C e. NN )
Assertion	flt4	|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 4 ) )

Proof

Step	Hyp	Ref	Expression
1		flt4.a	|- ( ph -> A e. NN )
2		flt4.b	|- ( ph -> B e. NN )
3		flt4.c	|- ( ph -> C e. NN )
4	3	nnsqcld	|- ( ph -> ( C ^ 2 ) e. NN )
5	1 2 4	nna4b4nsq	|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( ( C ^ 2 ) ^ 2 ) )
6	3	nncnd	|- ( ph -> C e. CC )
7	6	exp4sqsq	|- ( ph -> ( C ^ 4 ) = ( ( C ^ 2 ) ^ 2 ) )
8	5 7	neeqtrrd	|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 4 ) )