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

Metamath Proof Explorer

Theorem fltbccoprm

Description: A counterexample to FLT with A , B coprime also has B , C coprime. Proven from fltaccoprm using commutativity of addition. (Contributed by SN, 20-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 fltabcoprmex.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 fltabcoprmex.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 fltabcoprmex.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 fltabcoprmex.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 fltabcoprmex.1 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
6 fltaccoprm.1 ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
7 2 4 nnexpcld ⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) ∈ ℕ )
8 7 nncnd ⊢ ( 𝜑 → ( 𝐵 ↑ 𝑁 ) ∈ ℂ )
9 1 4 nnexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
10 9 nncnd ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
11 8 10 addcomd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 𝑁 ) + ( 𝐴 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) )
12 11 5 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 𝑁 ) + ( 𝐴 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
13 2 nnzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
14 1 nnzd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
15 13 14 gcdcomd ⊢ ( 𝜑 → ( 𝐵 gcd 𝐴 ) = ( 𝐴 gcd 𝐵 ) )
16 15 6 eqtrd ⊢ ( 𝜑 → ( 𝐵 gcd 𝐴 ) = 1 )
17 2 1 3 4 12 16 fltaccoprm ⊢ ( 𝜑 → ( 𝐵 gcd 𝐶 ) = 1 )