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 φA
fltabcoprm.b φB
fltabcoprm.c φC
fltabcoprm.2 φAgcdC=1
fltabcoprm.3 φA2+B2=C2
Assertion fltabcoprm φAgcdB=1

Proof

Step Hyp Ref Expression
1 fltabcoprm.a φA
2 fltabcoprm.b φB
3 fltabcoprm.c φC
4 fltabcoprm.2 φAgcdC=1
5 fltabcoprm.3 φA2+B2=C2
6 coprmgcdb ACiiAiCi=1AgcdC=1
7 1 3 6 syl2anc φiiAiCi=1AgcdC=1
8 4 7 mpbird φiiAiCi=1
9 simprl φiiAiBiA
10 simplr φiiAiBi
11 10 nnsqcld φiiAiBi2
12 11 nnzd φiiAiBi2
13 1 ad2antrr φiiAiBA
14 13 nnsqcld φiiAiBA2
15 14 nnzd φiiAiBA2
16 2 ad2antrr φiiAiBB
17 16 nnsqcld φiiAiBB2
18 17 nnzd φiiAiBB2
19 dvdssqlem iAiAi2A2
20 10 13 19 syl2anc φiiAiBiAi2A2
21 9 20 mpbid φiiAiBi2A2
22 simprr φiiAiBiB
23 dvdssqlem iBiBi2B2
24 10 16 23 syl2anc φiiAiBiBi2B2
25 22 24 mpbid φiiAiBi2B2
26 12 15 18 21 25 dvds2addd φiiAiBi2A2+B2
27 5 ad2antrr φiiAiBA2+B2=C2
28 26 27 breqtrd φiiAiBi2C2
29 3 ad2antrr φiiAiBC
30 dvdssqlem iCiCi2C2
31 10 29 30 syl2anc φiiAiBiCi2C2
32 28 31 mpbird φiiAiBiC
33 9 32 jca φiiAiBiAiC
34 33 ex φiiAiBiAiC
35 34 imim1d φiiAiCi=1iAiBi=1
36 35 ralimdva φiiAiCi=1iiAiBi=1
37 8 36 mpd φiiAiBi=1
38 coprmgcdb ABiiAiBi=1AgcdB=1
39 1 2 38 syl2anc φiiAiBi=1AgcdB=1
40 37 39 mpbid φAgcdB=1