Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
flt4.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
flt4.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
flt4ALT.r ⊢ ( 𝜑 → ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ∀ 𝑐 ∈ ℕ ( ( 𝑎 ↑ 4 ) − ( 𝑏 ↑ 4 ) ) ≠ ( 𝑐 ↑ 2 ) )
Assertion flt4ALT ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) ≠ ( 𝐶 ↑ 4 ) )

Proof

Step Hyp Ref Expression
1 flt4.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 flt4.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 flt4.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 flt4ALT.r ⊢ ( 𝜑 → ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ∀ 𝑐 ∈ ℕ ( ( 𝑎 ↑ 4 ) − ( 𝑏 ↑ 4 ) ) ≠ ( 𝑐 ↑ 2 ) )
5 1 nnsqcld ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℕ )
6 3 2 5 3jca ⊢ ( 𝜑 → ( 𝐶 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 ↑ 2 ) ∈ ℕ ) )
7 oveq1 ⊢ ( 𝑎 = 𝐶 → ( 𝑎 ↑ 4 ) = ( 𝐶 ↑ 4 ) )
8 7 oveq1d ⊢ ( 𝑎 = 𝐶 → ( ( 𝑎 ↑ 4 ) − ( 𝑏 ↑ 4 ) ) = ( ( 𝐶 ↑ 4 ) − ( 𝑏 ↑ 4 ) ) )
9 8 neeq1d ⊢ ( 𝑎 = 𝐶 → ( ( ( 𝑎 ↑ 4 ) − ( 𝑏 ↑ 4 ) ) ≠ ( 𝑐 ↑ 2 ) ↔ ( ( 𝐶 ↑ 4 ) − ( 𝑏 ↑ 4 ) ) ≠ ( 𝑐 ↑ 2 ) ) )
10 oveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ↑ 4 ) = ( 𝐵 ↑ 4 ) )
11 10 oveq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐶 ↑ 4 ) − ( 𝑏 ↑ 4 ) ) = ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) )
12 11 neeq1d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐶 ↑ 4 ) − ( 𝑏 ↑ 4 ) ) ≠ ( 𝑐 ↑ 2 ) ↔ ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) ≠ ( 𝑐 ↑ 2 ) ) )
13 oveq1 ⊢ ( 𝑐 = ( 𝐴 ↑ 2 ) → ( 𝑐 ↑ 2 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
14 13 neeq2d ⊢ ( 𝑐 = ( 𝐴 ↑ 2 ) → ( ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) ≠ ( 𝑐 ↑ 2 ) ↔ ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) ≠ ( ( 𝐴 ↑ 2 ) ↑ 2 ) ) )
15 9 12 14 rspc3v ⊢ ( ( 𝐶 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 ↑ 2 ) ∈ ℕ ) → ( ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ∀ 𝑐 ∈ ℕ ( ( 𝑎 ↑ 4 ) − ( 𝑏 ↑ 4 ) ) ≠ ( 𝑐 ↑ 2 ) → ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) ≠ ( ( 𝐴 ↑ 2 ) ↑ 2 ) ) )
16 6 4 15 sylc ⊢ ( 𝜑 → ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) ≠ ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
17 16 neneqd ⊢ ( 𝜑 → ¬ ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
18 4nn0 ⊢ 4 ∈ ℕ0
19 18 a1i ⊢ ( 𝜑 → 4 ∈ ℕ0 )
20 3 19 nnexpcld ⊢ ( 𝜑 → ( 𝐶 ↑ 4 ) ∈ ℕ )
21 20 nncnd ⊢ ( 𝜑 → ( 𝐶 ↑ 4 ) ∈ ℂ )
22 2 19 nnexpcld ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) ∈ ℕ )
23 22 nncnd ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) ∈ ℂ )
24 1 19 nnexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) ∈ ℕ )
25 24 nncnd ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) ∈ ℂ )
26 21 23 25 subadd2d ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) = ( 𝐴 ↑ 4 ) ↔ ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 4 ) ) )
27 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
28 27 exp4sqsq ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
29 28 eqeq2d ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) = ( 𝐴 ↑ 4 ) ↔ ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) ) )
30 26 29 bitr3d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 4 ) ↔ ( ( 𝐶 ↑ 4 ) − ( 𝐵 ↑ 4 ) ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) ) )
31 17 30 mtbird ⊢ ( 𝜑 → ¬ ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 4 ) )
32 31 neqned ⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) ≠ ( 𝐶 ↑ 4 ) )