Metamath Proof Explorer

Theorem pc2dvds

Description: A characterization of divisibility in terms of prime count. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion pc2dvds 
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A || B <-> A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) ) )

Proof

Step Hyp Ref Expression
1 pcdvdstr 
 |-  ( ( p e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) -> ( p pCnt A ) <_ ( p pCnt B ) )
2 1 ancoms 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ A || B ) /\ p e. Prime ) -> ( p pCnt A ) <_ ( p pCnt B ) )
3 2 ralrimiva 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ A || B ) -> A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) )
4 3 3expia 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A || B -> A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) ) )
5 oveq2 
 |-  ( A = 0 -> ( p pCnt A ) = ( p pCnt 0 ) )
6 5 breq1d 
 |-  ( A = 0 -> ( ( p pCnt A ) <_ ( p pCnt B ) <-> ( p pCnt 0 ) <_ ( p pCnt B ) ) )
7 6 ralbidv 
 |-  ( A = 0 -> ( A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) <-> A. p e. Prime ( p pCnt 0 ) <_ ( p pCnt B ) ) )
8 breq1 
 |-  ( A = 0 -> ( A || B <-> 0 || B ) )
9 7 8 imbi12d 
 |-  ( A = 0 -> ( ( A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) -> A || B ) <-> ( A. p e. Prime ( p pCnt 0 ) <_ ( p pCnt B ) -> 0 || B ) ) )
10 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
11 10 simpld 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) || A )
12 gcdcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. NN0 )
13 12 nn0zd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. ZZ )
14 simpl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A e. ZZ )
15 dvdsabsb 
 |-  ( ( ( A gcd B ) e. ZZ /\ A e. ZZ ) -> ( ( A gcd B ) || A <-> ( A gcd B ) || ( abs ` A ) ) )
16 13 14 15 syl2anc 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A <-> ( A gcd B ) || ( abs ` A ) ) )
17 11 16 mpbid 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) || ( abs ` A ) )
18 17 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( A gcd B ) || ( abs ` A ) )
19 simpl 
 |-  ( ( A = 0 /\ B = 0 ) -> A = 0 )
20 19 necon3ai 
 |-  ( A =/= 0 -> -. ( A = 0 /\ B = 0 ) )
21 gcdn0cl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A gcd B ) e. NN )
22 20 21 sylan2 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( A gcd B ) e. NN )
23 22 nnzd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( A gcd B ) e. ZZ )
24 22 nnne0d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( A gcd B ) =/= 0 )
25 nnabscl 
 |-  ( ( A e. ZZ /\ A =/= 0 ) -> ( abs ` A ) e. NN )
26 25 adantlr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( abs ` A ) e. NN )
27 26 nnzd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( abs ` A ) e. ZZ )
28 dvdsval2 
 |-  ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ ( abs ` A ) e. ZZ ) -> ( ( A gcd B ) || ( abs ` A ) <-> ( ( abs ` A ) / ( A gcd B ) ) e. ZZ ) )
29 23 24 27 28 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( A gcd B ) || ( abs ` A ) <-> ( ( abs ` A ) / ( A gcd B ) ) e. ZZ ) )
30 18 29 mpbid 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( abs ` A ) / ( A gcd B ) ) e. ZZ )
31 nnre 
 |-  ( ( abs ` A ) e. NN -> ( abs ` A ) e. RR )
32 nngt0 
 |-  ( ( abs ` A ) e. NN -> 0 < ( abs ` A ) )
33 31 32 jca 
 |-  ( ( abs ` A ) e. NN -> ( ( abs ` A ) e. RR /\ 0 < ( abs ` A ) ) )
34 nnre 
 |-  ( ( A gcd B ) e. NN -> ( A gcd B ) e. RR )
35 nngt0 
 |-  ( ( A gcd B ) e. NN -> 0 < ( A gcd B ) )
36 34 35 jca 
 |-  ( ( A gcd B ) e. NN -> ( ( A gcd B ) e. RR /\ 0 < ( A gcd B ) ) )
