Step | Hyp | Ref
| Expression |
1 | | elznn0 12577 |
. . 3
โข (๐ผ โ โค โ (๐ผ โ โ โง (๐ผ โ โ0 โจ
-๐ผ โ
โ0))) |
2 | | jm2.19lem3 42313 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |
3 | 2 | 3expia 1118 |
. . . . . 6
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ (๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
4 | 3 | adantr 480 |
. . . . 5
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ (๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
5 | | simplll 772 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ด โ
(โคโฅโ2)) |
6 | | simprl 768 |
. . . . . . . . 9
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โค) |
7 | 6 | ad2antrr 723 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โค) |
8 | | simprr 770 |
. . . . . . . . . 10
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โค) |
9 | 8 | ad2antrr 723 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โค) |
10 | | nn0z 12587 |
. . . . . . . . . . . 12
โข (-๐ผ โ โ0
โ -๐ผ โ
โค) |
11 | 10 | adantl 481 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ -๐ผ โ
โค) |
12 | | simplr 766 |
. . . . . . . . . . . . 13
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โ) |
13 | 12 | recnd 11246 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โ) |
14 | | znegclb 12603 |
. . . . . . . . . . . 12
โข (๐ผ โ โ โ (๐ผ โ โค โ -๐ผ โ
โค)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ โ โค โ -๐ผ โ
โค)) |
16 | 11, 15 | mpbird 257 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โค) |
17 | 16, 7 | zmulcld 12676 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ ยท ๐) โ โค) |
18 | 9, 17 | zaddcld 12674 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ + (๐ผ ยท ๐)) โ โค) |
19 | | simpr 484 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ -๐ผ โ
โ0) |
20 | | jm2.19lem3 42313 |
. . . . . . . 8
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง (๐ + (๐ผ ยท ๐)) โ โค) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))))) |
21 | 5, 7, 18, 19, 20 | syl121anc 1372 |
. . . . . . 7
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))))) |
22 | | zcn 12567 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
23 | 22 | ad2antrl 725 |
. . . . . . . . . . . . 13
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
24 | 23 | ad2antrr 723 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โ) |
25 | 13, 24 | mulneg1d 11671 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (-๐ผ ยท ๐) = -(๐ผ ยท ๐)) |
26 | 25 | oveq2d 7421 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐)) = ((๐ + (๐ผ ยท ๐)) + -(๐ผ ยท ๐))) |
27 | | zcn 12567 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
28 | 27 | ad2antll 726 |
. . . . . . . . . . . . 13
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
29 | 28 | ad2antrr 723 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โ) |
30 | 13, 24 | mulcld 11238 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ ยท ๐) โ โ) |
31 | 29, 30 | addcld 11237 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ + (๐ผ ยท ๐)) โ โ) |
32 | 31, 30 | negsubd 11581 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + -(๐ผ ยท ๐)) = ((๐ + (๐ผ ยท ๐)) โ (๐ผ ยท ๐))) |
33 | 29, 30 | pncand 11576 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) โ (๐ผ ยท ๐)) = ๐) |
34 | 26, 32, 33 | 3eqtrd 2770 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐)) = ๐) |
35 | 34 | oveq2d 7421 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))) = (๐ด Yrm ๐)) |
36 | 35 | breq2d 5153 |
. . . . . . 7
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ๐))) |
37 | 21, 36 | bitr2d 280 |
. . . . . 6
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |
38 | 37 | ex 412 |
. . . . 5
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ (-๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
39 | 4, 38 | jaod 856 |
. . . 4
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ ((๐ผ โ โ0 โจ -๐ผ โ โ0)
โ ((๐ด Yrm
๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
40 | 39 | expimpd 453 |
. . 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 (๐ + (๐ผ ยท ๐))))) |