Metamath Proof Explorer

Theorem pcgcd1

Description: The prime count of a GCD is the minimum of the prime counts of the arguments. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion pcgcd1 
|- ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( P pCnt A ) <_ ( P pCnt B ) ) -> ( P pCnt ( A gcd B ) ) = ( P pCnt A ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( B = 0 -> ( A gcd B ) = ( A gcd 0 ) )
2 1 oveq2d 
 |-  ( B = 0 -> ( P pCnt ( A gcd B ) ) = ( P pCnt ( A gcd 0 ) ) )
3 2 eqeq1d 
 |-  ( B = 0 -> ( ( P pCnt ( A gcd B ) ) = ( P pCnt A ) <-> ( P pCnt ( A gcd 0 ) ) = ( P pCnt A ) ) )
4 simpl1 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> P e. Prime )
5 simp2 
 |-  ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) -> A e. ZZ )
6 5 adantr 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> A e. ZZ )
7 simpl3 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> B e. ZZ )
8 simprr 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> B =/= 0 )
9 simpr 
 |-  ( ( A = 0 /\ B = 0 ) -> B = 0 )
10 9 necon3ai 
 |-  ( B =/= 0 -> -. ( A = 0 /\ B = 0 ) )
11 8 10 syl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> -. ( A = 0 /\ B = 0 ) )
12 gcdn0cl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A gcd B ) e. NN )
13 6 7 11 12 syl21anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( A gcd B ) e. NN )
14 13 nnzd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( A gcd B ) e. ZZ )
15 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
16 6 7 15 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
17 16 simpld 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( A gcd B ) || A )
18 pcdvdstr 
 |-  ( ( P e. Prime /\ ( ( A gcd B ) e. ZZ /\ A e. ZZ /\ ( A gcd B ) || A ) ) -> ( P pCnt ( A gcd B ) ) <_ ( P pCnt A ) )
19 4 14 6 17 18 syl13anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt ( A gcd B ) ) <_ ( P pCnt A ) )
20 zq 
 |-  ( A e. ZZ -> A e. QQ )
21 6 20 syl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> A e. QQ )
22 pcxcl 
 |-  ( ( P e. Prime /\ A e. QQ ) -> ( P pCnt A ) e. RR* )
23 4 21 22 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt A ) e. RR* )
24 pczcl 
 |-  ( ( P e. Prime /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( P pCnt B ) e. NN0 )
25 4 7 8 24 syl12anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt B ) e. NN0 )
26 25 nn0red 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt B ) e. RR )
27 pcge0 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> 0 <_ ( P pCnt A ) )
28 4 6 27 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> 0 <_ ( P pCnt A ) )
29 ge0gtmnf 
 |-  ( ( ( P pCnt A ) e. RR* /\ 0 <_ ( P pCnt A ) ) -> -oo < ( P pCnt A ) )
30 23 28 29 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> -oo < ( P pCnt A ) )
31 simprl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt A ) <_ ( P pCnt B ) )
32 xrre 
 |-  ( ( ( ( P pCnt A ) e. RR* /\ ( P pCnt B ) e. RR ) /\ ( -oo < ( P pCnt A ) /\ ( P pCnt A ) <_ ( P pCnt B ) ) ) -> ( P pCnt A ) e. RR )
33 23 26 30 31 32 syl22anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt A ) e. RR )
34 pnfnre 
 |-  +oo e/ RR
35 34 neli 
 |-  -. +oo e. RR
36 pc0 
 |-  ( P e. Prime -> ( P pCnt 0 ) = +oo )
37 4 36 syl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt 0 ) = +oo )
38 37 eleq1d 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( ( P pCnt 0 ) e. RR <-> +oo e. RR ) )
39 35 38 mtbiri 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> -. ( P pCnt 0 ) e. RR )
40 oveq2 
 |-  ( A = 0 -> ( P pCnt A ) = ( P pCnt 0 ) )
41 40 eleq1d 
 |-  ( A = 0 -> ( ( P pCnt A ) e. RR <-> ( P pCnt 0 ) e. RR ) )
42 41 notbid 
 |-  ( A = 0 -> ( -. ( P pCnt A ) e. RR <-> -. ( P pCnt 0 ) e. RR ) )
43 39 42 syl5ibrcom 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( A = 0 -> -. ( P pCnt A ) e. RR ) )
44 43 necon2ad 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( ( P pCnt A ) e. RR -> A =/= 0 ) )
45 33 44 mpd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> A =/= 0 )
46 pczdvds 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) ) -> ( P ^ ( P pCnt A ) ) || A )
47 4 6 45 46 syl12anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P ^ ( P pCnt A ) ) || A )
48 pczcl 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) ) -> ( P pCnt A ) e. NN0 )
49 4 6 45 48 syl12anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt A ) e. NN0 )
50 pcdvdsb 
 |-  ( ( P e. Prime /\ B e. ZZ /\ ( P pCnt A ) e. NN0 ) -> ( ( P pCnt A ) <_ ( P pCnt B ) <-> ( P ^ ( P pCnt A ) ) || B ) )
