fltoprm

Description: Fermat's last theorem holds for any exponent greater than 2 if it holds for odd prime exponents. (Contributed by AV, 15-Sep-2026)

	Ref	Expression
Hypotheses	fltoprm.a	$⊢ φ \to A \in ℕ$
	fltoprm.b	$⊢ φ \to B \in ℕ$
	fltoprm.c	$⊢ φ \to C \in ℕ$
	fltoprm.n	$⊢ φ \to N \in ℤ_{\geq 3}$
	fltoprm.r	$⊢ φ \to \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p})$
Assertion	fltoprm	$⊢ φ \to A^{N} + B^{N} \neq C^{N}$

Proof

Step	Hyp	Ref	Expression
1		fltoprm.a	$⊢ φ \to A \in ℕ$
2		fltoprm.b	$⊢ φ \to B \in ℕ$
3		fltoprm.c	$⊢ φ \to C \in ℕ$
4		fltoprm.n	$⊢ φ \to N \in ℤ_{\geq 3}$
5		fltoprm.r	$⊢ φ \to \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p})$
6		prmnn	$⊢ r \in ℙ \to r \in ℕ$
7		3nn	$⊢ 3 \in ℕ$
8		eluznn	$⊢ (3 \in ℕ \land N \in ℤ_{\geq 3}) \to N \in ℕ$
9	7 4 8	sylancr	$⊢ φ \to N \in ℕ$
10		nndivides	$⊢ (r \in ℕ \land N \in ℕ) \to (r ∥ N \leftrightarrow \exists k \in ℕ k r = N)$
11	6 9 10	syl2anr	$⊢ (φ \land r \in ℙ) \to (r ∥ N \leftrightarrow \exists k \in ℕ k r = N)$
12	5	adantr	$⊢ (φ \land r \in ℙ) \to \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p})$
13	12	ad2antrr	$⊢ (((φ \land r \in ℙ) \land k \in ℕ) \land 2 < r) \to \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p})$
14	1	ad2antrr	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to A \in ℕ$
15		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
16	15	adantl	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to k \in ℕ_{0}$
17	14 16	nnexpcld	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to A^{k} \in ℕ$
18	2	ad2antrr	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to B \in ℕ$
19	18 16	nnexpcld	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to B^{k} \in ℕ$
20	3	ad2antrr	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to C \in ℕ$
21	20 16	nnexpcld	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to C^{k} \in ℕ$
22	17 19 21	3jca	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to (A^{k} \in ℕ \land B^{k} \in ℕ \land C^{k} \in ℕ)$
23	22	adantr	$⊢ (((φ \land r \in ℙ) \land k \in ℕ) \land 2 < r) \to (A^{k} \in ℕ \land B^{k} \in ℕ \land C^{k} \in ℕ)$
24		oveq1	$⊢ a = A^{k} \to a^{p} = {(A^{k})}^{p}$
25	24	oveq1d	$⊢ a = A^{k} \to a^{p} + b^{p} = {(A^{k})}^{p} + b^{p}$
26	25	neeq1d	$⊢ a = A^{k} \to (a^{p} + b^{p} \neq c^{p} \leftrightarrow {(A^{k})}^{p} + b^{p} \neq c^{p})$
27	26	imbi2d	$⊢ a = A^{k} \to ((2 < p \to a^{p} + b^{p} \neq c^{p}) \leftrightarrow (2 < p \to {(A^{k})}^{p} + b^{p} \neq c^{p}))$
28	27	ralbidv	$⊢ a = A^{k} \to (\forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p}) \leftrightarrow \forall p \in ℙ (2 < p \to {(A^{k})}^{p} + b^{p} \neq c^{p}))$
29		oveq1	$⊢ b = B^{k} \to b^{p} = {(B^{k})}^{p}$
30	29	oveq2d	$⊢ b = B^{k} \to {(A^{k})}^{p} + b^{p} = {(A^{k})}^{p} + {(B^{k})}^{p}$
31	30	neeq1d	$⊢ b = B^{k} \to ({(A^{k})}^{p} + b^{p} \neq c^{p} \leftrightarrow {(A^{k})}^{p} + {(B^{k})}^{p} \neq c^{p})$
32	31	imbi2d	$⊢ b = B^{k} \to ((2 < p \to {(A^{k})}^{p} + b^{p} \neq c^{p}) \leftrightarrow (2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq c^{p}))$
33	32	ralbidv	$⊢ b = B^{k} \to (\forall p \in ℙ (2 < p \to {(A^{k})}^{p} + b^{p} \neq c^{p}) \leftrightarrow \forall p \in ℙ (2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq c^{p}))$
34		oveq1	$⊢ c = C^{k} \to c^{p} = {(C^{k})}^{p}$
35	34	neeq2d	$⊢ c = C^{k} \to ({(A^{k})}^{p} + {(B^{k})}^{p} \neq c^{p} \leftrightarrow {(A^{k})}^{p} + {(B^{k})}^{p} \neq {(C^{k})}^{p})$
36	35	imbi2d	$⊢ c = C^{k} \to ((2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq c^{p}) \leftrightarrow (2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq {(C^{k})}^{p}))$
37	36	ralbidv	$⊢ c = C^{k} \to (\forall p \in ℙ (2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq c^{p}) \leftrightarrow \forall p \in ℙ (2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq {(C^{k})}^{p}))$
38	28 33 37	rspc3v	$⊢ (A^{k} \in ℕ \land B^{k} \in ℕ \land C^{k} \in ℕ) \to (\forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p}) \to \forall p \in ℙ (2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq {(C^{k})}^{p}))$
39	23 38	syl	$⊢ (((φ \land r \in ℙ) \land k \in ℕ) \land 2 < r) \to (\forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p}) \to \forall p \in ℙ (2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq {(C^{k})}^{p}))$
40		breq2	$⊢ p = r \to (2 < p \leftrightarrow 2 < r)$
41		oveq2	$⊢ p = r \to {(A^{k})}^{p} = {(A^{k})}^{r}$
42		oveq2	$⊢ p = r \to {(B^{k})}^{p} = {(B^{k})}^{r}$
43	41 42	oveq12d	$⊢ p = r \to {(A^{k})}^{p} + {(B^{k})}^{p} = {(A^{k})}^{r} + {(B^{k})}^{r}$
44		oveq2	$⊢ p = r \to {(C^{k})}^{p} = {(C^{k})}^{r}$
45	43 44	neeq12d	$⊢ p = r \to ({(A^{k})}^{p} + {(B^{k})}^{p} \neq {(C^{k})}^{p} \leftrightarrow {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r})$
46	40 45	imbi12d	$⊢ p = r \to ((2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq {(C^{k})}^{p}) \leftrightarrow (2 < r \to {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r}))$
47	46	rspcv	$⊢ r \in ℙ \to (\forall p \in ℙ (2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq {(C^{k})}^{p}) \to (2 < r \to {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r}))$
48	47	adantl	$⊢ (φ \land r \in ℙ) \to (\forall p \in ℙ (2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq {(C^{k})}^{p}) \to (2 < r \to {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r}))$
49	48	ad2antrr	$⊢ (((φ \land r \in ℙ) \land k \in ℕ) \land 2 < r) \to (\forall p \in ℙ (2 < p \to {(A^{k})}^{p} + {(B^{k})}^{p} \neq {(C^{k})}^{p}) \to (2 < r \to {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r}))$
50		pm2.27	$⊢ 2 < r \to ((2 < r \to {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r}) \to {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r})$
51	50	adantl	$⊢ (((φ \land r \in ℙ) \land k \in ℕ) \land 2 < r) \to ((2 < r \to {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r}) \to {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r})$
52	39 49 51	3syld	$⊢ (((φ \land r \in ℙ) \land k \in ℕ) \land 2 < r) \to (\forall a \in ℕ \forall b \in ℕ \forall c \in ℕ \forall p \in ℙ (2 < p \to a^{p} + b^{p} \neq c^{p}) \to {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r})$
53	13 52	mpd	$⊢ (((φ \land r \in ℙ) \land k \in ℕ) \land 2 < r) \to {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r}$
54	1	nncnd	$⊢ φ \to A \in ℂ$
55	54	ad2antrr	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to A \in ℂ$
56	6	nnnn0d	$⊢ r \in ℙ \to r \in ℕ_{0}$
57	56	adantl	$⊢ (φ \land r \in ℙ) \to r \in ℕ_{0}$
58	57	adantr	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to r \in ℕ_{0}$
59	55 58 16	expmuld	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to A^{k r} = {(A^{k})}^{r}$
60	2	nncnd	$⊢ φ \to B \in ℂ$
61	60	ad2antrr	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to B \in ℂ$
62	61 58 16	expmuld	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to B^{k r} = {(B^{k})}^{r}$
63	59 62	oveq12d	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to A^{k r} + B^{k r} = {(A^{k})}^{r} + {(B^{k})}^{r}$
64	3	nncnd	$⊢ φ \to C \in ℂ$
65	64	ad2antrr	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to C \in ℂ$
66	65 58 16	expmuld	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to C^{k r} = {(C^{k})}^{r}$
67	63 66	neeq12d	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to (A^{k r} + B^{k r} \neq C^{k r} \leftrightarrow {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r})$
68	67	adantr	$⊢ (((φ \land r \in ℙ) \land k \in ℕ) \land 2 < r) \to (A^{k r} + B^{k r} \neq C^{k r} \leftrightarrow {(A^{k})}^{r} + {(B^{k})}^{r} \neq {(C^{k})}^{r})$
69	53 68	mpbird	$⊢ (((φ \land r \in ℙ) \land k \in ℕ) \land 2 < r) \to A^{k r} + B^{k r} \neq C^{k r}$
70		oveq2	$⊢ k r = N \to A^{k r} = A^{N}$
71		oveq2	$⊢ k r = N \to B^{k r} = B^{N}$
72	70 71	oveq12d	$⊢ k r = N \to A^{k r} + B^{k r} = A^{N} + B^{N}$
73		oveq2	$⊢ k r = N \to C^{k r} = C^{N}$
74	72 73	neeq12d	$⊢ k r = N \to (A^{k r} + B^{k r} \neq C^{k r} \leftrightarrow A^{N} + B^{N} \neq C^{N})$
75	69 74	syl5ibcom	$⊢ (((φ \land r \in ℙ) \land k \in ℕ) \land 2 < r) \to (k r = N \to A^{N} + B^{N} \neq C^{N})$
76	75	ex	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to (2 < r \to (k r = N \to A^{N} + B^{N} \neq C^{N}))$
77	76	com23	$⊢ ((φ \land r \in ℙ) \land k \in ℕ) \to (k r = N \to (2 < r \to A^{N} + B^{N} \neq C^{N}))$
78	77	rexlimdva	$⊢ (φ \land r \in ℙ) \to (\exists k \in ℕ k r = N \to (2 < r \to A^{N} + B^{N} \neq C^{N}))$
79	11 78	sylbid	$⊢ (φ \land r \in ℙ) \to (r ∥ N \to (2 < r \to A^{N} + B^{N} \neq C^{N}))$
80	79	impcomd	$⊢ (φ \land r \in ℙ) \to ((2 < r \land r ∥ N) \to A^{N} + B^{N} \neq C^{N})$
81	80	rexlimdva	$⊢ φ \to (\exists r \in ℙ (2 < r \land r ∥ N) \to A^{N} + B^{N} \neq C^{N})$
82	4	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land N = 2^{n}) \to N \in ℤ_{\geq 3}$
83		simplr	$⊢ ((φ \land n \in ℕ_{0}) \land N = 2^{n}) \to n \in ℕ_{0}$
84		simpr	$⊢ ((φ \land n \in ℕ_{0}) \land N = 2^{n}) \to N = 2^{n}$
85		fltoprmlem2	$⊢ (N \in ℤ_{\geq 3} \land n \in ℕ_{0} \land N = 2^{n}) \to 4 ∥ N$
86	82 83 84 85	syl3anc	$⊢ ((φ \land n \in ℕ_{0}) \land N = 2^{n}) \to 4 ∥ N$
87	86	ex	$⊢ (φ \land n \in ℕ_{0}) \to (N = 2^{n} \to 4 ∥ N)$
88		4nn	$⊢ 4 \in ℕ$
89	9 88	jctil	$⊢ φ \to (4 \in ℕ \land N \in ℕ)$
90	89	adantr	$⊢ (φ \land n \in ℕ_{0}) \to (4 \in ℕ \land N \in ℕ)$
91		nndivides	$⊢ (4 \in ℕ \land N \in ℕ) \to (4 ∥ N \leftrightarrow \exists k \in ℕ k \cdot 4 = N)$
92	90 91	syl	$⊢ (φ \land n \in ℕ_{0}) \to (4 ∥ N \leftrightarrow \exists k \in ℕ k \cdot 4 = N)$
93	1	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to A \in ℕ$
94	15	adantl	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to k \in ℕ_{0}$
95	93 94	nnexpcld	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to A^{k} \in ℕ$
96	2	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to B \in ℕ$
97	96 94	nnexpcld	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to B^{k} \in ℕ$
98	3	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to C \in ℕ$
99	98 94	nnexpcld	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to C^{k} \in ℕ$
100	95 97 99	flt4	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to {(A^{k})}^{4} + {(B^{k})}^{4} \neq {(C^{k})}^{4}$
101	54	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to A \in ℂ$
102		4nn0	$⊢ 4 \in ℕ_{0}$
103	102	a1i	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to 4 \in ℕ_{0}$
104	101 103 94	expmuld	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to A^{k \cdot 4} = {(A^{k})}^{4}$
105	2	adantr	$⊢ (φ \land n \in ℕ_{0}) \to B \in ℕ$
106	105	nncnd	$⊢ (φ \land n \in ℕ_{0}) \to B \in ℂ$
107	106	adantr	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to B \in ℂ$
108	107 103 94	expmuld	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to B^{k \cdot 4} = {(B^{k})}^{4}$
109	104 108	oveq12d	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to A^{k \cdot 4} + B^{k \cdot 4} = {(A^{k})}^{4} + {(B^{k})}^{4}$
110	64	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to C \in ℂ$
111	110 103 94	expmuld	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to C^{k \cdot 4} = {(C^{k})}^{4}$
112	100 109 111	3netr4d	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to A^{k \cdot 4} + B^{k \cdot 4} \neq C^{k \cdot 4}$
113		oveq2	$⊢ k \cdot 4 = N \to A^{k \cdot 4} = A^{N}$
114		oveq2	$⊢ k \cdot 4 = N \to B^{k \cdot 4} = B^{N}$
115	113 114	oveq12d	$⊢ k \cdot 4 = N \to A^{k \cdot 4} + B^{k \cdot 4} = A^{N} + B^{N}$
116		oveq2	$⊢ k \cdot 4 = N \to C^{k \cdot 4} = C^{N}$
117	115 116	neeq12d	$⊢ k \cdot 4 = N \to (A^{k \cdot 4} + B^{k \cdot 4} \neq C^{k \cdot 4} \leftrightarrow A^{N} + B^{N} \neq C^{N})$
118	112 117	syl5ibcom	$⊢ ((φ \land n \in ℕ_{0}) \land k \in ℕ) \to (k \cdot 4 = N \to A^{N} + B^{N} \neq C^{N})$
119	118	rexlimdva	$⊢ (φ \land n \in ℕ_{0}) \to (\exists k \in ℕ k \cdot 4 = N \to A^{N} + B^{N} \neq C^{N})$
120	92 119	sylbid	$⊢ (φ \land n \in ℕ_{0}) \to (4 ∥ N \to A^{N} + B^{N} \neq C^{N})$
121	87 120	syld	$⊢ (φ \land n \in ℕ_{0}) \to (N = 2^{n} \to A^{N} + B^{N} \neq C^{N})$
122	121	rexlimdva	$⊢ φ \to (\exists n \in ℕ_{0} N = 2^{n} \to A^{N} + B^{N} \neq C^{N})$
123		fltoprmlem1	$⊢ N \in ℕ \to (\exists r \in ℙ (2 < r \land r ∥ N) \lor \exists n \in ℕ_{0} N = 2^{n})$
124	9 123	syl	$⊢ φ \to (\exists r \in ℙ (2 < r \land r ∥ N) \lor \exists n \in ℕ_{0} N = 2^{n})$
125	81 122 124	mpjaod	$⊢ φ \to A^{N} + B^{N} \neq C^{N}$

Metamath Proof Explorer

Theorem fltoprm

Proof