37 divgt0 
 |-  ( ( ( ( abs ` A ) e. RR /\ 0 < ( abs ` A ) ) /\ ( ( A gcd B ) e. RR /\ 0 < ( A gcd B ) ) ) -> 0 < ( ( abs ` A ) / ( A gcd B ) ) )
38 33 36 37 syl2an 
 |-  ( ( ( abs ` A ) e. NN /\ ( A gcd B ) e. NN ) -> 0 < ( ( abs ` A ) / ( A gcd B ) ) )
39 26 22 38 syl2anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> 0 < ( ( abs ` A ) / ( A gcd B ) ) )
40 elnnz 
 |-  ( ( ( abs ` A ) / ( A gcd B ) ) e. NN <-> ( ( ( abs ` A ) / ( A gcd B ) ) e. ZZ /\ 0 < ( ( abs ` A ) / ( A gcd B ) ) ) )
41 30 39 40 sylanbrc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( abs ` A ) / ( A gcd B ) ) e. NN )
42 elnn1uz2 
 |-  ( ( ( abs ` A ) / ( A gcd B ) ) e. NN <-> ( ( ( abs ` A ) / ( A gcd B ) ) = 1 \/ ( ( abs ` A ) / ( A gcd B ) ) e. ( ZZ>= ` 2 ) ) )
43 41 42 sylib 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( ( abs ` A ) / ( A gcd B ) ) = 1 \/ ( ( abs ` A ) / ( A gcd B ) ) e. ( ZZ>= ` 2 ) ) )
44 10 simprd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) || B )
45 44 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( A gcd B ) || B )
46 breq1 
 |-  ( ( A gcd B ) = ( abs ` A ) -> ( ( A gcd B ) || B <-> ( abs ` A ) || B ) )
47 45 46 syl5ibcom 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( A gcd B ) = ( abs ` A ) -> ( abs ` A ) || B ) )
48 26 nncnd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( abs ` A ) e. CC )
49 22 nncnd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( A gcd B ) e. CC )
50 1cnd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> 1 e. CC )
51 48 49 50 24 divmuld 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( ( abs ` A ) / ( A gcd B ) ) = 1 <-> ( ( A gcd B ) x. 1 ) = ( abs ` A ) ) )
52 49 mulid1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( A gcd B ) x. 1 ) = ( A gcd B ) )
53 52 eqeq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( ( A gcd B ) x. 1 ) = ( abs ` A ) <-> ( A gcd B ) = ( abs ` A ) ) )
54 51 53 bitrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( ( abs ` A ) / ( A gcd B ) ) = 1 <-> ( A gcd B ) = ( abs ` A ) ) )
55 absdvdsb 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A || B <-> ( abs ` A ) || B ) )
56 55 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( A || B <-> ( abs ` A ) || B ) )
57 47 54 56 3imtr4d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( ( abs ` A ) / ( A gcd B ) ) = 1 -> A || B ) )
58 exprmfct 
 |-  ( ( ( abs ` A ) / ( A gcd B ) ) e. ( ZZ>= ` 2 ) -> E. p e. Prime p || ( ( abs ` A ) / ( A gcd B ) ) )
59 simprl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> p e. Prime )
60 26 adantr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( abs ` A ) e. NN )
61 60 nnzd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( abs ` A ) e. ZZ )
62 60 nnne0d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( abs ` A ) =/= 0 )
63 22 adantr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( A gcd B ) e. NN )
64 pcdiv 
 |-  ( ( p e. Prime /\ ( ( abs ` A ) e. ZZ /\ ( abs ` A ) =/= 0 ) /\ ( A gcd B ) e. NN ) -> ( p pCnt ( ( abs ` A ) / ( A gcd B ) ) ) = ( ( p pCnt ( abs ` A ) ) - ( p pCnt ( A gcd B ) ) ) )
65 59 61 62 63 64 syl121anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt ( ( abs ` A ) / ( A gcd B ) ) ) = ( ( p pCnt ( abs ` A ) ) - ( p pCnt ( A gcd B ) ) ) )
66 simplll 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> A e. ZZ )
67 zq 
 |-  ( A e. ZZ -> A e. QQ )
68 66 67 syl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> A e. QQ )
69 pcabs 
 |-  ( ( p e. Prime /\ A e. QQ ) -> ( p pCnt ( abs ` A ) ) = ( p pCnt A ) )
