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 27977

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 16829	. . . . . 6 ⊢ (𝑟 ∈ ℙ → 𝑟 ∈ ℕ)
2		3nn 12403	. . . . . . 7 ⊢ 3 ∈ ℕ
3		fltoprm.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘3))
4		eluznn 13026	. . . . . . 7 ⊢ ((3 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘3)) → 𝑁 ∈ ℕ)
5	2, 3, 4	sylancr 599	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6		nndivides 16412	. . . . . 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 12594	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
14	13	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
15	12, 14	nnexpcld 14369	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℕ)
16		fltoprm.b	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℕ)
17	16	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℕ)
18	17, 14	nnexpcld 14369	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) ∈ ℕ)
19		fltoprm.c	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℕ)
20	19	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℕ)
21	20, 14	nnexpcld 14369	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐶↑𝑘) ∈ ℕ)
22	15, 18, 21	3jca 1146	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝐴↑𝑘) ∈ ℕ ∧ (𝐵↑𝑘) ∈ ℕ ∧ (𝐶↑𝑘) ∈ ℕ))
23	22	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ((𝐴↑𝑘) ∈ ℕ ∧ (𝐵↑𝑘) ∈ ℕ ∧ (𝐶↑𝑘) ∈ ℕ))
24		oveq1 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝐴↑𝑘) → (𝑎↑𝑝) = ((𝐴↑𝑘)↑𝑝))
25	24	oveq1d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝐴↑𝑘) → ((𝑎↑𝑝) + (𝑏↑𝑝)) = (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)))
26	25	neeq1d 3015	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝐴↑𝑘) → (((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝) ↔ (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)))
27	26	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝐴↑𝑘) → ((2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝))))
28	27	ralbidv 3186	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝐴↑𝑘) → (∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝))))
29		oveq1 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝐵↑𝑘) → (𝑏↑𝑝) = ((𝐵↑𝑘)↑𝑝))
30	29	oveq2d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝐵↑𝑘) → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) = (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)))
31	30	neeq1d 3015	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝐵↑𝑘) → ((((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝) ↔ (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝)))
32	31	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝐵↑𝑘) → ((2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝))))
33	32	ralbidv 3186	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝐵↑𝑘) → (∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝))))
34		oveq1 7419	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐶↑𝑘) → (𝑐↑𝑝) = ((𝐶↑𝑘)↑𝑝))
35	34	neeq2d 3016	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐶↑𝑘) → ((((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝) ↔ (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝)))
36	35	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝐶↑𝑘) → ((2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝)) ↔ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
37	36	ralbidv 3186	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝐶↑𝑘) → (∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝)) ↔ ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
38	28, 33, 37	rspc3v 3592	. . . . . . . . . . . . 13 ⊢ (((𝐴↑𝑘) ∈ ℕ ∧ (𝐵↑𝑘) ∈ ℕ ∧ (𝐶↑𝑘) ∈ ℕ) → (∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) → ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
39	23, 38	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → (∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) → ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
40		breq2 5107	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑟 → (2 < 𝑝 ↔ 2 < 𝑟))
41		oveq2 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((𝐴↑𝑘)↑𝑝) = ((𝐴↑𝑘)↑𝑟))
42		oveq2 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((𝐵↑𝑘)↑𝑝) = ((𝐵↑𝑘)↑𝑟))
43	41, 42	oveq12d 7430	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑟 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) = (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)))
44		oveq2 7420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑟 → ((𝐶↑𝑘)↑𝑝) = ((𝐶↑𝑘)↑𝑟))
45	43, 44	neeq12d 3017	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑟 → ((((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝) ↔ (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
46	40, 45	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑟 → ((2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝)) ↔ (2 < 𝑟 → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟))))
47	46	rspcv 3573	. . . . . . . . . . . . . 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 12332	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℂ)
55	54	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
56	1	nnnn0d 12648	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ ℙ → 𝑟 ∈ ℕ₀)
57	56	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → 𝑟 ∈ ℕ₀)
58	57	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑟 ∈ ℕ₀)
59	55, 58, 14	expmuld 14272	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑘 · 𝑟)) = ((𝐴↑𝑘)↑𝑟))
60	16	nncnd 12332	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℂ)
61	60	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
62	61, 58, 14	expmuld 14272	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐵↑(𝑘 · 𝑟)) = ((𝐵↑𝑘)↑𝑟))
63	59, 62	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) = (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)))
64	19	nncnd 12332	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ℂ)
65	64	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
66	65, 58, 14	expmuld 14272	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐶↑(𝑘 · 𝑟)) = ((𝐶↑𝑘)↑𝑟))
67	63, 66	neeq12d 3017	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)) ↔ (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
68	67	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → (((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)) ↔ (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
69	53, 68	mpbird 260	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)))
70		oveq2 7420	. . . . . . . . . . 11 ⊢ ((𝑘 · 𝑟) = 𝑁 → (𝐴↑(𝑘 · 𝑟)) = (𝐴↑𝑁))
71		oveq2 7420	. . . . . . . . . . 11 ⊢ ((𝑘 · 𝑟) = 𝑁 → (𝐵↑(𝑘 · 𝑟)) = (𝐵↑𝑁))
72	70, 71	oveq12d 7430	. . . . . . . . . 10 ⊢ ((𝑘 · 𝑟) = 𝑁 → ((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) = ((𝐴↑𝑁) + (𝐵↑𝑁)))
73		oveq2 7420	. . . . . . . . . 10 ⊢ ((𝑘 · 𝑟) = 𝑁 → (𝐶↑(𝑘 · 𝑟)) = (𝐶↑𝑁))
74	72, 73	neeq12d 3017	. . . . . . . . 9 ⊢ ((𝑘 · 𝑟) = 𝑁 → (((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)) ↔ ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
75	69, 74	syl5ibcom 248	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ((𝑘 · 𝑟) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
76	75	ex 418	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2 < 𝑟 → ((𝑘 · 𝑟) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
77	76	com23 87	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · 𝑟) = 𝑁 → (2 < 𝑟 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
78	77	rexlimdva 3164	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (∃𝑘 ∈ ℕ (𝑘 · 𝑟) = 𝑁 → (2 < 𝑟 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
79	7, 78	sylbid 243	. . . 4 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (𝑟 ∥ 𝑁 → (2 < 𝑟 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
80	79	impcomd 417	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → ((2 < 𝑟 ∧ 𝑟 ∥ 𝑁) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
81	80	rexlimdva 3164	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℙ (2 < 𝑟 ∧ 𝑟 ∥ 𝑁) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
82	3	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 𝑁 ∈ (ℤ_≥‘3))
83		simplr 781	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 𝑛 ∈ ℕ₀)
84		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 𝑁 = (2↑𝑛))
85		fltoprmlem2 27976	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑛 ∈ ℕ₀ ∧ 𝑁 = (2↑𝑛)) → 4 ∥ 𝑁)
86	82, 83, 84, 85	syl3anc 1398	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 4 ∥ 𝑁)
87	86	ex 418	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑁 = (2↑𝑛) → 4 ∥ 𝑁))
88		4nn 12407	. . . . . . . 8 ⊢ 4 ∈ ℕ
89	5, 88	jctil 529	. . . . . . 7 ⊢ (𝜑 → (4 ∈ ℕ ∧ 𝑁 ∈ ℕ))
90	89	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (4 ∈ ℕ ∧ 𝑁 ∈ ℕ))
91		nndivides 16412	. . . . . 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 14369	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℕ)
96	16	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℕ)
97	96, 94	nnexpcld 14369	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) ∈ ℕ)
98	19	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℕ)
99	98, 94	nnexpcld 14369	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐶↑𝑘) ∈ ℕ)
100	95, 97, 99	flt4 27973	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (((𝐴↑𝑘)↑4) + ((𝐵↑𝑘)↑4)) ≠ ((𝐶↑𝑘)↑4))
101	54	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
102		4nn0 12606	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ₀
103	102	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 4 ∈ ℕ₀)
104	101, 103, 94	expmuld 14272	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑘 · 4)) = ((𝐴↑𝑘)↑4))
105	16	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐵 ∈ ℕ)
106	105	nncnd 12332	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐵 ∈ ℂ)
107	106	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
108	107, 103, 94	expmuld 14272	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐵↑(𝑘 · 4)) = ((𝐵↑𝑘)↑4))
109	104, 108	oveq12d 7430	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → ((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) = (((𝐴↑𝑘)↑4) + ((𝐵↑𝑘)↑4)))
110	64	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
111	110, 103, 94	expmuld 14272	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐶↑(𝑘 · 4)) = ((𝐶↑𝑘)↑4))
112	100, 109, 111	3netr4d 3033	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → ((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) ≠ (𝐶↑(𝑘 · 4)))
113		oveq2 7420	. . . . . . . . 9 ⊢ ((𝑘 · 4) = 𝑁 → (𝐴↑(𝑘 · 4)) = (𝐴↑𝑁))
114		oveq2 7420	. . . . . . . . 9 ⊢ ((𝑘 · 4) = 𝑁 → (𝐵↑(𝑘 · 4)) = (𝐵↑𝑁))
115	113, 114	oveq12d 7430	. . . . . . . 8 ⊢ ((𝑘 · 4) = 𝑁 → ((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) = ((𝐴↑𝑁) + (𝐵↑𝑁)))
116		oveq2 7420	. . . . . . . 8 ⊢ ((𝑘 · 4) = 𝑁 → (𝐶↑(𝑘 · 4)) = (𝐶↑𝑁))
117	115, 116	neeq12d 3017	. . . . . . 7 ⊢ ((𝑘 · 4) = 𝑁 → (((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) ≠ (𝐶↑(𝑘 · 4)) ↔ ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
118	112, 117	syl5ibcom 248	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → ((𝑘 · 4) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
119	118	rexlimdva 3164	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∃𝑘 ∈ ℕ (𝑘 · 4) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
120	92, 119	sylbid 243	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (4 ∥ 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
121	87, 120	syld 48	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑁 = (2↑𝑛) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
122	121	rexlimdva 3164	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℕ₀ 𝑁 = (2↑𝑛) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
123		fltoprmlem1 27975	. . 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 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 class class class wbr 5103 ‘cfv 6531 (class class class)co 7412 ℂcc 11179 + caddc 11184 · cmul 11186 < clt 11324 ℕcn 12316 2c2 12378 3c3 12379 4c4 12380 ℕ₀cn0 12587 ℤ_≥cuz 12946 ↑cexp 14184 ∥ cdvds 16402 ℙcprime 16826

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-2o 8461 df-er 8701 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-sup 9418 df-inf 9419 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-n0 12588 df-z 12675 df-uz 12947 df-q 13057 df-rp 13102 df-fz 13621 df-fl 13912 df-mod 13990 df-seq 14125 df-exp 14185 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-dvds 16403 df-gcd 16645 df-prm 16827 df-numer 16891 df-denom 16892 df-pc 16995

This theorem is used by: fltoprmgt3 27978

W3C validator