Step | Hyp | Ref
| Expression |
1 | | eluz2b3 12855 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ (๐ โ โ โง ๐ โ 1)) |
2 | 1 | simprbi 498 |
. . 3
โข (๐ โ
(โคโฅโ2) โ ๐ โ 1) |
3 | 2 | adantl 483 |
. 2
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โ ๐ โ 1) |
4 | | eluzelz 12781 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ2) โ ๐ โ โค) |
5 | 4 | ad2antlr 726 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ๐ โ โค) |
6 | | simpr 486 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ (๐ดโ๐) โ โ) |
7 | | simpll 766 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ๐ด โ โ) |
8 | | prmnn 16558 |
. . . . . . . . . . . 12
โข ((๐ดโ๐) โ โ โ (๐ดโ๐) โ โ) |
9 | 8 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ (๐ดโ๐) โ โ) |
10 | 9 | nnne0d 12211 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ (๐ดโ๐) โ 0) |
11 | | eluz2nn 12817 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
12 | 11 | ad2antlr 726 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ๐ โ โ) |
13 | 12 | 0expd 14053 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ (0โ๐) = 0) |
14 | 10, 13 | neeqtrrd 3015 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ (๐ดโ๐) โ (0โ๐)) |
15 | | oveq1 7368 |
. . . . . . . . . 10
โข (๐ด = 0 โ (๐ดโ๐) = (0โ๐)) |
16 | 15 | necon3i 2973 |
. . . . . . . . 9
โข ((๐ดโ๐) โ (0โ๐) โ ๐ด โ 0) |
17 | 14, 16 | syl 17 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ๐ด โ 0) |
18 | | pcqcl 16736 |
. . . . . . . 8
โข (((๐ดโ๐) โ โ โง (๐ด โ โ โง ๐ด โ 0)) โ ((๐ดโ๐) pCnt ๐ด) โ โค) |
19 | 6, 7, 17, 18 | syl12anc 836 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ((๐ดโ๐) pCnt ๐ด) โ โค) |
20 | | dvdsmul1 16168 |
. . . . . . 7
โข ((๐ โ โค โง ((๐ดโ๐) pCnt ๐ด) โ โค) โ ๐ โฅ (๐ ยท ((๐ดโ๐) pCnt ๐ด))) |
21 | 5, 19, 20 | syl2anc 585 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ๐ โฅ (๐ ยท ((๐ดโ๐) pCnt ๐ด))) |
22 | 9 | nncnd 12177 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ (๐ดโ๐) โ โ) |
23 | 22 | exp1d 14055 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ((๐ดโ๐)โ1) = (๐ดโ๐)) |
24 | 23 | oveq2d 7377 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ((๐ดโ๐) pCnt ((๐ดโ๐)โ1)) = ((๐ดโ๐) pCnt (๐ดโ๐))) |
25 | | 1z 12541 |
. . . . . . . 8
โข 1 โ
โค |
26 | | pcid 16753 |
. . . . . . . 8
โข (((๐ดโ๐) โ โ โง 1 โ โค)
โ ((๐ดโ๐) pCnt ((๐ดโ๐)โ1)) = 1) |
27 | 6, 25, 26 | sylancl 587 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ((๐ดโ๐) pCnt ((๐ดโ๐)โ1)) = 1) |
28 | | pcexp 16739 |
. . . . . . . 8
โข (((๐ดโ๐) โ โ โง (๐ด โ โ โง ๐ด โ 0) โง ๐ โ โค) โ ((๐ดโ๐) pCnt (๐ดโ๐)) = (๐ ยท ((๐ดโ๐) pCnt ๐ด))) |
29 | 6, 7, 17, 5, 28 | syl121anc 1376 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ((๐ดโ๐) pCnt (๐ดโ๐)) = (๐ ยท ((๐ดโ๐) pCnt ๐ด))) |
30 | 24, 27, 29 | 3eqtr3rd 2782 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ (๐ ยท ((๐ดโ๐) pCnt ๐ด)) = 1) |
31 | 21, 30 | breqtrd 5135 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โง (๐ดโ๐) โ โ) โ ๐ โฅ 1) |
32 | 31 | ex 414 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โ ((๐ดโ๐) โ โ โ ๐ โฅ 1)) |
33 | 11 | adantl 483 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โ ๐ โ โ) |
34 | 33 | nnnn0d 12481 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โ ๐ โ
โ0) |
35 | | dvds1 16209 |
. . . . 5
โข (๐ โ โ0
โ (๐ โฅ 1 โ
๐ = 1)) |
36 | 34, 35 | syl 17 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โ (๐ โฅ 1 โ ๐ = 1)) |
37 | 32, 36 | sylibd 238 |
. . 3
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โ ((๐ดโ๐) โ โ โ ๐ = 1)) |
38 | 37 | necon3ad 2953 |
. 2
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โ (๐ โ 1 โ ยฌ (๐ดโ๐) โ โ)) |
39 | 3, 38 | mpd 15 |
1
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ2)) โ ยฌ (๐ดโ๐) โ โ) |