70 59 68 69 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt ( abs ` A ) ) = ( p pCnt A ) )
71 70 oveq1d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( p pCnt ( abs ` A ) ) - ( p pCnt ( A gcd B ) ) ) = ( ( p pCnt A ) - ( p pCnt ( A gcd B ) ) ) )
72 65 71 eqtrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt ( ( abs ` A ) / ( A gcd B ) ) ) = ( ( p pCnt A ) - ( p pCnt ( A gcd B ) ) ) )
73 simprr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> p || ( ( abs ` A ) / ( A gcd B ) ) )
74 41 adantr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( abs ` A ) / ( A gcd B ) ) e. NN )
75 pcelnn 
 |-  ( ( p e. Prime /\ ( ( abs ` A ) / ( A gcd B ) ) e. NN ) -> ( ( p pCnt ( ( abs ` A ) / ( A gcd B ) ) ) e. NN <-> p || ( ( abs ` A ) / ( A gcd B ) ) ) )
76 59 74 75 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( p pCnt ( ( abs ` A ) / ( A gcd B ) ) ) e. NN <-> p || ( ( abs ` A ) / ( A gcd B ) ) ) )
77 73 76 mpbird 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt ( ( abs ` A ) / ( A gcd B ) ) ) e. NN )
78 72 77 eqeltrrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( p pCnt A ) - ( p pCnt ( A gcd B ) ) ) e. NN )
79 59 63 pccld 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt ( A gcd B ) ) e. NN0 )
80 79 nn0zd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt ( A gcd B ) ) e. ZZ )
81 simplr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> A =/= 0 )
82 pczcl 
 |-  ( ( p e. Prime /\ ( A e. ZZ /\ A =/= 0 ) ) -> ( p pCnt A ) e. NN0 )
83 59 66 81 82 syl12anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt A ) e. NN0 )
84 83 nn0zd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt A ) e. ZZ )
85 znnsub 
 |-  ( ( ( p pCnt ( A gcd B ) ) e. ZZ /\ ( p pCnt A ) e. ZZ ) -> ( ( p pCnt ( A gcd B ) ) < ( p pCnt A ) <-> ( ( p pCnt A ) - ( p pCnt ( A gcd B ) ) ) e. NN ) )
86 80 84 85 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( p pCnt ( A gcd B ) ) < ( p pCnt A ) <-> ( ( p pCnt A ) - ( p pCnt ( A gcd B ) ) ) e. NN ) )
87 78 86 mpbird 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt ( A gcd B ) ) < ( p pCnt A ) )
88 79 nn0red 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt ( A gcd B ) ) e. RR )
89 83 nn0red 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt A ) e. RR )
90 88 89 ltnled 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( p pCnt ( A gcd B ) ) < ( p pCnt A ) <-> -. ( p pCnt A ) <_ ( p pCnt ( A gcd B ) ) ) )
91 87 90 mpbid 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> -. ( p pCnt A ) <_ ( p pCnt ( A gcd B ) ) )
92 simpllr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> B e. ZZ )
93 nprmdvds1 
 |-  ( p e. Prime -> -. p || 1 )
94 93 ad2antrl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> -. p || 1 )
95 gcdid0 
 |-  ( A e. ZZ -> ( A gcd 0 ) = ( abs ` A ) )
96 66 95 syl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( A gcd 0 ) = ( abs ` A ) )
97 96 oveq2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( abs ` A ) / ( A gcd 0 ) ) = ( ( abs ` A ) / ( abs ` A ) ) )
98 48 adantr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( abs ` A ) e. CC )
99 98 62 dividd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( abs ` A ) / ( abs ` A ) ) = 1 )
100 97 99 eqtrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( abs ` A ) / ( A gcd 0 ) ) = 1 )
101 100 breq2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p || ( ( abs ` A ) / ( A gcd 0 ) ) <-> p || 1 ) )
102 94 101 mtbird 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> -. p || ( ( abs ` A ) / ( A gcd 0 ) ) )
103 oveq2 
 |-  ( B = 0 -> ( A gcd B ) = ( A gcd 0 ) )
104 103 oveq2d 
 |-  ( B = 0 -> ( ( abs ` A ) / ( A gcd B ) ) = ( ( abs ` A ) / ( A gcd 0 ) ) )
