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	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	fltabcoprmex.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	fltabcoprmex.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
	fltabcoprmex.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	fltabcoprmex.1	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
Assertion	fltabcoprmex	⊢ ( 𝜑 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) ) = ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fltabcoprmex.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2		fltabcoprmex.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		fltabcoprmex.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4		fltabcoprmex.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		fltabcoprmex.1	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( 𝐵 ↑ 𝑁 ) ) = ( 𝐶 ↑ 𝑁 ) )
6		gcdnncl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
7	1 2 6	syl2anc	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
8	7	nncnd	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ∈ ℂ )
9	7	nnne0d	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ≠ 0 )
10	1	nncnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
11	2	nncnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
12	3	nncnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
13	8 9 10 11 12 4 5	fltdiv	⊢ ( 𝜑 → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) + ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) ) = ( ( 𝐶 / ( 𝐴 gcd 𝐵 ) ) ↑ 𝑁 ) )