Theorem fltabcoprmex

Description: A counterexample to FLT implies a counterexample to FLT with A , B (assigned to A / ( A gcd B ) and B / ( A gcd B ) ) coprime (by divgcdcoprm0 ). (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 ) )
Assertion	fltabcoprmex	|- ( ph -> ( ( ( A / ( A gcd B ) ) ^ N ) + ( ( B / ( A gcd B ) ) ^ N ) ) = ( ( C / ( A gcd B ) ) ^ N ) )

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		gcdnncl	|- ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
7	1 2 6	syl2anc	|- ( ph -> ( A gcd B ) e. NN )
8	7	nncnd	|- ( ph -> ( A gcd B ) e. CC )
9	7	nnne0d	|- ( ph -> ( A gcd B ) =/= 0 )
10	1	nncnd	|- ( ph -> A e. CC )
11	2	nncnd	|- ( ph -> B e. CC )
12	3	nncnd	|- ( ph -> C e. CC )
13	8 9 10 11 12 4 5	fltdiv	|- ( ph -> ( ( ( A / ( A gcd B ) ) ^ N ) + ( ( B / ( A gcd B ) ) ^ N ) ) = ( ( C / ( A gcd B ) ) ^ N ) )