Step | Hyp | Ref
| Expression |
1 | | eluzelz 12778 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ ๐ด โ โค) |
2 | 1 | adantr 482 |
. . . 4
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ๐ด โ
โค) |
3 | 2 | zred 12612 |
. . 3
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ๐ด โ
โ) |
4 | | eluz2gt1 12850 |
. . . . 5
โข (๐ต โ
(โคโฅโ2) โ 1 < ๐ต) |
5 | 4 | adantl 483 |
. . . 4
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ 1 < ๐ต) |
6 | | eluzelz 12778 |
. . . . . . 7
โข (๐ต โ
(โคโฅโ2) โ ๐ต โ โค) |
7 | 6 | adantl 483 |
. . . . . 6
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ๐ต โ
โค) |
8 | 7 | zred 12612 |
. . . . 5
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ๐ต โ
โ) |
9 | | eluz2nn 12814 |
. . . . . . 7
โข (๐ด โ
(โคโฅโ2) โ ๐ด โ โ) |
10 | 9 | adantr 482 |
. . . . . 6
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ๐ด โ
โ) |
11 | 10 | nngt0d 12207 |
. . . . 5
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ 0 < ๐ด) |
12 | | ltmulgt11 12020 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง 0 <
๐ด) โ (1 < ๐ต โ ๐ด < (๐ด ยท ๐ต))) |
13 | 3, 8, 11, 12 | syl3anc 1372 |
. . . 4
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ (1 < ๐ต โ
๐ด < (๐ด ยท ๐ต))) |
14 | 5, 13 | mpbid 231 |
. . 3
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ๐ด < (๐ด ยท ๐ต)) |
15 | 3, 14 | ltned 11296 |
. 2
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ๐ด โ (๐ด ยท ๐ต)) |
16 | | dvdsmul1 16165 |
. . . . 5
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ด โฅ (๐ด ยท ๐ต)) |
17 | 1, 6, 16 | syl2an 597 |
. . . 4
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ๐ด โฅ (๐ด ยท ๐ต)) |
18 | | isprm4 16565 |
. . . . . . 7
โข ((๐ด ยท ๐ต) โ โ โ ((๐ด ยท ๐ต) โ (โคโฅโ2)
โง โ๐ฅ โ
(โคโฅโ2)(๐ฅ โฅ (๐ด ยท ๐ต) โ ๐ฅ = (๐ด ยท ๐ต)))) |
19 | 18 | simprbi 498 |
. . . . . 6
โข ((๐ด ยท ๐ต) โ โ โ โ๐ฅ โ
(โคโฅโ2)(๐ฅ โฅ (๐ด ยท ๐ต) โ ๐ฅ = (๐ด ยท ๐ต))) |
20 | | breq1 5109 |
. . . . . . . 8
โข (๐ฅ = ๐ด โ (๐ฅ โฅ (๐ด ยท ๐ต) โ ๐ด โฅ (๐ด ยท ๐ต))) |
21 | | eqeq1 2737 |
. . . . . . . 8
โข (๐ฅ = ๐ด โ (๐ฅ = (๐ด ยท ๐ต) โ ๐ด = (๐ด ยท ๐ต))) |
22 | 20, 21 | imbi12d 345 |
. . . . . . 7
โข (๐ฅ = ๐ด โ ((๐ฅ โฅ (๐ด ยท ๐ต) โ ๐ฅ = (๐ด ยท ๐ต)) โ (๐ด โฅ (๐ด ยท ๐ต) โ ๐ด = (๐ด ยท ๐ต)))) |
23 | 22 | rspcv 3576 |
. . . . . 6
โข (๐ด โ
(โคโฅโ2) โ (โ๐ฅ โ
(โคโฅโ2)(๐ฅ โฅ (๐ด ยท ๐ต) โ ๐ฅ = (๐ด ยท ๐ต)) โ (๐ด โฅ (๐ด ยท ๐ต) โ ๐ด = (๐ด ยท ๐ต)))) |
24 | 19, 23 | syl5 34 |
. . . . 5
โข (๐ด โ
(โคโฅโ2) โ ((๐ด ยท ๐ต) โ โ โ (๐ด โฅ (๐ด ยท ๐ต) โ ๐ด = (๐ด ยท ๐ต)))) |
25 | 24 | adantr 482 |
. . . 4
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ((๐ด ยท ๐ต) โ โ โ (๐ด โฅ (๐ด ยท ๐ต) โ ๐ด = (๐ด ยท ๐ต)))) |
26 | 17, 25 | mpid 44 |
. . 3
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ((๐ด ยท ๐ต) โ โ โ ๐ด = (๐ด ยท ๐ต))) |
27 | 26 | necon3ad 2953 |
. 2
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ (๐ด โ (๐ด ยท ๐ต) โ ยฌ (๐ด ยท ๐ต) โ โ)) |
28 | 15, 27 | mpd 15 |
1
โข ((๐ด โ
(โคโฅโ2) โง ๐ต โ (โคโฅโ2))
โ ยฌ (๐ด ยท
๐ต) โ
โ) |