Step | Hyp | Ref
| Expression |
1 | | elznn0 12521 |
. . 3
โข (๐ผ โ โค โ (๐ผ โ โ โง (๐ผ โ โ0 โจ
-๐ผ โ
โ0))) |
2 | | jm2.19lem3 41344 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |
3 | 2 | 3expia 1122 |
. . . . . 6
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ (๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
4 | 3 | adantr 482 |
. . . . 5
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ (๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
5 | | simplll 774 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ด โ
(โคโฅโ2)) |
6 | | simprl 770 |
. . . . . . . . 9
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โค) |
7 | 6 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โค) |
8 | | simprr 772 |
. . . . . . . . . 10
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โค) |
9 | 8 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โค) |
10 | | nn0z 12531 |
. . . . . . . . . . . 12
โข (-๐ผ โ โ0
โ -๐ผ โ
โค) |
11 | 10 | adantl 483 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ -๐ผ โ
โค) |
12 | | simplr 768 |
. . . . . . . . . . . . 13
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โ) |
13 | 12 | recnd 11190 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โ) |
14 | | znegclb 12547 |
. . . . . . . . . . . 12
โข (๐ผ โ โ โ (๐ผ โ โค โ -๐ผ โ
โค)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ โ โค โ -๐ผ โ
โค)) |
16 | 11, 15 | mpbird 257 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โค) |
17 | 16, 7 | zmulcld 12620 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ ยท ๐) โ โค) |
18 | 9, 17 | zaddcld 12618 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ + (๐ผ ยท ๐)) โ โค) |
19 | | simpr 486 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ -๐ผ โ
โ0) |
20 | | jm2.19lem3 41344 |
. . . . . . . 8
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง (๐ + (๐ผ ยท ๐)) โ โค) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))))) |
21 | 5, 7, 18, 19, 20 | syl121anc 1376 |
. . . . . . 7
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))))) |
22 | | zcn 12511 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
23 | 22 | ad2antrl 727 |
. . . . . . . . . . . . 13
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
24 | 23 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โ) |
25 | 13, 24 | mulneg1d 11615 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (-๐ผ ยท ๐) = -(๐ผ ยท ๐)) |
26 | 25 | oveq2d 7378 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐)) = ((๐ + (๐ผ ยท ๐)) + -(๐ผ ยท ๐))) |
27 | | zcn 12511 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
28 | 27 | ad2antll 728 |
. . . . . . . . . . . . 13
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
29 | 28 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โ) |
30 | 13, 24 | mulcld 11182 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ ยท ๐) โ โ) |
31 | 29, 30 | addcld 11181 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ + (๐ผ ยท ๐)) โ โ) |
32 | 31, 30 | negsubd 11525 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + -(๐ผ ยท ๐)) = ((๐ + (๐ผ ยท ๐)) โ (๐ผ ยท ๐))) |
33 | 29, 30 | pncand 11520 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) โ (๐ผ ยท ๐)) = ๐) |
34 | 26, 32, 33 | 3eqtrd 2781 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐)) = ๐) |
35 | 34 | oveq2d 7378 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))) = (๐ด Yrm ๐)) |
36 | 35 | breq2d 5122 |
. . . . . . 7
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ๐))) |
37 | 21, 36 | bitr2d 280 |
. . . . . 6
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |
38 | 37 | ex 414 |
. . . . 5
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ (-๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
39 | 4, 38 | jaod 858 |
. . . 4
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ ((๐ผ โ โ0 โจ -๐ผ โ โ0)
โ ((๐ด Yrm
๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
40 | 39 | expimpd 455 |
. . 3
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ผ โ โ โง (๐ผ โ โ0 โจ -๐ผ โ โ0))
โ ((๐ด Yrm
๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
41 | 1, 40 | biimtrid 241 |
. 2
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ (๐ผ โ โค โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
42 | 41 | 3impia 1118 |
1
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โค) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |