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	$$⊢\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$$
Assertion	fltabcoprmex	$$⊢\phi \to {\left(\frac{A}{A\gcd B}\right)}^N+{\left(\frac{B}{A\gcd B}\right)}^N={\left(\frac{C}{A\gcd B}\right)}^N$$

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		gcdnncl	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to A\gcd B\in \mathbb{N}$$
7	1 2 6	syl2anc	$$⊢\phi \to A\gcd B\in \mathbb{N}$$
8	7	nncnd	$$⊢\phi \to A\gcd B\in ℂ$$
9	7	nnne0d	$$⊢\phi \to A\gcd B\ne 0$$
10	1	nncnd	$$⊢\phi \to A\in ℂ$$
11	2	nncnd	$$⊢\phi \to B\in ℂ$$
12	3	nncnd	$$⊢\phi \to C\in ℂ$$
13	8 9 10 11 12 4 5	fltdiv	$$⊢\phi \to {\left(\frac{A}{A\gcd B}\right)}^N+{\left(\frac{B}{A\gcd B}\right)}^N={\left(\frac{C}{A\gcd B}\right)}^N$$