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 )