Step | Hyp | Ref
| Expression |
1 | | simp2l 1200 |
. . 3
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ด โ
โ) |
2 | | elq 12880 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ โค
โ๐ฆ โ โ
๐ด = (๐ฅ / ๐ฆ)) |
3 | 1, 2 | sylib 217 |
. 2
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ โ๐ฅ โ โค โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ)) |
4 | | simp3l 1202 |
. . 3
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ต โ
โ) |
5 | | elq 12880 |
. . 3
โข (๐ต โ โ โ
โ๐ง โ โค
โ๐ค โ โ
๐ต = (๐ง / ๐ค)) |
6 | 4, 5 | sylib 217 |
. 2
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค)) |
7 | | reeanv 3216 |
. . 3
โข
(โ๐ฅ โ
โค โ๐ง โ
โค (โ๐ฆ โ
โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (โ๐ฅ โ โค โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค))) |
8 | | reeanv 3216 |
. . . . 5
โข
(โ๐ฆ โ
โ โ๐ค โ
โ (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ค โ โ ๐ต = (๐ง / ๐ค))) |
9 | | simp2r 1201 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ด โ 0) |
10 | | simp3r 1203 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ต โ 0) |
11 | 9, 10 | jca 513 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ด โ 0 โง ๐ต โ 0)) |
12 | 11 | ad2antrr 725 |
. . . . . . 7
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ (๐ด โ 0 โง ๐ต โ 0)) |
13 | | simp1 1137 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ โ
โ) |
14 | | simprl 770 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ๐ฆ โ
โ) |
15 | 14 | nncnd 12174 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ๐ฆ โ
โ) |
16 | 14 | nnne0d 12208 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ๐ฆ โ 0) |
17 | 15, 16 | div0d 11935 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ (0 /
๐ฆ) = 0) |
18 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ฅ = 0 โ (๐ฅ / ๐ฆ) = (0 / ๐ฆ)) |
19 | 18 | eqeq1d 2735 |
. . . . . . . . . . . 12
โข (๐ฅ = 0 โ ((๐ฅ / ๐ฆ) = 0 โ (0 / ๐ฆ) = 0)) |
20 | 17, 19 | syl5ibrcom 247 |
. . . . . . . . . . 11
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ (๐ฅ = 0 โ (๐ฅ / ๐ฆ) = 0)) |
21 | 20 | necon3d 2961 |
. . . . . . . . . 10
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ((๐ฅ / ๐ฆ) โ 0 โ ๐ฅ โ 0)) |
22 | | simprr 772 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ๐ค โ
โ) |
23 | 22 | nncnd 12174 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ๐ค โ
โ) |
24 | 22 | nnne0d 12208 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ๐ค โ 0) |
25 | 23, 24 | div0d 11935 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ (0 /
๐ค) = 0) |
26 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ง = 0 โ (๐ง / ๐ค) = (0 / ๐ค)) |
27 | 26 | eqeq1d 2735 |
. . . . . . . . . . . 12
โข (๐ง = 0 โ ((๐ง / ๐ค) = 0 โ (0 / ๐ค) = 0)) |
28 | 25, 27 | syl5ibrcom 247 |
. . . . . . . . . . 11
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ (๐ง = 0 โ (๐ง / ๐ค) = 0)) |
29 | 28 | necon3d 2961 |
. . . . . . . . . 10
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ((๐ง / ๐ค) โ 0 โ ๐ง โ 0)) |
30 | | simpll 766 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ โ โ) |
31 | | simplrl 776 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ฅ โ โค) |
32 | | simplrr 777 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ง โ โค) |
33 | 31, 32 | zmulcld 12618 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ฅ ยท ๐ง) โ โค) |
34 | 31 | zcnd 12613 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ฅ โ โ) |
35 | 32 | zcnd 12613 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ง โ โ) |
36 | | simprrl 780 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ฅ โ 0) |
37 | | simprrr 781 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ง โ 0) |
38 | 34, 35, 36, 37 | mulne0d 11812 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ฅ ยท ๐ง) โ 0) |
39 | 14 | adantrr 716 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ฆ โ โ) |
40 | 22 | adantrr 716 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ค โ โ) |
41 | 39, 40 | nnmulcld 12211 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ฆ ยท ๐ค) โ โ) |
42 | | pcdiv 16729 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ((๐ฅ ยท ๐ง) โ โค โง (๐ฅ ยท ๐ง) โ 0) โง (๐ฆ ยท ๐ค) โ โ) โ (๐ pCnt ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค))) = ((๐ pCnt (๐ฅ ยท ๐ง)) โ (๐ pCnt (๐ฆ ยท ๐ค)))) |
43 | 30, 33, 38, 41, 42 | syl121anc 1376 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค))) = ((๐ pCnt (๐ฅ ยท ๐ง)) โ (๐ pCnt (๐ฆ ยท ๐ค)))) |
44 | | pcmul 16728 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฅ โ 0) โง (๐ง โ โค โง ๐ง โ 0)) โ (๐ pCnt (๐ฅ ยท ๐ง)) = ((๐ pCnt ๐ฅ) + (๐ pCnt ๐ง))) |
45 | 30, 31, 36, 32, 37, 44 | syl122anc 1380 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt (๐ฅ ยท ๐ง)) = ((๐ pCnt ๐ฅ) + (๐ pCnt ๐ง))) |
46 | 39 | nnzd 12531 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ฆ โ โค) |
47 | 16 | adantrr 716 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ฆ โ 0) |
48 | 40 | nnzd 12531 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ค โ โค) |
49 | 24 | adantrr 716 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ค โ 0) |
50 | | pcmul 16728 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง (๐ฆ โ โค โง ๐ฆ โ 0) โง (๐ค โ โค โง ๐ค โ 0)) โ (๐ pCnt (๐ฆ ยท ๐ค)) = ((๐ pCnt ๐ฆ) + (๐ pCnt ๐ค))) |
51 | 30, 46, 47, 48, 49, 50 | syl122anc 1380 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt (๐ฆ ยท ๐ค)) = ((๐ pCnt ๐ฆ) + (๐ pCnt ๐ค))) |
52 | 45, 51 | oveq12d 7376 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ((๐ pCnt (๐ฅ ยท ๐ง)) โ (๐ pCnt (๐ฆ ยท ๐ค))) = (((๐ pCnt ๐ฅ) + (๐ pCnt ๐ง)) โ ((๐ pCnt ๐ฆ) + (๐ pCnt ๐ค)))) |
53 | | pczcl 16725 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฅ โ 0)) โ (๐ pCnt ๐ฅ) โ
โ0) |
54 | 30, 31, 36, 53 | syl12anc 836 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ๐ฅ) โ
โ0) |
55 | 54 | nn0cnd 12480 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ๐ฅ) โ โ) |
56 | | pczcl 16725 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง (๐ง โ โค โง ๐ง โ 0)) โ (๐ pCnt ๐ง) โ
โ0) |
57 | 30, 32, 37, 56 | syl12anc 836 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ๐ง) โ
โ0) |
58 | 57 | nn0cnd 12480 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ๐ง) โ โ) |
59 | 30, 39 | pccld 16727 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ๐ฆ) โ
โ0) |
60 | 59 | nn0cnd 12480 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ๐ฆ) โ โ) |
61 | 30, 40 | pccld 16727 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ๐ค) โ
โ0) |
62 | 61 | nn0cnd 12480 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ๐ค) โ โ) |
63 | 55, 58, 60, 62 | addsub4d 11564 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (((๐ pCnt ๐ฅ) + (๐ pCnt ๐ง)) โ ((๐ pCnt ๐ฆ) + (๐ pCnt ๐ค))) = (((๐ pCnt ๐ฅ) โ (๐ pCnt ๐ฆ)) + ((๐ pCnt ๐ง) โ (๐ pCnt ๐ค)))) |
64 | 43, 52, 63 | 3eqtrd 2777 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค))) = (((๐ pCnt ๐ฅ) โ (๐ pCnt ๐ฆ)) + ((๐ pCnt ๐ง) โ (๐ pCnt ๐ค)))) |
65 | 15 | adantrr 716 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ฆ โ โ) |
66 | 23 | adantrr 716 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ๐ค โ โ) |
67 | 34, 65, 35, 66, 47, 49 | divmuldivd 11977 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค)) = ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค))) |
68 | 67 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค))) = (๐ pCnt ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค)))) |
69 | | pcdiv 16729 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฅ โ 0) โง ๐ฆ โ โ) โ (๐ pCnt (๐ฅ / ๐ฆ)) = ((๐ pCnt ๐ฅ) โ (๐ pCnt ๐ฆ))) |
70 | 30, 31, 36, 39, 69 | syl121anc 1376 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt (๐ฅ / ๐ฆ)) = ((๐ pCnt ๐ฅ) โ (๐ pCnt ๐ฆ))) |
71 | | pcdiv 16729 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง (๐ง โ โค โง ๐ง โ 0) โง ๐ค โ โ) โ (๐ pCnt (๐ง / ๐ค)) = ((๐ pCnt ๐ง) โ (๐ pCnt ๐ค))) |
72 | 30, 32, 37, 40, 71 | syl121anc 1376 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt (๐ง / ๐ค)) = ((๐ pCnt ๐ง) โ (๐ pCnt ๐ค))) |
73 | 70, 72 | oveq12d 7376 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ ((๐ pCnt (๐ฅ / ๐ฆ)) + (๐ pCnt (๐ง / ๐ค))) = (((๐ pCnt ๐ฅ) โ (๐ pCnt ๐ฆ)) + ((๐ pCnt ๐ง) โ (๐ pCnt ๐ค)))) |
74 | 64, 68, 73 | 3eqtr4d 2783 |
. . . . . . . . . . 11
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง ((๐ฆ โ โ โง ๐ค โ โ) โง (๐ฅ โ 0 โง ๐ง โ 0))) โ (๐ pCnt ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค))) = ((๐ pCnt (๐ฅ / ๐ฆ)) + (๐ pCnt (๐ง / ๐ค)))) |
75 | 74 | expr 458 |
. . . . . . . . . 10
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ((๐ฅ โ 0 โง ๐ง โ 0) โ (๐ pCnt ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค))) = ((๐ pCnt (๐ฅ / ๐ฆ)) + (๐ pCnt (๐ง / ๐ค))))) |
76 | 21, 29, 75 | syl2and 609 |
. . . . . . . . 9
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ
(((๐ฅ / ๐ฆ) โ 0 โง (๐ง / ๐ค) โ 0) โ (๐ pCnt ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค))) = ((๐ pCnt (๐ฅ / ๐ฆ)) + (๐ pCnt (๐ง / ๐ค))))) |
77 | | neeq1 3003 |
. . . . . . . . . . 11
โข (๐ด = (๐ฅ / ๐ฆ) โ (๐ด โ 0 โ (๐ฅ / ๐ฆ) โ 0)) |
78 | | neeq1 3003 |
. . . . . . . . . . 11
โข (๐ต = (๐ง / ๐ค) โ (๐ต โ 0 โ (๐ง / ๐ค) โ 0)) |
79 | 77, 78 | bi2anan9 638 |
. . . . . . . . . 10
โข ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ ((๐ด โ 0 โง ๐ต โ 0) โ ((๐ฅ / ๐ฆ) โ 0 โง (๐ง / ๐ค) โ 0))) |
80 | | oveq12 7367 |
. . . . . . . . . . . 12
โข ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (๐ด ยท ๐ต) = ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค))) |
81 | 80 | oveq2d 7374 |
. . . . . . . . . . 11
โข ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (๐ pCnt (๐ด ยท ๐ต)) = (๐ pCnt ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค)))) |
82 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ด = (๐ฅ / ๐ฆ) โ (๐ pCnt ๐ด) = (๐ pCnt (๐ฅ / ๐ฆ))) |
83 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ต = (๐ง / ๐ค) โ (๐ pCnt ๐ต) = (๐ pCnt (๐ง / ๐ค))) |
84 | 82, 83 | oveqan12d 7377 |
. . . . . . . . . . 11
โข ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ ((๐ pCnt ๐ด) + (๐ pCnt ๐ต)) = ((๐ pCnt (๐ฅ / ๐ฆ)) + (๐ pCnt (๐ง / ๐ค)))) |
85 | 81, 84 | eqeq12d 2749 |
. . . . . . . . . 10
โข ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ ((๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต)) โ (๐ pCnt ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค))) = ((๐ pCnt (๐ฅ / ๐ฆ)) + (๐ pCnt (๐ง / ๐ค))))) |
86 | 79, 85 | imbi12d 345 |
. . . . . . . . 9
โข ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (((๐ด โ 0 โง ๐ต โ 0) โ (๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต))) โ (((๐ฅ / ๐ฆ) โ 0 โง (๐ง / ๐ค) โ 0) โ (๐ pCnt ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค))) = ((๐ pCnt (๐ฅ / ๐ฆ)) + (๐ pCnt (๐ง / ๐ค)))))) |
87 | 76, 86 | syl5ibrcom 247 |
. . . . . . . 8
โข (((๐ โ โ โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ ((๐ด โ 0 โง ๐ต โ 0) โ (๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต))))) |
88 | 13, 87 | sylanl1 679 |
. . . . . . 7
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ ((๐ด โ 0 โง ๐ต โ 0) โ (๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต))))) |
89 | 12, 88 | mpid 44 |
. . . . . 6
โข ((((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ฅ โ โค โง ๐ง โ โค)) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต)))) |
90 | 89 | rexlimdvva 3202 |
. . . . 5
โข (((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ฅ โ โค โง ๐ง โ โค)) โ
(โ๐ฆ โ โ
โ๐ค โ โ
(๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต)))) |
91 | 8, 90 | biimtrrid 242 |
. . . 4
โข (((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ฅ โ โค โง ๐ง โ โค)) โ
((โ๐ฆ โ โ
๐ด = (๐ฅ / ๐ฆ) โง โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต)))) |
92 | 91 | rexlimdvva 3202 |
. . 3
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (โ๐ฅ โ โค โ๐ง โ โค (โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต)))) |
93 | 7, 92 | biimtrrid 242 |
. 2
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ((โ๐ฅ โ โค โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต)))) |
94 | 3, 6, 93 | mp2and 698 |
1
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต))) |