Step | Hyp | Ref
| Expression |
1 | | elznn0 12573 |
. 2
โข (๐ โ โค โ (๐ โ โ โง (๐ โ โ0 โจ
-๐ โ
โ0))) |
2 | | elznn0 12573 |
. 2
โข (๐ โ โค โ (๐ โ โ โง (๐ โ โ0 โจ
-๐ โ
โ0))) |
3 | | nn0mulcl 12508 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ ยท ๐) โ
โ0) |
4 | 3 | orcd 872 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0)) |
5 | 4 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0))) |
6 | | remulcl 11195 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
7 | 5, 6 | jctild 527 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ ยท ๐) โ โ โง ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0)))) |
8 | | nn0mulcl 12508 |
. . . . . . . . 9
โข ((-๐ โ โ0
โง ๐ โ
โ0) โ (-๐ ยท ๐) โ
โ0) |
9 | | recn 11200 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
10 | | recn 11200 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
11 | | mulneg1 11650 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (-๐ ยท ๐) = -(๐ ยท ๐)) |
12 | 9, 10, 11 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (-๐ ยท ๐) = -(๐ ยท ๐)) |
13 | 12 | eleq1d 2819 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ((-๐ ยท ๐) โ โ0 โ -(๐ ยท ๐) โ
โ0)) |
14 | 8, 13 | imbitrid 243 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((-๐ โ โ0
โง ๐ โ
โ0) โ -(๐ ยท ๐) โ
โ0)) |
15 | | olc 867 |
. . . . . . . 8
โข (-(๐ ยท ๐) โ โ0 โ ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0)) |
16 | 14, 15 | syl6 35 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((-๐ โ โ0
โง ๐ โ
โ0) โ ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0))) |
17 | 16, 6 | jctild 527 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((-๐ โ โ0
โง ๐ โ
โ0) โ ((๐ ยท ๐) โ โ โง ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0)))) |
18 | | nn0mulcl 12508 |
. . . . . . . . 9
โข ((๐ โ โ0
โง -๐ โ
โ0) โ (๐ ยท -๐) โ
โ0) |
19 | | mulneg2 11651 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท -๐) = -(๐ ยท ๐)) |
20 | 9, 10, 19 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท -๐) = -(๐ ยท ๐)) |
21 | 20 | eleq1d 2819 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท -๐) โ โ0 โ -(๐ ยท ๐) โ
โ0)) |
22 | 18, 21 | imbitrid 243 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ โ0
โง -๐ โ
โ0) โ -(๐ ยท ๐) โ
โ0)) |
23 | 22, 15 | syl6 35 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ โ0
โง -๐ โ
โ0) โ ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0))) |
24 | 23, 6 | jctild 527 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ โ โ0
โง -๐ โ
โ0) โ ((๐ ยท ๐) โ โ โง ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0)))) |
25 | | nn0mulcl 12508 |
. . . . . . . . 9
โข ((-๐ โ โ0
โง -๐ โ
โ0) โ (-๐ ยท -๐) โ
โ0) |
26 | | mul2neg 11653 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (-๐ ยท -๐) = (๐ ยท ๐)) |
27 | 9, 10, 26 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ (-๐ ยท -๐) = (๐ ยท ๐)) |
28 | 27 | eleq1d 2819 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ ((-๐ ยท -๐) โ โ0 โ (๐ ยท ๐) โ
โ0)) |
29 | 25, 28 | imbitrid 243 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((-๐ โ โ0
โง -๐ โ
โ0) โ (๐ ยท ๐) โ
โ0)) |
30 | | orc 866 |
. . . . . . . 8
โข ((๐ ยท ๐) โ โ0 โ ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0)) |
31 | 29, 30 | syl6 35 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((-๐ โ โ0
โง -๐ โ
โ0) โ ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0))) |
32 | 31, 6 | jctild 527 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ((-๐ โ โ0
โง -๐ โ
โ0) โ ((๐ ยท ๐) โ โ โง ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0)))) |
33 | 7, 17, 24, 32 | ccased 1038 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ โ โ0 โจ
-๐ โ
โ0) โง (๐ โ โ0 โจ -๐ โ โ0))
โ ((๐ ยท ๐) โ โ โง ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0)))) |
34 | | elznn0 12573 |
. . . . 5
โข ((๐ ยท ๐) โ โค โ ((๐ ยท ๐) โ โ โง ((๐ ยท ๐) โ โ0 โจ -(๐ ยท ๐) โ
โ0))) |
35 | 33, 34 | imbitrrdi 251 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ โ โ0 โจ
-๐ โ
โ0) โง (๐ โ โ0 โจ -๐ โ โ0))
โ (๐ ยท ๐) โ
โค)) |
36 | 35 | imp 408 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง ((๐ โ โ0 โจ
-๐ โ
โ0) โง (๐ โ โ0 โจ -๐ โ โ0)))
โ (๐ ยท ๐) โ
โค) |
37 | 36 | an4s 659 |
. 2
โข (((๐ โ โ โง (๐ โ โ0 โจ
-๐ โ
โ0)) โง (๐ โ โ โง (๐ โ โ0 โจ -๐ โ โ0)))
โ (๐ ยท ๐) โ
โค) |
38 | 1, 2, 37 | syl2anb 599 |
1
โข ((๐ โ โค โง ๐ โ โค) โ (๐ ยท ๐) โ โค) |