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 ( ๐ด + ๐ต ) ) ) |