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 φ A
prmdvdsncoprmbd.b φ B
Assertion prmdvdsncoprmbd φ p p A p B A gcd B 1

Proof

Step Hyp Ref Expression
1 prmdvdsncoprmbd.a φ A
2 prmdvdsncoprmbd.b φ B
3 prmuz2 p p 2
4 3 a1i φ p p 2
5 4 anim1d φ p p A p B p 2 p A p B
6 5 reximdv2 φ p p A p B p 2 p A p B
7 breq1 p = i p A i A
8 breq1 p = i p B i B
9 7 8 anbi12d p = i p A p B i A i B
10 9 cbvrexvw p 2 p A p B i 2 i A i B
11 6 10 syl6ib φ p p A p B i 2 i A i B
12 exprmfct i 2 p p i
13 12 ad2antrl φ i 2 i A i B p p i
14 prmnn p p
15 14 ad2antlr φ i 2 i A i B p p i p
16 15 nnzd φ i 2 i A i B p p i p
17 eluzelz i 2 i
18 17 ad2antrr i 2 i A i B p i i
19 18 ad4ant24 φ i 2 i A i B p p i i
20 1 ad3antrrr φ i 2 i A i B p p i A
21 20 nnzd φ i 2 i A i B p p i A
22 simpr φ i 2 i A i B p p i p i
23 simprrl φ i 2 i A i B i A
24 23 ad2antrr φ i 2 i A i B p p i i A
25 16 19 21 22 24 dvdstrd φ i 2 i A i B p p i p A
26 2 ad3antrrr φ i 2 i A i B p p i B
27 26 nnzd φ i 2 i A i B p p i B
28 simprrr φ i 2 i A i B i B
29 28 ad2antrr φ i 2 i A i B p p i i B
30 16 19 27 22 29 dvdstrd φ i 2 i A i B p p i p B
31 25 30 jca φ i 2 i A i B p p i p A p B
32 31 ex φ i 2 i A i B p p i p A p B
33 32 reximdva φ i 2 i A i B p p i p p A p B
34 13 33 mpd φ i 2 i A i B p p A p B
35 34 rexlimdvaa φ i 2 i A i B p p A p B
36 11 35 impbid φ p p A p B i 2 i A i B
37 ncoprmgcdne1b A B i 2 i A i B A gcd B 1
38 1 2 37 syl2anc φ i 2 i A i B A gcd B 1
39 36 38 bitrd φ p p A p B A gcd B 1