Step | Hyp | Ref
| Expression |
1 | | simp2l 1197 |
. . . . . . 7
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ด โ
โ) |
2 | | qcn 12953 |
. . . . . . 7
โข (๐ด โ โ โ ๐ด โ
โ) |
3 | 1, 2 | syl 17 |
. . . . . 6
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ด โ
โ) |
4 | | simp3l 1199 |
. . . . . . 7
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ต โ
โ) |
5 | | qcn 12953 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
6 | 4, 5 | syl 17 |
. . . . . 6
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ต โ
โ) |
7 | | simp3r 1200 |
. . . . . 6
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ต โ 0) |
8 | 3, 6, 7 | divcan1d 11997 |
. . . . 5
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ด / ๐ต) ยท ๐ต) = ๐ด) |
9 | 8 | oveq2d 7429 |
. . . 4
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt ((๐ด / ๐ต) ยท ๐ต)) = (๐ pCnt ๐ด)) |
10 | | simp1 1134 |
. . . . 5
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ โ
โ) |
11 | | qdivcl 12960 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด / ๐ต) โ โ) |
12 | 1, 4, 7, 11 | syl3anc 1369 |
. . . . 5
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ด / ๐ต) โ โ) |
13 | | simp2r 1198 |
. . . . . 6
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ด โ 0) |
14 | 3, 6, 13, 7 | divne0d 12012 |
. . . . 5
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ด / ๐ต) โ 0) |
15 | | pcqmul 16792 |
. . . . 5
โข ((๐ โ โ โง ((๐ด / ๐ต) โ โ โง (๐ด / ๐ต) โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt ((๐ด / ๐ต) ยท ๐ต)) = ((๐ pCnt (๐ด / ๐ต)) + (๐ pCnt ๐ต))) |
16 | 10, 12, 14, 4, 7, 15 | syl122anc 1377 |
. . . 4
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt ((๐ด / ๐ต) ยท ๐ต)) = ((๐ pCnt (๐ด / ๐ต)) + (๐ pCnt ๐ต))) |
17 | 9, 16 | eqtr3d 2772 |
. . 3
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt ๐ด) = ((๐ pCnt (๐ด / ๐ต)) + (๐ pCnt ๐ต))) |
18 | 17 | oveq1d 7428 |
. 2
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ pCnt ๐ด) โ (๐ pCnt ๐ต)) = (((๐ pCnt (๐ด / ๐ต)) + (๐ pCnt ๐ต)) โ (๐ pCnt ๐ต))) |
19 | | pcqcl 16795 |
. . . . 5
โข ((๐ โ โ โง ((๐ด / ๐ต) โ โ โง (๐ด / ๐ต) โ 0)) โ (๐ pCnt (๐ด / ๐ต)) โ โค) |
20 | 10, 12, 14, 19 | syl12anc 833 |
. . . 4
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt (๐ด / ๐ต)) โ โค) |
21 | 20 | zcnd 12673 |
. . 3
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt (๐ด / ๐ต)) โ โ) |
22 | | pcqcl 16795 |
. . . . 5
โข ((๐ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt ๐ต) โ โค) |
23 | 22 | 3adant2 1129 |
. . . 4
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt ๐ต) โ โค) |
24 | 23 | zcnd 12673 |
. . 3
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt ๐ต) โ โ) |
25 | 21, 24 | pncand 11578 |
. 2
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (((๐ pCnt (๐ด / ๐ต)) + (๐ pCnt ๐ต)) โ (๐ pCnt ๐ต)) = (๐ pCnt (๐ด / ๐ต))) |
26 | 18, 25 | eqtr2d 2771 |
1
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ pCnt (๐ด / ๐ต)) = ((๐ pCnt ๐ด) โ (๐ pCnt ๐ต))) |