Theorem flt4

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

	Ref	Expression
Hypotheses	flt4.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	flt4.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	flt4.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
Assertion	flt4	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) ≠ ( 𝐶 ↑ 4 ) )

Proof

Step	Hyp	Ref	Expression
1		flt4.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2		flt4.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		flt4.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4	3	nnsqcld	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℕ )
5	1 2 4	nna4b4nsq	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) ≠ ( ( 𝐶 ↑ 2 ) ↑ 2 ) )
6	3	nncnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
7	6	exp4sqsq	⊢ ( 𝜑 → ( 𝐶 ↑ 4 ) = ( ( 𝐶 ↑ 2 ) ↑ 2 ) )
8	5 7	neeqtrrd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) ≠ ( 𝐶 ↑ 4 ) )