Metamath Proof Explorer


Theorem coprmgcdb

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 ABiiAiBi=1AgcdB=1

Proof

Step Hyp Ref Expression
1 nnz AA
2 nnz BB
3 gcddvds ABAgcdBAAgcdBB
4 1 2 3 syl2an ABAgcdBAAgcdBB
5 simpr ABAgcdBAAgcdBBAgcdBAAgcdBB
6 gcdnncl ABAgcdB
7 6 adantr ABAgcdBAAgcdBBAgcdB
8 breq1 i=AgcdBiAAgcdBA
9 breq1 i=AgcdBiBAgcdBB
10 8 9 anbi12d i=AgcdBiAiBAgcdBAAgcdBB
11 eqeq1 i=AgcdBi=1AgcdB=1
12 10 11 imbi12d i=AgcdBiAiBi=1AgcdBAAgcdBBAgcdB=1
13 12 rspcv AgcdBiiAiBi=1AgcdBAAgcdBBAgcdB=1
14 7 13 syl ABAgcdBAAgcdBBiiAiBi=1AgcdBAAgcdBBAgcdB=1
15 5 14 mpid ABAgcdBAAgcdBBiiAiBi=1AgcdB=1
16 4 15 mpdan ABiiAiBi=1AgcdB=1
17 simpl ABAgcdB=1AB
18 17 anim1ci ABAgcdB=1iiAB
19 3anass iABiAB
20 18 19 sylibr ABAgcdB=1iiAB
21 nndvdslegcd iABiAiBiAgcdB
22 20 21 syl ABAgcdB=1iiAiBiAgcdB
23 breq2 AgcdB=1iAgcdBi1
24 23 adantr AgcdB=1iiAgcdBi1
25 nnge1 i1i
26 nnre ii
27 1red i1
28 26 27 letri3d ii=1i11i
29 28 biimprd ii11ii=1
30 25 29 mpan2d ii1i=1
31 30 adantl AgcdB=1ii1i=1
32 24 31 sylbid AgcdB=1iiAgcdBi=1
33 32 adantll ABAgcdB=1iiAgcdBi=1
34 22 33 syld ABAgcdB=1iiAiBi=1
35 34 ralrimiva ABAgcdB=1iiAiBi=1
36 35 ex ABAgcdB=1iiAiBi=1
37 16 36 impbid ABiiAiBi=1AgcdB=1