Theorem ncoprmgcdgt1b

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 greater than 1. (Contributed by AV, 9-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ncoprmgcdne1b	|- ( ( A e. NN /\ B e. NN ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) <-> ( A gcd B ) =/= 1 ) )
2		gcdnncl	|- ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
3		nngt1ne1	|- ( ( A gcd B ) e. NN -> ( 1 < ( A gcd B ) <-> ( A gcd B ) =/= 1 ) )
4	2 3	syl	|- ( ( A e. NN /\ B e. NN ) -> ( 1 < ( A gcd B ) <-> ( A gcd B ) =/= 1 ) )
5	1 4	bitr4d	|- ( ( A e. NN /\ B e. NN ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) <-> 1 < ( A gcd B ) ) )