Metamath Proof Explorer

Theorem fltabcoprm

Description: A counterexample to FLT with A , C coprime also has A , B coprime. Converse of fltaccoprm . (Contributed by SN, 22-Aug-2024)

Ref Expression
Hypotheses fltabcoprm.a 
|- ( ph -> A e. NN )
fltabcoprm.b 
|- ( ph -> B e. NN )
fltabcoprm.c 
|- ( ph -> C e. NN )
fltabcoprm.2 
|- ( ph -> ( A gcd C ) = 1 )
fltabcoprm.3 
|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
Assertion fltabcoprm 
|- ( ph -> ( A gcd B ) = 1 )

Proof

Step Hyp Ref Expression
1 fltabcoprm.a 
 |-  ( ph -> A e. NN )
2 fltabcoprm.b 
 |-  ( ph -> B e. NN )
3 fltabcoprm.c 
 |-  ( ph -> C e. NN )
4 fltabcoprm.2 
 |-  ( ph -> ( A gcd C ) = 1 )
5 fltabcoprm.3 
 |-  ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
6 coprmgcdb 
 |-  ( ( A e. NN /\ C e. NN ) -> ( A. i e. NN ( ( i || A /\ i || C ) -> i = 1 ) <-> ( A gcd C ) = 1 ) )
7 1 3 6 syl2anc 
 |-  ( ph -> ( A. i e. NN ( ( i || A /\ i || C ) -> i = 1 ) <-> ( A gcd C ) = 1 ) )
8 4 7 mpbird 
 |-  ( ph -> A. i e. NN ( ( i || A /\ i || C ) -> i = 1 ) )
9 simprl 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> i || A )
10 simplr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> i e. NN )
11 10 nnsqcld 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( i ^ 2 ) e. NN )
12 11 nnzd 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( i ^ 2 ) e. ZZ )
13 1 ad2antrr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> A e. NN )
14 13 nnsqcld 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( A ^ 2 ) e. NN )
15 14 nnzd 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( A ^ 2 ) e. ZZ )
16 2 ad2antrr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> B e. NN )
17 16 nnsqcld 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( B ^ 2 ) e. NN )
18 17 nnzd 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( B ^ 2 ) e. ZZ )
19 dvdssqlem 
 |-  ( ( i e. NN /\ A e. NN ) -> ( i || A <-> ( i ^ 2 ) || ( A ^ 2 ) ) )
20 10 13 19 syl2anc 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( i || A <-> ( i ^ 2 ) || ( A ^ 2 ) ) )
21 9 20 mpbid 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( i ^ 2 ) || ( A ^ 2 ) )
22 simprr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> i || B )
23 dvdssqlem 
 |-  ( ( i e. NN /\ B e. NN ) -> ( i || B <-> ( i ^ 2 ) || ( B ^ 2 ) ) )
24 10 16 23 syl2anc 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( i || B <-> ( i ^ 2 ) || ( B ^ 2 ) ) )
25 22 24 mpbid 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( i ^ 2 ) || ( B ^ 2 ) )
26 12 15 18 21 25 dvds2addd 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( i ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) )
27 5 ad2antrr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
28 26 27 breqtrd 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( i ^ 2 ) || ( C ^ 2 ) )
29 3 ad2antrr 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> C e. NN )
30 dvdssqlem 
 |-  ( ( i e. NN /\ C e. NN ) -> ( i || C <-> ( i ^ 2 ) || ( C ^ 2 ) ) )
31 10 29 30 syl2anc 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( i || C <-> ( i ^ 2 ) || ( C ^ 2 ) ) )
32 28 31 mpbird 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> i || C )
33 9 32 jca 
 |-  ( ( ( ph /\ i e. NN ) /\ ( i || A /\ i || B ) ) -> ( i || A /\ i || C ) )
34 33 ex 
 |-  ( ( ph /\ i e. NN ) -> ( ( i || A /\ i || B ) -> ( i || A /\ i || C ) ) )
35 34 imim1d 
 |-  ( ( ph /\ i e. NN ) -> ( ( ( i || A /\ i || C ) -> i = 1 ) -> ( ( i || A /\ i || B ) -> i = 1 ) ) )
36 35 ralimdva 
 |-  ( ph -> ( A. i e. NN ( ( i || A /\ i || C ) -> i = 1 ) -> A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) ) )
37 8 36 mpd 
 |-  ( ph -> A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) )
38 coprmgcdb 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) <-> ( A gcd B ) = 1 ) )
39 1 2 38 syl2anc 
 |-  ( ph -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) <-> ( A gcd B ) = 1 ) )
40 37 39 mpbid 
 |-  ( ph -> ( A gcd B ) = 1 )