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 
|- ( ph -> A e. NN )
prmdvdsncoprmbd.b 
|- ( ph -> B e. NN )
Assertion prmdvdsncoprmbd 
|- ( ph -> ( E. p e. Prime ( p || A /\ p || B ) <-> ( A gcd B ) =/= 1 ) )

Proof

Step Hyp Ref Expression
1 prmdvdsncoprmbd.a 
 |-  ( ph -> A e. NN )
2 prmdvdsncoprmbd.b 
 |-  ( ph -> B e. NN )
3 prmuz2 
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
4 3 a1i 
 |-  ( ph -> ( p e. Prime -> p e. ( ZZ>= ` 2 ) ) )
5 4 anim1d 
 |-  ( ph -> ( ( p e. Prime /\ ( p || A /\ p || B ) ) -> ( p e. ( ZZ>= ` 2 ) /\ ( p || A /\ p || B ) ) ) )
6 5 reximdv2 
 |-  ( ph -> ( E. p e. Prime ( p || A /\ p || B ) -> E. p e. ( ZZ>= ` 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 
 |-  ( E. p e. ( ZZ>= ` 2 ) ( p || A /\ p || B ) <-> E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) )
11 6 10 imbitrdi 
 |-  ( ph -> ( E. p e. Prime ( p || A /\ p || B ) -> E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) ) )
12 exprmfct 
 |-  ( i e. ( ZZ>= ` 2 ) -> E. p e. Prime p || i )
13 12 ad2antrl 
 |-  ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) -> E. p e. Prime p || i )
14 prmnn 
 |-  ( p e. Prime -> p e. NN )
15 14 ad2antlr 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> p e. NN )
16 15 nnzd 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> p e. ZZ )
17 eluzelz 
 |-  ( i e. ( ZZ>= ` 2 ) -> i e. ZZ )
18 17 ad2antrr 
 |-  ( ( ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) /\ p || i ) -> i e. ZZ )
19 18 ad4ant24 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> i e. ZZ )
20 1 ad3antrrr 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> A e. NN )
21 20 nnzd 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> A e. ZZ )
22 simpr 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> p || i )
23 simprrl 
 |-  ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) -> i || A )
24 23 ad2antrr 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> i || A )
25 16 19 21 22 24 dvdstrd 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> p || A )
26 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> B e. NN )
27 26 nnzd 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> B e. ZZ )
28 simprrr 
 |-  ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) -> i || B )
29 28 ad2antrr 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> i || B )
30 16 19 27 22 29 dvdstrd 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> p || B )
31 25 30 jca 
 |-  ( ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) /\ p || i ) -> ( p || A /\ p || B ) )
32 31 ex 
 |-  ( ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) /\ p e. Prime ) -> ( p || i -> ( p || A /\ p || B ) ) )
33 32 reximdva 
 |-  ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) -> ( E. p e. Prime p || i -> E. p e. Prime ( p || A /\ p || B ) ) )
34 13 33 mpd 
 |-  ( ( ph /\ ( i e. ( ZZ>= ` 2 ) /\ ( i || A /\ i || B ) ) ) -> E. p e. Prime ( p || A /\ p || B ) )
35 34 rexlimdvaa 
 |-  ( ph -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) -> E. p e. Prime ( p || A /\ p || B ) ) )
36 11 35 impbid 
 |-  ( ph -> ( E. p e. Prime ( p || A /\ p || B ) <-> E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) ) )
37 ncoprmgcdne1b 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) <-> ( A gcd B ) =/= 1 ) )
38 1 2 37 syl2anc 
 |-  ( ph -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) <-> ( A gcd B ) =/= 1 ) )
39 36 38 bitrd 
 |-  ( ph -> ( E. p e. Prime ( p || A /\ p || B ) <-> ( A gcd B ) =/= 1 ) )