51 4 7 49 50 syl3anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( ( P pCnt A ) <_ ( P pCnt B ) <-> ( P ^ ( P pCnt A ) ) || B ) )
52 31 51 mpbid 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P ^ ( P pCnt A ) ) || B )
53 prmnn 
 |-  ( P e. Prime -> P e. NN )
54 4 53 syl 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> P e. NN )
55 54 49 nnexpcld 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P ^ ( P pCnt A ) ) e. NN )
56 55 nnzd 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P ^ ( P pCnt A ) ) e. ZZ )
57 dvdsgcd 
 |-  ( ( ( P ^ ( P pCnt A ) ) e. ZZ /\ A e. ZZ /\ B e. ZZ ) -> ( ( ( P ^ ( P pCnt A ) ) || A /\ ( P ^ ( P pCnt A ) ) || B ) -> ( P ^ ( P pCnt A ) ) || ( A gcd B ) ) )
58 56 6 7 57 syl3anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( ( ( P ^ ( P pCnt A ) ) || A /\ ( P ^ ( P pCnt A ) ) || B ) -> ( P ^ ( P pCnt A ) ) || ( A gcd B ) ) )
59 47 52 58 mp2and 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P ^ ( P pCnt A ) ) || ( A gcd B ) )
60 pcdvdsb 
 |-  ( ( P e. Prime /\ ( A gcd B ) e. ZZ /\ ( P pCnt A ) e. NN0 ) -> ( ( P pCnt A ) <_ ( P pCnt ( A gcd B ) ) <-> ( P ^ ( P pCnt A ) ) || ( A gcd B ) ) )
61 4 14 49 60 syl3anc 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( ( P pCnt A ) <_ ( P pCnt ( A gcd B ) ) <-> ( P ^ ( P pCnt A ) ) || ( A gcd B ) ) )
62 59 61 mpbird 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt A ) <_ ( P pCnt ( A gcd B ) ) )
63 4 13 pccld 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt ( A gcd B ) ) e. NN0 )
64 63 nn0red 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt ( A gcd B ) ) e. RR )
65 64 33 letri3d 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( ( P pCnt ( A gcd B ) ) = ( P pCnt A ) <-> ( ( P pCnt ( A gcd B ) ) <_ ( P pCnt A ) /\ ( P pCnt A ) <_ ( P pCnt ( A gcd B ) ) ) ) )
66 19 62 65 mpbir2and 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( ( P pCnt A ) <_ ( P pCnt B ) /\ B =/= 0 ) ) -> ( P pCnt ( A gcd B ) ) = ( P pCnt A ) )
67 66 anassrs 
 |-  ( ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( P pCnt A ) <_ ( P pCnt B ) ) /\ B =/= 0 ) -> ( P pCnt ( A gcd B ) ) = ( P pCnt A ) )
68 gcdid0 
 |-  ( A e. ZZ -> ( A gcd 0 ) = ( abs ` A ) )
69 5 68 syl 
 |-  ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) -> ( A gcd 0 ) = ( abs ` A ) )
70 69 oveq2d 
 |-  ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) -> ( P pCnt ( A gcd 0 ) ) = ( P pCnt ( abs ` A ) ) )
71 pcabs 
 |-  ( ( P e. Prime /\ A e. QQ ) -> ( P pCnt ( abs ` A ) ) = ( P pCnt A ) )
72 20 71 sylan2 
 |-  ( ( P e. Prime /\ A e. ZZ ) -> ( P pCnt ( abs ` A ) ) = ( P pCnt A ) )
73 72 3adant3 
 |-  ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) -> ( P pCnt ( abs ` A ) ) = ( P pCnt A ) )
74 70 73 eqtrd 
 |-  ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) -> ( P pCnt ( A gcd 0 ) ) = ( P pCnt A ) )
75 74 adantr 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( P pCnt A ) <_ ( P pCnt B ) ) -> ( P pCnt ( A gcd 0 ) ) = ( P pCnt A ) )
76 3 67 75 pm2.61ne 
 |-  ( ( ( P e. Prime /\ A e. ZZ /\ B e. ZZ ) /\ ( P pCnt A ) <_ ( P pCnt B ) ) -> ( P pCnt ( A gcd B ) ) = ( P pCnt A ) )