fltoprm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fltoprm		Structured version Visualization version GIF version

Theorem fltoprm 28000

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.)

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

**Assertion**
Ref	Expression
fltoprm	⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))

Distinct variable groups: 𝐴,𝑎,𝑏,𝑐,𝑝 𝐵,𝑏,𝑐,𝑝 𝐶,𝑐,𝑝 Allowed substitution hints: 𝜑(𝑝, 𝑎, 𝑏, 𝑐) 𝐵(𝑎) 𝐶(𝑎, 𝑏) 𝑁(𝑝, 𝑎, 𝑏, 𝑐)

Proof of Theorem fltoprm Dummy variables 𝑛 𝑘 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmnn 16854	. . . . . 6 ⊢ (𝑟 ∈ ℙ → 𝑟 ∈ ℕ)
2		3nn 12425	. . . . . . 7 ⊢ 3 ∈ ℕ
3		fltoprm.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘3))
4		eluznn 13048	. . . . . . 7 ⊢ ((3 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘3)) → 𝑁 ∈ ℕ)
5	2, 3, 4	sylancr 599	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6		nndivides 16437	. . . . . 6 ⊢ ((𝑟 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑟 ∥ 𝑁 ↔ ∃𝑘 ∈ ℕ (𝑘 · 𝑟) = 𝑁))
7	1, 5, 6	syl2anr 609	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (𝑟 ∥ 𝑁 ↔ ∃𝑘 ∈ ℕ (𝑘 · 𝑟) = 𝑁))
8		fltoprm.r	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)))
9	8	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → ∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)))
10	9	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)))
11		fltoprm.a	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℕ)
12	11	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℕ)
13		nnnn0 12616	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
14	13	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
15	12, 14	nnexpcld 14392	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℕ)
16		fltoprm.b	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℕ)
17	16	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℕ)
18	17, 14	nnexpcld 14392	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) ∈ ℕ)
19		fltoprm.c	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℕ)
20	19	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℕ)
21	20, 14	nnexpcld 14392	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐶↑𝑘) ∈ ℕ)
22	15, 18, 21	3jca 1146	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝐴↑𝑘) ∈ ℕ ∧ (𝐵↑𝑘) ∈ ℕ ∧ (𝐶↑𝑘) ∈ ℕ))
23	22	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ((𝐴↑𝑘) ∈ ℕ ∧ (𝐵↑𝑘) ∈ ℕ ∧ (𝐶↑𝑘) ∈ ℕ))
24		oveq1 7427	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝐴↑𝑘) → (𝑎↑𝑝) = ((𝐴↑𝑘)↑𝑝))
25	24	oveq1d 7435	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝐴↑𝑘) → ((𝑎↑𝑝) + (𝑏↑𝑝)) = (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)))
26	25	neeq1d 3014	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝐴↑𝑘) → (((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝) ↔ (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)))
27	26	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝐴↑𝑘) → ((2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝))))
28	27	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝐴↑𝑘) → (∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝))))
29		oveq1 7427	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝐵↑𝑘) → (𝑏↑𝑝) = ((𝐵↑𝑘)↑𝑝))
30	29	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝐵↑𝑘) → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) = (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)))
31	30	neeq1d 3014	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝐵↑𝑘) → ((((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝) ↔ (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝)))
32	31	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝐵↑𝑘) → ((2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝))))
33	32	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝐵↑𝑘) → (∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝))))
34		oveq1 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐶↑𝑘) → (𝑐↑𝑝) = ((𝐶↑𝑘)↑𝑝))
35	34	neeq2d 3015	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐶↑𝑘) → ((((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝) ↔ (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝)))
36	35	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝐶↑𝑘) → ((2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝)) ↔ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
37	36	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝐶↑𝑘) → (∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝)) ↔ ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
38	28, 33, 37	rspc3v 3591	. . . . . . . . . . . . 13 ⊢ (((𝐴↑𝑘) ∈ ℕ ∧ (𝐵↑𝑘) ∈ ℕ ∧ (𝐶↑𝑘) ∈ ℕ) → (∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) → ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
39	23, 38	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → (∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) → ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
40		breq2 5106	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑟 → (2 < 𝑝 ↔ 2 < 𝑟))
41		oveq2 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((𝐴↑𝑘)↑𝑝) = ((𝐴↑𝑘)↑𝑟))
42		oveq2 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((𝐵↑𝑘)↑𝑝) = ((𝐵↑𝑘)↑𝑟))
43	41, 42	oveq12d 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑟 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) = (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)))
44		oveq2 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑟 → ((𝐶↑𝑘)↑𝑝) = ((𝐶↑𝑘)↑𝑟))
45	43, 44	neeq12d 3016	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑟 → ((((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝) ↔ (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
46	40, 45	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑟 → ((2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝)) ↔ (2 < 𝑟 → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟))))
47	46	rspcv 3572	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ℙ → (∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝)) → (2 < 𝑟 → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟))))
48	47	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝)) → (2 < 𝑟 → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟))))
49	48	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → (∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝)) → (2 < 𝑟 → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟))))
50		pm2.27 43	. . . . . . . . . . . . 13 ⊢ (2 < 𝑟 → ((2 < 𝑟 → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)) → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
51	50	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ((2 < 𝑟 → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)) → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
52	39, 49, 51	3syld 61	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → (∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
53	10, 52	mpd 16	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟))
54	11	nncnd 12354	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℂ)
55	54	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
56	1	nnnn0d 12670	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ ℙ → 𝑟 ∈ ℕ₀)
57	56	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → 𝑟 ∈ ℕ₀)
58	57	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑟 ∈ ℕ₀)
59	55, 58, 14	expmuld 14295	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑘 · 𝑟)) = ((𝐴↑𝑘)↑𝑟))
60	16	nncnd 12354	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℂ)
61	60	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
62	61, 58, 14	expmuld 14295	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐵↑(𝑘 · 𝑟)) = ((𝐵↑𝑘)↑𝑟))
63	59, 62	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) = (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)))
64	19	nncnd 12354	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ℂ)
65	64	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
66	65, 58, 14	expmuld 14295	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐶↑(𝑘 · 𝑟)) = ((𝐶↑𝑘)↑𝑟))
67	63, 66	neeq12d 3016	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)) ↔ (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
68	67	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → (((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)) ↔ (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
69	53, 68	mpbird 260	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)))
70		oveq2 7428	. . . . . . . . . . 11 ⊢ ((𝑘 · 𝑟) = 𝑁 → (𝐴↑(𝑘 · 𝑟)) = (𝐴↑𝑁))
71		oveq2 7428	. . . . . . . . . . 11 ⊢ ((𝑘 · 𝑟) = 𝑁 → (𝐵↑(𝑘 · 𝑟)) = (𝐵↑𝑁))
72	70, 71	oveq12d 7438	. . . . . . . . . 10 ⊢ ((𝑘 · 𝑟) = 𝑁 → ((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) = ((𝐴↑𝑁) + (𝐵↑𝑁)))
73		oveq2 7428	. . . . . . . . . 10 ⊢ ((𝑘 · 𝑟) = 𝑁 → (𝐶↑(𝑘 · 𝑟)) = (𝐶↑𝑁))
74	72, 73	neeq12d 3016	. . . . . . . . 9 ⊢ ((𝑘 · 𝑟) = 𝑁 → (((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)) ↔ ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
75	69, 74	syl5ibcom 248	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ((𝑘 · 𝑟) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
76	75	ex 418	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2 < 𝑟 → ((𝑘 · 𝑟) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
77	76	com23 87	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · 𝑟) = 𝑁 → (2 < 𝑟 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
78	77	rexlimdva 3163	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (∃𝑘 ∈ ℕ (𝑘 · 𝑟) = 𝑁 → (2 < 𝑟 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
79	7, 78	sylbid 243	. . . 4 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (𝑟 ∥ 𝑁 → (2 < 𝑟 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
80	79	impcomd 417	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → ((2 < 𝑟 ∧ 𝑟 ∥ 𝑁) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
81	80	rexlimdva 3163	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℙ (2 < 𝑟 ∧ 𝑟 ∥ 𝑁) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
82	3	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 𝑁 ∈ (ℤ_≥‘3))
83		simplr 781	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 𝑛 ∈ ℕ₀)
84		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 𝑁 = (2↑𝑛))
85		fltoprmlem2 27999	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑛 ∈ ℕ₀ ∧ 𝑁 = (2↑𝑛)) → 4 ∥ 𝑁)
86	82, 83, 84, 85	syl3anc 1398	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 4 ∥ 𝑁)
87	86	ex 418	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑁 = (2↑𝑛) → 4 ∥ 𝑁))
88		4nn 12429	. . . . . . . 8 ⊢ 4 ∈ ℕ
89	5, 88	jctil 529	. . . . . . 7 ⊢ (𝜑 → (4 ∈ ℕ ∧ 𝑁 ∈ ℕ))
90	89	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (4 ∈ ℕ ∧ 𝑁 ∈ ℕ))
91		nndivides 16437	. . . . . 6 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (4 ∥ 𝑁 ↔ ∃𝑘 ∈ ℕ (𝑘 · 4) = 𝑁))
92	90, 91	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (4 ∥ 𝑁 ↔ ∃𝑘 ∈ ℕ (𝑘 · 4) = 𝑁))
93	11	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℕ)
94	13	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
95	93, 94	nnexpcld 14392	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℕ)
96	16	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℕ)
97	96, 94	nnexpcld 14392	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) ∈ ℕ)
98	19	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℕ)
99	98, 94	nnexpcld 14392	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐶↑𝑘) ∈ ℕ)
100	95, 97, 99	flt4 27996	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (((𝐴↑𝑘)↑4) + ((𝐵↑𝑘)↑4)) ≠ ((𝐶↑𝑘)↑4))
101	54	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
102		4nn0 12628	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ₀
103	102	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 4 ∈ ℕ₀)
104	101, 103, 94	expmuld 14295	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑘 · 4)) = ((𝐴↑𝑘)↑4))
105	16	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐵 ∈ ℕ)
106	105	nncnd 12354	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐵 ∈ ℂ)
107	106	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
108	107, 103, 94	expmuld 14295	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐵↑(𝑘 · 4)) = ((𝐵↑𝑘)↑4))
109	104, 108	oveq12d 7438	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → ((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) = (((𝐴↑𝑘)↑4) + ((𝐵↑𝑘)↑4)))
110	64	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
111	110, 103, 94	expmuld 14295	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐶↑(𝑘 · 4)) = ((𝐶↑𝑘)↑4))
112	100, 109, 111	3netr4d 3032	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → ((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) ≠ (𝐶↑(𝑘 · 4)))
113		oveq2 7428	. . . . . . . . 9 ⊢ ((𝑘 · 4) = 𝑁 → (𝐴↑(𝑘 · 4)) = (𝐴↑𝑁))
114		oveq2 7428	. . . . . . . . 9 ⊢ ((𝑘 · 4) = 𝑁 → (𝐵↑(𝑘 · 4)) = (𝐵↑𝑁))
115	113, 114	oveq12d 7438	. . . . . . . 8 ⊢ ((𝑘 · 4) = 𝑁 → ((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) = ((𝐴↑𝑁) + (𝐵↑𝑁)))
116		oveq2 7428	. . . . . . . 8 ⊢ ((𝑘 · 4) = 𝑁 → (𝐶↑(𝑘 · 4)) = (𝐶↑𝑁))
117	115, 116	neeq12d 3016	. . . . . . 7 ⊢ ((𝑘 · 4) = 𝑁 → (((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) ≠ (𝐶↑(𝑘 · 4)) ↔ ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
118	112, 117	syl5ibcom 248	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → ((𝑘 · 4) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
119	118	rexlimdva 3163	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∃𝑘 ∈ ℕ (𝑘 · 4) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
120	92, 119	sylbid 243	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (4 ∥ 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
121	87, 120	syld 48	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑁 = (2↑𝑛) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
122	121	rexlimdva 3163	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℕ₀ 𝑁 = (2↑𝑛) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
123		fltoprmlem1 27998	. . 3 ⊢ (𝑁 ∈ ℕ → (∃𝑟 ∈ ℙ (2 < 𝑟 ∧ 𝑟 ∥ 𝑁) ∨ ∃𝑛 ∈ ℕ₀ 𝑁 = (2↑𝑛)))
124	5, 123	syl 18	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℙ (2 < 𝑟 ∧ 𝑟 ∥ 𝑁) ∨ ∃𝑛 ∈ ℕ₀ 𝑁 = (2↑𝑛)))
125	81, 122, 124	mpjaod 874	1 ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 class class class wbr 5102 ‘cfv 6538 (class class class)co 7420 ℂcc 11201 + caddc 11206 · cmul 11208 < clt 11346 ℕcn 12338 2c2 12400 3c3 12401 4c4 12402 ℕ₀cn0 12609 ℤ_≥cuz 12968 ↑cexp 14207 ∥ cdvds 16427 ℙcprime 16851

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-2o 8480 df-er 8720 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-sup 9437 df-inf 9438 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-3 12409 df-4 12410 df-n0 12610 df-z 12697 df-uz 12969 df-q 13079 df-rp 13124 df-fz 13643 df-fl 13935 df-mod 14013 df-seq 14148 df-exp 14208 df-cj 15271 df-re 15272 df-im 15273 df-sqrt 15407 df-abs 15408 df-dvds 16428 df-gcd 16670 df-prm 16852 df-numer 16916 df-denom 16917 df-pc 17020

This theorem is used by: fltoprmgt3 28001

W3C validator