Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ โค โง ๐ โ
โค)) |
2 | | znegcl 12545 |
. . . 4
โข (๐ โ โค โ -๐ โ
โค) |
3 | 2 | anim2i 618 |
. . 3
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ โค โง -๐ โ
โค)) |
4 | | znegcl 12545 |
. . . 4
โข (๐ฅ โ โค โ -๐ฅ โ
โค) |
5 | 4 | adantl 483 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ -๐ฅ โ
โค) |
6 | | zcn 12511 |
. . . . 5
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
7 | | zcn 12511 |
. . . . 5
โข (๐ โ โค โ ๐ โ
โ) |
8 | | mulneg1 11598 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ โ โ) โ (-๐ฅ ยท ๐) = -(๐ฅ ยท ๐)) |
9 | | negeq 11400 |
. . . . . . 7
โข ((๐ฅ ยท ๐) = ๐ โ -(๐ฅ ยท ๐) = -๐) |
10 | 9 | eqeq2d 2748 |
. . . . . 6
โข ((๐ฅ ยท ๐) = ๐ โ ((-๐ฅ ยท ๐) = -(๐ฅ ยท ๐) โ (-๐ฅ ยท ๐) = -๐)) |
11 | 8, 10 | syl5ibcom 244 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ โ โ) โ ((๐ฅ ยท ๐) = ๐ โ (-๐ฅ ยท ๐) = -๐)) |
12 | 6, 7, 11 | syl2anr 598 |
. . . 4
โข ((๐ โ โค โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) = ๐ โ (-๐ฅ ยท ๐) = -๐)) |
13 | 12 | adantlr 714 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) = ๐ โ (-๐ฅ ยท ๐) = -๐)) |
14 | 1, 3, 5, 13 | dvds1lem 16157 |
. 2
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ -๐)) |
15 | | zcn 12511 |
. . . . . 6
โข (๐ โ โค โ ๐ โ
โ) |
16 | | negeq 11400 |
. . . . . . . . . 10
โข ((๐ฅ ยท ๐) = -๐ โ -(๐ฅ ยท ๐) = --๐) |
17 | | negneg 11458 |
. . . . . . . . . 10
โข (๐ โ โ โ --๐ = ๐) |
18 | 16, 17 | sylan9eqr 2799 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ฅ ยท ๐) = -๐) โ -(๐ฅ ยท ๐) = ๐) |
19 | 8, 18 | sylan9eq 2797 |
. . . . . . . 8
โข (((๐ฅ โ โ โง ๐ โ โ) โง (๐ โ โ โง (๐ฅ ยท ๐) = -๐)) โ (-๐ฅ ยท ๐) = ๐) |
20 | 19 | expr 458 |
. . . . . . 7
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ โ โ) โ ((๐ฅ ยท ๐) = -๐ โ (-๐ฅ ยท ๐) = ๐)) |
21 | 20 | 3impa 1111 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ โ โ โง ๐ โ โ) โ ((๐ฅ ยท ๐) = -๐ โ (-๐ฅ ยท ๐) = ๐)) |
22 | 6, 7, 15, 21 | syl3an 1161 |
. . . . 5
โข ((๐ฅ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ฅ ยท ๐) = -๐ โ (-๐ฅ ยท ๐) = ๐)) |
23 | 22 | 3coml 1128 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) = -๐ โ (-๐ฅ ยท ๐) = ๐)) |
24 | 23 | 3expa 1119 |
. . 3
โข (((๐ โ โค โง ๐ โ โค) โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐) = -๐ โ (-๐ฅ ยท ๐) = ๐)) |
25 | 3, 1, 5, 24 | dvds1lem 16157 |
. 2
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ -๐ โ ๐ โฅ ๐)) |
26 | 14, 25 | impbid 211 |
1
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ -๐)) |