Metamath Proof Explorer

Theorem fltoprmgt3

Description: Fermat's last theorem holds for any exponent greater than 2 if it holds for all odd prime exponents greater than 3. (TODO-AV: after a proof is available for N = 3 , see flt3, the hypothesis fltoprmgt3.3 can be removed.) (Contributed by AV, 15-Sep-2026)

Ref Expression
Hypotheses fltoprmgt3.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
fltoprmgt3.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
fltoprmgt3.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
fltoprmgt3.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
fltoprmgt3.r ⊢ ( 𝜑 → ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ∀ 𝑐 ∈ ℕ ∀ 𝑝 ∈ ℙ ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) )
fltoprmgt3.3 ⊢ ( 𝜑 → ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) ≠ ( 𝑐 ↑ 3 ) )
Assertion fltoprmgt3 ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) ≠ ( 𝐶 ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fltoprmgt3.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 fltoprmgt3.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 fltoprmgt3.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 fltoprmgt3.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
5 fltoprmgt3.r ⊢ ( 𝜑 → ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ∀ 𝑐 ∈ ℕ ∀ 𝑝 ∈ ℙ ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) )
6 fltoprmgt3.3 ⊢ ( 𝜑 → ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) ≠ ( 𝑐 ↑ 3 ) )
7 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
8 2z ⊢ 2 ∈ ℤ
9 8 a1i ⊢ ( 𝑝 ∈ ℤ → 2 ∈ ℤ )
10 id ⊢ ( 𝑝 ∈ ℤ → 𝑝 ∈ ℤ )
11 9 10 zltp1led ⊢ ( 𝑝 ∈ ℤ → ( 2 < 𝑝 ↔ ( 2 + 1 ) ≤ 𝑝 ) )
12 2p1e3 ⊢ ( 2 + 1 ) = 3
13 12 breq1i ⊢ ( ( 2 + 1 ) ≤ 𝑝 ↔ 3 ≤ 𝑝 )
14 13 a1i ⊢ ( 𝑝 ∈ ℤ → ( ( 2 + 1 ) ≤ 𝑝 ↔ 3 ≤ 𝑝 ) )
15 3re ⊢ 3 ∈ ℝ
16 15 a1i ⊢ ( 𝑝 ∈ ℤ → 3 ∈ ℝ )
17 zre ⊢ ( 𝑝 ∈ ℤ → 𝑝 ∈ ℝ )
18 16 17 leloed ⊢ ( 𝑝 ∈ ℤ → ( 3 ≤ 𝑝 ↔ ( 3 < 𝑝 ∨ 3 = 𝑝 ) ) )
19 11 14 18 3bitrd ⊢ ( 𝑝 ∈ ℤ → ( 2 < 𝑝 ↔ ( 3 < 𝑝 ∨ 3 = 𝑝 ) ) )
20 7 19 syl ⊢ ( 𝑝 ∈ ℙ → ( 2 < 𝑝 ↔ ( 3 < 𝑝 ∨ 3 = 𝑝 ) ) )
21 20 adantl ⊢ ( ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 2 < 𝑝 ↔ ( 3 < 𝑝 ∨ 3 = 𝑝 ) ) )
22 21 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ) → ( 2 < 𝑝 ↔ ( 3 < 𝑝 ∨ 3 = 𝑝 ) ) )
23 pm2.27 ⊢ ( 3 < 𝑝 → ( ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) )
24 23 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ) → ( 3 < 𝑝 → ( ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) ) )
25 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ) ∧ 3 = 𝑝 ) → ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) ≠ ( 𝑐 ↑ 3 ) )
26 oveq2 ⊢ ( 3 = 𝑝 → ( 𝑎 ↑ 3 ) = ( 𝑎 ↑ 𝑝 ) )
27 oveq2 ⊢ ( 3 = 𝑝 → ( 𝑏 ↑ 3 ) = ( 𝑏 ↑ 𝑝 ) )
28 26 27 oveq12d ⊢ ( 3 = 𝑝 → ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) = ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) )
29 oveq2 ⊢ ( 3 = 𝑝 → ( 𝑐 ↑ 3 ) = ( 𝑐 ↑ 𝑝 ) )
30 28 29 neeq12d ⊢ ( 3 = 𝑝 → ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) ≠ ( 𝑐 ↑ 3 ) ↔ ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) )
31 30 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ) ∧ 3 = 𝑝 ) → ( ( ( 𝑎 ↑ 3 ) + ( 𝑏 ↑ 3 ) ) ≠ ( 𝑐 ↑ 3 ) ↔ ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) )
32 25 31 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ) ∧ 3 = 𝑝 ) → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) )
33 32 a1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ) ∧ 3 = 𝑝 ) → ( ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) )
34 33 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ) → ( 3 = 𝑝 → ( ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) ) )
35 24 34 jaod ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ) → ( ( 3 < 𝑝 ∨ 3 = 𝑝 ) → ( ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) ) )
36 22 35 sylbid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ) → ( 2 < 𝑝 → ( ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) ) )
37 36 com23 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ) → ( ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) → ( 2 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) ) )
38 37 ralimdvva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ) ) → ( ∀ 𝑐 ∈ ℕ ∀ 𝑝 ∈ ℙ ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) → ∀ 𝑐 ∈ ℕ ∀ 𝑝 ∈ ℙ ( 2 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) ) )
39 38 ralimdvva ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ∀ 𝑐 ∈ ℕ ∀ 𝑝 ∈ ℙ ( 3 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) → ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ∀ 𝑐 ∈ ℕ ∀ 𝑝 ∈ ℙ ( 2 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) ) )
40 5 39 mpd ⊢ ( 𝜑 → ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ∀ 𝑐 ∈ ℕ ∀ 𝑝 ∈ ℙ ( 2 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) )
41 1 2 3 4 40 fltoprm ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) ≠ ( 𝐶 ↑ 𝑁 ) )