Metamath Proof Explorer


Theorem pcadd

Description: An inequality for the prime count of a sum. This is the source of the ultrametric inequality for the p-adic metric. (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Hypotheses pcadd.1 โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™ )
pcadd.2 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„š )
pcadd.3 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„š )
pcadd.4 โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ๐ต ) )
Assertion pcadd ( ๐œ‘ โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 pcadd.1 โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™ )
2 pcadd.2 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„š )
3 pcadd.3 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„š )
4 pcadd.4 โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ๐ต ) )
5 elq โŠข ( ๐ด โˆˆ โ„š โ†” โˆƒ ๐‘ฅ โˆˆ โ„ค โˆƒ ๐‘ฆ โˆˆ โ„• ๐ด = ( ๐‘ฅ / ๐‘ฆ ) )
6 2 5 sylib โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘ฅ โˆˆ โ„ค โˆƒ ๐‘ฆ โˆˆ โ„• ๐ด = ( ๐‘ฅ / ๐‘ฆ ) )
7 elq โŠข ( ๐ต โˆˆ โ„š โ†” โˆƒ ๐‘ง โˆˆ โ„ค โˆƒ ๐‘ค โˆˆ โ„• ๐ต = ( ๐‘ง / ๐‘ค ) )
8 3 7 sylib โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘ง โˆˆ โ„ค โˆƒ ๐‘ค โˆˆ โ„• ๐ต = ( ๐‘ง / ๐‘ค ) )
9 pcxcl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐ด โˆˆ โ„š ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โˆˆ โ„* )
10 1 2 9 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ pCnt ๐ด ) โˆˆ โ„* )
11 10 xrleidd โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ๐ด ) )
12 11 adantr โŠข ( ( ๐œ‘ โˆง ๐ต = 0 ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ๐ด ) )
13 oveq2 โŠข ( ๐ต = 0 โ†’ ( ๐ด + ๐ต ) = ( ๐ด + 0 ) )
14 qcn โŠข ( ๐ด โˆˆ โ„š โ†’ ๐ด โˆˆ โ„‚ )
15 2 14 syl โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
16 15 addid1d โŠข ( ๐œ‘ โ†’ ( ๐ด + 0 ) = ๐ด )
17 13 16 sylan9eqr โŠข ( ( ๐œ‘ โˆง ๐ต = 0 ) โ†’ ( ๐ด + ๐ต ) = ๐ด )
18 17 oveq2d โŠข ( ( ๐œ‘ โˆง ๐ต = 0 ) โ†’ ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) = ( ๐‘ƒ pCnt ๐ด ) )
19 12 18 breqtrrd โŠข ( ( ๐œ‘ โˆง ๐ต = 0 ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) )
20 19 a1d โŠข ( ( ๐œ‘ โˆง ๐ต = 0 ) โ†’ ( ( โˆƒ ๐‘ฅ โˆˆ โ„ค โˆƒ ๐‘ฆ โˆˆ โ„• ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง โˆƒ ๐‘ง โˆˆ โ„ค โˆƒ ๐‘ค โˆˆ โ„• ๐ต = ( ๐‘ง / ๐‘ค ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) ) )
21 reeanv โŠข ( โˆƒ ๐‘ฅ โˆˆ โ„ค โˆƒ ๐‘ง โˆˆ โ„ค ( โˆƒ ๐‘ฆ โˆˆ โ„• ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง โˆƒ ๐‘ค โˆˆ โ„• ๐ต = ( ๐‘ง / ๐‘ค ) ) โ†” ( โˆƒ ๐‘ฅ โˆˆ โ„ค โˆƒ ๐‘ฆ โˆˆ โ„• ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง โˆƒ ๐‘ง โˆˆ โ„ค โˆƒ ๐‘ค โˆˆ โ„• ๐ต = ( ๐‘ง / ๐‘ค ) ) )
22 reeanv โŠข ( โˆƒ ๐‘ฆ โˆˆ โ„• โˆƒ ๐‘ค โˆˆ โ„• ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) โ†” ( โˆƒ ๐‘ฆ โˆˆ โ„• ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง โˆƒ ๐‘ค โˆˆ โ„• ๐ต = ( ๐‘ง / ๐‘ค ) ) )
23 1 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ƒ โˆˆ โ„™ )
24 prmnn โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„• )
25 23 24 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ƒ โˆˆ โ„• )
26 simplrl โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ฅ โˆˆ โ„ค )
27 simprrl โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐ด = ( ๐‘ฅ / ๐‘ฆ ) )
28 pc0 โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( ๐‘ƒ pCnt 0 ) = +โˆž )
29 23 28 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt 0 ) = +โˆž )
30 3 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐ต โˆˆ โ„š )
31 simpllr โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐ต โ‰  0 )
32 pcqcl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ต โˆˆ โ„š โˆง ๐ต โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt ๐ต ) โˆˆ โ„ค )
33 23 30 31 32 syl12anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐ต ) โˆˆ โ„ค )
34 33 zred โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐ต ) โˆˆ โ„ )
35 ltpnf โŠข ( ( ๐‘ƒ pCnt ๐ต ) โˆˆ โ„ โ†’ ( ๐‘ƒ pCnt ๐ต ) < +โˆž )
36 rexr โŠข ( ( ๐‘ƒ pCnt ๐ต ) โˆˆ โ„ โ†’ ( ๐‘ƒ pCnt ๐ต ) โˆˆ โ„* )
37 pnfxr โŠข +โˆž โˆˆ โ„*
38 xrltnle โŠข ( ( ( ๐‘ƒ pCnt ๐ต ) โˆˆ โ„* โˆง +โˆž โˆˆ โ„* ) โ†’ ( ( ๐‘ƒ pCnt ๐ต ) < +โˆž โ†” ยฌ +โˆž โ‰ค ( ๐‘ƒ pCnt ๐ต ) ) )
39 36 37 38 sylancl โŠข ( ( ๐‘ƒ pCnt ๐ต ) โˆˆ โ„ โ†’ ( ( ๐‘ƒ pCnt ๐ต ) < +โˆž โ†” ยฌ +โˆž โ‰ค ( ๐‘ƒ pCnt ๐ต ) ) )
40 35 39 mpbid โŠข ( ( ๐‘ƒ pCnt ๐ต ) โˆˆ โ„ โ†’ ยฌ +โˆž โ‰ค ( ๐‘ƒ pCnt ๐ต ) )
41 34 40 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ยฌ +โˆž โ‰ค ( ๐‘ƒ pCnt ๐ต ) )
42 29 41 eqnbrtrd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ยฌ ( ๐‘ƒ pCnt 0 ) โ‰ค ( ๐‘ƒ pCnt ๐ต ) )
43 4 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ๐ต ) )
44 oveq2 โŠข ( ๐ด = 0 โ†’ ( ๐‘ƒ pCnt ๐ด ) = ( ๐‘ƒ pCnt 0 ) )
45 44 breq1d โŠข ( ๐ด = 0 โ†’ ( ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ๐ต ) โ†” ( ๐‘ƒ pCnt 0 ) โ‰ค ( ๐‘ƒ pCnt ๐ต ) ) )
46 43 45 syl5ibcom โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐ด = 0 โ†’ ( ๐‘ƒ pCnt 0 ) โ‰ค ( ๐‘ƒ pCnt ๐ต ) ) )
47 46 necon3bd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ยฌ ( ๐‘ƒ pCnt 0 ) โ‰ค ( ๐‘ƒ pCnt ๐ต ) โ†’ ๐ด โ‰  0 ) )
48 42 47 mpd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐ด โ‰  0 )
49 27 48 eqnetrrd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ฅ / ๐‘ฆ ) โ‰  0 )
50 simprll โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ฆ โˆˆ โ„• )
51 50 nncnd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ฆ โˆˆ โ„‚ )
52 50 nnne0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ฆ โ‰  0 )
53 51 52 div0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( 0 / ๐‘ฆ ) = 0 )
54 oveq1 โŠข ( ๐‘ฅ = 0 โ†’ ( ๐‘ฅ / ๐‘ฆ ) = ( 0 / ๐‘ฆ ) )
55 54 eqeq1d โŠข ( ๐‘ฅ = 0 โ†’ ( ( ๐‘ฅ / ๐‘ฆ ) = 0 โ†” ( 0 / ๐‘ฆ ) = 0 ) )
56 53 55 syl5ibrcom โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ฅ = 0 โ†’ ( ๐‘ฅ / ๐‘ฆ ) = 0 ) )
57 56 necon3d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ฅ / ๐‘ฆ ) โ‰  0 โ†’ ๐‘ฅ โ‰  0 ) )
58 49 57 mpd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ฅ โ‰  0 )
59 pczcl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฅ โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt ๐‘ฅ ) โˆˆ โ„•0 )
60 23 26 58 59 syl12anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐‘ฅ ) โˆˆ โ„•0 )
61 25 60 nnexpcld โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) โˆˆ โ„• )
62 61 nncnd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) โˆˆ โ„‚ )
63 62 51 mulcomd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ยท ๐‘ฆ ) = ( ๐‘ฆ ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) )
64 63 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ฅ ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ยท ๐‘ฆ ) ) = ( ( ๐‘ฅ ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) / ( ๐‘ฆ ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) ) )
65 26 zcnd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
66 23 50 pccld โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐‘ฆ ) โˆˆ โ„•0 )
67 25 66 nnexpcld โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โˆˆ โ„• )
68 67 nncnd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โˆˆ โ„‚ )
69 61 nnne0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) โ‰  0 )
70 67 nnne0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โ‰  0 )
71 65 62 51 68 69 70 52 divdivdivd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) / ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) ) = ( ( ๐‘ฅ ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ยท ๐‘ฆ ) ) )
72 27 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) = ( ๐‘ƒ pCnt ( ๐‘ฅ / ๐‘ฆ ) ) )
73 pcdiv โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฅ โ‰  0 ) โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( ๐‘ƒ pCnt ( ๐‘ฅ / ๐‘ฆ ) ) = ( ( ๐‘ƒ pCnt ๐‘ฅ ) โˆ’ ( ๐‘ƒ pCnt ๐‘ฆ ) ) )
74 23 26 58 50 73 syl121anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ( ๐‘ฅ / ๐‘ฆ ) ) = ( ( ๐‘ƒ pCnt ๐‘ฅ ) โˆ’ ( ๐‘ƒ pCnt ๐‘ฆ ) ) )
75 72 74 eqtrd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) = ( ( ๐‘ƒ pCnt ๐‘ฅ ) โˆ’ ( ๐‘ƒ pCnt ๐‘ฆ ) ) )
76 75 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) = ( ๐‘ƒ โ†‘ ( ( ๐‘ƒ pCnt ๐‘ฅ ) โˆ’ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) )
77 25 nncnd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ƒ โˆˆ โ„‚ )
78 25 nnne0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ƒ โ‰  0 )
79 66 nn0zd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐‘ฆ ) โˆˆ โ„ค )
80 60 nn0zd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐‘ฅ ) โˆˆ โ„ค )
81 77 78 79 80 expsubd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ( ๐‘ƒ pCnt ๐‘ฅ ) โˆ’ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) = ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) )
82 76 81 eqtrd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) = ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) )
83 82 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐ด / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) ) = ( ๐ด / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) ) )
84 27 oveq1d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐ด / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) ) = ( ( ๐‘ฅ / ๐‘ฆ ) / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) ) )
85 65 51 62 68 52 70 69 divdivdivd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ฅ / ๐‘ฆ ) / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) ) = ( ( ๐‘ฅ ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) / ( ๐‘ฆ ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) ) )
86 83 84 85 3eqtrd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐ด / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) ) = ( ( ๐‘ฅ ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) / ( ๐‘ฆ ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) ) )
87 64 71 86 3eqtr4d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) / ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) ) = ( ๐ด / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) ) )
88 87 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) ยท ( ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) / ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) ) ) = ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) ยท ( ๐ด / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) ) ) )
89 2 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐ด โˆˆ โ„š )
90 89 14 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐ด โˆˆ โ„‚ )
91 pcqcl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐ด โˆˆ โ„š โˆง ๐ด โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โˆˆ โ„ค )
92 23 89 48 91 syl12anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โˆˆ โ„ค )
93 77 78 92 expclzd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) โˆˆ โ„‚ )
94 77 78 92 expne0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) โ‰  0 )
95 90 93 94 divcan2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) ยท ( ๐ด / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) ) ) = ๐ด )
96 88 95 eqtr2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐ด = ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ด ) ) ยท ( ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) / ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) ) ) )
97 simplrr โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ง โˆˆ โ„ค )
98 simprrr โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐ต = ( ๐‘ง / ๐‘ค ) )
99 98 31 eqnetrrd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ง / ๐‘ค ) โ‰  0 )
100 simprlr โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ค โˆˆ โ„• )
101 100 nncnd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ค โˆˆ โ„‚ )
102 100 nnne0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ค โ‰  0 )
103 101 102 div0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( 0 / ๐‘ค ) = 0 )
104 oveq1 โŠข ( ๐‘ง = 0 โ†’ ( ๐‘ง / ๐‘ค ) = ( 0 / ๐‘ค ) )
105 104 eqeq1d โŠข ( ๐‘ง = 0 โ†’ ( ( ๐‘ง / ๐‘ค ) = 0 โ†” ( 0 / ๐‘ค ) = 0 ) )
106 103 105 syl5ibrcom โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ง = 0 โ†’ ( ๐‘ง / ๐‘ค ) = 0 ) )
107 106 necon3d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ง / ๐‘ค ) โ‰  0 โ†’ ๐‘ง โ‰  0 ) )
108 99 107 mpd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ง โ‰  0 )
109 pczcl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐‘ง โˆˆ โ„ค โˆง ๐‘ง โ‰  0 ) ) โ†’ ( ๐‘ƒ pCnt ๐‘ง ) โˆˆ โ„•0 )
110 23 97 108 109 syl12anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐‘ง ) โˆˆ โ„•0 )
111 25 110 nnexpcld โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) โˆˆ โ„• )
112 111 nncnd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) โˆˆ โ„‚ )
113 112 101 mulcomd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ยท ๐‘ค ) = ( ๐‘ค ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) )
114 113 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ง ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ยท ๐‘ค ) ) = ( ( ๐‘ง ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) / ( ๐‘ค ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) ) )
115 97 zcnd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ง โˆˆ โ„‚ )
116 23 100 pccld โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐‘ค ) โˆˆ โ„•0 )
117 25 116 nnexpcld โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โˆˆ โ„• )
118 117 nncnd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โˆˆ โ„‚ )
119 111 nnne0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) โ‰  0 )
120 117 nnne0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โ‰  0 )
121 115 112 101 118 119 120 102 divdivdivd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) / ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) ) = ( ( ๐‘ง ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ยท ๐‘ค ) ) )
122 98 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐ต ) = ( ๐‘ƒ pCnt ( ๐‘ง / ๐‘ค ) ) )
123 pcdiv โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐‘ง โˆˆ โ„ค โˆง ๐‘ง โ‰  0 ) โˆง ๐‘ค โˆˆ โ„• ) โ†’ ( ๐‘ƒ pCnt ( ๐‘ง / ๐‘ค ) ) = ( ( ๐‘ƒ pCnt ๐‘ง ) โˆ’ ( ๐‘ƒ pCnt ๐‘ค ) ) )
124 23 97 108 100 123 syl121anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ( ๐‘ง / ๐‘ค ) ) = ( ( ๐‘ƒ pCnt ๐‘ง ) โˆ’ ( ๐‘ƒ pCnt ๐‘ค ) ) )
125 122 124 eqtrd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐ต ) = ( ( ๐‘ƒ pCnt ๐‘ง ) โˆ’ ( ๐‘ƒ pCnt ๐‘ค ) ) )
126 125 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) = ( ๐‘ƒ โ†‘ ( ( ๐‘ƒ pCnt ๐‘ง ) โˆ’ ( ๐‘ƒ pCnt ๐‘ค ) ) ) )
127 116 nn0zd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐‘ค ) โˆˆ โ„ค )
128 110 nn0zd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐‘ง ) โˆˆ โ„ค )
129 77 78 127 128 expsubd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ( ๐‘ƒ pCnt ๐‘ง ) โˆ’ ( ๐‘ƒ pCnt ๐‘ค ) ) ) = ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) )
130 126 129 eqtrd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) = ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) )
131 130 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐ต / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) ) = ( ๐ต / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) ) )
132 98 oveq1d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐ต / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) ) = ( ( ๐‘ง / ๐‘ค ) / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) ) )
133 115 101 112 118 102 120 119 divdivdivd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ง / ๐‘ค ) / ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) ) = ( ( ๐‘ง ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) / ( ๐‘ค ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) ) )
134 131 132 133 3eqtrd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐ต / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) ) = ( ( ๐‘ง ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) / ( ๐‘ค ยท ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) ) )
135 114 121 134 3eqtr4d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) / ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) ) = ( ๐ต / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) ) )
136 135 oveq2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) ยท ( ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) / ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) ) ) = ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) ยท ( ๐ต / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) ) ) )
137 qcn โŠข ( ๐ต โˆˆ โ„š โ†’ ๐ต โˆˆ โ„‚ )
138 30 137 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐ต โˆˆ โ„‚ )
139 77 78 33 expclzd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) โˆˆ โ„‚ )
140 77 78 33 expne0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) โ‰  0 )
141 138 139 140 divcan2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) ยท ( ๐ต / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) ) ) = ๐ต )
142 136 141 eqtr2d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐ต = ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐ต ) ) ยท ( ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) / ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) ) ) )
143 eluz โŠข ( ( ( ๐‘ƒ pCnt ๐ด ) โˆˆ โ„ค โˆง ( ๐‘ƒ pCnt ๐ต ) โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ pCnt ๐ต ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ƒ pCnt ๐ด ) ) โ†” ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ๐ต ) ) )
144 92 33 143 syl2anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ pCnt ๐ต ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ƒ pCnt ๐ด ) ) โ†” ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ๐ต ) ) )
145 43 144 mpbird โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐ต ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘ƒ pCnt ๐ด ) ) )
146 pczdvds โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฅ โ‰  0 ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) โˆฅ ๐‘ฅ )
147 23 26 58 146 syl12anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) โˆฅ ๐‘ฅ )
148 61 nnzd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) โˆˆ โ„ค )
149 dvdsval2 โŠข ( ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) โˆˆ โ„ค โˆง ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) โ‰  0 โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) โˆฅ ๐‘ฅ โ†” ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) โˆˆ โ„ค ) )
150 148 69 26 149 syl3anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) โˆฅ ๐‘ฅ โ†” ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) โˆˆ โ„ค ) )
151 147 150 mpbid โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) โˆˆ โ„ค )
152 pczndvds2 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฅ โ‰  0 ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) )
153 23 26 58 152 syl12anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) )
154 151 153 jca โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) โˆˆ โ„ค โˆง ยฌ ๐‘ƒ โˆฅ ( ๐‘ฅ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฅ ) ) ) ) )
155 pcdvds โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โˆฅ ๐‘ฆ )
156 23 50 155 syl2anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โˆฅ ๐‘ฆ )
157 67 nnzd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โˆˆ โ„ค )
158 50 nnzd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ฆ โˆˆ โ„ค )
159 dvdsval2 โŠข ( ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โˆˆ โ„ค โˆง ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โ‰  0 โˆง ๐‘ฆ โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โˆฅ ๐‘ฆ โ†” ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) โˆˆ โ„ค ) )
160 157 70 158 159 syl3anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โˆฅ ๐‘ฆ โ†” ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) โˆˆ โ„ค ) )
161 156 160 mpbid โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) โˆˆ โ„ค )
162 50 nnred โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ฆ โˆˆ โ„ )
163 67 nnred โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) โˆˆ โ„ )
164 50 nngt0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ 0 < ๐‘ฆ )
165 67 nngt0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ 0 < ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) )
166 162 163 164 165 divgt0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ 0 < ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) )
167 elnnz โŠข ( ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) โˆˆ โ„• โ†” ( ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) โˆˆ โ„ค โˆง 0 < ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) ) )
168 161 166 167 sylanbrc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) โˆˆ โ„• )
169 pcndvds2 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ฆ โˆˆ โ„• ) โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) )
170 23 50 169 syl2anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) )
171 168 170 jca โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) โˆˆ โ„• โˆง ยฌ ๐‘ƒ โˆฅ ( ๐‘ฆ / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ฆ ) ) ) ) )
172 pczdvds โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐‘ง โˆˆ โ„ค โˆง ๐‘ง โ‰  0 ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) โˆฅ ๐‘ง )
173 23 97 108 172 syl12anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) โˆฅ ๐‘ง )
174 111 nnzd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) โˆˆ โ„ค )
175 dvdsval2 โŠข ( ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) โˆˆ โ„ค โˆง ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) โ‰  0 โˆง ๐‘ง โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) โˆฅ ๐‘ง โ†” ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) โˆˆ โ„ค ) )
176 174 119 97 175 syl3anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) โˆฅ ๐‘ง โ†” ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) โˆˆ โ„ค ) )
177 173 176 mpbid โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) โˆˆ โ„ค )
178 pczndvds2 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ( ๐‘ง โˆˆ โ„ค โˆง ๐‘ง โ‰  0 ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) )
179 23 97 108 178 syl12anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) )
180 177 179 jca โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) โˆˆ โ„ค โˆง ยฌ ๐‘ƒ โˆฅ ( ๐‘ง / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ง ) ) ) ) )
181 pcdvds โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ค โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โˆฅ ๐‘ค )
182 23 100 181 syl2anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โˆฅ ๐‘ค )
183 117 nnzd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โˆˆ โ„ค )
184 100 nnzd โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ค โˆˆ โ„ค )
185 dvdsval2 โŠข ( ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โˆˆ โ„ค โˆง ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โ‰  0 โˆง ๐‘ค โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โˆฅ ๐‘ค โ†” ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) โˆˆ โ„ค ) )
186 183 120 184 185 syl3anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โˆฅ ๐‘ค โ†” ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) โˆˆ โ„ค ) )
187 182 186 mpbid โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) โˆˆ โ„ค )
188 100 nnred โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ๐‘ค โˆˆ โ„ )
189 117 nnred โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) โˆˆ โ„ )
190 100 nngt0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ 0 < ๐‘ค )
191 117 nngt0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ 0 < ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) )
192 188 189 190 191 divgt0d โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ 0 < ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) )
193 elnnz โŠข ( ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) โˆˆ โ„• โ†” ( ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) โˆˆ โ„ค โˆง 0 < ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) ) )
194 187 192 193 sylanbrc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) โˆˆ โ„• )
195 pcndvds2 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ค โˆˆ โ„• ) โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) )
196 23 100 195 syl2anc โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) )
197 194 196 jca โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) โˆˆ โ„• โˆง ยฌ ๐‘ƒ โˆฅ ( ๐‘ค / ( ๐‘ƒ โ†‘ ( ๐‘ƒ pCnt ๐‘ค ) ) ) ) )
198 23 96 142 145 154 171 180 197 pcaddlem โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) โˆง ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) )
199 198 expr โŠข ( ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โˆง ( ๐‘ฆ โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„• ) ) โ†’ ( ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) ) )
200 199 rexlimdvva โŠข ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โ†’ ( โˆƒ ๐‘ฆ โˆˆ โ„• โˆƒ ๐‘ค โˆˆ โ„• ( ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง ๐ต = ( ๐‘ง / ๐‘ค ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) ) )
201 22 200 syl5bir โŠข ( ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ง โˆˆ โ„ค ) ) โ†’ ( ( โˆƒ ๐‘ฆ โˆˆ โ„• ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง โˆƒ ๐‘ค โˆˆ โ„• ๐ต = ( ๐‘ง / ๐‘ค ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) ) )
202 201 rexlimdvva โŠข ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โ†’ ( โˆƒ ๐‘ฅ โˆˆ โ„ค โˆƒ ๐‘ง โˆˆ โ„ค ( โˆƒ ๐‘ฆ โˆˆ โ„• ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง โˆƒ ๐‘ค โˆˆ โ„• ๐ต = ( ๐‘ง / ๐‘ค ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) ) )
203 21 202 syl5bir โŠข ( ( ๐œ‘ โˆง ๐ต โ‰  0 ) โ†’ ( ( โˆƒ ๐‘ฅ โˆˆ โ„ค โˆƒ ๐‘ฆ โˆˆ โ„• ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง โˆƒ ๐‘ง โˆˆ โ„ค โˆƒ ๐‘ค โˆˆ โ„• ๐ต = ( ๐‘ง / ๐‘ค ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) ) )
204 20 203 pm2.61dane โŠข ( ๐œ‘ โ†’ ( ( โˆƒ ๐‘ฅ โˆˆ โ„ค โˆƒ ๐‘ฆ โˆˆ โ„• ๐ด = ( ๐‘ฅ / ๐‘ฆ ) โˆง โˆƒ ๐‘ง โˆˆ โ„ค โˆƒ ๐‘ค โˆˆ โ„• ๐ต = ( ๐‘ง / ๐‘ค ) ) โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) ) )
205 6 8 204 mp2and โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ pCnt ๐ด ) โ‰ค ( ๐‘ƒ pCnt ( ๐ด + ๐ต ) ) )