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	$$⊢\phi \to A\in \mathbb{N}$$
	fltabcoprmex.b	$$⊢\phi \to B\in \mathbb{N}$$
	fltabcoprmex.c	$$⊢\phi \to C\in \mathbb{N}$$
	fltabcoprmex.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	fltabcoprmex.1	$$⊢\phi \to A^N+B^N=C^N$$
	fltaccoprm.1	$$⊢\phi \to A\gcd B=1$$
Assertion	fltbccoprm	$$⊢\phi \to B\gcd C=1$$

Proof

Step	Hyp	Ref	Expression
1		fltabcoprmex.a	$$⊢\phi \to A\in \mathbb{N}$$
2		fltabcoprmex.b	$$⊢\phi \to B\in \mathbb{N}$$
3		fltabcoprmex.c	$$⊢\phi \to C\in \mathbb{N}$$
4		fltabcoprmex.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		fltabcoprmex.1	$$⊢\phi \to A^N+B^N=C^N$$
6		fltaccoprm.1	$$⊢\phi \to A\gcd B=1$$
7	2 4	nnexpcld	$$⊢\phi \to B^N\in \mathbb{N}$$
8	7	nncnd	$$⊢\phi \to B^N\in ℂ$$
9	1 4	nnexpcld	$$⊢\phi \to A^N\in \mathbb{N}$$
10	9	nncnd	$$⊢\phi \to A^N\in ℂ$$
11	8 10	addcomd	$$⊢\phi \to B^N+A^N=A^N+B^N$$
12	11 5	eqtrd	$$⊢\phi \to B^N+A^N=C^N$$
13	2	nnzd	$$⊢\phi \to B\in \mathbb{Z}$$
14	1	nnzd	$$⊢\phi \to A\in \mathbb{Z}$$
15	13 14	gcdcomd	$$⊢\phi \to B\gcd A=A\gcd B$$
16	15 6	eqtrd	$$⊢\phi \to B\gcd A=1$$
17	2 1 3 4 12 16	fltaccoprm	$$⊢\phi \to B\gcd C=1$$