Metamath Proof Explorer

Theorem ncoprmgcdne1b

Description: Two positive integers are not coprime, i.e. there is an integer greater than 1 which divides both integers, iff their greatest common divisor is not 1. See prmdvdsncoprmbd for a version where the existential quantifier is restricted to primes. (Contributed by AV, 9-Aug-2020)

Ref Expression
Assertion ncoprmgcdne1b 
|- ( ( A e. NN /\ B e. NN ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) <-> ( A gcd B ) =/= 1 ) )

Proof

Step Hyp Ref Expression
1 eluz2nn 
 |-  ( i e. ( ZZ>= ` 2 ) -> i e. NN )
2 1 adantr 
 |-  ( ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) -> i e. NN )
3 eluz2b3 
 |-  ( i e. ( ZZ>= ` 2 ) <-> ( i e. NN /\ i =/= 1 ) )
4 neneq 
 |-  ( i =/= 1 -> -. i = 1 )
5 3 4 simplbiim 
 |-  ( i e. ( ZZ>= ` 2 ) -> -. i = 1 )
6 5 anim1ci 
 |-  ( ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) -> ( ( i || A /\ i || B ) /\ -. i = 1 ) )
7 2 6 jca 
 |-  ( ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) -> ( i e. NN /\ ( ( i || A /\ i || B ) /\ -. i = 1 ) ) )
8 neqne 
 |-  ( -. i = 1 -> i =/= 1 )
9 8 anim1ci 
 |-  ( ( -. i = 1 /\ i e. NN ) -> ( i e. NN /\ i =/= 1 ) )
10 9 3 sylibr 
 |-  ( ( -. i = 1 /\ i e. NN ) -> i e. ( ZZ>= ` 2 ) )
11 10 ex 
 |-  ( -. i = 1 -> ( i e. NN -> i e. ( ZZ>= ` 2 ) ) )
12 11 adantl 
 |-  ( ( ( i || A /\ i || B ) /\ -. i = 1 ) -> ( i e. NN -> i e. ( ZZ>= ` 2 ) ) )
13 12 impcom 
 |-  ( ( i e. NN /\ ( ( i || A /\ i || B ) /\ -. i = 1 ) ) -> i e. ( ZZ>= ` 2 ) )
14 13 adantl 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( i e. NN /\ ( ( i || A /\ i || B ) /\ -. i = 1 ) ) ) -> i e. ( ZZ>= ` 2 ) )
15 simprrl 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( i e. NN /\ ( ( i || A /\ i || B ) /\ -. i = 1 ) ) ) -> ( i || A /\ i || B ) )
16 14 15 jca 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( i e. NN /\ ( ( i || A /\ i || B ) /\ -. i = 1 ) ) ) -> ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) )
17 16 ex 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( i e. NN /\ ( ( i || A /\ i || B ) /\ -. i = 1 ) ) -> ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) )
18 7 17 impbid2 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) <-> ( i e. NN /\ ( ( i || A /\ i || B ) /\ -. i = 1 ) ) ) )
19 18 rexbidv2 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) <-> E. i e. NN ( ( i || A /\ i || B ) /\ -. i = 1 ) ) )
20 rexanali 
 |-  ( E. i e. NN ( ( i || A /\ i || B ) /\ -. i = 1 ) <-> -. A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) )
21 20 a1i 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. i e. NN ( ( i || A /\ i || B ) /\ -. i = 1 ) <-> -. A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) ) )
22 coprmgcdb 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) <-> ( A gcd B ) = 1 ) )
23 22 necon3bbid 
 |-  ( ( A e. NN /\ B e. NN ) -> ( -. A. i e. NN ( ( i || A /\ i || B ) -> i = 1 ) <-> ( A gcd B ) =/= 1 ) )
24 19 21 23 3bitrd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) <-> ( A gcd B ) =/= 1 ) )