This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to A \in ℕ$
		fltabcoprmex.b	$⊢ φ \to B \in ℕ$
		fltabcoprmex.c	$⊢ φ \to C \in ℕ$
		fltabcoprmex.n	$⊢ φ \to N \in ℕ_{0}$
		fltabcoprmex.1	$⊢ φ \to A^{N} + B^{N} = C^{N}$
	Assertion	fltabcoprmex	$⊢ φ \to {(\frac{A}{A \gcd B})}^{N} + {(\frac{B}{A \gcd B})}^{N} = {(\frac{C}{A \gcd B})}^{N}$

Proof

Step	Hyp	Ref	Expression
1		fltabcoprmex.a	$⊢ φ \to A \in ℕ$
2		fltabcoprmex.b	$⊢ φ \to B \in ℕ$
3		fltabcoprmex.c	$⊢ φ \to C \in ℕ$
4		fltabcoprmex.n	$⊢ φ \to N \in ℕ_{0}$
5		fltabcoprmex.1	$⊢ φ \to A^{N} + B^{N} = C^{N}$
6		gcdnncl	$⊢ (A \in ℕ \land B \in ℕ) \to A \gcd B \in ℕ$
7	1 2 6	syl2anc	$⊢ φ \to A \gcd B \in ℕ$
8	7	nncnd	$⊢ φ \to A \gcd B \in ℂ$
9	7	nnne0d	$⊢ φ \to A \gcd B \neq 0$
10	1	nncnd	$⊢ φ \to A \in ℂ$
11	2	nncnd	$⊢ φ \to B \in ℂ$
12	3	nncnd	$⊢ φ \to C \in ℂ$
13	8 9 10 11 12 4 5	fltdiv	$⊢ φ \to {(\frac{A}{A \gcd B})}^{N} + {(\frac{B}{A \gcd B})}^{N} = {(\frac{C}{A \gcd B})}^{N}$