Step | Hyp | Ref
| Expression |
1 | | elznn0 12601 |
. . 3
โข (๐ผ โ โค โ (๐ผ โ โ โง (๐ผ โ โ0 โจ
-๐ผ โ
โ0))) |
2 | | jm2.19lem3 42476 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |
3 | 2 | 3expia 1118 |
. . . . . 6
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ (๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
4 | 3 | adantr 479 |
. . . . 5
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ (๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
5 | | simplll 773 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ด โ
(โคโฅโ2)) |
6 | | simprl 769 |
. . . . . . . . 9
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โค) |
7 | 6 | ad2antrr 724 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โค) |
8 | | simprr 771 |
. . . . . . . . . 10
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โค) |
9 | 8 | ad2antrr 724 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โค) |
10 | | nn0z 12611 |
. . . . . . . . . . . 12
โข (-๐ผ โ โ0
โ -๐ผ โ
โค) |
11 | 10 | adantl 480 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ -๐ผ โ
โค) |
12 | | simplr 767 |
. . . . . . . . . . . . 13
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โ) |
13 | 12 | recnd 11270 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โ) |
14 | | znegclb 12627 |
. . . . . . . . . . . 12
โข (๐ผ โ โ โ (๐ผ โ โค โ -๐ผ โ
โค)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ โ โค โ -๐ผ โ
โค)) |
16 | 11, 15 | mpbird 256 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โค) |
17 | 16, 7 | zmulcld 12700 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ ยท ๐) โ โค) |
18 | 9, 17 | zaddcld 12698 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ + (๐ผ ยท ๐)) โ โค) |
19 | | simpr 483 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ -๐ผ โ
โ0) |
20 | | jm2.19lem3 42476 |
. . . . . . . 8
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง (๐ + (๐ผ ยท ๐)) โ โค) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))))) |
21 | 5, 7, 18, 19, 20 | syl121anc 1372 |
. . . . . . 7
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))))) |
22 | | zcn 12591 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
23 | 22 | ad2antrl 726 |
. . . . . . . . . . . . 13
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
24 | 23 | ad2antrr 724 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โ) |
25 | 13, 24 | mulneg1d 11695 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (-๐ผ ยท ๐) = -(๐ผ ยท ๐)) |
26 | 25 | oveq2d 7431 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐)) = ((๐ + (๐ผ ยท ๐)) + -(๐ผ ยท ๐))) |
27 | | zcn 12591 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
28 | 27 | ad2antll 727 |
. . . . . . . . . . . . 13
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
29 | 28 | ad2antrr 724 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โ) |
30 | 13, 24 | mulcld 11262 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ ยท ๐) โ โ) |
31 | 29, 30 | addcld 11261 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ + (๐ผ ยท ๐)) โ โ) |
32 | 31, 30 | negsubd 11605 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + -(๐ผ ยท ๐)) = ((๐ + (๐ผ ยท ๐)) โ (๐ผ ยท ๐))) |
33 | 29, 30 | pncand 11600 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) โ (๐ผ ยท ๐)) = ๐) |
34 | 26, 32, 33 | 3eqtrd 2769 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐)) = ๐) |
35 | 34 | oveq2d 7431 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))) = (๐ด Yrm ๐)) |
36 | 35 | breq2d 5155 |
. . . . . . 7
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ๐))) |
37 | 21, 36 | bitr2d 279 |
. . . . . 6
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |
38 | 37 | ex 411 |
. . . . 5
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ (-๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
39 | 4, 38 | jaod 857 |
. . . 4
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ ((๐ผ โ โ0 โจ -๐ผ โ โ0)
โ ((๐ด Yrm
๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
40 | 39 | expimpd 452 |
. . 3
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ผ โ โ โง (๐ผ โ โ0 โจ -๐ผ โ โ0))
โ ((๐ด Yrm
๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
41 | 1, 40 | biimtrid 241 |
. 2
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ (๐ผ โ โค โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
42 | 41 | 3impia 1114 |
1
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โค) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |