Metamath Proof Explorer

Theorem pcqmul

Description: Multiplication property of the prime power function. (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Assertion pcqmul 
|- ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) )

Proof

Step Hyp Ref Expression
1 simp2l 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> A e. QQ )
2 elq 
 |-  ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
3 1 2 sylib 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> E. x e. ZZ E. y e. NN A = ( x / y ) )
4 simp3l 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> B e. QQ )
5 elq 
 |-  ( B e. QQ <-> E. z e. ZZ E. w e. NN B = ( z / w ) )
6 4 5 sylib 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> E. z e. ZZ E. w e. NN B = ( z / w ) )
7 reeanv 
 |-  ( E. x e. ZZ E. z e. ZZ ( E. y e. NN A = ( x / y ) /\ E. w e. NN B = ( z / w ) ) <-> ( E. x e. ZZ E. y e. NN A = ( x / y ) /\ E. z e. ZZ E. w e. NN B = ( z / w ) ) )
8 reeanv 
 |-  ( E. y e. NN E. w e. NN ( A = ( x / y ) /\ B = ( z / w ) ) <-> ( E. y e. NN A = ( x / y ) /\ E. w e. NN B = ( z / w ) ) )
9 simp2r 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> A =/= 0 )
10 simp3r 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> B =/= 0 )
11 9 10 jca 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> ( A =/= 0 /\ B =/= 0 ) )
12 11 ad2antrr 
 |-  ( ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( A =/= 0 /\ B =/= 0 ) )
13 simp1 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> P e. Prime )
14 simprl 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> y e. NN )
15 14 nncnd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> y e. CC )
16 14 nnne0d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> y =/= 0 )
17 15 16 div0d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( 0 / y ) = 0 )
18 oveq1 
 |-  ( x = 0 -> ( x / y ) = ( 0 / y ) )
19 18 eqeq1d 
 |-  ( x = 0 -> ( ( x / y ) = 0 <-> ( 0 / y ) = 0 ) )
20 17 19 syl5ibrcom 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( x = 0 -> ( x / y ) = 0 ) )
21 20 necon3d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( x / y ) =/= 0 -> x =/= 0 ) )
22 simprr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> w e. NN )
23 22 nncnd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> w e. CC )
24 22 nnne0d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> w =/= 0 )
25 23 24 div0d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( 0 / w ) = 0 )
26 oveq1 
 |-  ( z = 0 -> ( z / w ) = ( 0 / w ) )
27 26 eqeq1d 
 |-  ( z = 0 -> ( ( z / w ) = 0 <-> ( 0 / w ) = 0 ) )
28 25 27 syl5ibrcom 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( z = 0 -> ( z / w ) = 0 ) )
29 28 necon3d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( z / w ) =/= 0 -> z =/= 0 ) )
30 simpll 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> P e. Prime )
31 simplrl 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> x e. ZZ )
32 simplrr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> z e. ZZ )
33 31 32 zmulcld 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( x x. z ) e. ZZ )
34 31 zcnd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> x e. CC )
35 32 zcnd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> z e. CC )
36 simprrl 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> x =/= 0 )
37 simprrr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> z =/= 0 )
38 34 35 36 37 mulne0d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( x x. z ) =/= 0 )
39 14 adantrr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> y e. NN )
40 22 adantrr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> w e. NN )
41 39 40 nnmulcld 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( y x. w ) e. NN )
42 pcdiv 
 |-  ( ( P e. Prime /\ ( ( x x. z ) e. ZZ /\ ( x x. z ) =/= 0 ) /\ ( y x. w ) e. NN ) -> ( P pCnt ( ( x x. z ) / ( y x. w ) ) ) = ( ( P pCnt ( x x. z ) ) - ( P pCnt ( y x. w ) ) ) )
43 30 33 38 41 42 syl121anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt ( ( x x. z ) / ( y x. w ) ) ) = ( ( P pCnt ( x x. z ) ) - ( P pCnt ( y x. w ) ) ) )
44 pcmul 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) /\ ( z e. ZZ /\ z =/= 0 ) ) -> ( P pCnt ( x x. z ) ) = ( ( P pCnt x ) + ( P pCnt z ) ) )
45 30 31 36 32 37 44 syl122anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt ( x x. z ) ) = ( ( P pCnt x ) + ( P pCnt z ) ) )
46 39 nnzd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> y e. ZZ )
47 16 adantrr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> y =/= 0 )
48 40 nnzd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> w e. ZZ )
49 24 adantrr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> w =/= 0 )
50 pcmul 
 |-  ( ( P e. Prime /\ ( y e. ZZ /\ y =/= 0 ) /\ ( w e. ZZ /\ w =/= 0 ) ) -> ( P pCnt ( y x. w ) ) = ( ( P pCnt y ) + ( P pCnt w ) ) )
51 30 46 47 48 49 50 syl122anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt ( y x. w ) ) = ( ( P pCnt y ) + ( P pCnt w ) ) )
52 45 51 oveq12d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( ( P pCnt ( x x. z ) ) - ( P pCnt ( y x. w ) ) ) = ( ( ( P pCnt x ) + ( P pCnt z ) ) - ( ( P pCnt y ) + ( P pCnt w ) ) ) )
53 pczcl 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( P pCnt x ) e. NN0 )
54 30 31 36 53 syl12anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt x ) e. NN0 )
55 54 nn0cnd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt x ) e. CC )
56 pczcl 
 |-  ( ( P e. Prime /\ ( z e. ZZ /\ z =/= 0 ) ) -> ( P pCnt z ) e. NN0 )
57 30 32 37 56 syl12anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt z ) e. NN0 )
58 57 nn0cnd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt z ) e. CC )
59 30 39 pccld 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt y ) e. NN0 )
60 59 nn0cnd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt y ) e. CC )
61 30 40 pccld 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt w ) e. NN0 )
62 61 nn0cnd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt w ) e. CC )
63 55 58 60 62 addsub4d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( ( ( P pCnt x ) + ( P pCnt z ) ) - ( ( P pCnt y ) + ( P pCnt w ) ) ) = ( ( ( P pCnt x ) - ( P pCnt y ) ) + ( ( P pCnt z ) - ( P pCnt w ) ) ) )
64 43 52 63 3eqtrd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt ( ( x x. z ) / ( y x. w ) ) ) = ( ( ( P pCnt x ) - ( P pCnt y ) ) + ( ( P pCnt z ) - ( P pCnt w ) ) ) )
65 15 adantrr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> y e. CC )
66 23 adantrr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> w e. CC )
67 34 65 35 66 47 49 divmuldivd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( ( x / y ) x. ( z / w ) ) = ( ( x x. z ) / ( y x. w ) ) )
68 67 oveq2d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt ( ( x / y ) x. ( z / w ) ) ) = ( P pCnt ( ( x x. z ) / ( y x. w ) ) ) )
69 pcdiv 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) /\ y e. NN ) -> ( P pCnt ( x / y ) ) = ( ( P pCnt x ) - ( P pCnt y ) ) )
70 30 31 36 39 69 syl121anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt ( x / y ) ) = ( ( P pCnt x ) - ( P pCnt y ) ) )
71 pcdiv 
 |-  ( ( P e. Prime /\ ( z e. ZZ /\ z =/= 0 ) /\ w e. NN ) -> ( P pCnt ( z / w ) ) = ( ( P pCnt z ) - ( P pCnt w ) ) )
