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	mulridd	\|- ( ( ( 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	imbitrdi	\|- ( ( ( 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 ) ) )

Metamath Proof Explorer

Theorem pc2dvds

Proof