105 104 breq2d 
 |-  ( B = 0 -> ( p || ( ( abs ` A ) / ( A gcd B ) ) <-> p || ( ( abs ` A ) / ( A gcd 0 ) ) ) )
106 73 105 syl5ibcom 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( B = 0 -> p || ( ( abs ` A ) / ( A gcd 0 ) ) ) )
107 106 necon3bd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( -. p || ( ( abs ` A ) / ( A gcd 0 ) ) -> B =/= 0 ) )
108 102 107 mpd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> B =/= 0 )
109 pczcl 
 |-  ( ( p e. Prime /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( p pCnt B ) e. NN0 )
110 59 92 108 109 syl12anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt B ) e. NN0 )
111 110 nn0red 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt B ) e. RR )
112 lemin 
 |-  ( ( ( p pCnt A ) e. RR /\ ( p pCnt A ) e. RR /\ ( p pCnt B ) e. RR ) -> ( ( p pCnt A ) <_ if ( ( p pCnt A ) <_ ( p pCnt B ) , ( p pCnt A ) , ( p pCnt B ) ) <-> ( ( p pCnt A ) <_ ( p pCnt A ) /\ ( p pCnt A ) <_ ( p pCnt B ) ) ) )
113 89 89 111 112 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( p pCnt A ) <_ if ( ( p pCnt A ) <_ ( p pCnt B ) , ( p pCnt A ) , ( p pCnt B ) ) <-> ( ( p pCnt A ) <_ ( p pCnt A ) /\ ( p pCnt A ) <_ ( p pCnt B ) ) ) )
114 pcgcd 
 |-  ( ( p e. Prime /\ A e. ZZ /\ B e. ZZ ) -> ( p pCnt ( A gcd B ) ) = if ( ( p pCnt A ) <_ ( p pCnt B ) , ( p pCnt A ) , ( p pCnt B ) ) )
