Step | Hyp | Ref
| Expression |
1 | | pcadd.2 |
. . 3
โข (๐ โ ๐ด โ โ) |
2 | | elq 9621 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ โค
โ๐ฆ โ โ
๐ด = (๐ฅ / ๐ฆ)) |
3 | 1, 2 | sylib 122 |
. 2
โข (๐ โ โ๐ฅ โ โค โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ)) |
4 | | pcadd.3 |
. . 3
โข (๐ โ ๐ต โ โ) |
5 | | elq 9621 |
. . 3
โข (๐ต โ โ โ
โ๐ง โ โค
โ๐ค โ โ
๐ต = (๐ง / ๐ค)) |
6 | 4, 5 | sylib 122 |
. 2
โข (๐ โ โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค)) |
7 | | pcadd.1 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
8 | | pcxcl 12310 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ pCnt ๐ด) โ
โ*) |
9 | 7, 1, 8 | syl2anc 411 |
. . . . . . 7
โข (๐ โ (๐ pCnt ๐ด) โ
โ*) |
10 | 9 | xrleidd 9800 |
. . . . . 6
โข (๐ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ด)) |
11 | 10 | adantr 276 |
. . . . 5
โข ((๐ โง ๐ต = 0) โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ด)) |
12 | | oveq2 5882 |
. . . . . . 7
โข (๐ต = 0 โ (๐ด + ๐ต) = (๐ด + 0)) |
13 | | qcn 9633 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ) |
14 | 1, 13 | syl 14 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
15 | 14 | addid1d 8105 |
. . . . . . 7
โข (๐ โ (๐ด + 0) = ๐ด) |
16 | 12, 15 | sylan9eqr 2232 |
. . . . . 6
โข ((๐ โง ๐ต = 0) โ (๐ด + ๐ต) = ๐ด) |
17 | 16 | oveq2d 5890 |
. . . . 5
โข ((๐ โง ๐ต = 0) โ (๐ pCnt (๐ด + ๐ต)) = (๐ pCnt ๐ด)) |
18 | 11, 17 | breqtrrd 4031 |
. . . 4
โข ((๐ โง ๐ต = 0) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด + ๐ต))) |
19 | 18 | a1d 22 |
. . 3
โข ((๐ โง ๐ต = 0) โ ((โ๐ฅ โ โค โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด + ๐ต)))) |
20 | | reeanv 2646 |
. . . 4
โข
(โ๐ฅ โ
โค โ๐ง โ
โค (โ๐ฆ โ
โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (โ๐ฅ โ โค โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค))) |
21 | | reeanv 2646 |
. . . . . 6
โข
(โ๐ฆ โ
โ โ๐ค โ
โ (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ค โ โ ๐ต = (๐ง / ๐ค))) |
22 | 7 | ad3antrrr 492 |
. . . . . . . . 9
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ โ โ) |
23 | | prmnn 12109 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โ) |
24 | 22, 23 | syl 14 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ โ โ) |
25 | | simplrl 535 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ฅ โ โค) |
26 | | simprrl 539 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ด = (๐ฅ / ๐ฆ)) |
27 | | pc0 12303 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (๐ pCnt 0) =
+โ) |
28 | 22, 27 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt 0) = +โ) |
29 | 4 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ต โ โ) |
30 | | simpllr 534 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ต โ 0) |
31 | | pcqcl 12305 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt ๐ต) โ โค) |
32 | 22, 29, 30, 31 | syl12anc 1236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ต) โ โค) |
33 | 32 | zred 9374 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ต) โ โ) |
34 | 33 | ltpnfd 9780 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ต) < +โ) |
35 | | pnfxr 8009 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข +โ
โ โ* |
36 | 33 | rexrd 8006 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ต) โ
โ*) |
37 | | xrlenlt 8021 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
((+โ โ โ* โง (๐ pCnt ๐ต) โ โ*) โ
(+โ โค (๐ pCnt
๐ต) โ ยฌ (๐ pCnt ๐ต) < +โ)) |
38 | 35, 36, 37 | sylancr 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (+โ โค (๐ pCnt ๐ต) โ ยฌ (๐ pCnt ๐ต) < +โ)) |
39 | 38 | biimpd 144 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (+โ โค (๐ pCnt ๐ต) โ ยฌ (๐ pCnt ๐ต) < +โ)) |
40 | 34, 39 | mt2d 625 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ยฌ +โ โค (๐ pCnt ๐ต)) |
41 | 28, 40 | eqnbrtrd 4021 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ยฌ (๐ pCnt 0) โค (๐ pCnt ๐ต)) |
42 | | pcadd.4 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)) |
43 | 42 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต)) |
44 | | oveq2 5882 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ด = 0 โ (๐ pCnt ๐ด) = (๐ pCnt 0)) |
45 | 44 | breq1d 4013 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ด = 0 โ ((๐ pCnt ๐ด) โค (๐ pCnt ๐ต) โ (๐ pCnt 0) โค (๐ pCnt ๐ต))) |
46 | 43, 45 | syl5ibcom 155 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ด = 0 โ (๐ pCnt 0) โค (๐ pCnt ๐ต))) |
47 | 46 | necon3bd 2390 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (ยฌ (๐ pCnt 0) โค (๐ pCnt ๐ต) โ ๐ด โ 0)) |
48 | 41, 47 | mpd 13 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ด โ 0) |
49 | 26, 48 | eqnetrrd 2373 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ฅ / ๐ฆ) โ 0) |
50 | | simprll 537 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ฆ โ โ) |
51 | 50 | nncnd 8932 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ฆ โ โ) |
52 | 50 | nnap0d 8964 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ฆ # 0) |
53 | 51, 52 | div0apd 8743 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (0 / ๐ฆ) = 0) |
54 | | oveq1 5881 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ = 0 โ (๐ฅ / ๐ฆ) = (0 / ๐ฆ)) |
55 | 54 | eqeq1d 2186 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ = 0 โ ((๐ฅ / ๐ฆ) = 0 โ (0 / ๐ฆ) = 0)) |
56 | 53, 55 | syl5ibrcom 157 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ฅ = 0 โ (๐ฅ / ๐ฆ) = 0)) |
57 | 56 | necon3d 2391 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ฅ / ๐ฆ) โ 0 โ ๐ฅ โ 0)) |
58 | 49, 57 | mpd 13 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ฅ โ 0) |
59 | | pczcl 12297 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฅ โ 0)) โ (๐ pCnt ๐ฅ) โ
โ0) |
60 | 22, 25, 58, 59 | syl12anc 1236 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ฅ) โ
โ0) |
61 | 24, 60 | nnexpcld 10675 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฅ)) โ โ) |
62 | 61 | nncnd 8932 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฅ)) โ โ) |
63 | 62, 51 | mulcomd 7978 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ฅ)) ยท ๐ฆ) = (๐ฆ ยท (๐โ(๐ pCnt ๐ฅ)))) |
64 | 63 | oveq2d 5890 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ฅ ยท (๐โ(๐ pCnt ๐ฆ))) / ((๐โ(๐ pCnt ๐ฅ)) ยท ๐ฆ)) = ((๐ฅ ยท (๐โ(๐ pCnt ๐ฆ))) / (๐ฆ ยท (๐โ(๐ pCnt ๐ฅ))))) |
65 | 25 | zcnd 9375 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ฅ โ โ) |
66 | 61 | nnap0d 8964 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฅ)) # 0) |
67 | 62, 66 | jca 306 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ฅ)) โ โ โง (๐โ(๐ pCnt ๐ฅ)) # 0)) |
68 | 51, 52 | jca 306 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ฆ โ โ โง ๐ฆ # 0)) |
69 | 22, 50 | pccld 12299 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ฆ) โ
โ0) |
70 | 24, 69 | nnexpcld 10675 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฆ)) โ โ) |
71 | 70 | nncnd 8932 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฆ)) โ โ) |
72 | 70 | nnap0d 8964 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฆ)) # 0) |
73 | 71, 72 | jca 306 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ฆ)) โ โ โง (๐โ(๐ pCnt ๐ฆ)) # 0)) |
74 | | divdivdivap 8669 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ((๐โ(๐ pCnt ๐ฅ)) โ โ โง (๐โ(๐ pCnt ๐ฅ)) # 0)) โง ((๐ฆ โ โ โง ๐ฆ # 0) โง ((๐โ(๐ pCnt ๐ฆ)) โ โ โง (๐โ(๐ pCnt ๐ฆ)) # 0))) โ ((๐ฅ / (๐โ(๐ pCnt ๐ฅ))) / (๐ฆ / (๐โ(๐ pCnt ๐ฆ)))) = ((๐ฅ ยท (๐โ(๐ pCnt ๐ฆ))) / ((๐โ(๐ pCnt ๐ฅ)) ยท ๐ฆ))) |
75 | 65, 67, 68, 73, 74 | syl22anc 1239 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ฅ / (๐โ(๐ pCnt ๐ฅ))) / (๐ฆ / (๐โ(๐ pCnt ๐ฆ)))) = ((๐ฅ ยท (๐โ(๐ pCnt ๐ฆ))) / ((๐โ(๐ pCnt ๐ฅ)) ยท ๐ฆ))) |
76 | 26 | oveq2d 5890 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ด) = (๐ pCnt (๐ฅ / ๐ฆ))) |
77 | | pcdiv 12301 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฅ โ 0) โง ๐ฆ โ โ) โ (๐ pCnt (๐ฅ / ๐ฆ)) = ((๐ pCnt ๐ฅ) โ (๐ pCnt ๐ฆ))) |
78 | 22, 25, 58, 50, 77 | syl121anc 1243 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt (๐ฅ / ๐ฆ)) = ((๐ pCnt ๐ฅ) โ (๐ pCnt ๐ฆ))) |
79 | 76, 78 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ด) = ((๐ pCnt ๐ฅ) โ (๐ pCnt ๐ฆ))) |
80 | 79 | oveq2d 5890 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ด)) = (๐โ((๐ pCnt ๐ฅ) โ (๐ pCnt ๐ฆ)))) |
81 | 24 | nncnd 8932 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ โ โ) |
82 | 24 | nnap0d 8964 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ # 0) |
83 | 69 | nn0zd 9372 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ฆ) โ โค) |
84 | 60 | nn0zd 9372 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ฅ) โ โค) |
85 | 81, 82, 83, 84 | expsubapd 10664 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ((๐ pCnt ๐ฅ) โ (๐ pCnt ๐ฆ))) = ((๐โ(๐ pCnt ๐ฅ)) / (๐โ(๐ pCnt ๐ฆ)))) |
86 | 80, 85 | eqtrd 2210 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ด)) = ((๐โ(๐ pCnt ๐ฅ)) / (๐โ(๐ pCnt ๐ฆ)))) |
87 | 86 | oveq2d 5890 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ด / (๐โ(๐ pCnt ๐ด))) = (๐ด / ((๐โ(๐ pCnt ๐ฅ)) / (๐โ(๐ pCnt ๐ฆ))))) |
88 | 26 | oveq1d 5889 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ด / ((๐โ(๐ pCnt ๐ฅ)) / (๐โ(๐ pCnt ๐ฆ)))) = ((๐ฅ / ๐ฆ) / ((๐โ(๐ pCnt ๐ฅ)) / (๐โ(๐ pCnt ๐ฆ))))) |
89 | | divdivdivap 8669 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โ โง (๐ฆ โ โ โง ๐ฆ # 0)) โง (((๐โ(๐ pCnt ๐ฅ)) โ โ โง (๐โ(๐ pCnt ๐ฅ)) # 0) โง ((๐โ(๐ pCnt ๐ฆ)) โ โ โง (๐โ(๐ pCnt ๐ฆ)) # 0))) โ ((๐ฅ / ๐ฆ) / ((๐โ(๐ pCnt ๐ฅ)) / (๐โ(๐ pCnt ๐ฆ)))) = ((๐ฅ ยท (๐โ(๐ pCnt ๐ฆ))) / (๐ฆ ยท (๐โ(๐ pCnt ๐ฅ))))) |
90 | 65, 68, 67, 73, 89 | syl22anc 1239 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ฅ / ๐ฆ) / ((๐โ(๐ pCnt ๐ฅ)) / (๐โ(๐ pCnt ๐ฆ)))) = ((๐ฅ ยท (๐โ(๐ pCnt ๐ฆ))) / (๐ฆ ยท (๐โ(๐ pCnt ๐ฅ))))) |
91 | 87, 88, 90 | 3eqtrd 2214 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ด / (๐โ(๐ pCnt ๐ด))) = ((๐ฅ ยท (๐โ(๐ pCnt ๐ฆ))) / (๐ฆ ยท (๐โ(๐ pCnt ๐ฅ))))) |
92 | 64, 75, 91 | 3eqtr4d 2220 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ฅ / (๐โ(๐ pCnt ๐ฅ))) / (๐ฆ / (๐โ(๐ pCnt ๐ฆ)))) = (๐ด / (๐โ(๐ pCnt ๐ด)))) |
93 | 92 | oveq2d 5890 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ด)) ยท ((๐ฅ / (๐โ(๐ pCnt ๐ฅ))) / (๐ฆ / (๐โ(๐ pCnt ๐ฆ))))) = ((๐โ(๐ pCnt ๐ด)) ยท (๐ด / (๐โ(๐ pCnt ๐ด))))) |
94 | 1 | ad3antrrr 492 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ด โ โ) |
95 | 94, 13 | syl 14 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ด โ โ) |
96 | | pcqcl 12305 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0)) โ (๐ pCnt ๐ด) โ โค) |
97 | 22, 94, 48, 96 | syl12anc 1236 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ด) โ โค) |
98 | 81, 82, 97 | expclzapd 10658 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ด)) โ โ) |
99 | 81, 82, 97 | expap0d 10659 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ด)) # 0) |
100 | 95, 98, 99 | divcanap2d 8748 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ด)) ยท (๐ด / (๐โ(๐ pCnt ๐ด)))) = ๐ด) |
101 | 93, 100 | eqtr2d 2211 |
. . . . . . . . 9
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ด = ((๐โ(๐ pCnt ๐ด)) ยท ((๐ฅ / (๐โ(๐ pCnt ๐ฅ))) / (๐ฆ / (๐โ(๐ pCnt ๐ฆ)))))) |
102 | | simplrr 536 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ง โ โค) |
103 | | simprrr 540 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ต = (๐ง / ๐ค)) |
104 | 103, 30 | eqnetrrd 2373 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ง / ๐ค) โ 0) |
105 | | simprlr 538 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ค โ โ) |
106 | 105 | nncnd 8932 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ค โ โ) |
107 | 105 | nnap0d 8964 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ค # 0) |
108 | 106, 107 | div0apd 8743 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (0 / ๐ค) = 0) |
109 | | oveq1 5881 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ง = 0 โ (๐ง / ๐ค) = (0 / ๐ค)) |
110 | 109 | eqeq1d 2186 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง = 0 โ ((๐ง / ๐ค) = 0 โ (0 / ๐ค) = 0)) |
111 | 108, 110 | syl5ibrcom 157 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ง = 0 โ (๐ง / ๐ค) = 0)) |
112 | 111 | necon3d 2391 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ง / ๐ค) โ 0 โ ๐ง โ 0)) |
113 | 104, 112 | mpd 13 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ง โ 0) |
114 | | pczcl 12297 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง (๐ง โ โค โง ๐ง โ 0)) โ (๐ pCnt ๐ง) โ
โ0) |
115 | 22, 102, 113, 114 | syl12anc 1236 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ง) โ
โ0) |
116 | 24, 115 | nnexpcld 10675 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ง)) โ โ) |
117 | 116 | nncnd 8932 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ง)) โ โ) |
118 | 117, 106 | mulcomd 7978 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ง)) ยท ๐ค) = (๐ค ยท (๐โ(๐ pCnt ๐ง)))) |
119 | 118 | oveq2d 5890 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ง ยท (๐โ(๐ pCnt ๐ค))) / ((๐โ(๐ pCnt ๐ง)) ยท ๐ค)) = ((๐ง ยท (๐โ(๐ pCnt ๐ค))) / (๐ค ยท (๐โ(๐ pCnt ๐ง))))) |
120 | 102 | zcnd 9375 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ง โ โ) |
121 | 116 | nnap0d 8964 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ง)) # 0) |
122 | 117, 121 | jca 306 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ง)) โ โ โง (๐โ(๐ pCnt ๐ง)) # 0)) |
123 | 106, 107 | jca 306 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ค โ โ โง ๐ค # 0)) |
124 | 22, 105 | pccld 12299 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ค) โ
โ0) |
125 | 24, 124 | nnexpcld 10675 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ค)) โ โ) |
126 | 125 | nncnd 8932 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ค)) โ โ) |
127 | 125 | nnap0d 8964 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ค)) # 0) |
128 | 126, 127 | jca 306 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ค)) โ โ โง (๐โ(๐ pCnt ๐ค)) # 0)) |
129 | | divdivdivap 8669 |
. . . . . . . . . . . . 13
โข (((๐ง โ โ โง ((๐โ(๐ pCnt ๐ง)) โ โ โง (๐โ(๐ pCnt ๐ง)) # 0)) โง ((๐ค โ โ โง ๐ค # 0) โง ((๐โ(๐ pCnt ๐ค)) โ โ โง (๐โ(๐ pCnt ๐ค)) # 0))) โ ((๐ง / (๐โ(๐ pCnt ๐ง))) / (๐ค / (๐โ(๐ pCnt ๐ค)))) = ((๐ง ยท (๐โ(๐ pCnt ๐ค))) / ((๐โ(๐ pCnt ๐ง)) ยท ๐ค))) |
130 | 120, 122,
123, 128, 129 | syl22anc 1239 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ง / (๐โ(๐ pCnt ๐ง))) / (๐ค / (๐โ(๐ pCnt ๐ค)))) = ((๐ง ยท (๐โ(๐ pCnt ๐ค))) / ((๐โ(๐ pCnt ๐ง)) ยท ๐ค))) |
131 | 103 | oveq2d 5890 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ต) = (๐ pCnt (๐ง / ๐ค))) |
132 | | pcdiv 12301 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง (๐ง โ โค โง ๐ง โ 0) โง ๐ค โ โ) โ (๐ pCnt (๐ง / ๐ค)) = ((๐ pCnt ๐ง) โ (๐ pCnt ๐ค))) |
133 | 22, 102, 113, 105, 132 | syl121anc 1243 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt (๐ง / ๐ค)) = ((๐ pCnt ๐ง) โ (๐ pCnt ๐ค))) |
134 | 131, 133 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ต) = ((๐ pCnt ๐ง) โ (๐ pCnt ๐ค))) |
135 | 134 | oveq2d 5890 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ต)) = (๐โ((๐ pCnt ๐ง) โ (๐ pCnt ๐ค)))) |
136 | 124 | nn0zd 9372 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ค) โ โค) |
137 | 115 | nn0zd 9372 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ง) โ โค) |
138 | 81, 82, 136, 137 | expsubapd 10664 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ((๐ pCnt ๐ง) โ (๐ pCnt ๐ค))) = ((๐โ(๐ pCnt ๐ง)) / (๐โ(๐ pCnt ๐ค)))) |
139 | 135, 138 | eqtrd 2210 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ต)) = ((๐โ(๐ pCnt ๐ง)) / (๐โ(๐ pCnt ๐ค)))) |
140 | 139 | oveq2d 5890 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ต / (๐โ(๐ pCnt ๐ต))) = (๐ต / ((๐โ(๐ pCnt ๐ง)) / (๐โ(๐ pCnt ๐ค))))) |
141 | 103 | oveq1d 5889 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ต / ((๐โ(๐ pCnt ๐ง)) / (๐โ(๐ pCnt ๐ค)))) = ((๐ง / ๐ค) / ((๐โ(๐ pCnt ๐ง)) / (๐โ(๐ pCnt ๐ค))))) |
142 | | divdivdivap 8669 |
. . . . . . . . . . . . . 14
โข (((๐ง โ โ โง (๐ค โ โ โง ๐ค # 0)) โง (((๐โ(๐ pCnt ๐ง)) โ โ โง (๐โ(๐ pCnt ๐ง)) # 0) โง ((๐โ(๐ pCnt ๐ค)) โ โ โง (๐โ(๐ pCnt ๐ค)) # 0))) โ ((๐ง / ๐ค) / ((๐โ(๐ pCnt ๐ง)) / (๐โ(๐ pCnt ๐ค)))) = ((๐ง ยท (๐โ(๐ pCnt ๐ค))) / (๐ค ยท (๐โ(๐ pCnt ๐ง))))) |
143 | 120, 123,
122, 128, 142 | syl22anc 1239 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ง / ๐ค) / ((๐โ(๐ pCnt ๐ง)) / (๐โ(๐ pCnt ๐ค)))) = ((๐ง ยท (๐โ(๐ pCnt ๐ค))) / (๐ค ยท (๐โ(๐ pCnt ๐ง))))) |
144 | 140, 141,
143 | 3eqtrd 2214 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ต / (๐โ(๐ pCnt ๐ต))) = ((๐ง ยท (๐โ(๐ pCnt ๐ค))) / (๐ค ยท (๐โ(๐ pCnt ๐ง))))) |
145 | 119, 130,
144 | 3eqtr4d 2220 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ง / (๐โ(๐ pCnt ๐ง))) / (๐ค / (๐โ(๐ pCnt ๐ค)))) = (๐ต / (๐โ(๐ pCnt ๐ต)))) |
146 | 145 | oveq2d 5890 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ต)) ยท ((๐ง / (๐โ(๐ pCnt ๐ง))) / (๐ค / (๐โ(๐ pCnt ๐ค))))) = ((๐โ(๐ pCnt ๐ต)) ยท (๐ต / (๐โ(๐ pCnt ๐ต))))) |
147 | | qcn 9633 |
. . . . . . . . . . . 12
โข (๐ต โ โ โ ๐ต โ
โ) |
148 | 29, 147 | syl 14 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ต โ โ) |
149 | 81, 82, 32 | expclzapd 10658 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ต)) โ โ) |
150 | 81, 82, 32 | expap0d 10659 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ต)) # 0) |
151 | 148, 149,
150 | divcanap2d 8748 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ต)) ยท (๐ต / (๐โ(๐ pCnt ๐ต)))) = ๐ต) |
152 | 146, 151 | eqtr2d 2211 |
. . . . . . . . 9
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ต = ((๐โ(๐ pCnt ๐ต)) ยท ((๐ง / (๐โ(๐ pCnt ๐ง))) / (๐ค / (๐โ(๐ pCnt ๐ค)))))) |
153 | | eluz 9540 |
. . . . . . . . . . 11
โข (((๐ pCnt ๐ด) โ โค โง (๐ pCnt ๐ต) โ โค) โ ((๐ pCnt ๐ต) โ
(โคโฅโ(๐ pCnt ๐ด)) โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต))) |
154 | 97, 32, 153 | syl2anc 411 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ pCnt ๐ต) โ
(โคโฅโ(๐ pCnt ๐ด)) โ (๐ pCnt ๐ด) โค (๐ pCnt ๐ต))) |
155 | 43, 154 | mpbird 167 |
. . . . . . . . 9
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ต) โ
(โคโฅโ(๐ pCnt ๐ด))) |
156 | | pczdvds 12312 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฅ โ 0)) โ (๐โ(๐ pCnt ๐ฅ)) โฅ ๐ฅ) |
157 | 22, 25, 58, 156 | syl12anc 1236 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฅ)) โฅ ๐ฅ) |
158 | 61 | nnzd 9373 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฅ)) โ โค) |
159 | 61 | nnne0d 8963 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฅ)) โ 0) |
160 | | dvdsval2 11796 |
. . . . . . . . . . . 12
โข (((๐โ(๐ pCnt ๐ฅ)) โ โค โง (๐โ(๐ pCnt ๐ฅ)) โ 0 โง ๐ฅ โ โค) โ ((๐โ(๐ pCnt ๐ฅ)) โฅ ๐ฅ โ (๐ฅ / (๐โ(๐ pCnt ๐ฅ))) โ โค)) |
161 | 158, 159,
25, 160 | syl3anc 1238 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ฅ)) โฅ ๐ฅ โ (๐ฅ / (๐โ(๐ pCnt ๐ฅ))) โ โค)) |
162 | 157, 161 | mpbid 147 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ฅ / (๐โ(๐ pCnt ๐ฅ))) โ โค) |
163 | | pczndvds2 12316 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฅ โ 0)) โ ยฌ ๐ โฅ (๐ฅ / (๐โ(๐ pCnt ๐ฅ)))) |
164 | 22, 25, 58, 163 | syl12anc 1236 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ยฌ ๐ โฅ (๐ฅ / (๐โ(๐ pCnt ๐ฅ)))) |
165 | 162, 164 | jca 306 |
. . . . . . . . 9
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ฅ / (๐โ(๐ pCnt ๐ฅ))) โ โค โง ยฌ ๐ โฅ (๐ฅ / (๐โ(๐ pCnt ๐ฅ))))) |
166 | | pcdvds 12313 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ฆ โ โ) โ (๐โ(๐ pCnt ๐ฆ)) โฅ ๐ฆ) |
167 | 22, 50, 166 | syl2anc 411 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฆ)) โฅ ๐ฆ) |
168 | 70 | nnzd 9373 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฆ)) โ โค) |
169 | 70 | nnne0d 8963 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฆ)) โ 0) |
170 | 50 | nnzd 9373 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ฆ โ โค) |
171 | | dvdsval2 11796 |
. . . . . . . . . . . . 13
โข (((๐โ(๐ pCnt ๐ฆ)) โ โค โง (๐โ(๐ pCnt ๐ฆ)) โ 0 โง ๐ฆ โ โค) โ ((๐โ(๐ pCnt ๐ฆ)) โฅ ๐ฆ โ (๐ฆ / (๐โ(๐ pCnt ๐ฆ))) โ โค)) |
172 | 168, 169,
170, 171 | syl3anc 1238 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ฆ)) โฅ ๐ฆ โ (๐ฆ / (๐โ(๐ pCnt ๐ฆ))) โ โค)) |
173 | 167, 172 | mpbid 147 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ฆ / (๐โ(๐ pCnt ๐ฆ))) โ โค) |
174 | 50 | nnred 8931 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ฆ โ โ) |
175 | 70 | nnred 8931 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ฆ)) โ โ) |
176 | 50 | nngt0d 8962 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ 0 < ๐ฆ) |
177 | 70 | nngt0d 8962 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ 0 < (๐โ(๐ pCnt ๐ฆ))) |
178 | 174, 175,
176, 177 | divgt0d 8891 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ 0 < (๐ฆ / (๐โ(๐ pCnt ๐ฆ)))) |
179 | | elnnz 9262 |
. . . . . . . . . . 11
โข ((๐ฆ / (๐โ(๐ pCnt ๐ฆ))) โ โ โ ((๐ฆ / (๐โ(๐ pCnt ๐ฆ))) โ โค โง 0 < (๐ฆ / (๐โ(๐ pCnt ๐ฆ))))) |
180 | 173, 178,
179 | sylanbrc 417 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ฆ / (๐โ(๐ pCnt ๐ฆ))) โ โ) |
181 | | pcndvds2 12317 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ฆ โ โ) โ ยฌ
๐ โฅ (๐ฆ / (๐โ(๐ pCnt ๐ฆ)))) |
182 | 22, 50, 181 | syl2anc 411 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ยฌ ๐ โฅ (๐ฆ / (๐โ(๐ pCnt ๐ฆ)))) |
183 | 180, 182 | jca 306 |
. . . . . . . . 9
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ฆ / (๐โ(๐ pCnt ๐ฆ))) โ โ โง ยฌ ๐ โฅ (๐ฆ / (๐โ(๐ pCnt ๐ฆ))))) |
184 | | pczdvds 12312 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ง โ โค โง ๐ง โ 0)) โ (๐โ(๐ pCnt ๐ง)) โฅ ๐ง) |
185 | 22, 102, 113, 184 | syl12anc 1236 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ง)) โฅ ๐ง) |
186 | 116 | nnzd 9373 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ง)) โ โค) |
187 | 116 | nnne0d 8963 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ง)) โ 0) |
188 | | dvdsval2 11796 |
. . . . . . . . . . . 12
โข (((๐โ(๐ pCnt ๐ง)) โ โค โง (๐โ(๐ pCnt ๐ง)) โ 0 โง ๐ง โ โค) โ ((๐โ(๐ pCnt ๐ง)) โฅ ๐ง โ (๐ง / (๐โ(๐ pCnt ๐ง))) โ โค)) |
189 | 186, 187,
102, 188 | syl3anc 1238 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ง)) โฅ ๐ง โ (๐ง / (๐โ(๐ pCnt ๐ง))) โ โค)) |
190 | 185, 189 | mpbid 147 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ง / (๐โ(๐ pCnt ๐ง))) โ โค) |
191 | | pczndvds2 12316 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ง โ โค โง ๐ง โ 0)) โ ยฌ ๐ โฅ (๐ง / (๐โ(๐ pCnt ๐ง)))) |
192 | 22, 102, 113, 191 | syl12anc 1236 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ยฌ ๐ โฅ (๐ง / (๐โ(๐ pCnt ๐ง)))) |
193 | 190, 192 | jca 306 |
. . . . . . . . 9
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ง / (๐โ(๐ pCnt ๐ง))) โ โค โง ยฌ ๐ โฅ (๐ง / (๐โ(๐ pCnt ๐ง))))) |
194 | | pcdvds 12313 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ค โ โ) โ (๐โ(๐ pCnt ๐ค)) โฅ ๐ค) |
195 | 22, 105, 194 | syl2anc 411 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ค)) โฅ ๐ค) |
196 | 125 | nnzd 9373 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ค)) โ โค) |
197 | 125 | nnne0d 8963 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ค)) โ 0) |
198 | 105 | nnzd 9373 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ค โ โค) |
199 | | dvdsval2 11796 |
. . . . . . . . . . . . 13
โข (((๐โ(๐ pCnt ๐ค)) โ โค โง (๐โ(๐ pCnt ๐ค)) โ 0 โง ๐ค โ โค) โ ((๐โ(๐ pCnt ๐ค)) โฅ ๐ค โ (๐ค / (๐โ(๐ pCnt ๐ค))) โ โค)) |
200 | 196, 197,
198, 199 | syl3anc 1238 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐โ(๐ pCnt ๐ค)) โฅ ๐ค โ (๐ค / (๐โ(๐ pCnt ๐ค))) โ โค)) |
201 | 195, 200 | mpbid 147 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ค / (๐โ(๐ pCnt ๐ค))) โ โค) |
202 | 105 | nnred 8931 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ๐ค โ โ) |
203 | 125 | nnred 8931 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐โ(๐ pCnt ๐ค)) โ โ) |
204 | 105 | nngt0d 8962 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ 0 < ๐ค) |
205 | 125 | nngt0d 8962 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ 0 < (๐โ(๐ pCnt ๐ค))) |
206 | 202, 203,
204, 205 | divgt0d 8891 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ 0 < (๐ค / (๐โ(๐ pCnt ๐ค)))) |
207 | | elnnz 9262 |
. . . . . . . . . . 11
โข ((๐ค / (๐โ(๐ pCnt ๐ค))) โ โ โ ((๐ค / (๐โ(๐ pCnt ๐ค))) โ โค โง 0 < (๐ค / (๐โ(๐ pCnt ๐ค))))) |
208 | 201, 206,
207 | sylanbrc 417 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ค / (๐โ(๐ pCnt ๐ค))) โ โ) |
209 | | pcndvds2 12317 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ค โ โ) โ ยฌ
๐ โฅ (๐ค / (๐โ(๐ pCnt ๐ค)))) |
210 | 22, 105, 209 | syl2anc 411 |
. . . . . . . . . 10
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ยฌ ๐ โฅ (๐ค / (๐โ(๐ pCnt ๐ค)))) |
211 | 208, 210 | jca 306 |
. . . . . . . . 9
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ ((๐ค / (๐โ(๐ pCnt ๐ค))) โ โ โง ยฌ ๐ โฅ (๐ค / (๐โ(๐ pCnt ๐ค))))) |
212 | 22, 101, 152, 155, 165, 183, 193, 211 | pcaddlem 12337 |
. . . . . . . 8
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)))) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด + ๐ต))) |
213 | 212 | expr 375 |
. . . . . . 7
โข ((((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด + ๐ต)))) |
214 | 213 | rexlimdvva 2602 |
. . . . . 6
โข (((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โ (โ๐ฆ โ โ โ๐ค โ โ (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด + ๐ต)))) |
215 | 21, 214 | biimtrrid 153 |
. . . . 5
โข (((๐ โง ๐ต โ 0) โง (๐ฅ โ โค โง ๐ง โ โค)) โ ((โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด + ๐ต)))) |
216 | 215 | rexlimdvva 2602 |
. . . 4
โข ((๐ โง ๐ต โ 0) โ (โ๐ฅ โ โค โ๐ง โ โค (โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด + ๐ต)))) |
217 | 20, 216 | biimtrrid 153 |
. . 3
โข ((๐ โง ๐ต โ 0) โ ((โ๐ฅ โ โค โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด + ๐ต)))) |
218 | | 0z 9263 |
. . . . . 6
โข 0 โ
โค |
219 | | zq 9625 |
. . . . . 6
โข (0 โ
โค โ 0 โ โ) |
220 | 218, 219 | mp1i 10 |
. . . . 5
โข (๐ โ 0 โ
โ) |
221 | | qdceq 10246 |
. . . . 5
โข ((๐ต โ โ โง 0 โ
โ) โ DECID ๐ต = 0) |
222 | 4, 220, 221 | syl2anc 411 |
. . . 4
โข (๐ โ DECID ๐ต = 0) |
223 | | dcne 2358 |
. . . 4
โข
(DECID ๐ต = 0 โ (๐ต = 0 โจ ๐ต โ 0)) |
224 | 222, 223 | sylib 122 |
. . 3
โข (๐ โ (๐ต = 0 โจ ๐ต โ 0)) |
225 | 19, 217, 224 | mpjaodan 798 |
. 2
โข (๐ โ ((โ๐ฅ โ โค โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด + ๐ต)))) |
226 | 3, 6, 225 | mp2and 433 |
1
โข (๐ โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ด + ๐ต))) |