Metamath Proof Explorer

Theorem prmdvdsncoprmbd

Description: Two positive integers are not coprime iff a prime divides both integers. Deduction version of ncoprmgcdne1b with the existential quantifier over the primes instead of integers greater than or equal to 2. (Contributed by SN, 24-Aug-2024)

Ref Expression
Hypotheses prmdvdsncoprmbd.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
prmdvdsncoprmbd.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
Assertion prmdvdsncoprmbd ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )

Proof

Step Hyp Ref Expression
1 prmdvdsncoprmbd.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 prmdvdsncoprmbd.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 prmuz2 ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
4 3 a1i ⊢ ( 𝜑 → ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) ) )
5 4 anim1d ⊢ ( 𝜑 → ( ( 𝑝 ∈ ℙ ∧ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ) → ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ) ) )
6 5 reximdv2 ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) → ∃ 𝑝 ∈ ( ℤ≥ ‘ 2 ) ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ) )
7 breq1 ⊢ ( 𝑝 = 𝑖 → ( 𝑝 ∥ 𝐴 ↔ 𝑖 ∥ 𝐴 ) )
8 breq1 ⊢ ( 𝑝 = 𝑖 → ( 𝑝 ∥ 𝐵 ↔ 𝑖 ∥ 𝐵 ) )
9 7 8 anbi12d ⊢ ( 𝑝 = 𝑖 → ( ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ↔ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) )
10 9 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ( ℤ≥ ‘ 2 ) ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ↔ ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) )
11 6 10 imbitrdi ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) → ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) )
12 exprmfct ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑖 )
13 12 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑖 )
14 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
15 14 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝑝 ∈ ℕ )
16 15 nnzd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝑝 ∈ ℤ )
17 eluzelz ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) → 𝑖 ∈ ℤ )
18 17 ad2antrr ⊢ ( ( ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ∧ 𝑝 ∥ 𝑖 ) → 𝑖 ∈ ℤ )
19 18 ad4ant24 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝑖 ∈ ℤ )
20 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝐴 ∈ ℕ )
21 20 nnzd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝐴 ∈ ℤ )
22 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝑝 ∥ 𝑖 )
23 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) → 𝑖 ∥ 𝐴 )
24 23 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝑖 ∥ 𝐴 )
25 16 19 21 22 24 dvdstrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝑝 ∥ 𝐴 )
26 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝐵 ∈ ℕ )
27 26 nnzd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝐵 ∈ ℤ )
28 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) → 𝑖 ∥ 𝐵 )
29 28 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝑖 ∥ 𝐵 )
30 16 19 27 22 29 dvdstrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → 𝑝 ∥ 𝐵 )
31 25 30 jca ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑖 ) → ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) )
32 31 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝑖 → ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ) )
33 32 reximdva ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑖 → ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ) )
34 13 33 mpd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) )
35 34 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ) )
36 11 35 impbid ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ↔ ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) )
37 ncoprmgcdne1b ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
38 1 2 37 syl2anc ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )
39 36 38 bitrd ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) ↔ ( 𝐴 gcd 𝐵 ) ≠ 1 ) )