115 59 66 92 114 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt ( A gcd B ) ) = if ( ( p pCnt A ) <_ ( p pCnt B ) , ( p pCnt A ) , ( p pCnt B ) ) )
116 115 breq2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( p pCnt A ) <_ ( p pCnt ( A gcd B ) ) <-> ( p pCnt A ) <_ if ( ( p pCnt A ) <_ ( p pCnt B ) , ( p pCnt A ) , ( p pCnt B ) ) ) )
117 89 leidd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( p pCnt A ) <_ ( p pCnt A ) )
118 117 biantrurd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( p pCnt A ) <_ ( p pCnt B ) <-> ( ( p pCnt A ) <_ ( p pCnt A ) /\ ( p pCnt A ) <_ ( p pCnt B ) ) ) )
119 113 116 118 3bitr4rd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> ( ( p pCnt A ) <_ ( p pCnt B ) <-> ( p pCnt A ) <_ ( p pCnt ( A gcd B ) ) ) )
120 91 119 mtbird 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ ( p e. Prime /\ p || ( ( abs ` A ) / ( A gcd B ) ) ) ) -> -. ( p pCnt A ) <_ ( p pCnt B ) )
121 120 expr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) /\ p e. Prime ) -> ( p || ( ( abs ` A ) / ( A gcd B ) ) -> -. ( p pCnt A ) <_ ( p pCnt B ) ) )
122 121 reximdva 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( E. p e. Prime p || ( ( abs ` A ) / ( A gcd B ) ) -> E. p e. Prime -. ( p pCnt A ) <_ ( p pCnt B ) ) )
123 rexnal 
 |-  ( E. p e. Prime -. ( p pCnt A ) <_ ( p pCnt B ) <-> -. A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) )
124 122 123 syl6ib 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( E. p e. Prime p || ( ( abs ` A ) / ( A gcd B ) ) -> -. A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) ) )
125 58 124 syl5 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( ( abs ` A ) / ( A gcd B ) ) e. ( ZZ>= ` 2 ) -> -. A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) ) )
126 57 125 orim12d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( ( ( ( abs ` A ) / ( A gcd B ) ) = 1 \/ ( ( abs ` A ) / ( A gcd B ) ) e. ( ZZ>= ` 2 ) ) -> ( A || B \/ -. A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) ) ) )
127 43 126 mpd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( A || B \/ -. A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) ) )
128 127 ord 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( -. A || B -> -. A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) ) )
129 128 con4d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ A =/= 0 ) -> ( A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) -> A || B ) )
130 2prm 
 |-  2 e. Prime
131 130 ne0ii 
 |-  Prime =/= (/)
132 r19.2z 
 |-  ( ( Prime =/= (/) /\ A. p e. Prime ( p pCnt 0 ) <_ ( p pCnt B ) ) -> E. p e. Prime ( p pCnt 0 ) <_ ( p pCnt B ) )
133 131 132 mpan 
 |-  ( A. p e. Prime ( p pCnt 0 ) <_ ( p pCnt B ) -> E. p e. Prime ( p pCnt 0 ) <_ ( p pCnt B ) )
134 id 
 |-  ( p e. Prime -> p e. Prime )
135 zq 
 |-  ( B e. ZZ -> B e. QQ )
136 135 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. QQ )
137 pcxcl 
 |-  ( ( p e. Prime /\ B e. QQ ) -> ( p pCnt B ) e. RR* )
138 134 136 137 syl2anr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( p pCnt B ) e. RR* )
139 pnfge 
 |-  ( ( p pCnt B ) e. RR* -> ( p pCnt B ) <_ +oo )
140 138 139 syl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( p pCnt B ) <_ +oo )
141 140 biantrurd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( +oo <_ ( p pCnt B ) <-> ( ( p pCnt B ) <_ +oo /\ +oo <_ ( p pCnt B ) ) ) )
142 pc0 
 |-  ( p e. Prime -> ( p pCnt 0 ) = +oo )
143 142 adantl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( p pCnt 0 ) = +oo )
144 143 breq1d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( ( p pCnt 0 ) <_ ( p pCnt B ) <-> +oo <_ ( p pCnt B ) ) )
145 pnfxr 
 |-  +oo e. RR*
146 xrletri3 
 |-  ( ( ( p pCnt B ) e. RR* /\ +oo e. RR* ) -> ( ( p pCnt B ) = +oo <-> ( ( p pCnt B ) <_ +oo /\ +oo <_ ( p pCnt B ) ) ) )
147 138 145 146 sylancl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( ( p pCnt B ) = +oo <-> ( ( p pCnt B ) <_ +oo /\ +oo <_ ( p pCnt B ) ) ) )
148 141 144 147 3bitr4d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( ( p pCnt 0 ) <_ ( p pCnt B ) <-> ( p pCnt B ) = +oo ) )
149 pnfnre 
 |-  +oo e/ RR
150 149 neli 
 |-  -. +oo e. RR
151 eleq1 
 |-  ( ( p pCnt B ) = +oo -> ( ( p pCnt B ) e. RR <-> +oo e. RR ) )
152 150 151 mtbiri 
 |-  ( ( p pCnt B ) = +oo -> -. ( p pCnt B ) e. RR )
153 109 nn0red 
 |-  ( ( p e. Prime /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( p pCnt B ) e. RR )
154 153 adantll 
 |-  ( ( ( A e. ZZ /\ p e. Prime ) /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( p pCnt B ) e. RR )
155 154 an4s 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( p e. Prime /\ B =/= 0 ) ) -> ( p pCnt B ) e. RR )
156 155 expr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( B =/= 0 -> ( p pCnt B ) e. RR ) )
157 156 necon1bd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( -. ( p pCnt B ) e. RR -> B = 0 ) )
158 152 157 syl5 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( ( p pCnt B ) = +oo -> B = 0 ) )
159 148 158 sylbid 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( ( p pCnt 0 ) <_ ( p pCnt B ) -> B = 0 ) )
160 159 rexlimdva 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( E. p e. Prime ( p pCnt 0 ) <_ ( p pCnt B ) -> B = 0 ) )
161 0dvds 
 |-  ( B e. ZZ -> ( 0 || B <-> B = 0 ) )
162 161 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( 0 || B <-> B = 0 ) )
163 160 162 sylibrd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( E. p e. Prime ( p pCnt 0 ) <_ ( p pCnt B ) -> 0 || B ) )
164 133 163 syl5 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A. p e. Prime ( p pCnt 0 ) <_ ( p pCnt B ) -> 0 || B ) )
165 9 129 164 pm2.61ne 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) -> A || B ) )
166 4 165 impbid 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A || B <-> A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) ) )