Description: Two positive integers are coprime, i.e. the only positive integer that divides both of them is 1, iff their greatest common divisor is 1. (Contributed by AV, 9-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | coprmgcdb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnz | |
|
2 | nnz | |
|
3 | gcddvds | |
|
4 | 1 2 3 | syl2an | |
5 | simpr | |
|
6 | gcdnncl | |
|
7 | 6 | adantr | |
8 | breq1 | |
|
9 | breq1 | |
|
10 | 8 9 | anbi12d | |
11 | eqeq1 | |
|
12 | 10 11 | imbi12d | |
13 | 12 | rspcv | |
14 | 7 13 | syl | |
15 | 5 14 | mpid | |
16 | 4 15 | mpdan | |
17 | simpl | |
|
18 | 17 | anim1ci | |
19 | 3anass | |
|
20 | 18 19 | sylibr | |
21 | nndvdslegcd | |
|
22 | 20 21 | syl | |
23 | breq2 | |
|
24 | 23 | adantr | |
25 | nnge1 | |
|
26 | nnre | |
|
27 | 1red | |
|
28 | 26 27 | letri3d | |
29 | 28 | biimprd | |
30 | 25 29 | mpan2d | |
31 | 30 | adantl | |
32 | 24 31 | sylbid | |
33 | 32 | adantll | |
34 | 22 33 | syld | |
35 | 34 | ralrimiva | |
36 | 35 | ex | |
37 | 16 36 | impbid | |