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 28025

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 16878	. . . . . 6 ⊢ (𝑟 ∈ ℙ → 𝑟 ∈ ℕ)
2		3nn 12449	. . . . . . 7 ⊢ 3 ∈ ℕ
3		fltoprm.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘3))
4		eluznn 13072	. . . . . . 7 ⊢ ((3 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘3)) → 𝑁 ∈ ℕ)
5	2, 3, 4	sylancr 599	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6		nndivides 16461	. . . . . 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 12640	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
14	13	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
15	12, 14	nnexpcld 14416	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℕ)
16		fltoprm.b	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℕ)
17	16	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℕ)
18	17, 14	nnexpcld 14416	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) ∈ ℕ)
19		fltoprm.c	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ℕ)
20	19	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℕ)
21	20, 14	nnexpcld 14416	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐶↑𝑘) ∈ ℕ)
22	15, 18, 21	3jca 1146	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝐴↑𝑘) ∈ ℕ ∧ (𝐵↑𝑘) ∈ ℕ ∧ (𝐶↑𝑘) ∈ ℕ))
23	22	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ((𝐴↑𝑘) ∈ ℕ ∧ (𝐵↑𝑘) ∈ ℕ ∧ (𝐶↑𝑘) ∈ ℕ))
24		oveq1 7450	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝐴↑𝑘) → (𝑎↑𝑝) = ((𝐴↑𝑘)↑𝑝))
25	24	oveq1d 7458	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝐴↑𝑘) → ((𝑎↑𝑝) + (𝑏↑𝑝)) = (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)))
26	25	neeq1d 3018	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝐴↑𝑘) → (((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝) ↔ (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)))
27	26	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝐴↑𝑘) → ((2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝))))
28	27	ralbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝐴↑𝑘) → (∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝))))
29		oveq1 7450	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝐵↑𝑘) → (𝑏↑𝑝) = ((𝐵↑𝑘)↑𝑝))
30	29	oveq2d 7459	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝐵↑𝑘) → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) = (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)))
31	30	neeq1d 3018	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝐵↑𝑘) → ((((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝) ↔ (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝)))
32	31	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝐵↑𝑘) → ((2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝))))
33	32	ralbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝐵↑𝑘) → (∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) ↔ ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝))))
34		oveq1 7450	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐶↑𝑘) → (𝑐↑𝑝) = ((𝐶↑𝑘)↑𝑝))
35	34	neeq2d 3019	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐶↑𝑘) → ((((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝) ↔ (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝)))
36	35	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝐶↑𝑘) → ((2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝)) ↔ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
37	36	ralbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝐶↑𝑘) → (∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ (𝑐↑𝑝)) ↔ ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
38	28, 33, 37	rspc3v 3595	. . . . . . . . . . . . 13 ⊢ (((𝐴↑𝑘) ∈ ℕ ∧ (𝐵↑𝑘) ∈ ℕ ∧ (𝐶↑𝑘) ∈ ℕ) → (∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) → ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
39	23, 38	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → (∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)) → ∀𝑝 ∈ ℙ (2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝))))
40		breq2 5110	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑟 → (2 < 𝑝 ↔ 2 < 𝑟))
41		oveq2 7451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((𝐴↑𝑘)↑𝑝) = ((𝐴↑𝑘)↑𝑟))
42		oveq2 7451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → ((𝐵↑𝑘)↑𝑝) = ((𝐵↑𝑘)↑𝑟))
43	41, 42	oveq12d 7461	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑟 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) = (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)))
44		oveq2 7451	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑟 → ((𝐶↑𝑘)↑𝑝) = ((𝐶↑𝑘)↑𝑟))
45	43, 44	neeq12d 3020	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑟 → ((((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝) ↔ (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
46	40, 45	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑟 → ((2 < 𝑝 → (((𝐴↑𝑘)↑𝑝) + ((𝐵↑𝑘)↑𝑝)) ≠ ((𝐶↑𝑘)↑𝑝)) ↔ (2 < 𝑟 → (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟))))
47	46	rspcv 3576	. . . . . . . . . . . . . 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 12378	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℂ)
55	54	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
56	1	nnnn0d 12694	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ ℙ → 𝑟 ∈ ℕ₀)
57	56	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → 𝑟 ∈ ℕ₀)
58	57	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑟 ∈ ℕ₀)
59	55, 58, 14	expmuld 14319	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑘 · 𝑟)) = ((𝐴↑𝑘)↑𝑟))
60	16	nncnd 12378	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℂ)
61	60	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
62	61, 58, 14	expmuld 14319	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐵↑(𝑘 · 𝑟)) = ((𝐵↑𝑘)↑𝑟))
63	59, 62	oveq12d 7461	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) = (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)))
64	19	nncnd 12378	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ ℂ)
65	64	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
66	65, 58, 14	expmuld 14319	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐶↑(𝑘 · 𝑟)) = ((𝐶↑𝑘)↑𝑟))
67	63, 66	neeq12d 3020	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)) ↔ (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
68	67	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → (((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)) ↔ (((𝐴↑𝑘)↑𝑟) + ((𝐵↑𝑘)↑𝑟)) ≠ ((𝐶↑𝑘)↑𝑟)))
69	53, 68	mpbird 260	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)))
70		oveq2 7451	. . . . . . . . . . 11 ⊢ ((𝑘 · 𝑟) = 𝑁 → (𝐴↑(𝑘 · 𝑟)) = (𝐴↑𝑁))
71		oveq2 7451	. . . . . . . . . . 11 ⊢ ((𝑘 · 𝑟) = 𝑁 → (𝐵↑(𝑘 · 𝑟)) = (𝐵↑𝑁))
72	70, 71	oveq12d 7461	. . . . . . . . . 10 ⊢ ((𝑘 · 𝑟) = 𝑁 → ((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) = ((𝐴↑𝑁) + (𝐵↑𝑁)))
73		oveq2 7451	. . . . . . . . . 10 ⊢ ((𝑘 · 𝑟) = 𝑁 → (𝐶↑(𝑘 · 𝑟)) = (𝐶↑𝑁))
74	72, 73	neeq12d 3020	. . . . . . . . 9 ⊢ ((𝑘 · 𝑟) = 𝑁 → (((𝐴↑(𝑘 · 𝑟)) + (𝐵↑(𝑘 · 𝑟))) ≠ (𝐶↑(𝑘 · 𝑟)) ↔ ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
75	69, 74	syl5ibcom 248	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) ∧ 2 < 𝑟) → ((𝑘 · 𝑟) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
76	75	ex 418	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2 < 𝑟 → ((𝑘 · 𝑟) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
77	76	com23 87	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · 𝑟) = 𝑁 → (2 < 𝑟 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
78	77	rexlimdva 3167	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (∃𝑘 ∈ ℕ (𝑘 · 𝑟) = 𝑁 → (2 < 𝑟 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
79	7, 78	sylbid 243	. . . 4 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (𝑟 ∥ 𝑁 → (2 < 𝑟 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))))
80	79	impcomd 417	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → ((2 < 𝑟 ∧ 𝑟 ∥ 𝑁) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
81	80	rexlimdva 3167	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℙ (2 < 𝑟 ∧ 𝑟 ∥ 𝑁) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
82	3	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 𝑁 ∈ (ℤ_≥‘3))
83		simplr 781	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 𝑛 ∈ ℕ₀)
84		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 𝑁 = (2↑𝑛))
85		fltoprmlem2 28024	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑛 ∈ ℕ₀ ∧ 𝑁 = (2↑𝑛)) → 4 ∥ 𝑁)
86	82, 83, 84, 85	syl3anc 1399	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑁 = (2↑𝑛)) → 4 ∥ 𝑁)
87	86	ex 418	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑁 = (2↑𝑛) → 4 ∥ 𝑁))
88		4nn 12453	. . . . . . . 8 ⊢ 4 ∈ ℕ
89	5, 88	jctil 529	. . . . . . 7 ⊢ (𝜑 → (4 ∈ ℕ ∧ 𝑁 ∈ ℕ))
90	89	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (4 ∈ ℕ ∧ 𝑁 ∈ ℕ))
91		nndivides 16461	. . . . . 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 14416	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℕ)
96	16	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℕ)
97	96, 94	nnexpcld 14416	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) ∈ ℕ)
98	19	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℕ)
99	98, 94	nnexpcld 14416	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐶↑𝑘) ∈ ℕ)
100	95, 97, 99	flt4 28021	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (((𝐴↑𝑘)↑4) + ((𝐵↑𝑘)↑4)) ≠ ((𝐶↑𝑘)↑4))
101	54	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
102		4nn0 12652	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ₀
103	102	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 4 ∈ ℕ₀)
104	101, 103, 94	expmuld 14319	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑘 · 4)) = ((𝐴↑𝑘)↑4))
105	16	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐵 ∈ ℕ)
106	105	nncnd 12378	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐵 ∈ ℂ)
107	106	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
108	107, 103, 94	expmuld 14319	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐵↑(𝑘 · 4)) = ((𝐵↑𝑘)↑4))
109	104, 108	oveq12d 7461	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → ((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) = (((𝐴↑𝑘)↑4) + ((𝐵↑𝑘)↑4)))
110	64	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
111	110, 103, 94	expmuld 14319	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → (𝐶↑(𝑘 · 4)) = ((𝐶↑𝑘)↑4))
112	100, 109, 111	3netr4d 3036	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → ((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) ≠ (𝐶↑(𝑘 · 4)))
113		oveq2 7451	. . . . . . . . 9 ⊢ ((𝑘 · 4) = 𝑁 → (𝐴↑(𝑘 · 4)) = (𝐴↑𝑁))
114		oveq2 7451	. . . . . . . . 9 ⊢ ((𝑘 · 4) = 𝑁 → (𝐵↑(𝑘 · 4)) = (𝐵↑𝑁))
115	113, 114	oveq12d 7461	. . . . . . . 8 ⊢ ((𝑘 · 4) = 𝑁 → ((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) = ((𝐴↑𝑁) + (𝐵↑𝑁)))
116		oveq2 7451	. . . . . . . 8 ⊢ ((𝑘 · 4) = 𝑁 → (𝐶↑(𝑘 · 4)) = (𝐶↑𝑁))
117	115, 116	neeq12d 3020	. . . . . . 7 ⊢ ((𝑘 · 4) = 𝑁 → (((𝐴↑(𝑘 · 4)) + (𝐵↑(𝑘 · 4))) ≠ (𝐶↑(𝑘 · 4)) ↔ ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
118	112, 117	syl5ibcom 248	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑘 ∈ ℕ) → ((𝑘 · 4) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
119	118	rexlimdva 3167	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∃𝑘 ∈ ℕ (𝑘 · 4) = 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
120	92, 119	sylbid 243	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (4 ∥ 𝑁 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
121	87, 120	syld 48	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑁 = (2↑𝑛) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
122	121	rexlimdva 3167	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℕ₀ 𝑁 = (2↑𝑛) → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁)))
123		fltoprmlem1 28023	. . 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 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 class class class wbr 5106 ‘cfv 6558 (class class class)co 7443 ℂcc 11225 + caddc 11230 · cmul 11232 < clt 11370 ℕcn 12362 2c2 12424 3c3 12425 4c4 12426 ℕ₀cn0 12633 ℤ_≥cuz 12992 ↑cexp 14231 ∥ cdvds 16451 ℙcprime 16875

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-2o 8505 df-er 8745 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-sup 9461 df-inf 9462 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-n0 12634 df-z 12721 df-uz 12993 df-q 13103 df-rp 13148 df-fz 13667 df-fl 13959 df-mod 14037 df-seq 14172 df-exp 14232 df-cj 15295 df-re 15296 df-im 15297 df-sqrt 15431 df-abs 15432 df-dvds 16452 df-gcd 16694 df-prm 16876 df-numer 16940 df-denom 16941 df-pc 17044

This theorem is used by: fltoprmgt3 28026

W3C validator