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	|- ( ph -> A e. NN )
	fltabcoprmex.b	|- ( ph -> B e. NN )
	fltabcoprmex.c	|- ( ph -> C e. NN )
	fltabcoprmex.n	|- ( ph -> N e. NN0 )
	fltabcoprmex.1	|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
	fltaccoprm.1	|- ( ph -> ( A gcd B ) = 1 )
Assertion	fltbccoprm	|- ( ph -> ( B gcd C ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		fltabcoprmex.a	|- ( ph -> A e. NN )
2		fltabcoprmex.b	|- ( ph -> B e. NN )
3		fltabcoprmex.c	|- ( ph -> C e. NN )
4		fltabcoprmex.n	|- ( ph -> N e. NN0 )
5		fltabcoprmex.1	|- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) )
6		fltaccoprm.1	|- ( ph -> ( A gcd B ) = 1 )
7	2 4	nnexpcld	|- ( ph -> ( B ^ N ) e. NN )
8	7	nncnd	|- ( ph -> ( B ^ N ) e. CC )
9	1 4	nnexpcld	|- ( ph -> ( A ^ N ) e. NN )
10	9	nncnd	|- ( ph -> ( A ^ N ) e. CC )
11	8 10	addcomd	|- ( ph -> ( ( B ^ N ) + ( A ^ N ) ) = ( ( A ^ N ) + ( B ^ N ) ) )
12	11 5	eqtrd	|- ( ph -> ( ( B ^ N ) + ( A ^ N ) ) = ( C ^ N ) )
13	2	nnzd	|- ( ph -> B e. ZZ )
14	1	nnzd	|- ( ph -> A e. ZZ )
15	13 14	gcdcomd	|- ( ph -> ( B gcd A ) = ( A gcd B ) )
16	15 6	eqtrd	|- ( ph -> ( B gcd A ) = 1 )
17	2 1 3 4 12 16	fltaccoprm	|- ( ph -> ( B gcd C ) = 1 )