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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )

Proof

Step Hyp Ref Expression
1 eluz2nn ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) → 𝑖 ∈ ℕ )
2 1 adantr ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝑖 ∈ ℕ )
3 eluz2b3 ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑖 ∈ ℕ ∧ 𝑖 ≠ 1 ) )
4 neneq ⊢ ( 𝑖 ≠ 1 → ¬ 𝑖 = 1 )
5 3 4 simplbiim ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) → ¬ 𝑖 = 1 )
6 5 anim1ci ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) )
7 2 6 jca ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ∈ ℕ ∧ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) ) )
8 neqne ⊢ ( ¬ 𝑖 = 1 → 𝑖 ≠ 1 )
9 8 anim1ci ⊢ ( ( ¬ 𝑖 = 1 ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ∈ ℕ ∧ 𝑖 ≠ 1 ) )
10 9 3 sylibr ⊢ ( ( ¬ 𝑖 = 1 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ( ℤ≥ ‘ 2 ) )
11 10 ex ⊢ ( ¬ 𝑖 = 1 → ( 𝑖 ∈ ℕ → 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) )
12 11 adantl ⊢ ( ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) → ( 𝑖 ∈ ℕ → 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) )
13 12 impcom ⊢ ( ( 𝑖 ∈ ℕ ∧ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 2 ) )
14 13 adantl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑖 ∈ ℕ ∧ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 2 ) )
15 simprrl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑖 ∈ ℕ ∧ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) ) ) → ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) )
16 14 15 jca ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝑖 ∈ ℕ ∧ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) )
17 16 ex ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ∧ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) )
18 7 17 impbid2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ↔ ( 𝑖 ∈ ℕ ∧ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) ) ) )
19 18 rexbidv2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ↔ ∃ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) ) )
20 rexanali ⊢ ( ∃ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) ↔ ¬ ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) )
21 20 a1i ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ∧ ¬ 𝑖 = 1 ) ↔ ¬ ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ) )
22 coprmgcdb ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )
23 22 necon3bbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
24 19 21 23 3bitrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )