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	$⊢ φ \to A \in ℕ$
	fltoprmgt3.b	$⊢ φ \to B \in ℕ$
	fltoprmgt3.c	$⊢ φ \to C \in ℕ$
	fltoprmgt3.n	$⊢ φ \to N \in ℤ_{\geq 3}$
	fltoprmgt3.r	$⊢ φ \to \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (3 < p \to a^{p} + b^{p} \neq c^{p})$
	fltoprmgt3.3	$⊢ φ \to a^{3} + b^{3} \neq c^{3}$
Assertion	fltoprmgt3	$⊢ φ \to A^{N} + B^{N} \neq C^{N}$

Proof

Step	Hyp	Ref	Expression
1		fltoprmgt3.a	$⊢ φ \to A \in ℕ$
2		fltoprmgt3.b	$⊢ φ \to B \in ℕ$
3		fltoprmgt3.c	$⊢ φ \to C \in ℕ$
4		fltoprmgt3.n	$⊢ φ \to N \in ℤ_{\geq 3}$
5		fltoprmgt3.r	$⊢ φ \to \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (3 < p \to a^{p} + b^{p} \neq c^{p})$
6		fltoprmgt3.3	$⊢ φ \to a^{3} + b^{3} \neq c^{3}$
7		prmz	$⊢ p \in ℙ \to p \in ℤ$
8		2z	$⊢ 2 \in ℤ$
9	8	a1i	$⊢ p \in ℤ \to 2 \in ℤ$
10		id	$⊢ p \in ℤ \to p \in ℤ$
11	9 10	zltp1led	$⊢ p \in ℤ \to (2 < p \leftrightarrow 2 + 1 \leq p)$
12		2p1e3	$⊢ 2 + 1 = 3$
13	12	breq1i	$⊢ 2 + 1 \leq p \leftrightarrow 3 \leq p$
14	13	a1i	$⊢ p \in ℤ \to (2 + 1 \leq p \leftrightarrow 3 \leq p)$
15		3re	$⊢ 3 \in ℝ$
16	15	a1i	$⊢ p \in ℤ \to 3 \in ℝ$
17		zre	$⊢ p \in ℤ \to p \in ℝ$
18	16 17	leloed	$⊢ p \in ℤ \to (3 \leq p \leftrightarrow (3 < p \lor 3 = p))$
19	11 14 18	3bitrd	$⊢ p \in ℤ \to (2 < p \leftrightarrow (3 < p \lor 3 = p))$
20	7 19	syl	$⊢ p \in ℙ \to (2 < p \leftrightarrow (3 < p \lor 3 = p))$
21	20	adantl	$⊢ (c \in ℕ \land p \in ℙ) \to (2 < p \leftrightarrow (3 < p \lor 3 = p))$
22	21	adantl	$⊢ ((φ \land (a \in ℕ \land b \in ℕ)) \land (c \in ℕ \land p \in ℙ)) \to (2 < p \leftrightarrow (3 < p \lor 3 = p))$
23		pm2.27	$⊢ 3 < p \to ((3 < p \to a^{p} + b^{p} \neq c^{p}) \to a^{p} + b^{p} \neq c^{p})$
24	23	a1i	$⊢ ((φ \land (a \in ℕ \land b \in ℕ)) \land (c \in ℕ \land p \in ℙ)) \to (3 < p \to ((3 < p \to a^{p} + b^{p} \neq c^{p}) \to a^{p} + b^{p} \neq c^{p}))$
25	6	ad3antrrr	$⊢ (((φ \land (a \in ℕ \land b \in ℕ)) \land (c \in ℕ \land p \in ℙ)) \land 3 = p) \to a^{3} + b^{3} \neq c^{3}$
26		oveq2	$⊢ 3 = p \to a^{3} = a^{p}$
27		oveq2	$⊢ 3 = p \to b^{3} = b^{p}$
28	26 27	oveq12d	$⊢ 3 = p \to a^{3} + b^{3} = a^{p} + b^{p}$
29		oveq2	$⊢ 3 = p \to c^{3} = c^{p}$
30	28 29	neeq12d	$⊢ 3 = p \to (a^{3} + b^{3} \neq c^{3} \leftrightarrow a^{p} + b^{p} \neq c^{p})$
31	30	adantl	$⊢ (((φ \land (a \in ℕ \land b \in ℕ)) \land (c \in ℕ \land p \in ℙ)) \land 3 = p) \to (a^{3} + b^{3} \neq c^{3} \leftrightarrow a^{p} + b^{p} \neq c^{p})$
32	25 31	mpbid	$⊢ (((φ \land (a \in ℕ \land b \in ℕ)) \land (c \in ℕ \land p \in ℙ)) \land 3 = p) \to a^{p} + b^{p} \neq c^{p}$
33	32	a1d	$⊢ (((φ \land (a \in ℕ \land b \in ℕ)) \land (c \in ℕ \land p \in ℙ)) \land 3 = p) \to ((3 < p \to a^{p} + b^{p} \neq c^{p}) \to a^{p} + b^{p} \neq c^{p})$
34	33	ex	$⊢ ((φ \land (a \in ℕ \land b \in ℕ)) \land (c \in ℕ \land p \in ℙ)) \to (3 = p \to ((3 < p \to a^{p} + b^{p} \neq c^{p}) \to a^{p} + b^{p} \neq c^{p}))$
35	24 34	jaod	$⊢ ((φ \land (a \in ℕ \land b \in ℕ)) \land (c \in ℕ \land p \in ℙ)) \to ((3 < p \lor 3 = p) \to ((3 < p \to a^{p} + b^{p} \neq c^{p}) \to a^{p} + b^{p} \neq c^{p}))$
36	22 35	sylbid	$⊢ ((φ \land (a \in ℕ \land b \in ℕ)) \land (c \in ℕ \land p \in ℙ)) \to (2 < p \to ((3 < p \to a^{p} + b^{p} \neq c^{p}) \to a^{p} + b^{p} \neq c^{p}))$
37	36	com23	$⊢ ((φ \land (a \in ℕ \land b \in ℕ)) \land (c \in ℕ \land p \in ℙ)) \to ((3 < p \to a^{p} + b^{p} \neq c^{p}) \to (2 < p \to a^{p} + b^{p} \neq c^{p}))$
38	37	ralimdvva	$⊢ (φ \land (a \in ℕ \land b \in ℕ)) \to (\forall c \in ℕ \forall p \in ℙ (3 < p \to a^{p} + b^{p} \neq c^{p}) \to \forall c \in ℕ \forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p}))$
39	38	ralimdvva	$⊢ φ \to (\forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (3 < p \to a^{p} + b^{p} \neq c^{p}) \to \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p}))$
40	5 39	mpd	$⊢ φ \to \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p})$
41	1 2 3 4 40	fltoprm	$⊢ φ \to A^{N} + B^{N} \neq C^{N}$

Metamath Proof Explorer

Theorem fltoprmgt3

Proof