This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ ℕ ∧ B ∈ ℕ → ∃ i ∈ ℤ ≥ 2 i ∥ A ∧ i ∥ B ↔ 1 < A gcd B

Proof

Step Hyp Ref Expression
1 ncoprmgcdne1b ⊢ A ∈ ℕ ∧ B ∈ ℕ → ∃ i ∈ ℤ ≥ 2 i ∥ A ∧ i ∥ B ↔ A gcd B ≠ 1
2 gcdnncl ⊢ A ∈ ℕ ∧ B ∈ ℕ → A gcd B ∈ ℕ
3 nngt1ne1 ⊢ A gcd B ∈ ℕ → 1 < A gcd B ↔ A gcd B ≠ 1
4 2 3 syl ⊢ A ∈ ℕ ∧ B ∈ ℕ → 1 < A gcd B ↔ A gcd B ≠ 1
5 1 4 bitr4d ⊢ A ∈ ℕ ∧ B ∈ ℕ → ∃ i ∈ ℤ ≥ 2 i ∥ A ∧ i ∥ B ↔ 1 < A gcd B