72 30 32 37 40 71 syl121anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt ( z / w ) ) = ( ( P pCnt z ) - ( P pCnt w ) ) )
73 70 72 oveq12d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( ( P pCnt ( x / y ) ) + ( P pCnt ( z / w ) ) ) = ( ( ( P pCnt x ) - ( P pCnt y ) ) + ( ( P pCnt z ) - ( P pCnt w ) ) ) )
74 64 68 73 3eqtr4d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( ( y e. NN /\ w e. NN ) /\ ( x =/= 0 /\ z =/= 0 ) ) ) -> ( P pCnt ( ( x / y ) x. ( z / w ) ) ) = ( ( P pCnt ( x / y ) ) + ( P pCnt ( z / w ) ) ) )
75 74 expr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( x =/= 0 /\ z =/= 0 ) -> ( P pCnt ( ( x / y ) x. ( z / w ) ) ) = ( ( P pCnt ( x / y ) ) + ( P pCnt ( z / w ) ) ) ) )
76 21 29 75 syl2and 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( ( x / y ) =/= 0 /\ ( z / w ) =/= 0 ) -> ( P pCnt ( ( x / y ) x. ( z / w ) ) ) = ( ( P pCnt ( x / y ) ) + ( P pCnt ( z / w ) ) ) ) )
77 neeq1 
 |-  ( A = ( x / y ) -> ( A =/= 0 <-> ( x / y ) =/= 0 ) )
78 neeq1 
 |-  ( B = ( z / w ) -> ( B =/= 0 <-> ( z / w ) =/= 0 ) )
79 77 78 bi2anan9 
 |-  ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( ( A =/= 0 /\ B =/= 0 ) <-> ( ( x / y ) =/= 0 /\ ( z / w ) =/= 0 ) ) )
80 oveq12 
 |-  ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( A x. B ) = ( ( x / y ) x. ( z / w ) ) )
81 80 oveq2d 
 |-  ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( P pCnt ( A x. B ) ) = ( P pCnt ( ( x / y ) x. ( z / w ) ) ) )
82 oveq2 
 |-  ( A = ( x / y ) -> ( P pCnt A ) = ( P pCnt ( x / y ) ) )
83 oveq2 
 |-  ( B = ( z / w ) -> ( P pCnt B ) = ( P pCnt ( z / w ) ) )
84 82 83 oveqan12d 
 |-  ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( ( P pCnt A ) + ( P pCnt B ) ) = ( ( P pCnt ( x / y ) ) + ( P pCnt ( z / w ) ) ) )
85 81 84 eqeq12d 
 |-  ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) <-> ( P pCnt ( ( x / y ) x. ( z / w ) ) ) = ( ( P pCnt ( x / y ) ) + ( P pCnt ( z / w ) ) ) ) )
86 79 85 imbi12d 
 |-  ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( ( ( A =/= 0 /\ B =/= 0 ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) ) <-> ( ( ( x / y ) =/= 0 /\ ( z / w ) =/= 0 ) -> ( P pCnt ( ( x / y ) x. ( z / w ) ) ) = ( ( P pCnt ( x / y ) ) + ( P pCnt ( z / w ) ) ) ) ) )
87 76 86 syl5ibrcom 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( ( A =/= 0 /\ B =/= 0 ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) ) ) )
88 13 87 sylanl1 
 |-  ( ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( ( A =/= 0 /\ B =/= 0 ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) ) ) )
89 12 88 mpid 
 |-  ( ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) /\ ( x e. ZZ /\ z e. ZZ ) ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) ) )
90 89 rexlimdvva 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) /\ ( x e. ZZ /\ z e. ZZ ) ) -> ( E. y e. NN E. w e. NN ( A = ( x / y ) /\ B = ( z / w ) ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) ) )
91 8 90 syl5bir 
 |-  ( ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) /\ ( x e. ZZ /\ z e. ZZ ) ) -> ( ( E. y e. NN A = ( x / y ) /\ E. w e. NN B = ( z / w ) ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) ) )
92 91 rexlimdvva 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> ( E. x e. ZZ E. z e. ZZ ( E. y e. NN A = ( x / y ) /\ E. w e. NN B = ( z / w ) ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) ) )
93 7 92 syl5bir 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> ( ( E. x e. ZZ E. y e. NN A = ( x / y ) /\ E. z e. ZZ E. w e. NN B = ( z / w ) ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) ) )
94 3 6 93 mp2and 
 |-  ( ( P e. Prime /\ ( A e. QQ /\ A =/= 0 ) /\ ( B e. QQ /\ B =/= 0 ) ) -> ( P pCnt ( A x. B ) ) = ( ( P pCnt A ) + ( P pCnt B ) ) )