Step | Hyp | Ref
| Expression |
1 | | elznn0 12569 |
. . 3
โข (๐ผ โ โค โ (๐ผ โ โ โง (๐ผ โ โ0 โจ
-๐ผ โ
โ0))) |
2 | | jm2.19lem3 41715 |
. . . . . . 7
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |
3 | 2 | 3expia 1121 |
. . . . . 6
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ (๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
4 | 3 | adantr 481 |
. . . . 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 12579 |
. . . . . . . . . . . 12
โข (-๐ผ โ โ0
โ -๐ผ โ
โค) |
11 | 10 | adantl 482 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ -๐ผ โ
โค) |
12 | | simplr 767 |
. . . . . . . . . . . . 13
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โ) |
13 | 12 | recnd 11238 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โ) |
14 | | znegclb 12595 |
. . . . . . . . . . . 12
โข (๐ผ โ โ โ (๐ผ โ โค โ -๐ผ โ
โค)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ โ โค โ -๐ผ โ
โค)) |
16 | 11, 15 | mpbird 256 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ผ โ
โค) |
17 | 16, 7 | zmulcld 12668 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ ยท ๐) โ โค) |
18 | 9, 17 | zaddcld 12666 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ + (๐ผ ยท ๐)) โ โค) |
19 | | simpr 485 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ -๐ผ โ
โ0) |
20 | | jm2.19lem3 41715 |
. . . . . . . 8
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง (๐ + (๐ผ ยท ๐)) โ โค) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))))) |
21 | 5, 7, 18, 19, 20 | syl121anc 1375 |
. . . . . . 7
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))))) |
22 | | zcn 12559 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
23 | 22 | ad2antrl 726 |
. . . . . . . . . . . . 13
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
24 | 23 | ad2antrr 724 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โ) |
25 | 13, 24 | mulneg1d 11663 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (-๐ผ ยท ๐) = -(๐ผ ยท ๐)) |
26 | 25 | oveq2d 7421 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐)) = ((๐ + (๐ผ ยท ๐)) + -(๐ผ ยท ๐))) |
27 | | zcn 12559 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
28 | 27 | ad2antll 727 |
. . . . . . . . . . . . 13
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ๐ โ โ) |
29 | 28 | ad2antrr 724 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ๐ โ
โ) |
30 | 13, 24 | mulcld 11230 |
. . . . . . . . . . . 12
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ผ ยท ๐) โ โ) |
31 | 29, 30 | addcld 11229 |
. . . . . . . . . . 11
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ + (๐ผ ยท ๐)) โ โ) |
32 | 31, 30 | negsubd 11573 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + -(๐ผ ยท ๐)) = ((๐ + (๐ผ ยท ๐)) โ (๐ผ ยท ๐))) |
33 | 29, 30 | pncand 11568 |
. . . . . . . . . 10
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) โ (๐ผ ยท ๐)) = ๐) |
34 | 26, 32, 33 | 3eqtrd 2776 |
. . . . . . . . 9
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐)) = ๐) |
35 | 34 | oveq2d 7421 |
. . . . . . . 8
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))) = (๐ด Yrm ๐)) |
36 | 35 | breq2d 5159 |
. . . . . . 7
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ((๐ + (๐ผ ยท ๐)) + (-๐ผ ยท ๐))) โ (๐ด Yrm ๐) โฅ (๐ด Yrm ๐))) |
37 | 21, 36 | bitr2d 279 |
. . . . . 6
โข ((((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โง -๐ผ โ โ0) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |
38 | 37 | ex 413 |
. . . . 5
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ (-๐ผ โ โ0 โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
39 | 4, 38 | jaod 857 |
. . . 4
โข (((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โง ๐ผ โ โ) โ ((๐ผ โ โ0 โจ -๐ผ โ โ0)
โ ((๐ด Yrm
๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
40 | 39 | expimpd 454 |
. . 3
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ผ โ โ โง (๐ผ โ โ0 โจ -๐ผ โ โ0))
โ ((๐ด Yrm
๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
41 | 1, 40 | biimtrid 241 |
. 2
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค)) โ (๐ผ โ โค โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐)))))) |
42 | 41 | 3impia 1117 |
1
โข ((๐ด โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ โค) โง ๐ผ โ โค) โ ((๐ด Yrm ๐) โฅ (๐ด Yrm ๐) โ (๐ด Yrm ๐) โฅ (๐ด Yrm (๐ + (๐ผ ยท ๐))))) |