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 
|- ( ( A e. NN /\ B e. NN ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) <-> ( A gcd B ) = 1 ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( A e. NN -> A e. ZZ )
2 nnz 
 |-  ( B e. NN -> B e. ZZ )
3 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
4 1 2 3 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
5 simpr 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
6 gcdnncl 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
7 6 adantr 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) -> ( A gcd B ) e. NN )
8 breq1 
 |-  ( i = ( A gcd B ) -> ( i || A <-> ( A gcd B ) || A ) )
9 breq1 
 |-  ( i = ( A gcd B ) -> ( i || B <-> ( A gcd B ) || B ) )
10 8 9 anbi12d 
 |-  ( i = ( A gcd B ) -> ( ( i || A /\ i || B ) <-> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) )
11 eqeq1 
 |-  ( i = ( A gcd B ) -> ( i = 1 <-> ( A gcd B ) = 1 ) )
12 10 11 imbi12d 
 |-  ( i = ( A gcd B ) -> ( ( ( i || A /\ i || B ) -> i = 1 ) <-> ( ( ( A gcd B ) || A /\ ( A gcd B ) || B ) -> ( A gcd B ) = 1 ) ) )
13 12 rspcv 
 |-  ( ( A gcd B ) e. NN -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) -> ( ( ( A gcd B ) || A /\ ( A gcd B ) || B ) -> ( A gcd B ) = 1 ) ) )
14 7 13 syl 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) -> ( ( ( A gcd B ) || A /\ ( A gcd B ) || B ) -> ( A gcd B ) = 1 ) ) )
15 5 14 mpid 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) -> ( A gcd B ) = 1 ) )
16 4 15 mpdan 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) -> ( A gcd B ) = 1 ) )
17 simpl 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> ( A e. NN /\ B e. NN ) )
18 17 anim1ci 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) /\ i e. NN ) -> ( i e. NN /\ ( A e. NN /\ B e. NN ) ) )
19 3anass 
 |-  ( ( i e. NN /\ A e. NN /\ B e. NN ) <-> ( i e. NN /\ ( A e. NN /\ B e. NN ) ) )
20 18 19 sylibr 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) /\ i e. NN ) -> ( i e. NN /\ A e. NN /\ B e. NN ) )
21 nndvdslegcd 
 |-  ( ( i e. NN /\ A e. NN /\ B e. NN ) -> ( ( i || A /\ i || B ) -> i <_ ( A gcd B ) ) )
22 20 21 syl 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) /\ i e. NN ) -> ( ( i || A /\ i || B ) -> i <_ ( A gcd B ) ) )
23 breq2 
 |-  ( ( A gcd B ) = 1 -> ( i <_ ( A gcd B ) <-> i <_ 1 ) )
24 23 adantr 
 |-  ( ( ( A gcd B ) = 1 /\ i e. NN ) -> ( i <_ ( A gcd B ) <-> i <_ 1 ) )
25 nnge1 
 |-  ( i e. NN -> 1 <_ i )
26 nnre 
 |-  ( i e. NN -> i e. RR )
27 1red 
 |-  ( i e. NN -> 1 e. RR )
28 26 27 letri3d 
 |-  ( i e. NN -> ( i = 1 <-> ( i <_ 1 /\ 1 <_ i ) ) )
29 28 biimprd 
 |-  ( i e. NN -> ( ( i <_ 1 /\ 1 <_ i ) -> i = 1 ) )
30 25 29 mpan2d 
 |-  ( i e. NN -> ( i <_ 1 -> i = 1 ) )
31 30 adantl 
 |-  ( ( ( A gcd B ) = 1 /\ i e. NN ) -> ( i <_ 1 -> i = 1 ) )
32 24 31 sylbid 
 |-  ( ( ( A gcd B ) = 1 /\ i e. NN ) -> ( i <_ ( A gcd B ) -> i = 1 ) )
33 32 adantll 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) /\ i e. NN ) -> ( i <_ ( A gcd B ) -> i = 1 ) )
34 22 33 syld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) /\ i e. NN ) -> ( ( i || A /\ i || B ) -> i = 1 ) )
35 34 ralrimiva 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( A gcd B ) = 1 ) -> A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) )
36 35 ex 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) = 1 -> A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) ) )
37 16 36 impbid 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) <-> ( A gcd B ) = 1 ) )