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

Metamath Proof Explorer

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 )