Step | Hyp | Ref
| Expression |
1 | | 0z 9263 |
. . . 4
โข 0 โ
โค |
2 | | eleq1 2240 |
. . . 4
โข (๐ด = 0 โ (๐ด โ โค โ 0 โ
โค)) |
3 | 1, 2 | mpbiri 168 |
. . 3
โข (๐ด = 0 โ ๐ด โ โค) |
4 | 3 | adantl 277 |
. 2
โข (((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด = 0) โ ๐ด โ โค) |
5 | | simpll2 1037 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ ๐ โ โ) |
6 | 5 | nncnd 8932 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ ๐ โ โ) |
7 | 6 | mul01d 8349 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ ยท 0) = 0) |
8 | | simpr 110 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ ๐ โ โ) |
9 | | simpll3 1038 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ดโ๐) โ โค) |
10 | | simpll1 1036 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ ๐ด โ โ) |
11 | | qcn 9633 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ๐ด โ
โ) |
12 | 10, 11 | syl 14 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ ๐ด โ โ) |
13 | | simplr 528 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ ๐ด โ 0) |
14 | | zq 9625 |
. . . . . . . . . . . . . 14
โข (0 โ
โค โ 0 โ โ) |
15 | 1, 14 | ax-mp 5 |
. . . . . . . . . . . . 13
โข 0 โ
โ |
16 | | qapne 9638 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง 0 โ
โ) โ (๐ด # 0
โ ๐ด โ
0)) |
17 | 10, 15, 16 | sylancl 413 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ด # 0 โ ๐ด โ 0)) |
18 | 13, 17 | mpbird 167 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ ๐ด # 0) |
19 | 5 | nnzd 9373 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ ๐ โ โค) |
20 | 12, 18, 19 | expap0d 10659 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ดโ๐) # 0) |
21 | | 0zd 9264 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ 0 โ
โค) |
22 | | zapne 9326 |
. . . . . . . . . . 11
โข (((๐ดโ๐) โ โค โง 0 โ โค)
โ ((๐ดโ๐) # 0 โ (๐ดโ๐) โ 0)) |
23 | 9, 21, 22 | syl2anc 411 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ ((๐ดโ๐) # 0 โ (๐ดโ๐) โ 0)) |
24 | 20, 23 | mpbid 147 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ดโ๐) โ 0) |
25 | | pczcl 12297 |
. . . . . . . . 9
โข ((๐ โ โ โง ((๐ดโ๐) โ โค โง (๐ดโ๐) โ 0)) โ (๐ pCnt (๐ดโ๐)) โ
โ0) |
26 | 8, 9, 24, 25 | syl12anc 1236 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ pCnt (๐ดโ๐)) โ
โ0) |
27 | 26 | nn0ge0d 9231 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ 0 โค (๐ pCnt (๐ดโ๐))) |
28 | | pcexp 12308 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0) โง ๐ โ โค) โ (๐ pCnt (๐ดโ๐)) = (๐ ยท (๐ pCnt ๐ด))) |
29 | 8, 10, 13, 19, 28 | syl121anc 1243 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ pCnt (๐ดโ๐)) = (๐ ยท (๐ pCnt ๐ด))) |
30 | 27, 29 | breqtrd 4029 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ 0 โค (๐ ยท (๐ pCnt ๐ด))) |
31 | 7, 30 | eqbrtrd 4025 |
. . . . 5
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ ยท 0) โค (๐ ยท (๐ pCnt ๐ด))) |
32 | | 0red 7957 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ 0 โ
โ) |
33 | | pcqcl 12305 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ด โ โ โง ๐ด โ 0)) โ (๐ pCnt ๐ด) โ โค) |
34 | 8, 10, 13, 33 | syl12anc 1236 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ pCnt ๐ด) โ โค) |
35 | 34 | zred 9374 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (๐ pCnt ๐ด) โ โ) |
36 | 5 | nnred 8931 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ ๐ โ โ) |
37 | 5 | nngt0d 8962 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ 0 < ๐) |
38 | | lemul2 8813 |
. . . . . 6
โข ((0
โ โ โง (๐
pCnt ๐ด) โ โ
โง (๐ โ โ
โง 0 < ๐)) โ (0
โค (๐ pCnt ๐ด) โ (๐ ยท 0) โค (๐ ยท (๐ pCnt ๐ด)))) |
39 | 32, 35, 36, 37, 38 | syl112anc 1242 |
. . . . 5
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ (0 โค (๐ pCnt ๐ด) โ (๐ ยท 0) โค (๐ ยท (๐ pCnt ๐ด)))) |
40 | 31, 39 | mpbird 167 |
. . . 4
โข ((((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โง ๐ โ โ) โ 0 โค (๐ pCnt ๐ด)) |
41 | 40 | ralrimiva 2550 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โ โ๐ โ โ 0 โค (๐ pCnt ๐ด)) |
42 | | simpl1 1000 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โ ๐ด โ โ) |
43 | | pcz 12330 |
. . . 4
โข (๐ด โ โ โ (๐ด โ โค โ
โ๐ โ โ 0
โค (๐ pCnt ๐ด))) |
44 | 42, 43 | syl 14 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โ (๐ด โ โค โ โ๐ โ โ 0 โค (๐ pCnt ๐ด))) |
45 | 41, 44 | mpbird 167 |
. 2
โข (((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โง ๐ด โ 0) โ ๐ด โ โค) |
46 | | simp1 997 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โ ๐ด โ โ) |
47 | | qdceq 10246 |
. . . 4
โข ((๐ด โ โ โง 0 โ
โ) โ DECID ๐ด = 0) |
48 | 46, 15, 47 | sylancl 413 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โ
DECID ๐ด =
0) |
49 | | dcne 2358 |
. . 3
โข
(DECID ๐ด = 0 โ (๐ด = 0 โจ ๐ด โ 0)) |
50 | 48, 49 | sylib 122 |
. 2
โข ((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โ (๐ด = 0 โจ ๐ด โ 0)) |
51 | 4, 45, 50 | mpjaodan 798 |
1
โข ((๐ด โ โ โง ๐ โ โ โง (๐ดโ๐) โ โค) โ ๐ด โ โค) |