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 | |
|
fltabcoprm.b | |
||
fltabcoprm.c | |
||
fltabcoprm.2 | |
||
fltabcoprm.3 | |
||
Assertion | fltabcoprm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fltabcoprm.a | |
|
2 | fltabcoprm.b | |
|
3 | fltabcoprm.c | |
|
4 | fltabcoprm.2 | |
|
5 | fltabcoprm.3 | |
|
6 | coprmgcdb | |
|
7 | 1 3 6 | syl2anc | |
8 | 4 7 | mpbird | |
9 | simprl | |
|
10 | simplr | |
|
11 | 10 | nnsqcld | |
12 | 11 | nnzd | |
13 | 1 | ad2antrr | |
14 | 13 | nnsqcld | |
15 | 14 | nnzd | |
16 | 2 | ad2antrr | |
17 | 16 | nnsqcld | |
18 | 17 | nnzd | |
19 | dvdssqlem | |
|
20 | 10 13 19 | syl2anc | |
21 | 9 20 | mpbid | |
22 | simprr | |
|
23 | dvdssqlem | |
|
24 | 10 16 23 | syl2anc | |
25 | 22 24 | mpbid | |
26 | 12 15 18 21 25 | dvds2addd | |
27 | 5 | ad2antrr | |
28 | 26 27 | breqtrd | |
29 | 3 | ad2antrr | |
30 | dvdssqlem | |
|
31 | 10 29 30 | syl2anc | |
32 | 28 31 | mpbird | |
33 | 9 32 | jca | |
34 | 33 | ex | |
35 | 34 | imim1d | |
36 | 35 | ralimdva | |
37 | 8 36 | mpd | |
38 | coprmgcdb | |
|
39 | 1 2 38 | syl2anc | |
40 | 37 39 | mpbid | |