This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fltabcoprmex

Description: A counterexample to FLT implies a counterexample to FLT with A , B (assigned to A / ( A gcd B ) and B / ( A gcd B ) ) coprime (by divgcdcoprm0 ). (Contributed by SN, 20-Aug-2024)

Ref Expression
Hypotheses fltabcoprmex.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
fltabcoprmex.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
fltabcoprmex.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
fltabcoprmex.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
fltabcoprmex.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
Assertion fltabcoprmex ( 𝜑 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) ) = ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fltabcoprmex.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 fltabcoprmex.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 fltabcoprmex.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 fltabcoprmex.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 fltabcoprmex.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
6 gcdnncl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
7 1 2 6 syl2anc ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
8 7 nncnd ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℂ )
9 7 nnne0d ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ≠ 0 )
10 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
11 2 nncnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
12 3 nncnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
13 8 9 10 11 12 4 5 fltdiv ⊢ ( 𝜑 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) ) = ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) )