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 )