Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
fltoprm.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
fltoprm.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
fltoprm.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
fltoprm.r ⊢ ( 𝜑 → ∀ 𝑎 ∈ ℕ ∀ 𝑏 ∈ ℕ ∀ 𝑐 ∈ ℕ ∀ 𝑝 ∈ ℙ ( 2 < 𝑝 → ( ( 𝑎 ↑ 𝑝 ) + ( 𝑏 ↑ 𝑝 ) ) ≠ ( 𝑐 ↑ 𝑝 ) ) )
Assertion fltoprm ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) ≠ ( 𝐶 ↑ 𝑁 ) )

Proof

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